# HG changeset patch # User wenzelm # Date 1634312747 -7200 # Node ID 8ee3d5d3c1bf14e34448c2a3a4ff97a783cd8b74 # Parent 6c61341c1b31f660921332a343daad6895beb3d2 more accurate treatment of context, notably for nested Goal.proof / SUBPROOF; diff -r 6c61341c1b31 -r 8ee3d5d3c1bf src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Fri Oct 15 14:18:11 2021 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Fri Oct 15 17:45:47 2021 +0200 @@ -25,7 +25,7 @@ (put_simpset HOL_basic_ss ctxt addsimps inductive_atomize); fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt)); fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 - (Conv.params_conv ~1 (fn ctxt' => Conv.prems_conv ~1 (atomize_conv ctxt')) ctxt)); + (Conv.params_conv ~1 (Conv.prems_conv ~1 o atomize_conv) ctxt)); fun preds_of ps t = inter (op = o apsnd dest_Free) ps (Term.add_frees t []); @@ -275,10 +275,11 @@ val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"; val pt2_atoms = map (fn aT => Global_Theory.get_thm thy ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs; - val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy) - addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) - addsimprocs [mk_perm_bool_simproc [\<^const_name>\Fun.id\], - NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]); + fun eqvt_ss ctxt = + put_simpset HOL_basic_ss ctxt + addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) + addsimprocs [mk_perm_bool_simproc [\<^const_name>\Fun.id\], + NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; val fresh_bij = Global_Theory.get_thms thy "fresh_bij"; val perm_bij = Global_Theory.get_thms thy "perm_bij"; val fs_atoms = map (fn aT => Global_Theory.get_thm thy @@ -299,26 +300,26 @@ (HOLogic.exists_const T $ Abs ("x", T, NominalDatatype.fresh_const T (fastype_of p) $ Bound 0 $ p))) - (fn _ => EVERY - [resolve_tac ctxt exists_fresh' 1, - resolve_tac ctxt fs_atoms 1]); + (fn {context = goal_ctxt, ...} => EVERY + [resolve_tac goal_ctxt exists_fresh' 1, + resolve_tac goal_ctxt fs_atoms 1]); val (([(_, cx)], ths), ctxt') = Obtain.result - (fn ctxt' => EVERY - [eresolve_tac ctxt' [exE] 1, - full_simp_tac (put_simpset HOL_ss ctxt' addsimps (fresh_prod :: fresh_atm)) 1, - full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]) 1, - REPEAT (eresolve_tac ctxt [conjE] 1)]) + (fn goal_ctxt => EVERY + [eresolve_tac goal_ctxt [exE] 1, + full_simp_tac (put_simpset HOL_ss goal_ctxt addsimps (fresh_prod :: fresh_atm)) 1, + full_simp_tac (put_simpset HOL_basic_ss goal_ctxt addsimps [@{thm id_apply}]) 1, + REPEAT (eresolve_tac goal_ctxt [conjE] 1)]) [ex] ctxt in (freshs1 @ [Thm.term_of cx], freshs2 @ ths, ctxt') end; - fun mk_ind_proof ctxt' thss = - Goal.prove ctxt' [] prems' concl' (fn {prems = ihyps, context = ctxt} => - let val th = Goal.prove ctxt [] [] concl (fn {context, ...} => - resolve_tac context [raw_induct] 1 THEN + fun mk_ind_proof ctxt thss = + Goal.prove ctxt [] prems' concl' (fn {prems = ihyps, context = goal_ctxt} => + let val th = Goal.prove goal_ctxt [] [] concl (fn {context = goal_ctxt1, ...} => + resolve_tac goal_ctxt1 [raw_induct] 1 THEN EVERY (maps (fn ((((_, bvars, oprems, _), vc_compat_ths), ihyp), (vs, ihypt)) => - [REPEAT (resolve_tac context [allI] 1), - simp_tac (put_simpset eqvt_ss context) 1, - SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} => + [REPEAT (resolve_tac goal_ctxt1 [allI] 1), + simp_tac (eqvt_ss goal_ctxt1) 1, + SUBPROOF (fn {prems = gprems, params, concl, context = goal_ctxt2, ...} => let val (params', (pis, z)) = chop (length params - length atomTs - 1) (map (Thm.term_of o #2) params) ||> @@ -329,9 +330,9 @@ val pi_bvars = map (fn (t, _) => fold_rev (NominalDatatype.mk_perm []) pis t) bvars'; val (P, ts) = strip_comb (HOLogic.dest_Trueprop (Thm.term_of concl)); - val (freshs1, freshs2, ctxt'') = fold + val (freshs1, freshs2, ctxt') = fold (obtain_fresh_name (ts @ pi_bvars)) - (map snd bvars') ([], [], ctxt'); + (map snd bvars') ([], [], goal_ctxt2); val freshs2' = NominalDatatype.mk_not_sym freshs2; val pis' = map NominalDatatype.perm_of_pair (pi_bvars ~~ freshs1); fun concat_perm pi1 pi2 = @@ -349,19 +350,19 @@ map (fold_rev (NominalDatatype.mk_perm []) (rev pis' @ pis)) params' @ [z]))) ihyp; fun mk_pi th = - Simplifier.simplify (put_simpset HOL_basic_ss ctxt'' addsimps [@{thm id_apply}] + 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 ctxt'' o Thm.cterm_of ctxt'') + (Simplifier.simplify (eqvt_ss ctxt') + (fold_rev (mk_perm_bool ctxt' o Thm.cterm_of ctxt') (rev pis' @ pis) th)); val (gprems1, gprems2) = split_list (map (fn (th, t) => if null (preds_of ps t) then (SOME th, mk_pi th) else - (map_thm ctxt'' (split_conj (K o I) names) - (eresolve_tac ctxt'' [conjunct1] 1) monos NONE th, - mk_pi (the (map_thm ctxt'' (inst_conj_all names ps (rev pis'')) - (inst_conj_all_tac ctxt'' (length pis'')) monos (SOME t) th)))) + (map_thm ctxt' (split_conj (K o I) names) + (eresolve_tac ctxt' [conjunct1] 1) monos NONE th, + mk_pi (the (map_thm ctxt' (inst_conj_all names ps (rev pis'')) + (inst_conj_all_tac ctxt' (length pis'')) monos (SOME t) th)))) (gprems ~~ oprems)) |>> map_filter I; val vc_compat_ths' = map (fn th => let @@ -371,45 +372,48 @@ (fn t => fn u => fresh $ t $ u, lhs, rhs) | _ $ (_ $ (_ $ lhs $ rhs)) => (curry (HOLogic.mk_not o HOLogic.mk_eq), lhs, rhs)); - val th'' = Goal.prove ctxt'' [] [] (HOLogic.mk_Trueprop + val th'' = Goal.prove ctxt' [] [] (HOLogic.mk_Trueprop (bop (fold_rev (NominalDatatype.mk_perm []) pis lhs) (fold_rev (NominalDatatype.mk_perm []) pis rhs))) - (fn _ => simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps - (fresh_bij @ perm_bij)) 1 THEN resolve_tac ctxt'' [th'] 1) - in Simplifier.simplify (put_simpset eqvt_ss ctxt'' addsimps fresh_atm) th'' end) + (fn {context = goal_ctxt3, ...} => + simp_tac (put_simpset HOL_basic_ss goal_ctxt3 addsimps + (fresh_bij @ perm_bij)) 1 THEN resolve_tac goal_ctxt3 [th'] 1) + in Simplifier.simplify (eqvt_ss ctxt' addsimps fresh_atm) th'' end) vc_compat_ths; val vc_compat_ths'' = NominalDatatype.mk_not_sym vc_compat_ths'; (** Since swap_simps simplifies (pi :: 'a prm) o (x :: 'b) to x **) (** we have to pre-simplify the rewrite rules **) - val swap_simps_simpset = put_simpset HOL_ss ctxt'' addsimps swap_simps @ - map (Simplifier.simplify (put_simpset HOL_ss ctxt'' addsimps swap_simps)) + val swap_simps_simpset = put_simpset HOL_ss ctxt' addsimps swap_simps @ + map (Simplifier.simplify (put_simpset HOL_ss ctxt' addsimps swap_simps)) (vc_compat_ths'' @ freshs2'); - val th = Goal.prove ctxt'' [] [] + val th = Goal.prove ctxt' [] [] (HOLogic.mk_Trueprop (list_comb (P $ hd ts, map (fold (NominalDatatype.mk_perm []) pis') (tl ts)))) - (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1, - resolve_tac ctxt'' [ihyp'] 1, + (fn {context = goal_ctxt4, ...} => + EVERY ([simp_tac (eqvt_ss goal_ctxt4) 1, + resolve_tac goal_ctxt4 [ihyp'] 1, REPEAT_DETERM_N (Thm.nprems_of ihyp - length gprems) (simp_tac swap_simps_simpset 1), REPEAT_DETERM_N (length gprems) - (simp_tac (put_simpset HOL_basic_ss ctxt'' + (simp_tac (put_simpset HOL_basic_ss goal_ctxt4 addsimps [inductive_forall_def'] addsimprocs [NominalDatatype.perm_simproc]) 1 THEN - resolve_tac ctxt'' gprems2 1)])); - val final = Goal.prove ctxt'' [] [] (Thm.term_of concl) - (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss ctxt'' + resolve_tac goal_ctxt4 gprems2 1)])); + val final = Goal.prove ctxt' [] [] (Thm.term_of concl) + (fn {context = goal_ctxt5, ...} => + cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss goal_ctxt5 addsimps vc_compat_ths'' @ freshs2' @ perm_fresh_fresh @ fresh_atm) 1); - val final' = Proof_Context.export ctxt'' ctxt' [final]; - in resolve_tac ctxt' final' 1 end) context 1]) + val final' = Proof_Context.export ctxt' goal_ctxt2 [final]; + in resolve_tac goal_ctxt2 final' 1 end) goal_ctxt1 1]) (prems ~~ thss ~~ ihyps ~~ prems''))) in - cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac ctxt [conjE] 1) THEN - REPEAT (REPEAT (resolve_tac ctxt [conjI, impI] 1) THEN - eresolve_tac ctxt [impE] 1 THEN assume_tac ctxt 1 THEN - REPEAT (eresolve_tac ctxt @{thms allE_Nil} 1) THEN - asm_full_simp_tac ctxt 1) - end) |> singleton (Proof_Context.export ctxt' lthy); + cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac goal_ctxt [conjE] 1) THEN + REPEAT (REPEAT (resolve_tac goal_ctxt [conjI, impI] 1) THEN + eresolve_tac goal_ctxt [impE] 1 THEN assume_tac goal_ctxt 1 THEN + REPEAT (eresolve_tac goal_ctxt @{thms allE_Nil} 1) THEN + asm_full_simp_tac goal_ctxt 1) + end) |> singleton (Proof_Context.export ctxt lthy); (** strong case analysis rule **) @@ -460,18 +464,17 @@ concl)) in map mk_prem prems end) cases_prems; - val cases_eqvt_simpset = put_simpset HOL_ss (Proof_Context.init_global thy) - addsimps eqvt_thms @ swap_simps @ perm_pi_simp - addsimprocs [NominalPermeq.perm_simproc_app, - NominalPermeq.perm_simproc_fun]; + fun cases_eqvt_simpset ctxt = + put_simpset HOL_ss ctxt + addsimps eqvt_thms @ swap_simps @ perm_pi_simp + addsimprocs [NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; - val simp_fresh_atm = map - (Simplifier.simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) - addsimps fresh_atm)); + fun simp_fresh_atm ctxt = + Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps fresh_atm); - fun mk_cases_proof ((((name, thss), elim), (prem, args, concl, (prems, ctxt'))), + fun mk_cases_proof ((((name, thss), elim), (prem, args, concl, (prems, ctxt))), prems') = - (name, Goal.prove ctxt' [] (prem :: prems') concl + (name, Goal.prove ctxt [] (prem :: prems') concl (fn {prems = hyp :: hyps, context = ctxt1} => EVERY (resolve_tac ctxt1 [hyp RS elim] 1 :: map (fn (((_, vc_compat_ths), case_hyp), (_, qs, is, _)) => @@ -529,8 +532,8 @@ SUBPROOF (fn {context = ctxt5, prems = fresh_hyps, ...} => let val fresh_hyps' = NominalDatatype.mk_not_sym fresh_hyps; - val case_simpset = cases_eqvt_simpset addsimps freshs2' @ - simp_fresh_atm (vc_compat_ths' @ fresh_hyps'); + val case_simpset = cases_eqvt_simpset ctxt5 addsimps freshs2' @ + map (simp_fresh_atm ctxt5) (vc_compat_ths' @ fresh_hyps'); val fresh_fresh_simpset = case_simpset addsimps perm_fresh_fresh; val hyps1' = map (mk_pis #> Simplifier.simplify fresh_fresh_simpset) hyps1; @@ -545,7 +548,7 @@ val final = Proof_Context.export ctxt3 ctxt2 [th] in resolve_tac ctxt2 final 1 end) ctxt1 1) (thss ~~ hyps ~~ prems))) |> - singleton (Proof_Context.export ctxt' lthy)) + singleton (Proof_Context.export ctxt lthy)) in ctxt'' |> @@ -633,16 +636,16 @@ in error ("Could not prove equivariance for introduction rule\n" ^ Syntax.string_of_term ctxt' t ^ "\n" ^ s) end; - val res = SUBPROOF (fn {context = ctxt'', prems, params, ...} => + val res = SUBPROOF (fn {context = goal_ctxt, prems, params, ...} => let - 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 ctxt'') - (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) + val prems' = map (fn th => the_default th (map_thm goal_ctxt + (split_conj (K I) names) (eresolve_tac goal_ctxt [conjunct2] 1) monos NONE th)) prems; + val prems'' = map (fn th => Simplifier.simplify (eqvt_simpset goal_ctxt) + (mk_perm_bool goal_ctxt (Thm.cterm_of goal_ctxt pi) th)) prems'; + val intr' = infer_instantiate goal_ctxt (map (#1 o dest_Var) vs ~~ + map (Thm.cterm_of goal_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 + in (resolve_tac goal_ctxt [intr'] THEN_ALL_NEW (TRY o resolve_tac goal_ctxt prems'')) 1 end) ctxt 1 st in case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of @@ -662,10 +665,10 @@ HOLogic.mk_imp (p, list_comb (h, ts1 @ map (NominalDatatype.mk_perm [] pi') ts2)) end) ps))) - (fn {context = ctxt'', ...} => - EVERY (resolve_tac ctxt'' [raw_induct] 1 :: map (fn intr_vs => - full_simp_tac (eqvt_simpset ctxt'') 1 THEN - eqvt_tac ctxt'' pi' intr_vs) intrs')) |> + (fn {context = goal_ctxt, ...} => + EVERY (resolve_tac goal_ctxt [raw_induct] 1 :: map (fn intr_vs => + full_simp_tac (eqvt_simpset goal_ctxt) 1 THEN + eqvt_tac goal_ctxt pi' intr_vs) intrs')) |> singleton (Proof_Context.export ctxt1 lthy))) end) atoms in diff -r 6c61341c1b31 -r 8ee3d5d3c1bf src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Fri Oct 15 14:18:11 2021 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Oct 15 17:45:47 2021 +0200 @@ -26,7 +26,7 @@ (put_simpset HOL_basic_ss ctxt addsimps inductive_atomize); fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt)); fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 - (Conv.params_conv ~1 (K (Conv.prems_conv ~1 (atomize_conv ctxt))) ctxt)); + (Conv.params_conv ~1 (Conv.prems_conv ~1 o atomize_conv) ctxt)); fun fresh_postprocess ctxt = Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps @@ -136,10 +136,10 @@ let val prop = Thm.prop_of th; fun prove t = - Goal.prove ctxt [] [] t (fn _ => - EVERY [cut_facts_tac [th] 1, eresolve_tac ctxt [rev_mp] 1, - REPEAT_DETERM (FIRSTGOAL (resolve_tac ctxt monos)), - REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))]) + Goal.prove ctxt [] [] t (fn {context = goal_ctxt, ...} => + EVERY [cut_facts_tac [th] 1, eresolve_tac goal_ctxt [rev_mp] 1, + REPEAT_DETERM (FIRSTGOAL (resolve_tac goal_ctxt monos)), + REPEAT_DETERM (resolve_tac goal_ctxt [impI] 1 THEN (assume_tac goal_ctxt 1 ORELSE tac))]) in Option.map prove (map_term f prop (the_default prop opt)) end; fun abs_params params t = @@ -294,10 +294,11 @@ val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"; val pt2_atoms = map (fn a => Global_Theory.get_thm thy ("pt_" ^ Long_Name.base_name a ^ "2")) atoms; - val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy) - addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) - addsimprocs [mk_perm_bool_simproc [\<^const_name>\Fun.id\], - NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]); + fun eqvt_ss ctxt = + put_simpset HOL_basic_ss ctxt + addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) + addsimprocs [mk_perm_bool_simproc [\<^const_name>\Fun.id\], + NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij"; val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms; val at_insts = map (NominalAtoms.at_inst_of thy) atoms; @@ -343,22 +344,23 @@ (Logic.list_all (map (pair "pi") pTs, HOLogic.mk_Trueprop (f $ fold_rev (NominalDatatype.mk_perm (rev pTs)) (pis1 @ pi :: pis2) l $ r))) - (fn _ => cut_facts_tac [th2] 1 THEN - full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps perm_set_forget) 1) |> - Simplifier.simplify (put_simpset eqvt_ss ctxt') + (fn {context = goal_ctxt, ...} => + cut_facts_tac [th2] 1 THEN + full_simp_tac (put_simpset HOL_basic_ss goal_ctxt addsimps perm_set_forget) 1) |> + Simplifier.simplify (eqvt_ss ctxt') in (freshs @ [Thm.term_of cx], ths1 @ ths, ths2 @ [th1], ths3 @ [th2'], ctxt') end; - fun mk_ind_proof ctxt' thss = - Goal.prove ctxt' [] prems' concl' (fn {prems = ihyps, context = ctxt} => - let val th = Goal.prove ctxt [] [] concl (fn {context, ...} => - resolve_tac ctxt [raw_induct] 1 THEN + fun mk_ind_proof ctxt thss = + Goal.prove ctxt [] prems' concl' (fn {prems = ihyps, context = goal_ctxt} => + let val th = Goal.prove goal_ctxt [] [] concl (fn {context = goal_ctxt1, ...} => + resolve_tac goal_ctxt1 [raw_induct] 1 THEN EVERY (maps (fn (((((_, sets, oprems, _), vc_compat_ths), vc_compat_vs), ihyp), vs_ihypt) => - [REPEAT (resolve_tac ctxt [allI] 1), simp_tac (put_simpset eqvt_ss context) 1, - SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} => + [REPEAT (resolve_tac goal_ctxt1 [allI] 1), simp_tac (eqvt_ss goal_ctxt1) 1, + SUBPROOF (fn {prems = gprems, params, concl, context = goal_ctxt2, ...} => let val (cparams', (pis, z)) = chop (length params - length atomTs - 1) (map #2 params) ||> @@ -371,8 +373,8 @@ val gprems1 = map_filter (fn (th, t) => if null (preds_of ps t) then SOME th else - map_thm ctxt' (split_conj (K o I) names) - (eresolve_tac ctxt' [conjunct1] 1) monos NONE th) + map_thm goal_ctxt2 (split_conj (K o I) names) + (eresolve_tac goal_ctxt2 [conjunct1] 1) monos NONE th) (gprems ~~ oprems); val vc_compat_ths' = map2 (fn th => fn p => let @@ -380,20 +382,21 @@ val (h, ts) = strip_comb (HOLogic.dest_Trueprop (Thm.concl_of th')) in - Goal.prove ctxt' [] [] + Goal.prove goal_ctxt2 [] [] (HOLogic.mk_Trueprop (list_comb (h, map (fold_rev (NominalDatatype.mk_perm []) pis) ts))) - (fn _ => simp_tac (put_simpset HOL_basic_ss ctxt' addsimps - (fresh_star_bij @ finite_ineq)) 1 THEN resolve_tac ctxt' [th'] 1) + (fn {context = goal_ctxt3, ...} => + simp_tac (put_simpset HOL_basic_ss goal_ctxt3 addsimps + (fresh_star_bij @ finite_ineq)) 1 THEN resolve_tac goal_ctxt3 [th'] 1) end) vc_compat_ths vc_compat_vs; val (vc_compat_ths1, vc_compat_ths2) = chop (length vc_compat_ths - length sets) vc_compat_ths'; val vc_compat_ths1' = map (Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv - (Simplifier.rewrite (put_simpset eqvt_ss ctxt'))))) vc_compat_ths1; + (Simplifier.rewrite (eqvt_ss goal_ctxt2))))) vc_compat_ths1; val (pis', fresh_ths1, fresh_ths2, fresh_ths3, ctxt'') = fold (obtain_fresh_name ts sets) - (map snd sets' ~~ vc_compat_ths2) ([], [], [], [], ctxt'); + (map snd sets' ~~ vc_compat_ths2) ([], [], [], [], goal_ctxt2); fun concat_perm pi1 pi2 = let val T = fastype_of pi1 in if T = fastype_of pi2 then @@ -405,16 +408,17 @@ (map (fold_rev (NominalDatatype.mk_perm []) (pis' @ pis) #> Thm.global_cterm_of thy) params' @ [Thm.global_cterm_of thy z]); fun mk_pi th = - Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}] + 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 ctxt' o Thm.cterm_of ctxt') + (Simplifier.simplify (eqvt_ss ctxt'') + (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 else - mk_pi (the (map_thm ctxt' (inst_conj_all names ps (rev pis'')) - (inst_conj_all_tac ctxt' (length pis'')) monos (SOME t) th))) + mk_pi (the (map_thm ctxt'' (inst_conj_all names ps (rev pis'')) + (inst_conj_all_tac ctxt'' (length pis'')) monos (SOME t) th))) (gprems ~~ oprems); val perm_freshs_freshs' = map (fn (th, (_, T)) => th RS the (AList.lookup op = perm_freshs_freshs T)) @@ -422,31 +426,32 @@ val th = Goal.prove ctxt'' [] [] (HOLogic.mk_Trueprop (list_comb (P $ hd ts, map (fold_rev (NominalDatatype.mk_perm []) pis') (tl ts)))) - (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1, - resolve_tac ctxt'' [ihyp'] 1] @ - map (fn th => resolve_tac ctxt'' [th] 1) fresh_ths3 @ + (fn {context = goal_ctxt4, ...} => + EVERY ([simp_tac (eqvt_ss goal_ctxt4) 1, + resolve_tac goal_ctxt4 [ihyp'] 1] @ + map (fn th => resolve_tac goal_ctxt4 [th] 1) fresh_ths3 @ [REPEAT_DETERM_N (length gprems) - (simp_tac (put_simpset HOL_basic_ss ctxt'' + (simp_tac (put_simpset HOL_basic_ss goal_ctxt4 addsimps [inductive_forall_def'] addsimprocs [NominalDatatype.perm_simproc]) 1 THEN - resolve_tac ctxt'' gprems2 1)])); + resolve_tac goal_ctxt4 gprems2 1)])); val final = Goal.prove ctxt'' [] [] (Thm.term_of concl) - (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss ctxt'' + (fn {context = goal_ctxt5, ...} => + cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss goal_ctxt5 addsimps vc_compat_ths1' @ fresh_ths1 @ perm_freshs_freshs') 1); - val final' = Proof_Context.export ctxt'' ctxt' [final]; - in resolve_tac ctxt' final' 1 end) context 1]) + val final' = Proof_Context.export ctxt'' goal_ctxt2 [final]; + in resolve_tac goal_ctxt2 final' 1 end) goal_ctxt1 1]) (prems ~~ thss ~~ vc_compat' ~~ ihyps ~~ prems''))) in - cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac ctxt' [conjE] 1) THEN - REPEAT (REPEAT (resolve_tac ctxt' [conjI, impI] 1) THEN - eresolve_tac ctxt' [impE] 1 THEN - assume_tac ctxt' 1 THEN REPEAT (eresolve_tac ctxt' @{thms allE_Nil} 1) THEN - asm_full_simp_tac ctxt 1) + cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac goal_ctxt [conjE] 1) THEN + REPEAT (REPEAT (resolve_tac goal_ctxt [conjI, impI] 1) THEN + eresolve_tac goal_ctxt [impE] 1 THEN + assume_tac goal_ctxt 1 THEN REPEAT (eresolve_tac goal_ctxt @{thms allE_Nil} 1) THEN + asm_full_simp_tac goal_ctxt 1) end) |> - fresh_postprocess ctxt' |> - singleton (Proof_Context.export ctxt' lthy); - + fresh_postprocess ctxt |> + singleton (Proof_Context.export ctxt lthy); in ctxt'' |> Proof.theorem NONE (fn thss => fn lthy1 =>