src/Tools/eqsubst.ML
changeset 49340 25fc6e0da459
parent 49339 d1fcb4de8349
child 51717 9e7d1c139569
     1.1 --- a/src/Tools/eqsubst.ML	Wed Sep 12 22:00:29 2012 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Wed Sep 12 23:18:26 2012 +0200
     1.3 @@ -260,15 +260,15 @@
     1.4  (* conclthm is a theorem of for just the conclusion *)
     1.5  (* m is instantiation/match information *)
     1.6  (* rule is the equation for substitution *)
     1.7 -fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
     1.8 -    (RWInst.rw m rule conclthm)
     1.9 +fun apply_subst_in_concl ctxt i th (cfvs, conclthm) rule m =
    1.10 +    (RWInst.rw ctxt m rule conclthm)
    1.11        |> IsaND.unfix_frees cfvs
    1.12        |> RWInst.beta_eta_contract
    1.13        |> (fn r => Tactic.rtac r i th);
    1.14  
    1.15  (* substitute within the conclusion of goal i of gth, using a meta
    1.16  equation rule. Note that we assume rule has var indicies zero'd *)
    1.17 -fun prep_concl_subst i gth =
    1.18 +fun prep_concl_subst ctxt i gth =
    1.19      let
    1.20        val th = Thm.incr_indexes 1 gth;
    1.21        val tgt_term = Thm.prop_of th;
    1.22 @@ -277,7 +277,7 @@
    1.23        val ctermify = Thm.cterm_of sgn;
    1.24        val trivify = Thm.trivial o ctermify;
    1.25  
    1.26 -      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
    1.27 +      val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
    1.28        val cfvs = rev (map ctermify fvs);
    1.29  
    1.30        val conclterm = Logic.strip_imp_concl fixedbody;
    1.31 @@ -294,12 +294,12 @@
    1.32  (* substitute using an object or meta level equality *)
    1.33  fun eqsubst_tac' ctxt searchf instepthm i th =
    1.34      let
    1.35 -      val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
    1.36 +      val (cvfsconclthm, searchinfo) = prep_concl_subst ctxt i th;
    1.37        val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
    1.38        fun rewrite_with_thm r =
    1.39            let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
    1.40            in searchf searchinfo lhs
    1.41 -             |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
    1.42 +             |> Seq.maps (apply_subst_in_concl ctxt i th cvfsconclthm r) end;
    1.43      in stepthms |> Seq.maps rewrite_with_thm end;
    1.44  
    1.45  
    1.46 @@ -347,11 +347,11 @@
    1.47      SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
    1.48  
    1.49  (* apply a substitution inside assumption j, keeps asm in the same place *)
    1.50 -fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
    1.51 +fun apply_subst_in_asm ctxt i th rule ((cfvs, j, ngoalprems, pth),m) =
    1.52      let
    1.53        val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
    1.54        val preelimrule =
    1.55 -          (RWInst.rw m rule pth)
    1.56 +          (RWInst.rw ctxt m rule pth)
    1.57              |> (Seq.hd o prune_params_tac)
    1.58              |> Thm.permute_prems 0 ~1 (* put old asm first *)
    1.59              |> IsaND.unfix_frees cfvs (* unfix any global params *)
    1.60 @@ -380,7 +380,7 @@
    1.61  subgoal i of gth. Note the repetition of work done for each
    1.62  assumption, i.e. this can be made more efficient for search over
    1.63  multiple assumptions.  *)
    1.64 -fun prep_subst_in_asm i gth j =
    1.65 +fun prep_subst_in_asm ctxt i gth j =
    1.66      let
    1.67        val th = Thm.incr_indexes 1 gth;
    1.68        val tgt_term = Thm.prop_of th;
    1.69 @@ -389,7 +389,7 @@
    1.70        val ctermify = Thm.cterm_of sgn;
    1.71        val trivify = Thm.trivial o ctermify;
    1.72  
    1.73 -      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
    1.74 +      val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
    1.75        val cfvs = rev (map ctermify fvs);
    1.76  
    1.77        val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
    1.78 @@ -404,8 +404,8 @@
    1.79      in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
    1.80  
    1.81  (* prepare subst in every possible assumption *)
    1.82 -fun prep_subst_in_asms i gth =
    1.83 -    map (prep_subst_in_asm i gth)
    1.84 +fun prep_subst_in_asms ctxt i gth =
    1.85 +    map (prep_subst_in_asm ctxt i gth)
    1.86          ((fn l => Library.upto (1, length l))
    1.87             (Logic.prems_of_goal (Thm.prop_of gth) i));
    1.88  
    1.89 @@ -413,7 +413,7 @@
    1.90  (* substitute in an assumption using an object or meta level equality *)
    1.91  fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
    1.92      let
    1.93 -      val asmpreps = prep_subst_in_asms i th;
    1.94 +      val asmpreps = prep_subst_in_asms ctxt i th;
    1.95        val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
    1.96        fun rewrite_with_thm r =
    1.97            let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
    1.98 @@ -426,7 +426,7 @@
    1.99                                 (occ_search 1 moreasms))
   1.100                                (* find later substs also *)
   1.101            in
   1.102 -            occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
   1.103 +            occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm ctxt i th r)
   1.104            end;
   1.105      in stepthms |> Seq.maps rewrite_with_thm end;
   1.106