# HG changeset patch # User dixon # Date 1115292065 -7200 # Node ID 68bd1e16552a09b5ec429c23a3886425018a3721 # Parent 66b165ee016ca086ef3bc7b2711ef373afc4fe23 lucas - added option to select occurance to rewrite e.g. (occ 4) diff -r 66b165ee016c -r 68bd1e16552a src/Provers/eqsubst.ML --- a/src/Provers/eqsubst.ML Thu May 05 11:58:59 2005 +0200 +++ b/src/Provers/eqsubst.ML Thu May 05 13:21:05 2005 +0200 @@ -91,30 +91,30 @@ (Sign.sg -> int -> Term.term -> BasicIsaFTerm.FcTerm -> - match Seq.seq) + match Seq.seq Seq.seq) val searchf_tlr_unify_valid : (Sign.sg -> int -> Term.term -> BasicIsaFTerm.FcTerm -> - match Seq.seq) + match Seq.seq Seq.seq) - val eqsubst_asm_meth : Thm.thm list -> Proof.method - val eqsubst_asm_tac : Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq + val eqsubst_asm_meth : int -> Thm.thm list -> Proof.method + val eqsubst_asm_tac : int -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq val eqsubst_asm_tac' : (Sign.sg -> int -> Term.term -> BasicIsaFTerm.FcTerm -> match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq - val eqsubst_meth : Thm.thm list -> Proof.method - val eqsubst_tac : Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq + val eqsubst_meth : int -> Thm.thm list -> Proof.method + val eqsubst_tac : int -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq val eqsubst_tac' : (Sign.sg -> int -> Term.term -> BasicIsaFTerm.FcTerm -> match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq - val meth : bool * Thm.thm list -> Proof.context -> Proof.method + val meth : (bool * int) * Thm.thm list -> Proof.context -> Proof.method val setup : (Theory.theory -> Theory.theory) list end; @@ -166,10 +166,10 @@ in (case t' of (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft), - Seq.append(f ft, + Seq.cons(f ft, maux (IsaFTerm.focus_right ft))) - | (Abs _) => Seq.append(f ft, maux (IsaFTerm.focus_abs ft)) - | leaf => f ft) end + | (Abs _) => Seq.cons(f ft, maux (IsaFTerm.focus_abs ft)) + | leaf => Seq.single (f ft)) end in maux ft end; (* search from top, left to right, then down *) @@ -181,10 +181,10 @@ in (case (IsaFTerm.focus_of_fcterm ft) of (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft), - Seq.append(hereseq, + Seq.cons(hereseq, maux (IsaFTerm.focus_right ft))) - | (Abs _) => Seq.append(hereseq, maux (IsaFTerm.focus_abs ft)) - | leaf => hereseq) + | (Abs _) => Seq.cons(hereseq, maux (IsaFTerm.focus_abs ft)) + | leaf => Seq.single (hereseq)) end in maux ft end; @@ -200,6 +200,18 @@ search_tlr_valid_f (IsaFTerm.clean_unify_ft sgn maxidx lhs); +(* special tactic to skip the first "occ" occurances - ie start at the nth match *) +fun skip_first_occs_search occ searchf sgn i t ft = + let + fun skip_occs n sq = + if n <= 1 then sq + else + (case (Seq.pull sq) of NONE => Seq.empty + | SOME (h,t) => + (case Seq.pull h of NONE => skip_occs n t + | SOME _ => skip_occs (n - 1) t)) + in Seq.flat (skip_occs occ (searchf sgn i t ft)) end; + (* apply a substitution in the conclusion of the theorem th *) (* cfvs are certified free var placeholders for goal params *) @@ -264,17 +276,18 @@ (* substitute using one of the given theorems *) -fun eqsubst_tac instepthms i th = +fun eqsubst_tac occ instepthms i th = if Thm.nprems_of th < i then Seq.empty else (Seq.of_list instepthms) - :-> (fn r => eqsubst_tac' searchf_tlr_unify_valid r i th); + :-> (fn r => eqsubst_tac' (skip_first_occs_search + occ searchf_tlr_unify_valid) r i th); (* inthms are the given arguments in Isar, and treated as eqstep with the first one, then the second etc *) -fun eqsubst_meth inthms = +fun eqsubst_meth occ inthms = Method.METHOD (fn facts => - HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac inthms )); + HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac occ inthms )); fun apply_subst_in_asm i th (cfvs, j, nprems, pth) rule m = @@ -353,33 +366,38 @@ end; (* substitute using one of the given theorems *) -fun eqsubst_asm_tac instepthms i th = +fun eqsubst_asm_tac occ instepthms i th = if Thm.nprems_of th < i then Seq.empty else (Seq.of_list instepthms) - :-> (fn r => eqsubst_asm_tac' searchf_tlr_unify_valid r i th); + :-> (fn r => eqsubst_asm_tac' (skip_first_occs_search + occ searchf_tlr_unify_valid) r i th); (* inthms are the given arguments in Isar, and treated as eqstep with the first one, then the second etc *) -fun eqsubst_asm_meth inthms = +fun eqsubst_asm_meth occ inthms = Method.METHOD (fn facts => - HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac inthms )); + HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac occ inthms )); (* combination method that takes a flag (true indicates that subst should be done to an assumption, false = apply to the conclusion of the goal) as well as the theorems to use *) -fun meth (asmflag, inthms) ctxt = - if asmflag then eqsubst_asm_meth inthms else eqsubst_meth inthms; +fun meth ((asmflag, occ), inthms) ctxt = + if asmflag then eqsubst_asm_meth occ inthms else eqsubst_meth occ inthms; (* syntax for options, given "(asm)" will give back true, without gives back false *) val options_syntax = (Args.parens (Args.$$$ "asm") >> (K true)) || (Scan.succeed false); +val ith_syntax = + (Args.parens ((Args.$$$ "occ") |-- Args.nat)) + || (Scan.succeed 0); (* method syntax, first take options, then theorems *) fun meth_syntax meth src ctxt = meth (snd (Method.syntax ((Scan.lift options_syntax) + -- (Scan.lift ith_syntax) -- Attrib.local_thms) src ctxt)) ctxt;