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} =>