1.1 --- a/src/Provers/eqsubst.ML Wed May 18 11:31:00 2005 +0200
1.2 +++ b/src/Provers/eqsubst.ML Wed May 18 23:04:13 2005 +0200
1.3 @@ -13,6 +13,8 @@
1.4 *)
1.5 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
1.6
1.7 +
1.8 +
1.9 (* Logic specific data stub *)
1.10 signature EQRULE_DATA =
1.11 sig
1.12 @@ -30,6 +32,7 @@
1.13 exception eqsubst_occL_exp of
1.14 string * (int list) * (Thm.thm list) * int * Thm.thm;
1.15
1.16 +
1.17 type match =
1.18 ((Term.indexname * (Term.sort * Term.typ)) list (* type instantiations *)
1.19 * (Term.indexname * (Term.typ * Term.term)) list) (* term instantiations *)
1.20 @@ -37,48 +40,45 @@
1.21 * (string * Term.typ) list (* type abs env *)
1.22 * Term.term (* outer term *)
1.23
1.24 + type searchinfo =
1.25 + Sign.sg (* sign for matching *)
1.26 + * int (* maxidx *)
1.27 + * BasicIsaFTerm.FcTerm (* focusterm to search under *)
1.28 +
1.29 val prep_subst_in_asm :
1.30 - (Sign.sg (* sign for matching *)
1.31 - -> int (* maxidx *)
1.32 - -> 'a (* input object kind *)
1.33 - -> BasicIsaFTerm.FcTerm (* focusterm to search under *)
1.34 - -> 'b) (* result type *)
1.35 - -> int (* subgoal to subst in *)
1.36 + int (* subgoal to subst in *)
1.37 -> Thm.thm (* target theorem with subgoals *)
1.38 -> int (* premise to subst in *)
1.39 -> (Thm.cterm list (* certified free var placeholders for vars *)
1.40 * int (* premice no. to subst *)
1.41 * int (* number of assumptions of premice *)
1.42 * Thm.thm) (* premice as a new theorem for forward reasoning *)
1.43 - * ('a -> 'b) (* matchf *)
1.44 + * searchinfo (* search info: prem id etc *)
1.45
1.46 val prep_subst_in_asms :
1.47 - (Sign.sg -> int -> 'a -> BasicIsaFTerm.FcTerm -> 'b)
1.48 - -> int (* subgoal to subst in *)
1.49 + int (* subgoal to subst in *)
1.50 -> Thm.thm (* target theorem with subgoals *)
1.51 -> ((Thm.cterm list (* certified free var placeholders for vars *)
1.52 * int (* premice no. to subst *)
1.53 * int (* number of assumptions of premice *)
1.54 * Thm.thm) (* premice as a new theorem for forward reasoning *)
1.55 - * ('a -> 'b)) (* matchf *)
1.56 - Seq.seq
1.57 + * searchinfo) list
1.58
1.59 val apply_subst_in_asm :
1.60 int (* subgoal *)
1.61 -> Thm.thm (* overall theorem *)
1.62 + -> Thm.thm (* rule *)
1.63 -> (Thm.cterm list (* certified free var placeholders for vars *)
1.64 * int (* assump no being subst *)
1.65 * int (* num of premises of asm *)
1.66 * Thm.thm) (* premthm *)
1.67 - -> Thm.thm (* rule *)
1.68 - -> match
1.69 + * match
1.70 -> Thm.thm Seq.seq
1.71
1.72 val prep_concl_subst :
1.73 - (Sign.sg -> int -> 'a -> BasicIsaFTerm.FcTerm -> 'b) (* searchf *)
1.74 - -> int (* subgoal *)
1.75 + int (* subgoal *)
1.76 -> Thm.thm (* overall goal theorem *)
1.77 - -> (Thm.cterm list * Thm.thm) * ('a -> 'b) (* (cvfs, conclthm), matchf *)
1.78 + -> (Thm.cterm list * Thm.thm) * searchinfo (* (cvfs, conclthm), matchf *)
1.79
1.80 val apply_subst_in_concl :
1.81 int (* subgoal *)
1.82 @@ -90,37 +90,49 @@
1.83 -> match
1.84 -> Thm.thm Seq.seq (* substituted goal *)
1.85
1.86 + (* basic notion of search *)
1.87 val searchf_tlr_unify_all :
1.88 - (Sign.sg -> int ->
1.89 - Term.term ->
1.90 - BasicIsaFTerm.FcTerm ->
1.91 - match Seq.seq Seq.seq)
1.92 + (searchinfo
1.93 + -> Term.term (* lhs *)
1.94 + -> match Seq.seq Seq.seq)
1.95 val searchf_tlr_unify_valid :
1.96 - (Sign.sg -> int ->
1.97 - Term.term ->
1.98 - BasicIsaFTerm.FcTerm ->
1.99 - match Seq.seq Seq.seq)
1.100 + (searchinfo
1.101 + -> Term.term (* lhs *)
1.102 + -> match Seq.seq Seq.seq)
1.103
1.104 + (* specialise search constructor for conclusion skipping occurnaces. *)
1.105 + val skip_first_occs_search :
1.106 + int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
1.107 + (* specialised search constructor for assumptions using skips *)
1.108 + val skip_first_asm_occs_search :
1.109 + ('a -> 'b -> 'c Seq.seq Seq.seq) ->
1.110 + 'a -> int -> 'b -> 'c IsaPLib.skipseqT
1.111 +
1.112 + (* tactics and methods *)
1.113 val eqsubst_asm_meth : int list -> Thm.thm list -> Proof.method
1.114 - val eqsubst_asm_tac : int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
1.115 + val eqsubst_asm_tac :
1.116 + int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
1.117 val eqsubst_asm_tac' :
1.118 - (Sign.sg -> int ->
1.119 - Term.term ->
1.120 - BasicIsaFTerm.FcTerm ->
1.121 - match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
1.122 + (* search function with skips *)
1.123 + (searchinfo -> int -> Term.term -> match IsaPLib.skipseqT)
1.124 + -> int (* skip to *)
1.125 + -> Thm.thm (* rule *)
1.126 + -> int (* subgoal number *)
1.127 + -> Thm.thm (* tgt theorem with subgoals *)
1.128 + -> Thm.thm Seq.seq (* new theorems *)
1.129
1.130 val eqsubst_meth : int list -> Thm.thm list -> Proof.method
1.131 - val eqsubst_tac : int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
1.132 + val eqsubst_tac :
1.133 + int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
1.134 val eqsubst_tac' :
1.135 - (Sign.sg -> int ->
1.136 - Term.term ->
1.137 - BasicIsaFTerm.FcTerm ->
1.138 - match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
1.139 + (searchinfo -> Term.term -> match Seq.seq)
1.140 + -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
1.141
1.142 val meth : (bool * int list) * Thm.thm list -> Proof.context -> Proof.method
1.143 val setup : (Theory.theory -> Theory.theory) list
1.144 end;
1.145
1.146 +
1.147 functor EQSubstTacFUN (structure EqRuleData : EQRULE_DATA)
1.148 : EQSUBST_TAC
1.149 = struct
1.150 @@ -133,6 +145,10 @@
1.151 * (string * Term.typ) list (* type abs env *)
1.152 * Term.term (* outer term *)
1.153
1.154 + type searchinfo =
1.155 + Sign.sg (* sign for matching *)
1.156 + * int (* maxidx *)
1.157 + * BasicIsaFTerm.FcTerm (* focusterm to search under *)
1.158
1.159 (* FOR DEBUGGING...
1.160 type trace_subst_errT = int (* subgoal *)
1.161 @@ -192,28 +208,18 @@
1.162 in maux ft end;
1.163
1.164 (* search all unifications *)
1.165 -fun searchf_tlr_unify_all sgn maxidx lhs =
1.166 +fun searchf_tlr_unify_all (sgn, maxidx, ft) lhs =
1.167 IsaFTerm.find_fcterm_matches
1.168 search_tlr_all_f
1.169 - (IsaFTerm.clean_unify_ft sgn maxidx lhs);
1.170 + (IsaFTerm.clean_unify_ft sgn maxidx lhs)
1.171 + ft;
1.172
1.173 (* search only for 'valid' unifiers (non abs subterms and non vars) *)
1.174 -fun searchf_tlr_unify_valid sgn maxidx lhs =
1.175 +fun searchf_tlr_unify_valid (sgn, maxidx, ft) lhs =
1.176 IsaFTerm.find_fcterm_matches
1.177 search_tlr_valid_f
1.178 - (IsaFTerm.clean_unify_ft sgn maxidx lhs);
1.179 -
1.180 -(* special tactic to skip the first "occ" occurances - ie start at the nth match *)
1.181 -fun skip_first_occs_search occ searchf sgn i t ft =
1.182 - let
1.183 - fun skip_occs n sq =
1.184 - if n <= 1 then sq
1.185 - else
1.186 - (case (Seq.pull sq) of NONE => Seq.empty
1.187 - | SOME (h,t) =>
1.188 - (case Seq.pull h of NONE => skip_occs n t
1.189 - | SOME _ => skip_occs (n - 1) t))
1.190 - in Seq.flat (skip_occs occ (searchf sgn i t ft)) end;
1.191 + (IsaFTerm.clean_unify_ft sgn maxidx lhs)
1.192 + ft;
1.193
1.194
1.195 (* apply a substitution in the conclusion of the theorem th *)
1.196 @@ -226,16 +232,13 @@
1.197 |> IsaND.unfix_frees cfvs
1.198 |> RWInst.beta_eta_contract
1.199 |> (fn r => Tactic.rtac r i th);
1.200 -
1.201 (*
1.202 -
1.203 |> (fn r => Thm.bicompose false (false, r, Thm.nprems_of r) i th)
1.204 -
1.205 *)
1.206
1.207 (* substitute within the conclusion of goal i of gth, using a meta
1.208 equation rule. Note that we assume rule has var indicies zero'd *)
1.209 -fun prep_concl_subst searchf i gth =
1.210 +fun prep_concl_subst i gth =
1.211 let
1.212 val th = Thm.incr_indexes 1 gth;
1.213 val tgt_term = Thm.prop_of th;
1.214 @@ -250,33 +253,29 @@
1.215 val conclterm = Logic.strip_imp_concl fixedbody;
1.216 val conclthm = trivify conclterm;
1.217 val maxidx = Term.maxidx_of_term conclterm;
1.218 + val ft = ((IsaFTerm.focus_right
1.219 + o IsaFTerm.focus_left
1.220 + o IsaFTerm.fcterm_of_term
1.221 + o Thm.prop_of) conclthm)
1.222 in
1.223 - ((cfvs, conclthm),
1.224 - (fn lhs => searchf sgn maxidx lhs
1.225 - ((IsaFTerm.focus_right
1.226 - o IsaFTerm.focus_left
1.227 - o IsaFTerm.fcterm_of_term
1.228 - o Thm.prop_of) conclthm)))
1.229 + ((cfvs, conclthm), (sgn, maxidx, ft))
1.230 end;
1.231
1.232 (* substitute using an object or meta level equality *)
1.233 fun eqsubst_tac' searchf instepthm i th =
1.234 let
1.235 - val (cvfsconclthm, findmatchf) =
1.236 - prep_concl_subst searchf i th;
1.237 -
1.238 + val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
1.239 val stepthms =
1.240 Seq.map Drule.zero_var_indexes
1.241 (Seq.of_list (EqRuleData.prep_meta_eq instepthm));
1.242 -
1.243 fun rewrite_with_thm r =
1.244 let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
1.245 - in (findmatchf lhs)
1.246 + in (searchf searchinfo lhs)
1.247 :-> (apply_subst_in_concl i th cvfsconclthm r) end;
1.248 + in stepthms :-> rewrite_with_thm end;
1.249
1.250 - in (stepthms :-> rewrite_with_thm) end;
1.251
1.252 -(* Tactic.distinct_subgoals_tac *)
1.253 +(* Tactic.distinct_subgoals_tac -- fails to free type variables *)
1.254
1.255 (* custom version of distinct subgoals that works with term and
1.256 type variables. Asssumes th is in beta-eta normal form.
1.257 @@ -299,30 +298,29 @@
1.258 the given theorems*)
1.259 exception eqsubst_occL_exp of
1.260 string * (int list) * (Thm.thm list) * int * Thm.thm;
1.261 -fun eqsubst_occL tac occL thms i th =
1.262 +fun skip_first_occs_search occ srchf sinfo lhs =
1.263 + case (IsaPLib.skipto_seqseq occ (srchf sinfo lhs)) of
1.264 + IsaPLib.skipmore _ => Seq.empty
1.265 + | IsaPLib.skipseq ss => Seq.flat ss;
1.266 +
1.267 +fun eqsubst_tac occL thms i th =
1.268 let val nprems = Thm.nprems_of th in
1.269 if nprems < i then Seq.empty else
1.270 let val thmseq = (Seq.of_list thms)
1.271 fun apply_occ occ th =
1.272 thmseq :->
1.273 - (fn r => tac (skip_first_occs_search
1.274 + (fn r => eqsubst_tac' (skip_first_occs_search
1.275 occ searchf_tlr_unify_valid) r
1.276 (i + ((Thm.nprems_of th) - nprems))
1.277 th);
1.278 + val sortedoccL =
1.279 + Library.sort (Library.rev_order o Library.int_ord) occL;
1.280 in
1.281 - Seq.map distinct_subgoals
1.282 - (Seq.EVERY (map apply_occ
1.283 - (Library.sort (Library.rev_order
1.284 - o Library.int_ord) occL)) th)
1.285 + Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
1.286 end
1.287 end
1.288 handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
1.289
1.290 -
1.291 -
1.292 -(* implicit argus: occL thms i th *)
1.293 -val eqsubst_tac = eqsubst_occL eqsubst_tac';
1.294 -
1.295
1.296 (* inthms are the given arguments in Isar, and treated as eqstep with
1.297 the first one, then the second etc *)
1.298 @@ -331,24 +329,29 @@
1.299 (fn facts =>
1.300 HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac occL inthms ));
1.301
1.302 -
1.303 -fun apply_subst_in_asm i th (cfvs, j, nprems, pth) rule m =
1.304 - (RWInst.rw m rule pth)
1.305 - |> Thm.permute_prems 0 ~1
1.306 - |> IsaND.unfix_frees cfvs
1.307 - |> RWInst.beta_eta_contract
1.308 - |> (fn r => Tactic.dtac r i th);
1.309 -
1.310 -(*
1.311 -? should I be using bicompose what if we match more than one
1.312 -assumption, even after instantiation ? (back will work, but it would
1.313 -be nice to avoid the redudent search)
1.314 -
1.315 -something like...
1.316 - |> Thm.lift_rule (th, i)
1.317 - |> (fn r => Thm.bicompose false (false, r, Thm.nprems_of r - nprems) i th)
1.318 -
1.319 -*)
1.320 +(* apply a substitution inside assumption j, keeps asm in the same place *)
1.321 +fun apply_subst_in_asm i th rule ((cfvs, j, nprems, pth),m) =
1.322 + let
1.323 + val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
1.324 + val preelimrule =
1.325 + (RWInst.rw m rule pth)
1.326 + |> (Seq.hd o Tactic.prune_params_tac)
1.327 + |> Thm.permute_prems 0 ~1 (* put old asm first *)
1.328 + |> IsaND.unfix_frees cfvs (* unfix any global params *)
1.329 + |> RWInst.beta_eta_contract; (* normal form *)
1.330 + val elimrule =
1.331 + preelimrule
1.332 + |> Tactic.make_elim (* make into elim rule *)
1.333 + |> Thm.lift_rule (th2, i); (* lift into context *)
1.334 + in
1.335 + (* ~j because new asm starts at back, thus we subtract 1 *)
1.336 + Seq.map (Thm.rotate_rule (~j) (nprems + i))
1.337 + (Thm.bicompose
1.338 + false (* use unification *)
1.339 + (true, (* elim resolution *)
1.340 + elimrule, 2 + nprems)
1.341 + i th2)
1.342 + end;
1.343
1.344
1.345 (* prepare to substitute within the j'th premise of subgoal i of gth,
1.346 @@ -357,7 +360,7 @@
1.347 subgoal i of gth. Note the repetition of work done for each
1.348 assumption, i.e. this can be made more efficient for search over
1.349 multiple assumptions. *)
1.350 -fun prep_subst_in_asm searchf i gth j =
1.351 +fun prep_subst_in_asm i gth j =
1.352 let
1.353 val th = Thm.incr_indexes 1 gth;
1.354 val tgt_term = Thm.prop_of th;
1.355 @@ -375,42 +378,65 @@
1.356 val pth = trivify asmt;
1.357 val maxidx = Term.maxidx_of_term asmt;
1.358
1.359 - in
1.360 - ((cfvs, j, asm_nprems, pth),
1.361 - (fn lhs => (searchf sgn maxidx lhs
1.362 - ((IsaFTerm.focus_right
1.363 - o IsaFTerm.fcterm_of_term
1.364 - o Thm.prop_of) pth))))
1.365 - end;
1.366 + val ft = ((IsaFTerm.focus_right
1.367 + o IsaFTerm.fcterm_of_term
1.368 + o Thm.prop_of) pth)
1.369 + in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
1.370
1.371 (* prepare subst in every possible assumption *)
1.372 -fun prep_subst_in_asms searchf i gth =
1.373 - Seq.map
1.374 - (prep_subst_in_asm searchf i gth)
1.375 - (Seq.of_list (IsaPLib.mk_num_list
1.376 - (length (Logic.prems_of_goal (Thm.prop_of gth) i))));
1.377 +fun prep_subst_in_asms i gth =
1.378 + map (prep_subst_in_asm i gth)
1.379 + ((rev o IsaPLib.mk_num_list o length)
1.380 + (Logic.prems_of_goal (Thm.prop_of gth) i));
1.381
1.382
1.383 (* substitute in an assumption using an object or meta level equality *)
1.384 -fun eqsubst_asm_tac' searchf instepthm i th =
1.385 +fun eqsubst_asm_tac' searchf skipocc instepthm i th =
1.386 let
1.387 - val asmpreps = prep_subst_in_asms searchf i th;
1.388 + val asmpreps = prep_subst_in_asms i th;
1.389 val stepthms =
1.390 Seq.map Drule.zero_var_indexes
1.391 - (Seq.of_list (EqRuleData.prep_meta_eq instepthm))
1.392 + (Seq.of_list (EqRuleData.prep_meta_eq instepthm))
1.393 + fun rewrite_with_thm r =
1.394 + let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
1.395 + fun occ_search occ [] = Seq.empty
1.396 + | occ_search occ ((asminfo, searchinfo)::moreasms) =
1.397 + (case searchf searchinfo occ lhs of
1.398 + IsaPLib.skipmore i => occ_search i moreasms
1.399 + | IsaPLib.skipseq ss =>
1.400 + Seq.append (Seq.map (Library.pair asminfo)
1.401 + (Seq.flat ss),
1.402 + occ_search 1 moreasms))
1.403 + (* find later substs also *)
1.404 + in
1.405 + (occ_search skipocc asmpreps) :-> (apply_subst_in_asm i th r)
1.406 + end;
1.407 + in stepthms :-> rewrite_with_thm end;
1.408
1.409 - fun rewrite_with_thm (asminfo, findmatchf) r =
1.410 - let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
1.411 - in (findmatchf lhs)
1.412 - :-> (apply_subst_in_asm i th asminfo r) end;
1.413 +
1.414 +fun skip_first_asm_occs_search searchf sinfo occ lhs =
1.415 + IsaPLib.skipto_seqseq occ (searchf sinfo lhs);
1.416 +
1.417 +fun eqsubst_asm_tac occL thms i th =
1.418 + let val nprems = Thm.nprems_of th
1.419 in
1.420 - (asmpreps :-> (fn a => stepthms :-> rewrite_with_thm a))
1.421 - end;
1.422 -
1.423 -(* substitute using one of the given theorems in an assumption.
1.424 -Implicit args: occL thms i th *)
1.425 -val eqsubst_asm_tac = eqsubst_occL eqsubst_asm_tac';
1.426 -
1.427 + if nprems < i then Seq.empty else
1.428 + let val thmseq = (Seq.of_list thms)
1.429 + fun apply_occ occK th =
1.430 + thmseq :->
1.431 + (fn r =>
1.432 + eqsubst_asm_tac' (skip_first_asm_occs_search
1.433 + searchf_tlr_unify_valid) occK r
1.434 + (i + ((Thm.nprems_of th) - nprems))
1.435 + th);
1.436 + val sortedoccs =
1.437 + Library.sort (Library.rev_order o Library.int_ord) occL
1.438 + in
1.439 + Seq.map distinct_subgoals
1.440 + (Seq.EVERY (map apply_occ sortedoccs) th)
1.441 + end
1.442 + end
1.443 + handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
1.444
1.445 (* inthms are the given arguments in Isar, and treated as eqstep with
1.446 the first one, then the second etc *)