# HG changeset patch # User wenzelm # Date 1437937004 -7200 # Node ID 12cd198f07afc8c4b71041ed60c0122c166a9a5f # Parent 659117cc29635b2954fe2c9dd4e895788a267659 updated to infer_instantiate; clarified context; diff -r 659117cc2963 -r 12cd198f07af src/HOL/Nominal/nominal_datatype.ML --- 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) = diff -r 659117cc2963 -r 12cd198f07af src/HOL/Nominal/nominal_induct.ML --- 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 = diff -r 659117cc2963 -r 12cd198f07af src/HOL/Nominal/nominal_inductive.ML --- 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 diff -r 659117cc2963 -r 12cd198f07af src/HOL/Nominal/nominal_inductive2.ML --- 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 diff -r 659117cc2963 -r 12cd198f07af src/HOL/Nominal/nominal_permeq.ML --- 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, diff -r 659117cc2963 -r 12cd198f07af src/HOL/Nominal/nominal_thmdecls.ML --- 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))]