1 (* Title: Provers/eqsubst.ML
3 Author: Lucas Dixon, University of Edinburgh, lucas.dixon@ed.ac.uk
5 A proof method to perform a substiution using an equation.
10 val setup : theory -> theory
13 structure EqSubst: EQSUBST =
16 fun prep_meta_eq ctxt =
17 let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
18 in mk #> map Drule.zero_var_indexes end;
21 (* a type abriviation for match information *)
23 ((indexname * (sort * typ)) list (* type instantiations *)
24 * (indexname * (typ * term)) list) (* term instantiations *)
25 * (string * typ) list (* fake named type abs env *)
26 * (string * typ) list (* type abs env *)
27 * term (* outer term *)
32 * BasicIsaFTerm.FcTerm (* focusterm to search under *)
35 type trace_subst_errT = int (* subgoal *)
36 * thm (* thm with all goals *)
37 * (Thm.cterm list (* certified free var placeholders for vars *)
38 * thm) (* trivial thm of goal concl *)
39 (* possible matches/unifiers *)
41 * (((indexname * typ) list (* type instantiations *)
42 * (indexname * term) list ) (* term instantiations *)
43 * (string * typ) list (* Type abs env *)
44 * term) (* outer term *);
46 val trace_subst_err = (ref NONE : trace_subst_errT option ref);
47 val trace_subst_search = ref false;
48 exception trace_subst_exp of trace_subst_errT;
51 (* search from top, left to right, then down *)
52 fun search_tlr_all_f f ft =
55 let val t' = (IsaFTerm.focus_of_fcterm ft)
57 if !trace_subst_search then
58 (writeln ("Examining: " ^ (TermLib.string_of_term t'));
59 TermLib.writeterm t'; ())
63 (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
65 maux (IsaFTerm.focus_right ft)))
66 | (Abs _) => Seq.cons(f ft, maux (IsaFTerm.focus_abs ft))
67 | leaf => Seq.single (f ft)) end
70 (* search from top, left to right, then down *)
71 fun search_tlr_valid_f f ft =
75 val hereseq = if IsaFTerm.valid_match_start ft then f ft else Seq.empty
77 (case (IsaFTerm.focus_of_fcterm ft) of
78 (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
80 maux (IsaFTerm.focus_right ft)))
81 | (Abs _) => Seq.cons(hereseq, maux (IsaFTerm.focus_abs ft))
82 | leaf => Seq.single (hereseq))
86 (* search all unifications *)
87 fun searchf_tlr_unify_all (sgn, maxidx, ft) lhs =
88 IsaFTerm.find_fcterm_matches
90 (IsaFTerm.clean_unify_ft sgn maxidx lhs)
93 (* search only for 'valid' unifiers (non abs subterms and non vars) *)
94 fun searchf_tlr_unify_valid (sgn, maxidx, ft) lhs =
95 IsaFTerm.find_fcterm_matches
97 (IsaFTerm.clean_unify_ft sgn maxidx lhs)
101 (* apply a substitution in the conclusion of the theorem th *)
102 (* cfvs are certified free var placeholders for goal params *)
103 (* conclthm is a theorem of for just the conclusion *)
104 (* m is instantiation/match information *)
105 (* rule is the equation for substitution *)
106 fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
107 (RWInst.rw m rule conclthm)
108 |> IsaND.unfix_frees cfvs
109 |> RWInst.beta_eta_contract
110 |> (fn r => Tactic.rtac r i th);
112 (* substitute within the conclusion of goal i of gth, using a meta
113 equation rule. Note that we assume rule has var indicies zero'd *)
114 fun prep_concl_subst i gth =
116 val th = Thm.incr_indexes 1 gth;
117 val tgt_term = Thm.prop_of th;
119 val sgn = Thm.sign_of_thm th;
120 val ctermify = Thm.cterm_of sgn;
121 val trivify = Thm.trivial o ctermify;
123 val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
124 val cfvs = rev (map ctermify fvs);
126 val conclterm = Logic.strip_imp_concl fixedbody;
127 val conclthm = trivify conclterm;
128 val maxidx = Term.maxidx_of_term conclterm;
129 val ft = ((IsaFTerm.focus_right
130 o IsaFTerm.focus_left
131 o IsaFTerm.fcterm_of_term
132 o Thm.prop_of) conclthm)
134 ((cfvs, conclthm), (sgn, maxidx, ft))
137 (* substitute using an object or meta level equality *)
138 fun eqsubst_tac' ctxt searchf instepthm i th =
140 val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
141 val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
142 fun rewrite_with_thm r =
143 let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
144 in searchf searchinfo lhs
145 |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
146 in stepthms |> Seq.maps rewrite_with_thm end;
149 (* Tactic.distinct_subgoals_tac -- fails to free type variables *)
151 (* custom version of distinct subgoals that works with term and
152 type variables. Asssumes th is in beta-eta normal form.
153 Also, does nothing if flexflex contraints are present. *)
154 fun distinct_subgoals th =
155 if List.null (Thm.tpairs_of th) then
156 let val (fixes,fixedthm) = IsaND.fix_vars_and_tvars th
157 val (fixedthconcl,cprems) = IsaND.hide_prems fixedthm
159 IsaND.unfix_frees_and_tfrees
161 (Drule.implies_intr_list
162 (Library.gen_distinct
163 (fn (x, y) => Thm.term_of x = Thm.term_of y)
164 cprems) fixedthconcl)
168 (* General substiuttion of multiple occurances using one of
170 exception eqsubst_occL_exp of
171 string * (int list) * (thm list) * int * thm;
172 fun skip_first_occs_search occ srchf sinfo lhs =
173 case (IsaPLib.skipto_seqseq occ (srchf sinfo lhs)) of
174 IsaPLib.skipmore _ => Seq.empty
175 | IsaPLib.skipseq ss => Seq.flat ss;
177 fun eqsubst_tac ctxt occL thms i th =
178 let val nprems = Thm.nprems_of th in
179 if nprems < i then Seq.empty else
180 let val thmseq = (Seq.of_list thms)
181 fun apply_occ occ th =
183 (fn r => eqsubst_tac' ctxt (skip_first_occs_search
184 occ searchf_tlr_unify_valid) r
185 (i + ((Thm.nprems_of th) - nprems))
188 Library.sort (Library.rev_order o Library.int_ord) occL;
190 Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
193 handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
196 (* inthms are the given arguments in Isar, and treated as eqstep with
197 the first one, then the second etc *)
198 fun eqsubst_meth ctxt occL inthms =
201 HEADGOAL (Method.insert_tac facts THEN' eqsubst_tac ctxt occL inthms));
203 (* apply a substitution inside assumption j, keeps asm in the same place *)
204 fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
206 val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
208 (RWInst.rw m rule pth)
209 |> (Seq.hd o Tactic.prune_params_tac)
210 |> Thm.permute_prems 0 ~1 (* put old asm first *)
211 |> IsaND.unfix_frees cfvs (* unfix any global params *)
212 |> RWInst.beta_eta_contract; (* normal form *)
215 |> Tactic.make_elim (* make into elim rule *)
216 |> Thm.lift_rule (th2, i); (* lift into context *)
219 (* ~j because new asm starts at back, thus we subtract 1 *)
220 Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
221 (Tactic.dtac preelimrule i th2)
224 false (* use unification *)
225 (true, (* elim resolution *)
226 elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
231 (* prepare to substitute within the j'th premise of subgoal i of gth,
232 using a meta-level equation. Note that we assume rule has var indicies
233 zero'd. Note that we also assume that premt is the j'th premice of
234 subgoal i of gth. Note the repetition of work done for each
235 assumption, i.e. this can be made more efficient for search over
236 multiple assumptions. *)
237 fun prep_subst_in_asm i gth j =
239 val th = Thm.incr_indexes 1 gth;
240 val tgt_term = Thm.prop_of th;
242 val sgn = Thm.sign_of_thm th;
243 val ctermify = Thm.cterm_of sgn;
244 val trivify = Thm.trivial o ctermify;
246 val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
247 val cfvs = rev (map ctermify fvs);
249 val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
250 val asm_nprems = length (Logic.strip_imp_prems asmt);
252 val pth = trivify asmt;
253 val maxidx = Term.maxidx_of_term asmt;
255 val ft = ((IsaFTerm.focus_right
256 o IsaFTerm.fcterm_of_term
258 in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
260 (* prepare subst in every possible assumption *)
261 fun prep_subst_in_asms i gth =
262 map (prep_subst_in_asm i gth)
263 ((rev o IsaPLib.mk_num_list o length)
264 (Logic.prems_of_goal (Thm.prop_of gth) i));
267 (* substitute in an assumption using an object or meta level equality *)
268 fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
270 val asmpreps = prep_subst_in_asms i th;
271 val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
272 fun rewrite_with_thm r =
273 let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
274 fun occ_search occ [] = Seq.empty
275 | occ_search occ ((asminfo, searchinfo)::moreasms) =
276 (case searchf searchinfo occ lhs of
277 IsaPLib.skipmore i => occ_search i moreasms
278 | IsaPLib.skipseq ss =>
279 Seq.append (Seq.map (Library.pair asminfo)
281 occ_search 1 moreasms))
282 (* find later substs also *)
284 occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
286 in stepthms |> Seq.maps rewrite_with_thm end;
289 fun skip_first_asm_occs_search searchf sinfo occ lhs =
290 IsaPLib.skipto_seqseq occ (searchf sinfo lhs);
292 fun eqsubst_asm_tac ctxt occL thms i th =
293 let val nprems = Thm.nprems_of th
295 if nprems < i then Seq.empty else
296 let val thmseq = (Seq.of_list thms)
297 fun apply_occ occK th =
300 eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
301 searchf_tlr_unify_valid) occK r
302 (i + ((Thm.nprems_of th) - nprems))
305 Library.sort (Library.rev_order o Library.int_ord) occL
307 Seq.map distinct_subgoals
308 (Seq.EVERY (map apply_occ sortedoccs) th)
311 handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
313 (* inthms are the given arguments in Isar, and treated as eqstep with
314 the first one, then the second etc *)
315 fun eqsubst_asm_meth ctxt occL inthms =
318 HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac ctxt occL inthms ));
320 (* syntax for options, given "(asm)" will give back true, without
323 (Args.parens (Args.$$$ "asm") >> (K true)) ||
324 (Scan.succeed false);
327 (Args.parens (Scan.repeat Args.nat))
328 || (Scan.succeed [0]);
330 (* combination method that takes a flag (true indicates that subst
331 should be done to an assumption, false = apply to the conclusion of
332 the goal) as well as the theorems to use *)
334 Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
335 #> (fn (ctxt, ((asmflag, occL), inthms)) =>
336 (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
340 Method.add_method ("subst", subst_meth, "single-step substitution");