--- 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 \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> 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
--- 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 [])
--- 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 \<bullet> X = {x. - p \<bullet> x \<in> X}"
+ shows "p \<bullet> X = {x. - p \<bullet> x \<in> 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 \<bullet> t") = {* fn _ => fn ss => fn ctrm =>
+simproc_setup perm_simproc ("p \<bullet> 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 \<sharp> (f::'a::pt \<Rightarrow>'b::pt)") = {* fn _ => fn ss => fn ctrm =>
+simproc_setup fresh_fun_simproc ("a \<sharp> (f::'a::pt \<Rightarrow>'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 \<noteq> (y::'a::at_base)") = {* fn _ => fn ss => fn ctrm =>
+simproc_setup fresh_ineq ("x \<noteq> (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 \<Rightarrow> 'b::pt)") = {* fn _ => fn ss => fn ctrm =>
+simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> '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
--- 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)
--- 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},
--- 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} =>
--- 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
--- 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
--- 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
--- 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);
--- 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
--- 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
--- 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"
--- 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
--- 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 _ =>