1.1 --- a/src/Provers/eqsubst.ML Thu May 05 11:58:59 2005 +0200
1.2 +++ b/src/Provers/eqsubst.ML Thu May 05 13:21:05 2005 +0200
1.3 @@ -91,30 +91,30 @@
1.4 (Sign.sg -> int ->
1.5 Term.term ->
1.6 BasicIsaFTerm.FcTerm ->
1.7 - match Seq.seq)
1.8 + match Seq.seq Seq.seq)
1.9 val searchf_tlr_unify_valid :
1.10 (Sign.sg -> int ->
1.11 Term.term ->
1.12 BasicIsaFTerm.FcTerm ->
1.13 - match Seq.seq)
1.14 + match Seq.seq Seq.seq)
1.15
1.16 - val eqsubst_asm_meth : Thm.thm list -> Proof.method
1.17 - val eqsubst_asm_tac : Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
1.18 + val eqsubst_asm_meth : int -> Thm.thm list -> Proof.method
1.19 + val eqsubst_asm_tac : int -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
1.20 val eqsubst_asm_tac' :
1.21 (Sign.sg -> int ->
1.22 Term.term ->
1.23 BasicIsaFTerm.FcTerm ->
1.24 match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
1.25
1.26 - val eqsubst_meth : Thm.thm list -> Proof.method
1.27 - val eqsubst_tac : Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
1.28 + val eqsubst_meth : int -> Thm.thm list -> Proof.method
1.29 + val eqsubst_tac : int -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
1.30 val eqsubst_tac' :
1.31 (Sign.sg -> int ->
1.32 Term.term ->
1.33 BasicIsaFTerm.FcTerm ->
1.34 match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
1.35
1.36 - val meth : bool * Thm.thm list -> Proof.context -> Proof.method
1.37 + val meth : (bool * int) * Thm.thm list -> Proof.context -> Proof.method
1.38 val setup : (Theory.theory -> Theory.theory) list
1.39 end;
1.40
1.41 @@ -166,10 +166,10 @@
1.42 in
1.43 (case t' of
1.44 (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
1.45 - Seq.append(f ft,
1.46 + Seq.cons(f ft,
1.47 maux (IsaFTerm.focus_right ft)))
1.48 - | (Abs _) => Seq.append(f ft, maux (IsaFTerm.focus_abs ft))
1.49 - | leaf => f ft) end
1.50 + | (Abs _) => Seq.cons(f ft, maux (IsaFTerm.focus_abs ft))
1.51 + | leaf => Seq.single (f ft)) end
1.52 in maux ft end;
1.53
1.54 (* search from top, left to right, then down *)
1.55 @@ -181,10 +181,10 @@
1.56 in
1.57 (case (IsaFTerm.focus_of_fcterm ft) of
1.58 (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
1.59 - Seq.append(hereseq,
1.60 + Seq.cons(hereseq,
1.61 maux (IsaFTerm.focus_right ft)))
1.62 - | (Abs _) => Seq.append(hereseq, maux (IsaFTerm.focus_abs ft))
1.63 - | leaf => hereseq)
1.64 + | (Abs _) => Seq.cons(hereseq, maux (IsaFTerm.focus_abs ft))
1.65 + | leaf => Seq.single (hereseq))
1.66 end
1.67 in maux ft end;
1.68
1.69 @@ -200,6 +200,18 @@
1.70 search_tlr_valid_f
1.71 (IsaFTerm.clean_unify_ft sgn maxidx lhs);
1.72
1.73 +(* special tactic to skip the first "occ" occurances - ie start at the nth match *)
1.74 +fun skip_first_occs_search occ searchf sgn i t ft =
1.75 + let
1.76 + fun skip_occs n sq =
1.77 + if n <= 1 then sq
1.78 + else
1.79 + (case (Seq.pull sq) of NONE => Seq.empty
1.80 + | SOME (h,t) =>
1.81 + (case Seq.pull h of NONE => skip_occs n t
1.82 + | SOME _ => skip_occs (n - 1) t))
1.83 + in Seq.flat (skip_occs occ (searchf sgn i t ft)) end;
1.84 +
1.85
1.86 (* apply a substitution in the conclusion of the theorem th *)
1.87 (* cfvs are certified free var placeholders for goal params *)
1.88 @@ -264,17 +276,18 @@
1.89
1.90
1.91 (* substitute using one of the given theorems *)
1.92 -fun eqsubst_tac instepthms i th =
1.93 +fun eqsubst_tac occ instepthms i th =
1.94 if Thm.nprems_of th < i then Seq.empty else
1.95 (Seq.of_list instepthms)
1.96 - :-> (fn r => eqsubst_tac' searchf_tlr_unify_valid r i th);
1.97 + :-> (fn r => eqsubst_tac' (skip_first_occs_search
1.98 + occ searchf_tlr_unify_valid) r i th);
1.99
1.100 (* inthms are the given arguments in Isar, and treated as eqstep with
1.101 the first one, then the second etc *)
1.102 -fun eqsubst_meth inthms =
1.103 +fun eqsubst_meth occ inthms =
1.104 Method.METHOD
1.105 (fn facts =>
1.106 - HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac inthms ));
1.107 + HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac occ inthms ));
1.108
1.109
1.110 fun apply_subst_in_asm i th (cfvs, j, nprems, pth) rule m =
1.111 @@ -353,33 +366,38 @@
1.112 end;
1.113
1.114 (* substitute using one of the given theorems *)
1.115 -fun eqsubst_asm_tac instepthms i th =
1.116 +fun eqsubst_asm_tac occ instepthms i th =
1.117 if Thm.nprems_of th < i then Seq.empty else
1.118 (Seq.of_list instepthms)
1.119 - :-> (fn r => eqsubst_asm_tac' searchf_tlr_unify_valid r i th);
1.120 + :-> (fn r => eqsubst_asm_tac' (skip_first_occs_search
1.121 + occ searchf_tlr_unify_valid) r i th);
1.122
1.123 (* inthms are the given arguments in Isar, and treated as eqstep with
1.124 the first one, then the second etc *)
1.125 -fun eqsubst_asm_meth inthms =
1.126 +fun eqsubst_asm_meth occ inthms =
1.127 Method.METHOD
1.128 (fn facts =>
1.129 - HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac inthms ));
1.130 + HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac occ inthms ));
1.131
1.132 (* combination method that takes a flag (true indicates that subst
1.133 should be done to an assumption, false = apply to the conclusion of
1.134 the goal) as well as the theorems to use *)
1.135 -fun meth (asmflag, inthms) ctxt =
1.136 - if asmflag then eqsubst_asm_meth inthms else eqsubst_meth inthms;
1.137 +fun meth ((asmflag, occ), inthms) ctxt =
1.138 + if asmflag then eqsubst_asm_meth occ inthms else eqsubst_meth occ inthms;
1.139
1.140 (* syntax for options, given "(asm)" will give back true, without
1.141 gives back false *)
1.142 val options_syntax =
1.143 (Args.parens (Args.$$$ "asm") >> (K true)) ||
1.144 (Scan.succeed false);
1.145 +val ith_syntax =
1.146 + (Args.parens ((Args.$$$ "occ") |-- Args.nat))
1.147 + || (Scan.succeed 0);
1.148
1.149 (* method syntax, first take options, then theorems *)
1.150 fun meth_syntax meth src ctxt =
1.151 meth (snd (Method.syntax ((Scan.lift options_syntax)
1.152 + -- (Scan.lift ith_syntax)
1.153 -- Attrib.local_thms) src ctxt))
1.154 ctxt;
1.155