# HG changeset patch # User Christian Urban # Date 1366326652 -3600 # Node ID 89158f401b070ceb606314bbe7a74c88541ffa00 # Parent d67a6a48f1c732b2ba1af163f7f4ff91a6b1117a updated to simplifier changes diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Mon Apr 01 23:22:53 2013 +0100 +++ b/Nominal/Nominal2.thy Fri Apr 19 00:10:52 2013 +0100 @@ -28,7 +28,7 @@ (****************************************************) (* inductive definition involving nominal datatypes *) -ML_file "nominal_inductive.ML" +ML_file "nominal_inductive.ML" (***************************************) @@ -442,15 +442,17 @@ (* postprocessing of eq and fv theorems *) val qeq_iffs' = qeq_iffs - |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms)) - |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) + |> map (simplify (put_simpset HOL_basic_ss lthyC addsimps qfv_supp_thms)) + |> map (simplify (put_simpset HOL_basic_ss lthyC + addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) (* filters the theorems that are of the form "qfv = supp" *) fun is_qfv_thm (@{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ _)) = member (op=) qfvs lhs | is_qfv_thm _ = false val qsupp_constrs = qfv_defs - |> map (simplify (HOL_basic_ss addsimps (filter (is_qfv_thm o prop_of) qfv_supp_thms))) + |> map (simplify (put_simpset HOL_basic_ss lthyC + addsimps (filter (is_qfv_thm o prop_of) qfv_supp_thms))) val transform_thm = @{lemma "x = y \ a \ x \ a \ y" by simp} val transform_thms = @@ -461,7 +463,7 @@ val qfresh_constrs = qsupp_constrs |> map (fn thm => thm RS transform_thm) - |> map (simplify (HOL_basic_ss addsimps transform_thms)) + |> map (simplify (put_simpset HOL_basic_ss lthyC addsimps transform_thms)) (* proving that the qbn result is finite *) val qbn_finite_thms = prove_bns_finite qtys qbns qinduct qbn_defs lthyC diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/Nominal2_Abs.thy --- a/Nominal/Nominal2_Abs.thy Mon Apr 01 23:22:53 2013 +0100 +++ b/Nominal/Nominal2_Abs.thy Fri Apr 19 00:10:52 2013 +0100 @@ -922,9 +922,8 @@ ML {* -fun alpha_single_simproc thm _ ss ctrm = +fun alpha_single_simproc thm _ ctxt ctrm = let - val ctxt = Simplifier.the_context ss val thy = Proof_Context.theory_of ctxt val _ $ (_ $ x) $ (_ $ y) = term_of ctrm val cvrs = union (op =) (Term.add_frees x []) (Term.add_frees y []) diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Mon Apr 01 23:22:53 2013 +0100 +++ b/Nominal/Nominal2_Base.thy Fri Apr 19 00:10:52 2013 +0100 @@ -446,7 +446,7 @@ end lemma permute_set_eq: - shows "p \ X = {x. - p \ x \ X}" + shows "p \ X = {x. - p \ x \ X}" unfolding permute_set_def by (auto) (metis permute_minus_cancel(1)) @@ -823,14 +823,13 @@ {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} {* pushes permutations inside, raises an error if it cannot solve all permutations. *} -simproc_setup perm_simproc ("p \ t") = {* fn _ => fn ss => fn ctrm => +simproc_setup perm_simproc ("p \ t") = {* fn _ => fn ctxt => fn ctrm => case term_of (Thm.dest_arg ctrm) of Free _ => NONE | Var _ => NONE | Const (@{const_name permute}, _) $ _ $ _ => NONE | _ => let - val ctxt = Simplifier.the_context ss val thm = Nominal_Permeq.eqvt_conv ctxt Nominal_Permeq.eqvt_strict_config ctrm handle ERROR _ => Thm.reflexive ctrm in @@ -1864,14 +1863,14 @@ text {* for handling of freshness of functions *} -simproc_setup fresh_fun_simproc ("a \ (f::'a::pt \'b::pt)") = {* fn _ => fn ss => fn ctrm => +simproc_setup fresh_fun_simproc ("a \ (f::'a::pt \'b::pt)") = {* fn _ => fn ctxt => fn ctrm => let val _ $ _ $ f = term_of ctrm in case (Term.add_frees f [], Term.add_vars f []) of ([], []) => SOME(@{thm fresh_fun_eqvt[simplified eqvt_def, THEN Eq_TrueI]}) | (x::_, []) => let - val thy = Proof_Context.theory_of (Simplifier.the_context ss) + val thy = Proof_Context.theory_of ctxt val argx = Free x val absf = absfree x f val cty_inst = [SOME (ctyp_of thy (fastype_of argx)), SOME (ctyp_of thy (fastype_of f))] @@ -2928,7 +2927,7 @@ by (simp_all add: fresh_at_base) -simproc_setup fresh_ineq ("x \ (y::'a::at_base)") = {* fn _ => fn ss => fn ctrm => +simproc_setup fresh_ineq ("x \ (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm => let fun first_is_neg lhs rhs [] = NONE | first_is_neg lhs rhs (thm::thms) = @@ -2940,10 +2939,10 @@ | _ => first_is_neg lhs rhs thms) val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff} - val prems = Simplifier.prems_of ss + val prems = Simplifier.prems_of ctxt |> filter (fn thm => case Thm.prop_of thm of _ $ (Const (@{const_name fresh}, _) $ _ $ _) => true | _ => false) - |> map (simplify (HOL_basic_ss addsimps simp_thms)) + |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps simp_thms)) |> map HOLogic.conj_elims |> flat in @@ -3319,15 +3318,14 @@ apply (auto simp add: fresh_Pair intro: a) done -simproc_setup Fresh_simproc ("Fresh (h::'a::at \ 'b::pt)") = {* fn _ => fn ss => fn ctrm => +simproc_setup Fresh_simproc ("Fresh (h::'a::at \ 'b::pt)") = {* fn _ => fn ctxt => fn ctrm => let - val ctxt = Simplifier.the_context ss val _ $ h = term_of ctrm val cfresh = @{const_name fresh} val catom = @{const_name atom} - val atoms = Simplifier.prems_of ss + val atoms = Simplifier.prems_of ctxt |> map_filter (fn thm => case Thm.prop_of thm of _ $ (Const (cfresh, _) $ (Const (catom, _) $ atm) $ _) => SOME (atm) | _ => NONE) |> distinct (op=) @@ -3337,8 +3335,8 @@ val goal1 = HOLogic.mk_Trueprop (mk_fresh (mk_atom atm) h) val goal2 = HOLogic.mk_Trueprop (mk_fresh (mk_atom atm) (h $ atm)) - val thm1 = Goal.prove ctxt [] [] goal1 (K (asm_simp_tac ss 1)) - val thm2 = Goal.prove ctxt [] [] goal2 (K (asm_simp_tac ss 1)) + val thm1 = Goal.prove ctxt [] [] goal1 (K (asm_simp_tac ctxt 1)) + val thm2 = Goal.prove ctxt [] [] goal2 (K (asm_simp_tac ctxt 1)) in SOME (@{thm Fresh_apply'} OF [thm1, thm2] RS eq_reflection) end handle ERROR _ => NONE diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/Nominal2_FCB.thy --- a/Nominal/Nominal2_FCB.thy Mon Apr 01 23:22:53 2013 +0100 +++ b/Nominal/Nominal2_FCB.thy Fri Apr 19 00:10:52 2013 +0100 @@ -12,7 +12,7 @@ val all_trivials : (Proof.context -> Method.method) context_parser = Scan.succeed (fn ctxt => let - val tac = TRYALL (SOLVED' (full_simp_tac (simpset_of ctxt))) + val tac = TRYALL (SOLVED' (full_simp_tac ctxt)) in Method.SIMPLE_METHOD' (K tac) end) diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Mon Apr 01 23:22:53 2013 +0100 +++ b/Nominal/nominal_dt_alpha.ML Fri Apr 19 00:10:52 2013 +0100 @@ -391,9 +391,9 @@ |> HOLogic.mk_Trueprop end -fun distinct_tac cases_thms distinct_thms = +fun distinct_tac ctxt cases_thms distinct_thms = rtac notI THEN' eresolve_tac cases_thms - THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) + THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps distinct_thms) fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info = let @@ -407,7 +407,7 @@ val goal = mk_distinct_goal ty_trm_assoc raw_distinct_trm in Goal.prove ctxt [] [] goal - (K (distinct_tac alpha_cases raw_distinct_thms 1)) + (K (distinct_tac ctxt alpha_cases raw_distinct_thms 1)) end in map (mk_alpha_distinct o prop_of) raw_distinct_thms @@ -425,11 +425,11 @@ @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI} | _ => thm -fun alpha_eq_iff_tac dist_inj intros elims = - SOLVED' (asm_full_simp_tac (HOL_ss addsimps intros)) ORELSE' +fun alpha_eq_iff_tac ctxt dist_inj intros elims = + SOLVED' (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)) ORELSE' (rtac @{thm iffI} THEN' - RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps dist_inj), - asm_full_simp_tac (HOL_ss addsimps intros)]) + RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj), + asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)]) fun mk_alpha_eq_iff_goal thm = let @@ -449,7 +449,7 @@ val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; val goals = map mk_alpha_eq_iff_goal thms_imp; - val tac = alpha_eq_iff_tac (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_cases 1; + val tac = alpha_eq_iff_tac ctxt (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_cases 1; val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; in Variable.export ctxt' ctxt thms @@ -470,7 +470,7 @@ val bound_tac = EVERY' [ rtac exi_zero, resolve_tac @{thms alpha_refl}, - asm_full_simp_tac (HOL_ss addsimps prod_simps) ] + asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ] in resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac] end @@ -509,7 +509,7 @@ EVERY' [ etac exi_neg, resolve_tac @{thms alpha_sym_eqvt}, - asm_full_simp_tac (HOL_ss addsimps prod_simps), + asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps), eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, trans_prem_tac pred_names ctxt] end @@ -559,7 +559,7 @@ val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel_def} in resolve_tac intros - THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' + THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN' TRY o EVERY' (* if binders are present *) [ etac @{thm exE}, etac @{thm exE}, @@ -568,7 +568,7 @@ atac, aatac pred_names ctxt, eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, - asm_full_simp_tac (HOL_ss addsimps prod_simps) ]) + asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]) end fun prove_trans_tac alpha_result raw_dt_thms alpha_eqvt ctxt = @@ -577,7 +577,7 @@ val alpha_names = alpha_names @ alpha_bn_names fun all_cases ctxt = - asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) + asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps raw_dt_thms) THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt in EVERY' [ rtac @{thm allI}, rtac @{thm impI}, @@ -684,11 +684,12 @@ val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns) val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns - val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} + val simpset = + put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) in alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_raw_induct - (K (asm_full_simp_tac ss)) ctxt + (K (asm_full_simp_tac simpset)) ctxt end @@ -704,10 +705,11 @@ val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys)) - val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def + val simpset = + put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def permute_prod_def prod.cases prod.recs}) - val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss + val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac simpset in alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt end @@ -715,16 +717,16 @@ (* respectfulness for constructors *) -fun raw_constr_rsp_tac alpha_intros simps = +fun raw_constr_rsp_tac ctxt alpha_intros simps = let - val pre_ss = HOL_ss addsimps @{thms fun_rel_def} - val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel_def + val pre_simpset = put_simpset HOL_ss ctxt addsimps @{thms fun_rel_def} + val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def prod_rel_def prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps in - asm_full_simp_tac pre_ss + asm_full_simp_tac pre_simpset THEN' REPEAT o (resolve_tac @{thms allI impI}) THEN' resolve_tac alpha_intros - THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss) + THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_simpset) end fun raw_constrs_rsp ctxt alpha_result constrs simps = @@ -752,7 +754,7 @@ map (fn constrs => Goal.prove_multi ctxt [] [] (map prep_goal constrs) (K (HEADGOAL - (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps)))) constrs + (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac ctxt alpha_intros simps)))) constrs end @@ -799,7 +801,7 @@ val prems'' = map (transform_prem1 context (alpha_names @ alpha_bn_names)) prems' in HEADGOAL - (simp_tac (HOL_basic_ss addsimps (simps @ prems')) + (simp_tac (put_simpset HOL_basic_ss ctxt addsimps (simps @ prems')) THEN' TRY o REPEAT_ALL_NEW (FIRST' [ rtac @{thm TrueI}, rtac @{thm conjI}, diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Mon Apr 01 23:22:53 2013 +0100 +++ b/Nominal/nominal_dt_quot.ML Fri Apr 19 00:10:52 2013 +0100 @@ -192,12 +192,14 @@ fun supports_tac ctxt perm_simps = let - val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]} - val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair} + val simpset1 = + put_simpset HOL_basic_ss ctxt addsimps @{thms supports_def fresh_def[symmetric]} + val simpset2 = + put_simpset HOL_ss ctxt addsimps @{thms swap_fresh_fresh fresh_Pair} in - EVERY' [ simp_tac ss1, + EVERY' [ simp_tac simpset1, eqvt_tac ctxt (eqvt_strict_config addpres perm_simps), - simp_tac ss2 ] + simp_tac simpset2 ] end fun prove_supports_single ctxt perm_simps qtrm = @@ -228,7 +230,8 @@ val tac = EVERY' [ rtac @{thm supports_finite}, resolve_tac qsupports_thms, - asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ] + asm_simp_tac (put_simpset HOL_ss ctxt + addsimps @{thms finite_supp supp_Pair finite_Un}) ] in Goal.prove ctxt' [] [] goals (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) @@ -271,8 +274,7 @@ fun mk_fvs_goals fv = gen_mk_goals fv mk_supp fun mk_fv_bns_goals fv_bn alpha_bn = gen_mk_goals fv_bn (mk_supp_rel alpha_bn) -fun add_ss thms = - HOL_basic_ss addsimps thms +fun add_simpset ctxt thms = put_simpset HOL_basic_ss ctxt addsimps thms fun symmetric thms = map (fn thm => thm RS @{thm sym}) thms @@ -289,13 +291,13 @@ | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs -fun mk_bn_supp_abs_tac trm = +fun mk_bn_supp_abs_tac ctxt trm = trm |> fastype_of |> body_type |> (fn ty => case ty of - @{typ "atom set"} => simp_tac (add_ss supp_Abs_set) - | @{typ "atom list"} => simp_tac (add_ss supp_Abs_lst) + @{typ "atom set"} => simp_tac (add_simpset ctxt supp_Abs_set) + | @{typ "atom list"} => simp_tac (add_simpset ctxt supp_Abs_lst) | _ => raise TERM ("mk_bn_supp_abs_tac", [trm])) @@ -322,22 +324,22 @@ val supp_abs_tac = case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses) - | NONE => mk_bn_supp_abs_tac fv_fun + | NONE => mk_bn_supp_abs_tac ctxt fv_fun val eqvt_rconfig = eqvt_relaxed_config addpres (perm_simps @ fv_bn_eqvts) in - EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), + EVERY' [ TRY o asm_full_simp_tac (add_simpset ctxt (@{thm supp_Pair[symmetric]}::fv_simps)), TRY o supp_abs_tac, - TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), + TRY o simp_tac (add_simpset ctxt @{thms supp_def supp_rel_def}), TRY o eqvt_tac ctxt eqvt_rconfig, - TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), - TRY o asm_full_simp_tac (add_ss thms3), - TRY o simp_tac (add_ss thms2), - TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts)))] i + TRY o simp_tac (add_simpset ctxt (@{thms Abs_eq_iff} @ eq_iffs)), + TRY o asm_full_simp_tac (add_simpset ctxt thms3), + TRY o simp_tac (add_simpset ctxt thms2), + TRY o asm_full_simp_tac (add_simpset ctxt (thms1 @ (symmetric fv_bn_eqvts)))] i end) in induct_prove qtys (goals1 @ goals2) qinduct tac ctxt |> map atomize - |> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]})) + |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms fun_eq_iff[symmetric]})) end @@ -352,7 +354,7 @@ end val props = map mk_goal qbns - val ss_tac = asm_full_simp_tac (HOL_basic_ss addsimps (qbn_simps @ + val ss_tac = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps (qbn_simps @ @{thms set.simps set_append finite_insert finite.emptyI finite_Un})) in induct_prove qtys props qinduct (K ss_tac) ctxt @@ -373,11 +375,11 @@ val props = map2 mk_goal qperm_bns alpha_bns val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls - val ss_tac = asm_full_simp_tac (HOL_ss addsimps ss) + val ss_tac = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps ss) in induct_prove qtys props qinduct (K ss_tac) ctxt' |> Proof_Context.export ctxt' ctxt - |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) + |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms id_def})) end fun prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qbn_eqvts ctxt = @@ -397,13 +399,13 @@ val props = map2 mk_goal qbns qperm_bns val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs val ss_tac = - EVERY' [asm_full_simp_tac (HOL_basic_ss addsimps ss), + EVERY' [asm_full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss), TRY o eqvt_tac ctxt' (eqvt_strict_config addpres qbn_eqvts), - TRY o asm_full_simp_tac HOL_basic_ss] + TRY o asm_full_simp_tac (put_simpset HOL_basic_ss ctxt')] in induct_prove qtys props qinduct (K ss_tac) ctxt' |> Proof_Context.export ctxt' ctxt - |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) + |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms id_def})) end @@ -499,7 +501,7 @@ in Goal.prove ctxt [] [] goal (K (HEADGOAL (rtac @{thm at_set_avoiding1} - THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss))))) + THEN_ALL_NEW (simp_tac (put_simpset HOL_ss ctxt addsimps ss))))) end @@ -539,7 +541,9 @@ then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} else resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} - val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss] + val tac2 = + EVERY' [simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss), + TRY o simp_tac (put_simpset HOL_ss ctxt)] in [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2))) |> (if rec_flag @@ -563,19 +567,20 @@ val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un} val (([(_, fperm)], fprops), ctxt') = Obtain.result - (K (EVERY1 [etac exE, - full_simp_tac (HOL_basic_ss addsimps ss), - REPEAT o (etac @{thm conjE})])) [fthm] ctxt + (fn ctxt' => EVERY1 [etac exE, + full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss), + REPEAT o (etac @{thm conjE})]) [fthm] ctxt val abs_eq_thms = flat (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_eqvt permute_bns) bclauses) val ((_, eqs), ctxt'') = Obtain.result - (K (EVERY1 + (fn ctxt'' => EVERY1 [ REPEAT o (etac @{thm exE}), REPEAT o (etac @{thm conjE}), REPEAT o (dtac setify), - full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt' + full_simp_tac (put_simpset HOL_basic_ss ctxt'' + addsimps @{thms set_append set.simps})]) abs_eq_thms ctxt' val (abs_eqs, peqs) = split_filter is_abs_eq eqs @@ -585,7 +590,7 @@ (* for freshness conditions *) val tac1 = SOLVED' (EVERY' - [ simp_tac (HOL_basic_ss addsimps peqs), + [ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs), rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}), conj_tac (DETERM o resolve_tac fprops') ]) @@ -729,10 +734,11 @@ in rtac thm' 1 end) ctxt - THEN_ALL_NEW asm_full_simp_tac HOL_basic_ss + THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) + (* FIXME proper goal context *) val size_simp_tac = - simp_tac (size_simpset addsimps (@{thms comp_def snd_conv} @ size_thms)) + simp_tac (put_simpset size_ss lthy'' addsimps (@{thms comp_def snd_conv} @ size_thms)) in Goal.prove_multi lthy'' [] prems' concls (fn {prems, context} => diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Mon Apr 01 23:22:53 2013 +0100 +++ b/Nominal/nominal_dt_rawfuns.ML Fri Apr 19 00:10:52 2013 +0100 @@ -52,7 +52,7 @@ (* strip_bn_fun takes a rhs of a bn function: this can only contain unions or appends of elements; in case of recursive calls it returns also the applied bn function *) -fun strip_bn_fun lthy args t = +fun strip_bn_fun ctxt args t = let fun aux t = case t of @@ -65,14 +65,14 @@ | Const (@{const_name bot}, _) => [] | Const (@{const_name Nil}, _) => [] | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)] - | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term lthy t)) + | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term ctxt t)) in aux t end (** definition of the raw binding functions **) -fun prep_bn_info lthy dt_names dts bn_funs eqs = +fun prep_bn_info ctxt dt_names dts bn_funs eqs = let fun process_eq eq = let @@ -85,7 +85,7 @@ val dt_index = find_index (fn x => x = ty_name) dt_names val (cnstr_head, cnstr_args) = strip_comb cnstr val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head)) - val rhs_elements = strip_bn_fun lthy cnstr_args rhs + val rhs_elements = strip_bn_fun ctxt cnstr_args rhs in ((bn_fun, dt_index), (cnstr_name, rhs_elements)) end @@ -344,7 +344,7 @@ (** proves the two pt-type class properties **) -fun prove_permute_zero induct perm_defs perm_fns lthy = +fun prove_permute_zero induct perm_defs perm_fns ctxt = let val perm_types = map (body_type o fastype_of) perm_fns val perm_indnames = Datatype_Prop.make_tnames perm_types @@ -356,17 +356,17 @@ HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) - val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) + val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_zero} :: perm_defs) val tac = (Datatype_Aux.ind_tac induct perm_indnames - THEN_ALL_NEW asm_simp_tac simps) 1 + THEN_ALL_NEW asm_simp_tac simpset) 1 in - Goal.prove lthy perm_indnames [] goals (K tac) + Goal.prove ctxt perm_indnames [] goals (K tac) |> Datatype_Aux.split_conj_thm end -fun prove_permute_plus induct perm_defs perm_fns lthy = +fun prove_permute_plus induct perm_defs perm_fns ctxt = let val p = Free ("p", @{typ perm}) val q = Free ("q", @{typ perm}) @@ -380,12 +380,13 @@ HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) - val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) + (* FIXME proper goal context *) + val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_plus} :: perm_defs) val tac = (Datatype_Aux.ind_tac induct perm_indnames - THEN_ALL_NEW asm_simp_tac simps) 1 + THEN_ALL_NEW asm_simp_tac simpset) 1 in - Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) + Goal.prove ctxt ("p" :: "q" :: perm_indnames) [] goals (K tac) |> Datatype_Aux.split_conj_thm end @@ -458,11 +459,11 @@ val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} fun subproof_tac const_names simps = - SUBPROOF (fn {prems, context, ...} => + SUBPROOF (fn {prems, context = ctxt, ...} => HEADGOAL - (simp_tac (HOL_basic_ss addsimps simps) - THEN' eqvt_tac context (eqvt_relaxed_config addexcls const_names) - THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym])))) + (simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) + THEN' eqvt_tac ctxt (eqvt_relaxed_config addexcls const_names) + THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps (prems @ [eqvt_apply_sym])))) fun prove_eqvt_tac insts ind_thms const_names simps ctxt = HEADGOAL diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/nominal_eqvt.ML --- a/Nominal/nominal_eqvt.ML Mon Apr 01 23:22:53 2013 +0100 +++ b/Nominal/nominal_eqvt.ML Fri Apr 19 00:10:52 2013 +0100 @@ -18,14 +18,14 @@ open Nominal_Permeq; open Nominal_ThmDecls; -val atomize_conv = +fun atomize_conv ctxt = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE)) - (HOL_basic_ss addsimps @{thms induct_atomize}) + (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_atomize}) -val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv) +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)) + (Conv.params_conv ~1 (K (Conv.prems_conv ~1 (atomize_conv ctxt))) ctxt)) (** equivariance tactics **) @@ -36,8 +36,10 @@ val cpi = Thm.cterm_of thy pi val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI} val eqvt_sconfig = eqvt_strict_config addexcls pred_names - val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def permute_self split_paired_all} - val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def permute_minus_cancel(2)} + val simps1 = + put_simpset HOL_basic_ss ctxt addsimps @{thms permute_fun_def permute_self split_paired_all} + val simps2 = + put_simpset HOL_basic_ss ctxt addsimps @{thms permute_bool_def permute_minus_cancel(2)} in eqvt_tac ctxt eqvt_sconfig THEN' SUBPROOF (fn {prems, context as ctxt, ...} => @@ -86,7 +88,7 @@ val pred_names = map (name_of o head_of) preds val raw_induct' = atomize_induct ctxt raw_induct - val intrs' = map atomize_intr intrs + val intrs' = map (atomize_intr ctxt) intrs val (([raw_concl], [raw_pi]), ctxt') = ctxt diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/nominal_function_core.ML --- a/Nominal/nominal_function_core.ML Mon Apr 01 23:22:53 2013 +0100 +++ b/Nominal/nominal_function_core.ML Fri Apr 19 00:10:52 2013 +0100 @@ -349,7 +349,8 @@ Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs val (eql, _) = - Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree + Function_Ctx_Tree.rewrite_by_tree (Proof_Context.init_global thy) + h ih_elim_case (Ris ~~ h_assums) tree val replace_lemma = (eql RS meta_eq_to_obj_eq) |> Thm.implies_intr (cprop_of case_hyp) @@ -483,7 +484,8 @@ val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs - val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro + val ih_intro_case = + full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [case_hyp]) ih_intro fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) @@ -516,7 +518,7 @@ ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)] |> curry (op COMP) existence |> curry (op COMP) uniqueness - |> simplify (HOL_basic_ss addsimps [case_hyp RS sym]) + |> simplify (Simplifier.global_context thy HOL_basic_ss addsimps [case_hyp RS sym]) |> Thm.implies_intr (cprop_of case_hyp) |> fold_rev (Thm.implies_intr o cprop_of) ags |> fold_rev Thm.forall_intr cqs @@ -731,7 +733,7 @@ |> Thm.forall_intr (cterm_of thy z) |> (fn it => it COMP valthm) |> Thm.implies_intr lhs_acc - |> asm_simplify (HOL_basic_ss addsimps [f_iff]) + |> asm_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [f_iff]) |> fold_rev (Thm.implies_intr o cprop_of) ags |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) end @@ -885,7 +887,8 @@ val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, qglr=(oqs, _, _, _), ...} = clause - val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp + val ih_case = + full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [case_hyp]) ihyp fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = let @@ -975,7 +978,7 @@ |> Thm.forall_intr (cterm_of thy R') |> Thm.forall_elim (cterm_of thy (inrel_R)) |> curry op RS wf_in_rel - |> full_simplify (HOL_basic_ss addsimps [in_rel_def]) + |> full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [in_rel_def]) |> Thm.forall_intr (cterm_of thy Rrel) end diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/nominal_induct.ML --- a/Nominal/nominal_induct.ML Mon Apr 01 23:22:53 2013 +0100 +++ b/Nominal/nominal_induct.ML Fri Apr 19 00:10:52 2013 +0100 @@ -22,8 +22,8 @@ Library.funpow (length Ts) HOLogic.mk_split (Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T)); -val split_all_tuples = - Simplifier.full_simplify (HOL_basic_ss addsimps +fun split_all_tuples ctxt = + Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms split_conv split_paired_all unit_all_eq1} @ @{thms fresh_Unit_elim fresh_Pair_elim} @ @{thms fresh_star_Unit_elim fresh_star_Pair_elim fresh_star_Un_elim} @ @@ -93,7 +93,7 @@ val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs; val finish_rule = - split_all_tuples + split_all_tuples defs_ctxt #> rename_params_rule true (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding); diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/nominal_inductive.ML --- a/Nominal/nominal_inductive.ML Mon Apr 01 23:22:53 2013 +0100 +++ b/Nominal/nominal_inductive.ML Fri Apr 19 00:10:52 2013 +0100 @@ -172,7 +172,7 @@ |> flag ? (all_elims [p]) |> flag ? (eqvt_srule context) in - asm_full_simp_tac (HOL_ss addsimps (prm' :: @{thms induct_forall_def})) 1 + asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps (prm' :: @{thms induct_forall_def})) 1 end) ctxt fun non_binder_tac prem intr_cvars Ps ctxt = @@ -215,7 +215,7 @@ val ss = @{thms finite_supp supp_Pair finite_Un permute_finite} @ @{thms fresh_star_Pair fresh_star_permute_iff} - val simp = asm_full_simp_tac (HOL_ss addsimps ss) + val simp = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps ss) in Goal.prove ctxt [] [] fresh_goal (K (HEADGOAL (rtac @{thm at_set_avoiding2} @@ -241,13 +241,14 @@ val concl_args' = map (subst_free (param_trms ~~ prm_trms)) concl_args val user_thm' = map (cterm_instantiate (intr_cvars ~~ prms)) user_thm - |> map (full_simplify (HOL_ss addsimps (@{thm fresh_star_Pair}::prems))) + |> map (full_simplify (put_simpset HOL_ss ctxt addsimps (@{thm fresh_star_Pair}::prems))) val fthm = fresh_thm ctxt user_thm' (term_of p) (term_of c) concl_args' avoid_trm' val (([(_, q)], fprop :: fresh_eqs), ctxt') = Obtain.result (K (EVERY1 [etac @{thm exE}, - full_simp_tac (HOL_basic_ss addsimps @{thms supp_Pair fresh_star_Un}), + full_simp_tac (put_simpset HOL_basic_ss ctxt + addsimps @{thms supp_Pair fresh_star_Un}), REPEAT o etac @{thm conjE}, dtac fresh_star_plus, REPEAT o dtac supp_perm_eq'])) [fthm] ctxt @@ -262,7 +263,7 @@ |> eqvt_srule ctxt val fprop' = eqvt_srule ctxt' fprop - val tac_fresh = simp_tac (HOL_basic_ss addsimps [fprop']) + val tac_fresh = simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [fprop']) (* for inductive-premises*) fun tac1 prm = helper_tac true prm (mk_cplus q p) ctxt' @@ -370,7 +371,8 @@ |> singleton (Proof_Context.export ctxt ctxt_outside) |> Datatype_Aux.split_conj_thm |> map (fn thm => thm RS normalise) - |> map (asm_full_simplify (HOL_basic_ss addsimps @{thms permute_zero induct_rulify})) + |> map (asm_full_simplify (put_simpset HOL_basic_ss ctxt + addsimps @{thms permute_zero induct_rulify})) |> map (Drule.rotate_prems (length ind_prems')) |> map zero_var_indexes diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/nominal_library.ML --- a/Nominal/nominal_library.ML Mon Apr 01 23:22:53 2013 +0100 +++ b/Nominal/nominal_library.ML Fri Apr 19 00:10:52 2013 +0100 @@ -89,7 +89,7 @@ val all_dtyp_constrs_types: Datatype_Aux.descr -> cns_info list (* tactics for function package *) - val size_simpset: simpset + val size_ss: simpset val pat_completeness_simp: thm list -> Proof.context -> tactic val prove_termination_ind: Proof.context -> int -> tactic val prove_termination_fun: thm list -> Proof.context -> Function.info * local_theory @@ -346,19 +346,21 @@ (** function package tactics **) -fun pat_completeness_simp simps lthy = +fun pat_completeness_simp simps ctxt = let - val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps) + val simpset = + put_simpset HOL_basic_ss ctxt addsimps (@{thms sum.inject sum.distinct} @ simps) in - Pat_Completeness.pat_completeness_tac lthy 1 - THEN ALLGOALS (asm_full_simp_tac simp_set) + Pat_Completeness.pat_completeness_tac ctxt 1 + THEN ALLGOALS (asm_full_simp_tac simpset) end (* simpset for size goals *) -val size_simpset = HOL_ss +val size_ss = + simpset_of (put_simpset HOL_ss @{context} addsimprocs [@{simproc natless_cancel_numerals}] addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral - zero_less_Suc prod.size(1) mult_Suc_right} + zero_less_Suc prod.size(1) mult_Suc_right}) val natT = @{typ nat} @@ -413,7 +415,7 @@ val tac = Function_Relation.relation_tac ctxt measure_trm - THEN_ALL_NEW simp_tac (size_simpset addsimps size_simps) + THEN_ALL_NEW simp_tac (put_simpset size_ss ctxt addsimps size_simps) in Function.prove_termination NONE (HEADGOAL tac) ctxt end @@ -446,10 +448,10 @@ fun map_thm_tac ctxt tac thm = let val monos = Inductive.get_monos ctxt - val simps = HOL_basic_ss addsimps @{thms split_def} + val simpset = put_simpset HOL_basic_ss ctxt addsimps @{thms split_def} in EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, - REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)), + REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac monos)), REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] end diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/nominal_mutual.ML --- a/Nominal/nominal_mutual.ML Mon Apr 01 23:22:53 2013 +0100 +++ b/Nominal/nominal_mutual.ML Fri Apr 19 00:10:52 2013 +0100 @@ -198,7 +198,7 @@ (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs) THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 - THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *) + THEN (simp_tac ctxt) 1) |> restore_cond |> export end @@ -223,7 +223,8 @@ |> Variable.variant_fixes ["p"] val p = Free (p, @{typ perm}) - val ss = HOL_basic_ss addsimps + val simpset = + put_simpset HOL_basic_ss ctxt' addsimps @{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric]} @ @{thms Projr.simps Projl.simps} @ [(cond MRS eqvt_thm) RS @{thm sym}] @ @@ -233,7 +234,7 @@ in Goal.prove ctxt' [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (goal_lhs, goal_rhs)) (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs) - THEN (asm_full_simp_tac ss 1)) + THEN (asm_full_simp_tac simpset 1)) |> singleton (Proof_Context.export ctxt' ctxt) |> restore_cond |> export @@ -250,9 +251,9 @@ |> Thm.forall_elim_vars 0 end -fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, parts, ...}) = +fun mutual_induct_rules ctxt induct all_f_defs (Mutual {n, ST, parts, ...}) = let - val cert = cterm_of (Proof_Context.theory_of lthy) + val cert = cterm_of (Proof_Context.theory_of ctxt) val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => Free (Pname, cargTs ---> HOLogic.boolT)) @@ -271,8 +272,8 @@ val induct_inst = Thm.forall_elim (cert case_exp) induct - |> full_simplify SumTree.sumcase_split_ss - |> full_simplify (HOL_basic_ss addsimps all_f_defs) + |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt) + |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs) fun project rule (MutualPart {cargTs, i, ...}) k = let @@ -281,7 +282,7 @@ in (rule |> Thm.forall_elim (cert inj) - |> full_simplify SumTree.sumcase_split_ss + |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt) |> fold_rev (Thm.forall_intr o cert) (afs @ newPs), k + length cargTs) end @@ -350,7 +351,7 @@ |> map (fn th => th RS mp) end -fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = +fun mk_partial_rules_mutual ctxt inner_cont (m as Mutual {parts, fqgars, ...}) proof = let val result = inner_cont proof @@ -359,7 +360,7 @@ val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => - (mk_applied_form lthy cargTs (Thm.symmetric f_def), f)) + (mk_applied_form ctxt cargTs (Thm.symmetric f_def), f)) parts |> split_list @@ -370,18 +371,18 @@ map (fn MutualPart {f = SOME f, cargTs, ...} => cargTs) parts fun mk_mpsimp fqgar sum_psimp = - in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp + in_context ctxt fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp fun mk_meqvts fqgar sum_psimp = - in_context lthy fqgar (recover_mutual_eqvt eqvt all_orig_fdefs parts) sum_psimp + in_context ctxt fqgar (recover_mutual_eqvt eqvt all_orig_fdefs parts) sum_psimp - val rew_ss = HOL_basic_ss addsimps all_f_defs + val rew_simpset = put_simpset HOL_basic_ss ctxt addsimps all_f_defs val mpsimps = map2 mk_mpsimp fqgars psimps - val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m - val mtermination = full_simplify rew_ss termination - val mdomintros = Option.map (map (full_simplify rew_ss)) domintros + val minducts = mutual_induct_rules ctxt simple_pinduct all_f_defs m + val mtermination = full_simplify rew_simpset termination + val mdomintros = Option.map (map (full_simplify rew_simpset)) domintros val meqvts = map2 mk_meqvts fqgars psimps - val meqvt_funs = prove_eqvt lthy fs cargTss meqvts minducts + val meqvt_funs = prove_eqvt ctxt fs cargTss meqvts minducts in NominalFunctionResult { fs=fs, G=G, R=R, psimps=mpsimps, simple_pinducts=minducts, @@ -472,26 +473,27 @@ |> all x |> all y val simp_thms = @{thms Projl.simps Projr.simps sum.inject sum.cases sum.distinct o_apply} - val ss0 = HOL_basic_ss addsimps simp_thms - val ss1 = HOL_ss addsimps simp_thms + val simpset0 = put_simpset HOL_basic_ss lthy''' addsimps simp_thms + val simpset1 = put_simpset HOL_ss lthy''' addsimps simp_thms val inj_thm = Goal.prove lthy''' [] [] goal_inj - (K (HEADGOAL (DETERM o etac G_aux_induct THEN_ALL_NEW asm_simp_tac ss1))) + (K (HEADGOAL (DETERM o etac G_aux_induct THEN_ALL_NEW asm_simp_tac simpset1))) fun aux_tac thm = - rtac (Drule.gen_all thm) THEN_ALL_NEW (asm_full_simp_tac (ss1 addsimps [inj_thm])) + rtac (Drule.gen_all thm) THEN_ALL_NEW (asm_full_simp_tac (simpset1 addsimps [inj_thm])) val iff1_thm = Goal.prove lthy''' [] [] goal_iff1 (K (HEADGOAL (DETERM o etac G_aux_induct THEN' RANGE (map aux_tac GIntro_thms)))) |> Drule.gen_all val iff2_thm = Goal.prove lthy''' [] [] goal_iff2 - (K (HEADGOAL (DETERM o etac G_induct THEN' RANGE (map (aux_tac o simplify ss0) GIntro_aux_thms)))) + (K (HEADGOAL (DETERM o etac G_induct THEN' RANGE + (map (aux_tac o simplify simpset0) GIntro_aux_thms)))) |> Drule.gen_all val iff_thm = Goal.prove lthy''' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (G, G_aux))) (K (HEADGOAL (EVERY' ((map rtac @{thms ext ext iffI}) @ [etac iff2_thm, etac iff1_thm])))) - val tac = HEADGOAL (simp_tac (HOL_basic_ss addsimps [iff_thm])) + val tac = HEADGOAL (simp_tac (put_simpset HOL_basic_ss lthy''' addsimps [iff_thm])) val goalstate' = case (SINGLE tac) goalstate of NONE => error "auxiliary equivalence proof failed" diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/nominal_termination.ML --- a/Nominal/nominal_termination.ML Mon Apr 01 23:22:53 2013 +0100 +++ b/Nominal/nominal_termination.ML Fri Apr 19 00:10:52 2013 +0100 @@ -49,7 +49,8 @@ let val totality = Thm.close_derivation totality val remove_domain_condition = - full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}]) + full_simplify (put_simpset HOL_basic_ss lthy + addsimps [totality, @{thm True_implies_equals}]) val tsimps = map remove_domain_condition psimps val tinducts = map remove_domain_condition pinducts val teqvts = map remove_domain_condition eqvts diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/nominal_thmdecls.ML --- a/Nominal/nominal_thmdecls.ML Mon Apr 01 23:22:53 2013 +0100 +++ b/Nominal/nominal_thmdecls.ML Fri Apr 19 00:10:52 2013 +0100 @@ -173,12 +173,12 @@ (* Transforms a theorem of the form (1) into the form (4). *) local -fun tac thm = +fun tac ctxt thm = let val ss_thms = @{thms "permute_minus_cancel" "permute_prod.simps" "split_paired_all"} in REPEAT o FIRST' - [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms), + [CHANGED o simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms), rtac (thm RS @{thm "trans"}), rtac @{thm "trans"[OF "permute_fun_def"]} THEN' rtac @{thm "ext"}] end @@ -192,7 +192,7 @@ val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt in - Goal.prove ctxt [] [] goal' (fn _ => tac thm 1) + Goal.prove ctxt [] [] goal' (fn {context, ...} => tac context thm 1) |> singleton (Proof_Context.export ctxt' ctxt) |> (fn th => th RS @{thm "eq_reflection"}) |> zero_var_indexes @@ -205,12 +205,13 @@ (* Transforms a theorem of the form (2) into the form (1). *) local -fun tac thm thm' = +fun tac ctxt thm thm' = let val ss_thms = @{thms "permute_minus_cancel"(2)} in EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, atac, - rtac @{thm "permute_boolI"}, dtac thm', full_simp_tac (HOL_basic_ss addsimps ss_thms)] + rtac @{thm "permute_boolI"}, dtac thm', + full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms)] end in @@ -230,7 +231,7 @@ val certify = cterm_of (theory_of_thm thm) val thm' = Drule.cterm_instantiate [(certify p, certify (mk_minus p'))] thm in - Goal.prove ctxt' [] [] goal' (fn _ => tac thm thm' 1) + Goal.prove ctxt' [] [] goal' (fn {context, ...} => tac context thm thm' 1) |> singleton (Proof_Context.export ctxt' ctxt) end handle TERM _ =>