tuned -- prefer terminology of tactic / goal state;
authorwenzelm
Thu May 30 14:37:06 2013 +0200 (2013-05-30)
changeset 52236fb82b42eb498
parent 52235 6aff6b8bec13
child 52237 ab3ba550cbe7
tuned -- prefer terminology of tactic / goal state;
src/Tools/eqsubst.ML
     1.1 --- a/src/Tools/eqsubst.ML	Thu May 30 14:17:56 2013 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Thu May 30 14:37:06 2013 +0200
     1.3 @@ -239,16 +239,16 @@
     1.4  
     1.5  val searchf_bt_unify_valid = searchf_unify_gen (search_bt_valid valid_match_start);
     1.6  
     1.7 -(* apply a substitution in the conclusion of the theorem th *)
     1.8 +(* apply a substitution in the conclusion of the theorem *)
     1.9  (* cfvs are certified free var placeholders for goal params *)
    1.10  (* conclthm is a theorem of for just the conclusion *)
    1.11  (* m is instantiation/match information *)
    1.12  (* rule is the equation for substitution *)
    1.13 -fun apply_subst_in_concl ctxt i th (cfvs, conclthm) rule m =
    1.14 +fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m =
    1.15    RWInst.rw ctxt m rule conclthm
    1.16    |> IsaND.unfix_frees cfvs
    1.17    |> RWInst.beta_eta_contract
    1.18 -  |> (fn r => Tactic.rtac r i th);
    1.19 +  |> (fn r => Tactic.rtac r i st);
    1.20  
    1.21  (* substitute within the conclusion of goal i of gth, using a meta
    1.22  equation rule. Note that we assume rule has var indicies zero'd *)
    1.23 @@ -276,27 +276,23 @@
    1.24    end;
    1.25  
    1.26  (* substitute using an object or meta level equality *)
    1.27 -fun eqsubst_tac' ctxt searchf instepthm i th =
    1.28 +fun eqsubst_tac' ctxt searchf instepthm i st =
    1.29    let
    1.30 -    val (cvfsconclthm, searchinfo) = prep_concl_subst ctxt i th;
    1.31 +    val (cvfsconclthm, searchinfo) = prep_concl_subst ctxt i st;
    1.32      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
    1.33      fun rewrite_with_thm r =
    1.34        let val (lhs,_) = Logic.dest_equals (Thm.concl_of r) in
    1.35          searchf searchinfo lhs
    1.36 -        |> Seq.maps (apply_subst_in_concl ctxt i th cvfsconclthm r)
    1.37 +        |> Seq.maps (apply_subst_in_concl ctxt i st cvfsconclthm r)
    1.38        end;
    1.39    in stepthms |> Seq.maps rewrite_with_thm end;
    1.40  
    1.41  
    1.42 -(* distinct subgoals *)
    1.43 -fun distinct_subgoals th = the_default th (SINGLE distinct_subgoals_tac th);
    1.44 -
    1.45 -
    1.46  (* General substitution of multiple occurances using one of
    1.47     the given theorems *)
    1.48  
    1.49  fun skip_first_occs_search occ srchf sinfo lhs =
    1.50 -  (case (skipto_skipseq occ (srchf sinfo lhs)) of
    1.51 +  (case skipto_skipseq occ (srchf sinfo lhs) of
    1.52      SkipMore _ => Seq.empty
    1.53    | SkipSeq ss => Seq.flat ss);
    1.54  
    1.55 @@ -305,19 +301,19 @@
    1.56  occurences, but all earlier ones are skipped. Thus you can use [0] to
    1.57  just find all rewrites. *)
    1.58  
    1.59 -fun eqsubst_tac ctxt occL thms i th =
    1.60 -  let val nprems = Thm.nprems_of th in
    1.61 +fun eqsubst_tac ctxt occL thms i st =
    1.62 +  let val nprems = Thm.nprems_of st in
    1.63      if nprems < i then Seq.empty else
    1.64      let
    1.65 -      val thmseq = (Seq.of_list thms);
    1.66 -      fun apply_occ occ th =
    1.67 +      val thmseq = Seq.of_list thms;
    1.68 +      fun apply_occ occ st =
    1.69          thmseq |> Seq.maps (fn r =>
    1.70            eqsubst_tac' ctxt
    1.71              (skip_first_occs_search occ searchf_lr_unify_valid) r
    1.72 -            (i + (Thm.nprems_of th - nprems)) th);
    1.73 +            (i + (Thm.nprems_of st - nprems)) st);
    1.74        val sortedoccL = Library.sort (rev_order o int_ord) occL;
    1.75      in
    1.76 -      Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
    1.77 +      Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sortedoccL) st)
    1.78      end
    1.79    end;
    1.80  
    1.81 @@ -327,9 +323,9 @@
    1.82  fun eqsubst_meth ctxt occL inthms = SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
    1.83  
    1.84  (* apply a substitution inside assumption j, keeps asm in the same place *)
    1.85 -fun apply_subst_in_asm ctxt i th rule ((cfvs, j, _, pth),m) =
    1.86 +fun apply_subst_in_asm ctxt i st rule ((cfvs, j, _, pth),m) =
    1.87    let
    1.88 -    val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
    1.89 +    val st2 = Thm.rotate_rule (j - 1) i st; (* put premice first *)
    1.90      val preelimrule =
    1.91        RWInst.rw ctxt m rule pth
    1.92        |> (Seq.hd o prune_params_tac)
    1.93 @@ -339,7 +335,7 @@
    1.94    in
    1.95      (* ~j because new asm starts at back, thus we subtract 1 *)
    1.96      Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i))
    1.97 -      (Tactic.dtac preelimrule i th2)
    1.98 +      (Tactic.dtac preelimrule i st2)
    1.99    end;
   1.100  
   1.101  
   1.102 @@ -380,9 +376,9 @@
   1.103  
   1.104  
   1.105  (* substitute in an assumption using an object or meta level equality *)
   1.106 -fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
   1.107 +fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i st =
   1.108    let
   1.109 -    val asmpreps = prep_subst_in_asms ctxt i th;
   1.110 +    val asmpreps = prep_subst_in_asms ctxt i st;
   1.111      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
   1.112      fun rewrite_with_thm r =
   1.113        let
   1.114 @@ -395,7 +391,7 @@
   1.115                    Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
   1.116                      (occ_search 1 moreasms)) (* find later substs also *)
   1.117        in
   1.118 -        occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm ctxt i th r)
   1.119 +        occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm ctxt i st r)
   1.120        end;
   1.121    in stepthms |> Seq.maps rewrite_with_thm end;
   1.122  
   1.123 @@ -403,20 +399,20 @@
   1.124  fun skip_first_asm_occs_search searchf sinfo occ lhs =
   1.125    skipto_skipseq occ (searchf sinfo lhs);
   1.126  
   1.127 -fun eqsubst_asm_tac ctxt occL thms i th =
   1.128 -  let val nprems = Thm.nprems_of th in
   1.129 +fun eqsubst_asm_tac ctxt occL thms i st =
   1.130 +  let val nprems = Thm.nprems_of st in
   1.131      if nprems < i then Seq.empty
   1.132      else
   1.133        let
   1.134          val thmseq = Seq.of_list thms;
   1.135 -        fun apply_occ occK th =
   1.136 +        fun apply_occ occK st =
   1.137            thmseq |> Seq.maps (fn r =>
   1.138              eqsubst_asm_tac' ctxt
   1.139                (skip_first_asm_occs_search searchf_lr_unify_valid) occK r
   1.140 -              (i + (Thm.nprems_of th - nprems)) th);
   1.141 +              (i + (Thm.nprems_of st - nprems)) st);
   1.142          val sortedoccs = Library.sort (rev_order o int_ord) occL;
   1.143        in
   1.144 -        Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccs) th)
   1.145 +        Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sortedoccs) st)
   1.146        end
   1.147    end;
   1.148