--- a/src/HOL/Tools/Lifting/lifting_def.ML Fri Mar 06 23:33:25 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri Mar 06 23:38:59 2015 +0100
@@ -56,8 +56,7 @@
fun try_prove_reflexivity ctxt prop =
let
- val thy = Proof_Context.theory_of ctxt
- val cprop = Thm.global_cterm_of thy prop
+ val cprop = Thm.cterm_of ctxt prop
val rule = @{thm ge_eq_refl}
val concl_pat = Drule.strip_imp_concl (Thm.cprop_of rule)
val insts = Thm.first_order_match (concl_pat, cprop)
@@ -85,7 +84,6 @@
let
val tm = (strip_args 2 o HOLogic.dest_Trueprop o Thm.concl_of) thm;
val param_rel = (snd o dest_comb o fst o dest_comb) tm;
- val thy = Proof_Context.theory_of ctxt;
val free_vars = Term.add_vars param_rel [];
fun make_subst (var as (_, typ)) subst =
@@ -99,7 +97,7 @@
end;
val subst = fold make_subst free_vars [];
- val csubst = map (apply2 (Thm.global_cterm_of thy)) subst;
+ val csubst = map (apply2 (Thm.cterm_of ctxt)) subst;
val inst_thm = Drule.cterm_instantiate csubst thm;
in
Conv.fconv_rule
@@ -108,37 +106,37 @@
(Raw_Simplifier.rewrite ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm
end
- fun inst_relcomppI thy ant1 ant2 =
+ fun inst_relcomppI ctxt ant1 ant2 =
let
val t1 = (HOLogic.dest_Trueprop o Thm.concl_of) ant1
val t2 = (HOLogic.dest_Trueprop o Thm.prop_of) ant2
- val fun1 = Thm.global_cterm_of thy (strip_args 2 t1)
- val args1 = map (Thm.global_cterm_of thy) (get_args 2 t1)
- val fun2 = Thm.global_cterm_of thy (strip_args 2 t2)
- val args2 = map (Thm.global_cterm_of thy) (get_args 1 t2)
+ val fun1 = Thm.cterm_of ctxt (strip_args 2 t1)
+ val args1 = map (Thm.cterm_of ctxt) (get_args 2 t1)
+ val fun2 = Thm.cterm_of ctxt (strip_args 2 t2)
+ val args2 = map (Thm.cterm_of ctxt) (get_args 1 t2)
val relcomppI = Drule.incr_indexes2 ant1 ant2 @{thm relcomppI}
val vars = (rev (Term.add_vars (Thm.prop_of relcomppI) []))
- val subst = map (apfst (Thm.global_cterm_of thy o Var)) (vars ~~ ([fun1] @ args1 @ [fun2] @ args2))
+ val subst = map (apfst (Thm.cterm_of ctxt o Var)) (vars ~~ ([fun1] @ args1 @ [fun2] @ args2))
in
Drule.cterm_instantiate subst relcomppI
end
fun zip_transfer_rules ctxt thm =
let
- val thy = Proof_Context.theory_of ctxt
fun mk_POS ty = Const (@{const_name POS}, ty --> ty --> HOLogic.boolT)
val rel = (Thm.dest_fun2 o Thm.dest_arg o Thm.cprop_of) thm
val typ = Thm.typ_of_cterm rel
- val POS_const = Thm.global_cterm_of thy (mk_POS typ)
- val var = Thm.global_cterm_of thy (Var (("X", Thm.maxidx_of_cterm rel + 1), typ))
+ val POS_const = Thm.cterm_of ctxt (mk_POS typ)
+ val var = Thm.cterm_of ctxt (Var (("X", Thm.maxidx_of_cterm rel + 1), typ))
val goal =
- Thm.apply (Thm.global_cterm_of thy HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var)
+ Thm.apply (Thm.cterm_of ctxt HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var)
in
[Lifting_Term.merge_transfer_relations ctxt goal, thm] MRSL @{thm POS_apply}
end
- val thm = (inst_relcomppI (Proof_Context.theory_of ctxt) parametric_transfer_rule transfer_rule)
- OF [parametric_transfer_rule, transfer_rule]
+ val thm =
+ inst_relcomppI ctxt parametric_transfer_rule transfer_rule
+ OF [parametric_transfer_rule, transfer_rule]
val preprocessed_thm = preprocess ctxt thm
val orig_ctxt = ctxt
val (fixed_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) preprocessed_thm ctxt
@@ -215,8 +213,7 @@
| dest_abs tm = raise TERM("get_abs_var",[tm])
val (var_name, T) = dest_abs (Thm.term_of rhs)
val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt
- val thy = Proof_Context.theory_of ctxt'
- val refl_thm = Thm.reflexive (Thm.global_cterm_of thy (Free (hd new_var_names, T)))
+ val refl_thm = Thm.reflexive (Thm.cterm_of ctxt' (Free (hd new_var_names, T)))
in
Thm.combination def refl_thm |>
singleton (Proof_Context.export ctxt' ctxt)
@@ -301,7 +298,7 @@
SOME mono_eq_thm =>
let
val rep_abs_eq = mono_eq_thm RS rep_abs_thm
- val rep = (Thm.global_cterm_of thy o quot_thm_rep) quot_thm
+ val rep = Thm.cterm_of ctxt (quot_thm_rep quot_thm)
val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
val code_cert = [repped_eq, rep_abs_eq] MRSL trans
@@ -378,9 +375,9 @@
end
local
- fun encode_code_eq thy abs_eq opt_rep_eq (rty, qty) =
+ fun encode_code_eq ctxt abs_eq opt_rep_eq (rty, qty) =
let
- fun mk_type typ = typ |> Logic.mk_type |> Thm.global_cterm_of thy |> Drule.mk_term
+ fun mk_type typ = typ |> Logic.mk_type |> Thm.cterm_of ctxt |> Drule.mk_term
in
Conjunction.intr_balanced [abs_eq, (the_default TrueI opt_rep_eq), mk_type rty, mk_type qty]
end
@@ -429,8 +426,7 @@
fun register_code_eq abs_eq_thm opt_rep_eq_thm (rty, qty) lthy =
let
- val thy = Proof_Context.theory_of lthy
- val encoded_code_eq = encode_code_eq thy abs_eq_thm opt_rep_eq_thm (rty, qty)
+ val encoded_code_eq = encode_code_eq lthy abs_eq_thm opt_rep_eq_thm (rty, qty)
in
if no_no_code lthy (rty, qty) then
(snd oo Local_Theory.note) ((Binding.empty, [register_code_eq_attrib]), [encoded_code_eq]) lthy
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri Mar 06 23:33:25 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri Mar 06 23:38:59 2015 +0100
@@ -106,10 +106,9 @@
let
val typ = (snd o relation_types o snd o dest_Var) var
val sort = Type.sort_of_atyp typ
- val (fresh_var, ctxt) = yield_singleton Variable.invent_types sort ctxt
- val thy = Proof_Context.theory_of ctxt
+ val (fresh_var, ctxt') = yield_singleton Variable.invent_types sort ctxt
in
- ((Thm.global_cterm_of thy var, Thm.global_cterm_of thy (HOLogic.eq_const (TFree fresh_var))), ctxt)
+ (apply2 (Thm.cterm_of ctxt') (var, HOLogic.eq_const (TFree fresh_var)), ctxt')
end
val orig_lthy = lthy
@@ -287,12 +286,10 @@
in
fun reduce_goal not_fix goal tac ctxt =
let
- val thy = Proof_Context.theory_of ctxt
- val orig_ctxt = ctxt
- val (fixed_goal, ctxt) = yield_singleton (import_terms_exclude not_fix) goal ctxt
- val init_goal = Goal.init (Thm.global_cterm_of thy fixed_goal)
+ val (fixed_goal, ctxt') = yield_singleton (import_terms_exclude not_fix) goal ctxt
+ val init_goal = Goal.init (Thm.cterm_of ctxt' fixed_goal)
in
- (singleton (Variable.export ctxt orig_ctxt) o Goal.conclude) (the (SINGLE tac init_goal))
+ (singleton (Variable.export ctxt' ctxt) o Goal.conclude) (the (SINGLE tac init_goal))
end
end
@@ -304,16 +301,14 @@
let
fun generate_transfer_rule pcr_def constraint goal ctxt =
let
- val thy = Proof_Context.theory_of ctxt
- val orig_ctxt = ctxt
- val (fixed_goal, ctxt) = yield_singleton (Variable.import_terms true) goal ctxt
- val init_goal = Goal.init (Thm.global_cterm_of thy fixed_goal)
- val rules = Transfer.get_transfer_raw ctxt
+ val (fixed_goal, ctxt') = yield_singleton (Variable.import_terms true) goal ctxt
+ val init_goal = Goal.init (Thm.cterm_of ctxt' fixed_goal)
+ val rules = Transfer.get_transfer_raw ctxt'
val rules = constraint :: OO_rules @ rules
val tac =
- K (Local_Defs.unfold_tac ctxt [pcr_def]) THEN' REPEAT_ALL_NEW (resolve_tac ctxt rules)
+ K (Local_Defs.unfold_tac ctxt' [pcr_def]) THEN' REPEAT_ALL_NEW (resolve_tac ctxt' rules)
in
- (singleton (Variable.export ctxt orig_ctxt) o Goal.conclude) (the (SINGLE (tac 1) init_goal))
+ (singleton (Variable.export ctxt' ctxt) o Goal.conclude) (the (SINGLE (tac 1) init_goal))
end
fun make_goal pcr_def constr =
@@ -371,18 +366,16 @@
in
fun generate_parametric_id lthy rty id_transfer_rule =
let
- val orig_lthy = lthy
(* it doesn't raise an exception because it would have already raised it in define_pcrel *)
- val (quot_thm, _, lthy) = Lifting_Term.prove_param_quot_thm lthy rty
- val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm)
- val lthy = orig_lthy
+ val (quot_thm, _, ctxt') = Lifting_Term.prove_param_quot_thm lthy rty
+ val parametrized_relator =
+ singleton (Variable.export_terms ctxt' lthy) (quot_thm_crel quot_thm)
val id_transfer =
@{thm id_transfer}
|> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
|> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
val var = Var (hd (Term.add_vars (Thm.prop_of id_transfer) []))
- val thy = Proof_Context.theory_of lthy
- val inst = [(Thm.global_cterm_of thy var, Thm.global_cterm_of thy parametrized_relator)]
+ val inst = [(Thm.cterm_of lthy var, Thm.cterm_of lthy parametrized_relator)]
val id_par_thm = Drule.cterm_instantiate inst id_transfer
in
Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
--- a/src/HOL/Tools/Lifting/lifting_term.ML Fri Mar 06 23:33:25 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Fri Mar 06 23:38:59 2015 +0100
@@ -273,13 +273,13 @@
end
handle QUOT_THM_INTERNAL pretty_msg => raise QUOT_THM (rty, qty, pretty_msg)
-fun force_qty_type thy qty quot_thm =
+fun force_qty_type ctxt qty quot_thm =
let
+ val thy = Proof_Context.theory_of ctxt
val (_, qty_schematic) = quot_thm_rty_qty quot_thm
val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty
- fun prep_ty thy (x, (S, ty)) =
- (Thm.global_ctyp_of thy (TVar (x, S)), Thm.global_ctyp_of thy ty)
- val ty_inst = Vartab.fold (cons o (prep_ty thy)) match_env []
+ fun prep_ty (x, (S, ty)) = apply2 (Thm.ctyp_of ctxt) (TVar (x, S), ty)
+ val ty_inst = Vartab.fold (cons o prep_ty) match_env []
in
Thm.instantiate (ty_inst, []) quot_thm
end
@@ -304,9 +304,8 @@
fun prove_quot_thm ctxt (rty, qty) =
let
- val thy = Proof_Context.theory_of ctxt
val schematic_quot_thm = prove_schematic_quot_thm ctxt (rty, qty)
- val quot_thm = force_qty_type thy qty schematic_quot_thm
+ val quot_thm = force_qty_type ctxt qty schematic_quot_thm
val _ = check_rty_type ctxt rty quot_thm
in
quot_thm
@@ -371,9 +370,8 @@
if null tys
then
let
- val thy = Proof_Context.theory_of ctxt
val instantiated_id_quot_thm =
- instantiate' [SOME (Thm.global_ctyp_of thy ty)] [] @{thm identity_quotient}
+ instantiate' [SOME (Thm.ctyp_of ctxt ty)] [] @{thm identity_quotient}
in
(instantiated_id_quot_thm, (table, ctxt))
end
@@ -388,10 +386,9 @@
then (the (AList.lookup (op=) table ty), (table, ctxt))
else
let
- val thy = Proof_Context.theory_of ctxt
val (Q_t, ctxt') = get_fresh_Q_t ctxt
- val Q_thm = Thm.assume (Thm.global_cterm_of thy Q_t)
- val table' = (ty, Q_thm)::table
+ val Q_thm = Thm.assume (Thm.cterm_of ctxt' Q_t)
+ val table' = (ty, Q_thm) :: table
in
(Q_thm, (table', ctxt'))
end