--- a/src/HOL/Nominal/nominal_datatype.ML Sun Jul 26 20:54:02 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Sun Jul 26 20:56:44 2015 +0200
@@ -1640,7 +1640,7 @@
HOLogic.mk_Trueprop (fresh_const aT T $ a $ x)] @
freshs))
(HOLogic.mk_Trueprop (fresh_const aT U $ a $ y))
- (fn {prems, context} =>
+ (fn {prems, context = ctxt} =>
let
val (finite_prems, rec_prem :: unique_prem ::
fresh_prems) = chop (length finite_prems) prems;
@@ -1649,28 +1649,28 @@
val _ $ (_ $ (_ $ S $ _)) $ _ = Thm.prop_of supports_fresh;
val tuple = foldr1 HOLogic.mk_prod (x :: rec_fns')
in EVERY
- [resolve_tac context [Drule.cterm_instantiate
- [(Thm.global_cterm_of thy11 S,
- Thm.global_cterm_of thy11 (Const (@{const_name Nominal.supp},
+ [resolve_tac ctxt [infer_instantiate ctxt
+ [(#1 (dest_Var S),
+ Thm.cterm_of ctxt (Const (@{const_name Nominal.supp},
fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))]
supports_fresh] 1,
- simp_tac (put_simpset HOL_basic_ss context addsimps
+ simp_tac (put_simpset HOL_basic_ss ctxt addsimps
[supports_def, Thm.symmetric fresh_def, fresh_prod]) 1,
- REPEAT_DETERM (resolve_tac context [allI, impI] 1),
- REPEAT_DETERM (eresolve_tac context [conjE] 1),
- resolve_tac context [unique] 1,
- SUBPROOF (fn {context = ctxt, prems = prems', params = [(_, a), (_, b)], ...} =>
+ REPEAT_DETERM (resolve_tac ctxt [allI, impI] 1),
+ REPEAT_DETERM (eresolve_tac ctxt [conjE] 1),
+ resolve_tac ctxt [unique] 1,
+ SUBPROOF (fn {context = ctxt', prems = prems', params = [(_, a), (_, b)], ...} =>
EVERY [cut_facts_tac [rec_prem] 1,
- resolve_tac ctxt [Thm.instantiate ([],
+ resolve_tac ctxt' [Thm.instantiate ([],
[((("pi", 0), mk_permT aT),
- Thm.global_cterm_of thy11
+ Thm.cterm_of ctxt'
(perm_of_pair (Thm.term_of a, Thm.term_of b)))]) eqvt_th] 1,
- asm_simp_tac (put_simpset HOL_ss context addsimps
- (prems' @ perm_swap @ perm_fresh_fresh)) 1]) context 1,
- resolve_tac context [rec_prem] 1,
- simp_tac (put_simpset HOL_ss context addsimps (fs_name ::
+ asm_simp_tac (put_simpset HOL_ss ctxt' addsimps
+ (prems' @ perm_swap @ perm_fresh_fresh)) 1]) ctxt 1,
+ resolve_tac ctxt [rec_prem] 1,
+ simp_tac (put_simpset HOL_ss ctxt addsimps (fs_name ::
supp_prod :: finite_Un :: finite_prems)) 1,
- simp_tac (put_simpset HOL_ss context addsimps (Thm.symmetric fresh_def ::
+ simp_tac (put_simpset HOL_ss ctxt addsimps (Thm.symmetric fresh_def ::
fresh_prod :: fresh_prems)) 1]
end))
end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ eqvt_ths)
@@ -1690,16 +1690,17 @@
Abs ("y", U, R $ Free x $ Bound 0))
(rec_unique_frees ~~ rec_result_Ts ~~ rec_sets);
- val induct_aux_rec = Drule.cterm_instantiate
- (map (apply2 (Thm.global_cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort))
- (map (fn (aT, f) => (Logic.varify_global f, Abs ("z", HOLogic.unitT,
+ val induct_aux_rec =
+ infer_instantiate (Proof_Context.init_global thy11)
+ (map (apsnd (Thm.global_cterm_of thy11 o augment_sort thy11 fs_cp_sort))
+ (map (fn (aT, f) => (#1 (dest_Var (Logic.varify_global f)), Abs ("z", HOLogic.unitT,
Const (@{const_name Nominal.supp}, fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
fresh_fs @
map (fn (((P, T), (x, U)), Q) =>
- (Var ((P, 0), Logic.varifyT_global (fsT' --> T --> HOLogic.boolT)),
+ ((P, 0),
Abs ("z", HOLogic.unitT, absfree (x, U) Q)))
(pnames ~~ recTs ~~ rec_unique_frees ~~ rec_unique_concls) @
- map (fn (s, T) => (Var ((s, 0), Logic.varifyT_global T), Free (s, T)))
+ map (fn (s, T) => ((s, 0), Free (s, T)))
rec_unique_frees)) induct_aux;
fun obtain_fresh_name vs ths rec_fin_supp T (freshs1, freshs2, ctxt) =
--- a/src/HOL/Nominal/nominal_induct.ML Sun Jul 26 20:54:02 2015 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Sun Jul 26 20:56:44 2015 +0200
@@ -54,9 +54,9 @@
end;
val substs =
map2 subst insts concls |> flat |> distinct (op =)
- |> map (apply2 (Thm.cterm_of ctxt));
+ |> map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of ctxt u));
in
- (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule)
+ (((cases, nconcls), consumes), infer_instantiate ctxt substs joined_rule)
end;
fun rename_params_rule internal xs rule =
--- a/src/HOL/Nominal/nominal_inductive.ML Sun Jul 26 20:54:02 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Sun Jul 26 20:56:44 2015 +0200
@@ -36,8 +36,8 @@
val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
(Drule.strip_imp_concl (Thm.cprop_of perm_boolI))));
-fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
- [(perm_boolI_pi, pi)] perm_boolI;
+fun mk_perm_bool ctxt pi th =
+ th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI;
fun mk_perm_bool_simproc names =
Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
@@ -348,7 +348,7 @@
Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
addsimprocs [NominalDatatype.perm_simproc])
(Simplifier.simplify (put_simpset eqvt_ss ctxt')
- (fold_rev (mk_perm_bool o Thm.global_cterm_of thy)
+ (fold_rev (mk_perm_bool ctxt' o Thm.cterm_of ctxt')
(rev pis' @ pis) th));
val (gprems1, gprems2) = split_list
(map (fn (th, t) =>
@@ -509,7 +509,7 @@
val freshs2' = NominalDatatype.mk_not_sym freshs2;
val pis = map (NominalDatatype.perm_of_pair)
((freshs1 ~~ map fst qs) @ (params' ~~ freshs1));
- val mk_pis = fold_rev mk_perm_bool (map (Thm.global_cterm_of thy) pis);
+ val mk_pis = fold_rev (mk_perm_bool ctxt3) (map (Thm.cterm_of ctxt3) pis);
val obj = Thm.global_cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms
(fn x as Free _ =>
if member (op =) args x then x
@@ -634,9 +634,9 @@
val prems' = map (fn th => the_default th (map_thm ctxt''
(split_conj (K I) names) (eresolve_tac ctxt'' [conjunct2] 1) monos NONE th)) prems;
val prems'' = map (fn th => Simplifier.simplify eqvt_simpset
- (mk_perm_bool (Thm.global_cterm_of thy pi) th)) prems';
- val intr' = Drule.cterm_instantiate (map (Thm.global_cterm_of thy) vs ~~
- map (Thm.global_cterm_of thy o NominalDatatype.mk_perm [] pi o Thm.term_of o #2) params)
+ (mk_perm_bool ctxt'' (Thm.cterm_of ctxt'' pi) th)) prems';
+ val intr' = infer_instantiate ctxt'' (map (#1 o dest_Var) vs ~~
+ map (Thm.cterm_of ctxt'' o NominalDatatype.mk_perm [] pi o Thm.term_of o #2) params)
intr
in (resolve_tac ctxt'' [intr'] THEN_ALL_NEW (TRY o resolve_tac ctxt'' prems'')) 1
end) ctxt' 1 st
--- a/src/HOL/Nominal/nominal_inductive2.ML Sun Jul 26 20:54:02 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Sun Jul 26 20:56:44 2015 +0200
@@ -40,8 +40,8 @@
val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
(Drule.strip_imp_concl (Thm.cprop_of perm_boolI))));
-fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
- [(perm_boolI_pi, pi)] perm_boolI;
+fun mk_perm_bool ctxt pi th =
+ th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI;
fun mk_perm_bool_simproc names =
Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
@@ -402,7 +402,7 @@
Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
addsimprocs [NominalDatatype.perm_simproc])
(Simplifier.simplify (put_simpset eqvt_ss ctxt')
- (fold_rev (mk_perm_bool o Thm.global_cterm_of thy)
+ (fold_rev (mk_perm_bool ctxt' o Thm.cterm_of ctxt')
(pis' @ pis) th));
val gprems2 = map (fn (th, t) =>
if null (preds_of ps t) then mk_pi th
--- a/src/HOL/Nominal/nominal_permeq.ML Sun Jul 26 20:54:02 2015 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Sun Jul 26 20:56:44 2015 +0200
@@ -305,8 +305,9 @@
val supports_rule' = Thm.lift_rule goal supports_rule;
val _ $ (_ $ S $ _) =
Logic.strip_assums_concl (hd (Thm.prems_of supports_rule'));
- val supports_rule'' = Drule.cterm_instantiate
- [apply2 (Thm.cterm_of ctxt) (head_of S, s')] supports_rule'
+ val supports_rule'' =
+ infer_instantiate ctxt
+ [(#1 (dest_Var (head_of S)), Thm.cterm_of ctxt s')] supports_rule';
val fin_supp = Proof_Context.get_thms ctxt "fin_supp"
val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
in
@@ -348,8 +349,9 @@
val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
val _ $ (_ $ S $ _) =
Logic.strip_assums_concl (hd (Thm.prems_of supports_fresh_rule'));
- val supports_fresh_rule'' = Drule.cterm_instantiate
- [apply2 (Thm.cterm_of ctxt) (head_of S, s')] supports_fresh_rule'
+ val supports_fresh_rule'' =
+ infer_instantiate ctxt
+ [(#1 (dest_Var (head_of S)), Thm.cterm_of ctxt s')] supports_fresh_rule';
in
(tactical ctxt ("guessing of the right set that supports the goal",
(EVERY [compose_tac ctxt (false, supports_fresh_rule'', 3) i,
--- a/src/HOL/Nominal/nominal_thmdecls.ML Sun Jul 26 20:54:02 2015 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Sun Jul 26 20:56:44 2015 +0200
@@ -53,16 +53,15 @@
fun prove_eqvt_tac ctxt orig_thm pi pi' =
let
val thy = Proof_Context.theory_of ctxt
- val mypi = Thm.global_cterm_of thy pi
val T = fastype_of pi'
- val mypifree = Thm.global_cterm_of thy (Const (@{const_name "rev"}, T --> T) $ pi')
+ val mypifree = Thm.cterm_of ctxt (Const (@{const_name "rev"}, T --> T) $ pi')
val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"
in
EVERY1 [tactic ctxt ("iffI applied", resolve_tac ctxt @{thms iffI}),
tactic ctxt ("remove pi with perm_boolE", dresolve_tac ctxt @{thms perm_boolE}),
tactic ctxt ("solve with orig_thm", eresolve_tac ctxt [orig_thm]),
tactic ctxt ("applies orig_thm instantiated with rev pi",
- dresolve_tac ctxt [Drule.cterm_instantiate [(mypi,mypifree)] orig_thm]),
+ dresolve_tac ctxt [infer_instantiate ctxt [(#1 (dest_Var pi), mypifree)] orig_thm]),
tactic ctxt ("getting rid of the pi on the right", resolve_tac ctxt @{thms perm_boolI}),
tactic ctxt ("getting rid of all remaining perms",
full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps perm_pi_simp))]