1.1 --- a/src/Provers/eqsubst.ML	Fri May 06 16:03:56 2005 +0200
     1.2 +++ b/src/Provers/eqsubst.ML	Fri May 06 18:01:44 2005 +0200
     1.3 @@ -98,23 +98,23 @@
     1.4         BasicIsaFTerm.FcTerm ->
     1.5         match Seq.seq Seq.seq)
     1.6  
     1.7 -  val eqsubst_asm_meth : int -> Thm.thm list -> Proof.method
     1.8 -  val eqsubst_asm_tac : int -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
     1.9 +  val eqsubst_asm_meth : int list -> Thm.thm list -> Proof.method
    1.10 +  val eqsubst_asm_tac : int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
    1.11    val eqsubst_asm_tac' : 
    1.12        (Sign.sg -> int ->
    1.13         Term.term ->
    1.14         BasicIsaFTerm.FcTerm ->
    1.15         match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
    1.16  
    1.17 -  val eqsubst_meth : int -> Thm.thm list -> Proof.method
    1.18 -  val eqsubst_tac : int -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
    1.19 +  val eqsubst_meth : int list -> Thm.thm list -> Proof.method
    1.20 +  val eqsubst_tac : int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
    1.21    val eqsubst_tac' : 
    1.22        (Sign.sg -> int ->
    1.23         Term.term ->
    1.24         BasicIsaFTerm.FcTerm ->
    1.25         match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
    1.26  
    1.27 -  val meth : (bool * int) * Thm.thm list -> Proof.context -> Proof.method
    1.28 +  val meth : (bool * int list) * Thm.thm list -> Proof.context -> Proof.method
    1.29    val setup : (Theory.theory -> Theory.theory) list
    1.30  end;
    1.31  
    1.32 @@ -256,7 +256,6 @@
    1.33                              o Thm.prop_of) conclthm)))
    1.34      end;
    1.35  
    1.36 -
    1.37  (* substitute using an object or meta level equality *)
    1.38  fun eqsubst_tac' searchf instepthm i th = 
    1.39      let 
    1.40 @@ -275,19 +274,34 @@
    1.41      in (stepthms :-> rewrite_with_thm) end;
    1.42  
    1.43  
    1.44 -(* substitute using one of the given theorems *)
    1.45 -fun eqsubst_tac occ instepthms i th = 
    1.46 -    if Thm.nprems_of th < i then Seq.empty else
    1.47 -    (Seq.of_list instepthms) 
    1.48 -    :-> (fn r => eqsubst_tac' (skip_first_occs_search 
    1.49 -                                     occ searchf_tlr_unify_valid) r i th);
    1.50 +(* General substiuttion of multiple occurances using one of 
    1.51 +   the given theorems*)
    1.52 +fun eqsubst_occL tac occL thms i th = 
    1.53 +    let val nprems = Thm.nprems_of th in
    1.54 +      if nprems < i then Seq.empty else
    1.55 +      let val thmseq = (Seq.of_list thms) 
    1.56 +        fun apply_occ occ th = 
    1.57 +            thmseq :-> 
    1.58 +                    (fn r => tac (skip_first_occs_search 
    1.59 +                                    occ searchf_tlr_unify_valid) r
    1.60 +                                 (i + ((Thm.nprems_of th) - nprems))
    1.61 +                                 th);
    1.62 +      in
    1.63 +        Seq.EVERY (map apply_occ (Library.sort (Library.rev_order o Library.int_ord) occL)) 
    1.64 +                  th
    1.65 +      end
    1.66 +    end;
    1.67 +
    1.68 +(* implicit argus: occL thms i th *)
    1.69 +val eqsubst_tac = eqsubst_occL eqsubst_tac';
    1.70 +
    1.71  
    1.72  (* inthms are the given arguments in Isar, and treated as eqstep with
    1.73     the first one, then the second etc *)
    1.74 -fun eqsubst_meth occ inthms =
    1.75 +fun eqsubst_meth occL inthms =
    1.76      Method.METHOD 
    1.77        (fn facts =>
    1.78 -          HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac occ inthms ));
    1.79 +          HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac occL inthms ));
    1.80  
    1.81  
    1.82  fun apply_subst_in_asm i th (cfvs, j, nprems, pth) rule m = 
    1.83 @@ -365,34 +379,33 @@
    1.84        (asmpreps :-> (fn a => stepthms :-> rewrite_with_thm a))
    1.85      end;
    1.86  
    1.87 -(* substitute using one of the given theorems *)
    1.88 -fun eqsubst_asm_tac occ instepthms i th = 
    1.89 -    if Thm.nprems_of th < i then Seq.empty else
    1.90 -    (Seq.of_list instepthms) 
    1.91 -    :-> (fn r => eqsubst_asm_tac' (skip_first_occs_search 
    1.92 -                                     occ searchf_tlr_unify_valid) r i th);
    1.93 +(* substitute using one of the given theorems in an assumption.
    1.94 +Implicit args: occL thms i th *)
    1.95 +val eqsubst_asm_tac = eqsubst_occL eqsubst_asm_tac'; 
    1.96 +
    1.97  
    1.98  (* inthms are the given arguments in Isar, and treated as eqstep with
    1.99     the first one, then the second etc *)
   1.100 -fun eqsubst_asm_meth occ inthms =
   1.101 +fun eqsubst_asm_meth occL inthms =
   1.102      Method.METHOD 
   1.103        (fn facts =>
   1.104 -          HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac occ inthms ));
   1.105 +          HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac occL inthms ));
   1.106  
   1.107  (* combination method that takes a flag (true indicates that subst
   1.108  should be done to an assumption, false = apply to the conclusion of
   1.109  the goal) as well as the theorems to use *)
   1.110 -fun meth ((asmflag, occ), inthms) ctxt = 
   1.111 -    if asmflag then eqsubst_asm_meth occ inthms else eqsubst_meth occ inthms;
   1.112 +fun meth ((asmflag, occL), inthms) ctxt = 
   1.113 +    if asmflag then eqsubst_asm_meth occL inthms else eqsubst_meth occL inthms;
   1.114  
   1.115  (* syntax for options, given "(asm)" will give back true, without
   1.116     gives back false *)
   1.117  val options_syntax =
   1.118      (Args.parens (Args.$$$ "asm") >> (K true)) ||
   1.119       (Scan.succeed false);
   1.120 +
   1.121  val ith_syntax =
   1.122 -    (Args.parens ((Args.$$$ "occ") |-- Args.nat)) 
   1.123 -      || (Scan.succeed 0);
   1.124 +    (Args.parens (Scan.repeat Args.nat))
   1.125 +      || (Scan.succeed [0]);
   1.126  
   1.127  (* method syntax, first take options, then theorems *)
   1.128  fun meth_syntax meth src ctxt =