clarified context;
authorwenzelm
Fri Mar 06 23:55:55 2015 +0100 (2015-03-06)
changeset 59641a2d056424d3c
parent 59640 a6d29266f01c
child 59642 929984c529d3
clarified context;
src/Tools/IsaPlanner/isand.ML
src/Tools/IsaPlanner/rw_inst.ML
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Fri Mar 06 23:55:04 2015 +0100
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Fri Mar 06 23:55:55 2015 +0100
     1.3 @@ -91,10 +91,9 @@
     1.4  
     1.5  fun fix_alls_cterm ctxt i th =
     1.6    let
     1.7 -    val cert = Thm.global_cterm_of (Thm.theory_of_thm th);
     1.8      val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th);
     1.9 -    val cfvs = rev (map cert fvs);
    1.10 -    val ct_body = cert fixedbody;
    1.11 +    val cfvs = rev (map (Thm.cterm_of ctxt) fvs);
    1.12 +    val ct_body = Thm.cterm_of ctxt fixedbody;
    1.13    in (ct_body, cfvs) end;
    1.14  
    1.15  fun fix_alls' ctxt i = apfst Thm.trivial o fix_alls_cterm ctxt i;
    1.16 @@ -140,12 +139,12 @@
    1.17  *)
    1.18  fun subgoal_thms th =
    1.19    let
    1.20 -    val cert = Thm.global_cterm_of (Thm.theory_of_thm th);
    1.21 +    val thy = Thm.theory_of_thm th;
    1.22  
    1.23      val t = Thm.prop_of th;
    1.24  
    1.25      val prems = Logic.strip_imp_prems t;
    1.26 -    val aprems = map (Thm.trivial o cert) prems;
    1.27 +    val aprems = map (Thm.trivial o Thm.global_cterm_of thy) prems;
    1.28  
    1.29      fun explortf premths = Drule.implies_elim_list th premths;
    1.30    in (aprems, explortf) end;
     2.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Fri Mar 06 23:55:04 2015 +0100
     2.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Fri Mar 06 23:55:55 2015 +0100
     2.3 @@ -32,13 +32,13 @@
     2.4  *)
     2.5  fun allify_conditions Ts th =
     2.6    let
     2.7 -    val cert = Thm.global_cterm_of (Thm.theory_of_thm th);
     2.8 +    val thy = Thm.theory_of_thm th;
     2.9  
    2.10      fun allify (x, T) t =
    2.11        Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t));
    2.12  
    2.13 -    val cTs = map (cert o Free) Ts;
    2.14 -    val cterm_asms = map (cert o fold_rev allify Ts) (Thm.prems_of th);
    2.15 +    val cTs = map (Thm.global_cterm_of thy o Free) Ts;
    2.16 +    val cterm_asms = map (Thm.global_cterm_of thy o fold_rev allify Ts) (Thm.prems_of th);
    2.17      val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms;
    2.18    in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
    2.19  
    2.20 @@ -62,8 +62,6 @@
    2.21  (* Note, we take abstraction in the order of last abstraction first *)
    2.22  fun mk_abstractedrule ctxt TsFake Ts rule =
    2.23    let
    2.24 -    val cert = Thm.global_cterm_of (Thm.theory_of_thm rule);
    2.25 -
    2.26      (* now we change the names of temporary free vars that represent
    2.27         bound vars with binders outside the redex *)
    2.28  
    2.29 @@ -72,8 +70,8 @@
    2.30  
    2.31      val (fromnames, tonames, Ts') =
    2.32        fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') =>
    2.33 -              (cert (Free(faken,ty)) :: rnf,
    2.34 -               cert (Free(n2,ty)) :: rnt,
    2.35 +              (Thm.cterm_of ctxt (Free(faken,ty)) :: rnf,
    2.36 +               Thm.cterm_of ctxt (Free(n2,ty)) :: rnt,
    2.37                 (n2,ty) :: Ts''))
    2.38              (TsFake ~~ Ts ~~ ns) ([], [], []);
    2.39  
    2.40 @@ -171,10 +169,6 @@
    2.41  
    2.42  fun rw ctxt ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
    2.43    let
    2.44 -    val thy = Thm.theory_of_thm target_thm;
    2.45 -    val cert = Thm.global_cterm_of thy;
    2.46 -    val certT = Thm.global_ctyp_of thy;
    2.47 -
    2.48      (* fix all non-instantiated tvars *)
    2.49      val (fixtyinsts, othertfrees) = (* FIXME proper context!? *)
    2.50        mk_fixtvar_tyinsts nonfixed_typinsts
    2.51 @@ -182,7 +176,7 @@
    2.52      val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
    2.53  
    2.54      (* certified instantiations for types *)
    2.55 -    val ctyp_insts = map (fn (ix, (s, ty)) => (certT (TVar (ix, s)), certT ty)) typinsts;
    2.56 +    val ctyp_insts = map (fn (ix, (s, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar (ix, s), ty)) typinsts;
    2.57  
    2.58      (* type instantiated versions *)
    2.59      val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
    2.60 @@ -206,7 +200,7 @@
    2.61  
    2.62      (* create certms of instantiations *)
    2.63      val cinsts_tyinst =
    2.64 -      map (fn (ix, (ty, t)) => (cert (Var (ix, ty)), cert t)) insts_tyinst_inst;
    2.65 +      map (fn (ix, (ty, t)) => apply2 (Thm.cterm_of ctxt) (Var (ix, ty), t)) insts_tyinst_inst;
    2.66  
    2.67      (* The instantiated rule *)
    2.68      val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
    2.69 @@ -215,14 +209,14 @@
    2.70      other uninstantiated vars in the hyps the *instantiated* rule
    2.71      ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
    2.72      val renamings = mk_renamings ctxt (Thm.prop_of tgt_th_tyinst) rule_inst;
    2.73 -    val cterm_renamings = map (fn (x, y) => (cert (Var x), cert y)) renamings;
    2.74 +    val cterm_renamings = map (fn (x, y) => apply2 (Thm.cterm_of ctxt) (Var x, y)) renamings;
    2.75  
    2.76      (* Create the specific version of the rule for this target application *)
    2.77      val outerterm_inst =
    2.78        outerterm_tyinst
    2.79        |> Term.subst_Vars (map (fn (ix, (ty, t)) => (ix, t)) insts_tyinst_inst)
    2.80        |> Term.subst_Vars (map (fn ((ix, ty), t) => (ix, t)) renamings);
    2.81 -    val couter_inst = Thm.reflexive (cert outerterm_inst);
    2.82 +    val couter_inst = Thm.reflexive (Thm.cterm_of ctxt outerterm_inst);
    2.83      val (cprems, abstract_rule_inst) =
    2.84        rule_inst
    2.85        |> Thm.instantiate ([], cterm_renamings)