clarified context;
authorwenzelm
Wed Jun 03 19:25:05 2015 +0200 (2015-06-03)
changeset 60367e201bd8973db
parent 60366 df3e916bcd26
child 60368 d3f561aa2af6
clarified context;
src/HOL/Eisbach/match_method.ML
src/HOL/Import/import_rule.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Transfer/transfer.ML
src/Pure/Isar/code.ML
src/Pure/Isar/proof_context.ML
src/Pure/drule.ML
src/Pure/more_thm.ML
src/Pure/subgoal.ML
src/Pure/variable.ML
src/Tools/Code/code_preproc.ML
     1.1 --- a/src/HOL/Eisbach/match_method.ML	Tue Jun 02 23:00:50 2015 +0200
     1.2 +++ b/src/HOL/Eisbach/match_method.ML	Wed Jun 03 19:25:05 2015 +0200
     1.3 @@ -181,7 +181,7 @@
     1.4                    val (param_thm', ctxt'') = Thm.proof_attributes atts param_thm ctxt';
     1.5  
     1.6                    fun label_thm thm =
     1.7 -                    Thm.cterm_of ctxt' (Free (nm, propT))
     1.8 +                    Thm.cterm_of ctxt'' (Free (nm, propT))
     1.9                      |> Drule.mk_term
    1.10                      |> not (null abs_nms) ? Conjunction.intr thm
    1.11  
    1.12 @@ -509,19 +509,18 @@
    1.13  (* Fix schematics in the goal *)
    1.14  fun focus_concl ctxt i goal =
    1.15    let
    1.16 -    val ({context, concl, params, prems, asms, schematics}, goal') =
    1.17 +    val ({context = ctxt', concl, params, prems, asms, schematics}, goal') =
    1.18        Subgoal.focus_params ctxt i goal;
    1.19  
    1.20 -    val ((_, schematic_terms), context') =
    1.21 -      Variable.import_inst true [Thm.term_of concl] context
    1.22 -      |>> Thm.certify_inst (Thm.theory_of_thm goal');
    1.23 +    val (inst, ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';
    1.24 +    val (_, schematic_terms) = Thm.certify_inst ctxt'' inst;
    1.25  
    1.26      val goal'' = Thm.instantiate ([], schematic_terms) goal';
    1.27      val concl' = Thm.instantiate_cterm ([], schematic_terms) concl;
    1.28      val (schematic_types, schematic_terms') = schematics;
    1.29      val schematics' = (schematic_types, schematic_terms @ schematic_terms');
    1.30    in
    1.31 -    ({context = context', concl = concl', params = params, prems = prems,
    1.32 +    ({context = ctxt'', concl = concl', params = params, prems = prems,
    1.33        schematics = schematics', asms = asms} : Subgoal.focus, goal'')
    1.34    end;
    1.35  
     2.1 --- a/src/HOL/Import/import_rule.ML	Tue Jun 02 23:00:50 2015 +0200
     2.2 +++ b/src/HOL/Import/import_rule.ML	Wed Jun 03 19:25:05 2015 +0200
     2.3 @@ -328,13 +328,14 @@
     2.4  
     2.5  fun store_thm binding thm thy =
     2.6    let
     2.7 +    val ctxt = Proof_Context.init_global thy
     2.8      val thm = Drule.export_without_context_open thm
     2.9      val tvs = Term.add_tvars (Thm.prop_of thm) []
    2.10      val tns = map (fn (_, _) => "'") tvs
    2.11 -    val nms = fst (fold_map Name.variant tns (Variable.names_of (Proof_Context.init_global thy)))
    2.12 +    val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt))
    2.13      val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs))
    2.14 -    val cvs = map (Thm.global_ctyp_of thy) vs
    2.15 -    val ctvs = map (Thm.global_ctyp_of thy) (map TVar tvs)
    2.16 +    val cvs = map (Thm.ctyp_of ctxt) vs
    2.17 +    val ctvs = map (Thm.ctyp_of ctxt) (map TVar tvs)
    2.18      val thm' = Thm.instantiate ((ctvs ~~ cvs), []) thm
    2.19    in
    2.20      snd (Global_Theory.add_thm ((binding, thm'), []) thy)
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Jun 02 23:00:50 2015 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Jun 03 19:25:05 2015 +0200
     3.3 @@ -947,7 +947,7 @@
     3.4      val U = TFree ("'u", @{sort type})
     3.5      val y = Free (yname, U)
     3.6      val f' = absdummy (U --> T') (Bound 0 $ y)
     3.7 -    val th' = Thm.certify_instantiate
     3.8 +    val th' = Thm.certify_instantiate ctxt
     3.9        ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
    3.10         [((fst (dest_Var f), (U --> T') --> T'), f')]) th
    3.11      val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
    3.12 @@ -1086,13 +1086,13 @@
    3.13                if not (fst (dest_Const pred) = fst (dest_Const pred')) then
    3.14                  raise Fail "Trying to instantiate another predicate"
    3.15                else ()
    3.16 -          in Thm.certify_instantiate (subst_of (pred', pred), []) th end
    3.17 +          in Thm.certify_instantiate ctxt' (subst_of (pred', pred), []) th end
    3.18          fun instantiate_ho_args th =
    3.19            let
    3.20              val (_, args') =
    3.21                (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th
    3.22              val ho_args' = map dest_Var (ho_args_of_typ T args')
    3.23 -          in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
    3.24 +          in Thm.certify_instantiate ctxt' ([], ho_args' ~~ ho_args) th end
    3.25          val outp_pred =
    3.26            Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
    3.27          val ((_, ths'), ctxt1) =
     4.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Tue Jun 02 23:00:50 2015 +0200
     4.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Wed Jun 03 19:25:05 2015 +0200
     4.3 @@ -697,7 +697,7 @@
     4.4      val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
     4.5                  |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
     4.6      val thm2 = thm1
     4.7 -      |> Thm.certify_instantiate (instT, [])
     4.8 +      |> Thm.certify_instantiate ctxt (instT, [])
     4.9        |> Raw_Simplifier.rewrite_rule ctxt pre_simps
    4.10      val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
    4.11      val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
    4.12 @@ -733,7 +733,7 @@
    4.13      val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
    4.14                  |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
    4.15      val thm2 = thm1
    4.16 -      |> Thm.certify_instantiate (instT, [])
    4.17 +      |> Thm.certify_instantiate ctxt (instT, [])
    4.18        |> Raw_Simplifier.rewrite_rule ctxt pre_simps
    4.19      val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
    4.20      val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
     5.1 --- a/src/Pure/Isar/code.ML	Tue Jun 02 23:00:50 2015 +0200
     5.2 +++ b/src/Pure/Isar/code.ML	Wed Jun 03 19:25:05 2015 +0200
     5.3 @@ -635,19 +635,19 @@
     5.4      else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
     5.5    end;
     5.6  
     5.7 -fun desymbolize_tvars thms =
     5.8 +fun desymbolize_tvars thy thms =
     5.9    let
    5.10      val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
    5.11      val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
    5.12 -  in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
    5.13 +  in map (Thm.global_certify_instantiate thy (tvar_subst, [])) thms end;
    5.14  
    5.15 -fun desymbolize_vars thm =
    5.16 +fun desymbolize_vars thy thm =
    5.17    let
    5.18      val vs = Term.add_vars (Thm.prop_of thm) [];
    5.19      val var_subst = mk_desymbolization I I Var vs;
    5.20 -  in Thm.certify_instantiate ([], var_subst) thm end;
    5.21 +  in Thm.global_certify_instantiate thy ([], var_subst) thm end;
    5.22  
    5.23 -fun canonize_thms thy = desymbolize_tvars #> same_arity thy #> map desymbolize_vars;
    5.24 +fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
    5.25  
    5.26  
    5.27  (* abstype certificates *)
    5.28 @@ -706,7 +706,7 @@
    5.29    in
    5.30      thm
    5.31      |> Thm.varifyT_global
    5.32 -    |> Thm.certify_instantiate (inst, [])
    5.33 +    |> Thm.global_certify_instantiate thy (inst, [])
    5.34      |> pair subst
    5.35    end;
    5.36  
    5.37 @@ -771,7 +771,7 @@
    5.38          val sorts = map_transpose inter_sorts vss;
    5.39          val vts = Name.invent_names Name.context Name.aT sorts;
    5.40          val thms' =
    5.41 -          map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
    5.42 +          map2 (fn vs => Thm.certify_instantiate ctxt (vs ~~ map TFree vts, [])) vss thms;
    5.43          val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
    5.44          fun head_conv ct = if can Thm.dest_comb ct
    5.45            then Conv.fun_conv head_conv ct
     6.1 --- a/src/Pure/Isar/proof_context.ML	Tue Jun 02 23:00:50 2015 +0200
     6.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Jun 03 19:25:05 2015 +0200
     6.3 @@ -935,7 +935,7 @@
     6.4  
     6.5  fun comp_hhf_tac ctxt th i st =
     6.6    PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
     6.7 -    (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
     6.8 +    (false, Drule.lift_all ctxt (Thm.cprem_of st i) th, 0) i) st;
     6.9  
    6.10  fun comp_incr_tac _ [] _ = no_tac
    6.11    | comp_incr_tac ctxt (th :: ths) i =
     7.1 --- a/src/Pure/drule.ML	Tue Jun 02 23:00:50 2015 +0200
     7.2 +++ b/src/Pure/drule.ML	Wed Jun 03 19:25:05 2015 +0200
     7.3 @@ -17,7 +17,7 @@
     7.4    val forall_intr_vars: thm -> thm
     7.5    val forall_elim_list: cterm list -> thm -> thm
     7.6    val gen_all: int -> thm -> thm
     7.7 -  val lift_all: cterm -> thm -> thm
     7.8 +  val lift_all: Proof.context -> cterm -> thm -> thm
     7.9    val implies_elim_list: thm -> thm list -> thm
    7.10    val implies_intr_list: cterm list -> thm -> thm
    7.11    val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
    7.12 @@ -192,9 +192,12 @@
    7.13  
    7.14  (*lift vars wrt. outermost goal parameters
    7.15    -- reverses the effect of gen_all modulo higher-order unification*)
    7.16 -fun lift_all goal th =
    7.17 +fun lift_all ctxt raw_goal raw_th =
    7.18    let
    7.19 -    val thy = Theory.merge (Thm.theory_of_cterm goal, Thm.theory_of_thm th);
    7.20 +    val thy = Proof_Context.theory_of ctxt;
    7.21 +    val goal = Thm.transfer_cterm thy raw_goal;
    7.22 +    val th = Thm.transfer thy raw_th;
    7.23 +
    7.24      val maxidx = Thm.maxidx_of th;
    7.25      val ps = outer_params (Thm.term_of goal)
    7.26        |> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T));
    7.27 @@ -204,8 +207,8 @@
    7.28        |> map (fn (xi, T) => ((xi, T), Term.list_comb (Var (xi, Ts ---> T), ps)));
    7.29    in
    7.30      th
    7.31 -    |> Thm.instantiate (Thm.certify_inst thy ([], inst))
    7.32 -    |> fold_rev (Thm.forall_intr o Thm.global_cterm_of thy) ps
    7.33 +    |> Thm.certify_instantiate ctxt ([], inst)
    7.34 +    |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps
    7.35    end;
    7.36  
    7.37  (*direct generalization*)
    7.38 @@ -225,10 +228,8 @@
    7.39    | zero_var_indexes_list ths =
    7.40        let
    7.41          val thy = Theory.merge_list (map Thm.theory_of_thm ths);
    7.42 -        val inst =
    7.43 -          Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths)
    7.44 -          |> Thm.certify_inst thy;
    7.45 -      in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate inst) ths end;
    7.46 +        val insts = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
    7.47 +      in map (Thm.adjust_maxidx_thm ~1 o Thm.global_certify_instantiate thy insts) ths end;
    7.48  
    7.49  val zero_var_indexes = singleton zero_var_indexes_list;
    7.50  
    7.51 @@ -359,7 +360,7 @@
    7.52    Context.>>> (Context.map_theory_result (Global_Theory.store_thm_open (name, th)));
    7.53  
    7.54  fun store_standard_thm name th = store_thm name (export_without_context th);
    7.55 -fun store_standard_thm_open name thm = store_thm_open name (export_without_context_open thm);
    7.56 +fun store_standard_thm_open name th = store_thm_open name (export_without_context_open th);
    7.57  
    7.58  val reflexive_thm =
    7.59    let val cx = certify (Var(("x",0),TVar(("'a",0),[])))
     8.1 --- a/src/Pure/more_thm.ML	Tue Jun 02 23:00:50 2015 +0200
     8.2 +++ b/src/Pure/more_thm.ML	Wed Jun 03 19:25:05 2015 +0200
     8.3 @@ -60,10 +60,15 @@
     8.4    val elim_implies: thm -> thm -> thm
     8.5    val forall_elim_var: int -> thm -> thm
     8.6    val forall_elim_vars: int -> thm -> thm
     8.7 -  val certify_inst: theory ->
     8.8 +  val global_certify_inst: theory ->
     8.9      ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
    8.10      (ctyp * ctyp) list * (cterm * cterm) list
    8.11 -  val certify_instantiate:
    8.12 +  val global_certify_instantiate: theory ->
    8.13 +    ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
    8.14 +  val certify_inst: Proof.context ->
    8.15 +    ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
    8.16 +    (ctyp * ctyp) list * (cterm * cterm) list
    8.17 +  val certify_instantiate: Proof.context ->
    8.18      ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
    8.19    val forall_intr_frees: thm -> thm
    8.20    val unvarify_global: thm -> thm
    8.21 @@ -351,12 +356,19 @@
    8.22  
    8.23  (* certify_instantiate *)
    8.24  
    8.25 -fun certify_inst thy (instT, inst) =
    8.26 +fun global_certify_inst thy (instT, inst) =
    8.27   (map (fn (v, T) => apply2 (Thm.global_ctyp_of thy) (TVar v, T)) instT,
    8.28    map (fn (v, t) => apply2 (Thm.global_cterm_of thy) (Var v, t)) inst);
    8.29  
    8.30 -fun certify_instantiate insts th =
    8.31 -  Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th;
    8.32 +fun global_certify_instantiate thy insts th =
    8.33 +  Thm.instantiate (global_certify_inst thy insts) th;
    8.34 +
    8.35 +fun certify_inst ctxt (instT, inst) =
    8.36 + (map (fn (v, T) => apply2 (Thm.ctyp_of ctxt) (TVar v, T)) instT,
    8.37 +  map (fn (v, t) => apply2 (Thm.cterm_of ctxt) (Var v, t)) inst);
    8.38 +
    8.39 +fun certify_instantiate ctxt insts th =
    8.40 +  Thm.instantiate (certify_inst ctxt insts) th;
    8.41  
    8.42  
    8.43  (* forall_intr_frees: generalization over all suitable Free variables *)
    8.44 @@ -375,6 +387,8 @@
    8.45  
    8.46  fun unvarify_global th =
    8.47    let
    8.48 +    val thy = Thm.theory_of_thm th;
    8.49 +
    8.50      val prop = Thm.full_prop_of th;
    8.51      val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th)
    8.52        handle TERM (msg, _) => raise THM (msg, 0, [th]);
    8.53 @@ -383,7 +397,7 @@
    8.54      val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
    8.55        let val T' = Term_Subst.instantiateT instT T
    8.56        in (((a, i), T'), Free ((a, T'))) end);
    8.57 -  in certify_instantiate (instT, inst) th end;
    8.58 +  in global_certify_instantiate thy (instT, inst) th end;
    8.59  
    8.60  
    8.61  (* close_derivation *)
    8.62 @@ -444,7 +458,7 @@
    8.63      val _ = Sign.no_vars ctxt prop;
    8.64      val (strip, recover, prop') = stripped_sorts thy prop;
    8.65      val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
    8.66 -    val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.global_ctyp_of thy T, S)) strip;
    8.67 +    val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of ctxt T, S)) strip;
    8.68  
    8.69      val thy' = thy
    8.70        |> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop'));
    8.71 @@ -461,7 +475,7 @@
    8.72  fun add_def ctxt unchecked overloaded (b, prop) thy =
    8.73    let
    8.74      val _ = Sign.no_vars ctxt prop;
    8.75 -    val prems = map (Thm.global_cterm_of thy) (Logic.strip_imp_prems prop);
    8.76 +    val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop);
    8.77      val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
    8.78  
    8.79      val thy' = Theory.add_def ctxt unchecked overloaded (b, concl') thy;
     9.1 --- a/src/Pure/subgoal.ML	Tue Jun 02 23:00:50 2015 +0200
     9.2 +++ b/src/Pure/subgoal.ML	Wed Jun 03 19:25:05 2015 +0200
     9.3 @@ -31,7 +31,9 @@
     9.4  
     9.5  fun gen_focus (do_prems, do_concl) ctxt i raw_st =
     9.6    let
     9.7 -    val st = Simplifier.norm_hhf_protect ctxt raw_st;
     9.8 +    val st = raw_st
     9.9 +      |> Thm.transfer (Proof_Context.theory_of ctxt)
    9.10 +      |> Simplifier.norm_hhf_protect ctxt;
    9.11      val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
    9.12      val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
    9.13  
    9.14 @@ -40,9 +42,8 @@
    9.15        else ([], goal);
    9.16      val text = asms @ (if do_concl then [concl] else []);
    9.17  
    9.18 -    val ((_, schematic_terms), ctxt3) =
    9.19 -      Variable.import_inst true (map Thm.term_of text) ctxt2
    9.20 -      |>> Thm.certify_inst (Thm.theory_of_thm raw_st);
    9.21 +    val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
    9.22 +    val (_, schematic_terms) = Thm.certify_inst ctxt3 inst;
    9.23  
    9.24      val schematics = (schematic_types, schematic_terms);
    9.25      val asms' = map (Thm.instantiate_cterm schematics) asms;
    10.1 --- a/src/Pure/variable.ML	Tue Jun 02 23:00:50 2015 +0200
    10.2 +++ b/src/Pure/variable.ML	Wed Jun 03 19:25:05 2015 +0200
    10.3 @@ -578,9 +578,8 @@
    10.4  
    10.5  fun importT ths ctxt =
    10.6    let
    10.7 -    val thy = Proof_Context.theory_of ctxt;
    10.8      val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
    10.9 -    val insts' as (instT', _) = Thm.certify_inst thy (instT, []);
   10.10 +    val insts' as (instT', _) = Thm.certify_inst ctxt' (instT, []);
   10.11      val ths' = map (Thm.instantiate insts') ths;
   10.12    in ((instT', ths'), ctxt') end;
   10.13  
   10.14 @@ -592,9 +591,8 @@
   10.15  
   10.16  fun import is_open ths ctxt =
   10.17    let
   10.18 -    val thy = Proof_Context.theory_of ctxt;
   10.19      val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
   10.20 -    val insts' = Thm.certify_inst thy insts;
   10.21 +    val insts' = Thm.certify_inst ctxt' insts;
   10.22      val ths' = map (Thm.instantiate insts') ths;
   10.23    in ((insts', ths'), ctxt') end;
   10.24  
    11.1 --- a/src/Tools/Code/code_preproc.ML	Tue Jun 02 23:00:50 2015 +0200
    11.2 +++ b/src/Tools/Code/code_preproc.ML	Wed Jun 03 19:25:05 2015 +0200
    11.3 @@ -178,7 +178,7 @@
    11.4      if eq_list (eq_fst (op =)) (vs_normalized, vs_original)
    11.5      then (I, ct)
    11.6      else
    11.7 -     (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global,
    11.8 +     (Thm.certify_instantiate ctxt (normalization, []) o Thm.varifyT_global,
    11.9        Thm.cterm_of ctxt (map_types normalize t))
   11.10    end;
   11.11