--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Thu Mar 13 09:21:31 2014 +0000
@@ -98,8 +98,8 @@
apply blast
--""
apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh)
- apply (subgoal_tac "Lam b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)")
- apply (subgoal_tac "Lam ba (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)")
+ apply (subgoal_tac "Lam b (Sum_Type.projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Lam a (Sum_Type.projr (CPSv_CPS_sumC (Inr M))<(a~)>)")
+ apply (subgoal_tac "Lam ba (Sum_Type.projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Lam a (Sum_Type.projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)")
apply (simp only:)
apply (erule Abs_lst1_fcb)
apply (simp add: Abs_fresh_iff)
--- a/Nominal/Ex/Lambda.thy Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/Ex/Lambda.thy Thu Mar 13 09:21:31 2014 +0000
@@ -593,7 +593,7 @@
"transdb (Var x) l = vindex l x 0"
| "transdb (App t1 t2) xs =
Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))"
-| "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))"
+| "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map_option DBLam (transdb t (x # xs))"
apply(simp add: eqvt_def transdb_graph_aux_def)
apply(rule TrueI)
apply (case_tac x)
--- a/Nominal/Ex/Pi.thy Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/Ex/Pi.thy Thu Mar 13 09:21:31 2014 +0000
@@ -130,20 +130,20 @@
lemma testl:
assumes a: "\<exists>y. f = Inl y"
- shows "(p \<bullet> (Sum_Type.Projl f)) = Sum_Type.Projl (p \<bullet> f)"
+ shows "(p \<bullet> (Sum_Type.projl f)) = Sum_Type.projl (p \<bullet> f)"
using a by auto
lemma testrr:
assumes a: "\<exists>y. f = Inr (Inr y)"
- shows "(p \<bullet> (Sum_Type.Projr (Sum_Type.Projr f))) = Sum_Type.Projr (Sum_Type.Projr (p \<bullet> f))"
+ shows "(p \<bullet> (Sum_Type.projr (Sum_Type.projr f))) = Sum_Type.projr (Sum_Type.projr (p \<bullet> f))"
using a by auto
lemma testlr:
assumes a: "\<exists>y. f = Inr (Inl y)"
- shows "(p \<bullet> (Sum_Type.Projl (Sum_Type.Projr f))) = Sum_Type.Projl (Sum_Type.Projr (p \<bullet> f))"
+ shows "(p \<bullet> (Sum_Type.projl (Sum_Type.projr f))) = Sum_Type.projl (Sum_Type.projr (p \<bullet> f))"
using a by auto
-nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (sum_case (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
+nominal_primrec (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix" ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and
subsList_mix :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix" ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and
subs_mix :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix" ("_[_::=\<onesuperior>_]" [100, 100, 100] 100)
@@ -240,33 +240,33 @@
apply (metis Inr_not_Inl)
apply (metis Inr_inject Inr_not_Inl)
apply (metis Inr_inject Inr_not_Inl)
-apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.Projr
- (Sum_Type.Projr
+apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="Sum_Type.Projr
- (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
- Sum_Type.Projr
- (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
+apply (rule_tac x="Sum_Type.projr
+ (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
+ Sum_Type.projr
+ (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.Projr
- (Sum_Type.Projr
+apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.Projl
- (Sum_Type.Projr
+apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.Projr
- (Sum_Type.Projr
+apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum
(Inr (Inr (Pb, xb, y)))))" in exI)
apply clarify
@@ -333,33 +333,33 @@
apply (metis Inr_not_Inl)
apply (metis Inr_inject Inr_not_Inl)
apply (metis Inr_inject Inr_not_Inl)
-apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.Projr
- (Sum_Type.Projr
+apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="Sum_Type.Projr
- (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
- Sum_Type.Projr
- (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
+apply (rule_tac x="Sum_Type.projr
+ (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
+ Sum_Type.projr
+ (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.Projr
- (Sum_Type.Projr
+apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.Projl
- (Sum_Type.Projr
+apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.Projr
- (Sum_Type.Projr
+apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
+ (Sum_Type.projr
(subsGuard_mix_subsList_mix_subs_mix_sum
(Inr (Inr (Pb, xb, y)))))" in exI)
apply clarify
--- a/Nominal/Ex/TypeSchemes2.thy Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/Ex/TypeSchemes2.thy Thu Mar 13 09:21:31 2014 +0000
@@ -41,27 +41,27 @@
lemma TEST1:
assumes "x = Inl y"
- shows "(p \<bullet> Sum_Type.Projl x) = Sum_Type.Projl (p \<bullet> x)"
+ shows "(p \<bullet> Sum_Type.projl x) = Sum_Type.projl (p \<bullet> x)"
using assms by simp
lemma TEST2:
assumes "x = Inr y"
- shows "(p \<bullet> Sum_Type.Projr x) = Sum_Type.Projr (p \<bullet> x)"
+ shows "(p \<bullet> Sum_Type.projr x) = Sum_Type.projr (p \<bullet> x)"
using assms by simp
lemma test:
assumes a: "\<exists>y. f x = Inl y"
- shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
-using a
-by (metis Inl_eqvt Projl_Inl permute_fun_app_eq)
+ shows "(p \<bullet> (Sum_Type.projl (f x))) = Sum_Type.projl ((p \<bullet> f) (p \<bullet> x))"
+using a TEST1
+by (metis eqvt_bound eqvt_lambda permute_eq_iff)
lemma test2:
assumes a: "\<exists>y. f x = Inl y"
- shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))"
+ shows "(p \<bullet> (Sum_Type.projl (f x))) = Sum_Type.projl (p \<bullet> (f x))"
using a
by clarsimp
-nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
+nominal_primrec (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
where
@@ -103,8 +103,8 @@
apply clarify
apply (rule the1_equality)
apply blast apply assumption
-apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1))))
- (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)
+apply (rule_tac x="(Fun (Sum_Type.projl (subst_substs_sum (Inl (\<theta>, T1))))
+ (Sum_Type.projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)
apply clarify
apply (rule the1_equality)
apply blast apply assumption
--- a/Nominal/GPerm.thy Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/GPerm.thy Thu Mar 13 09:21:31 2014 +0000
@@ -53,7 +53,7 @@
by (rule perm_eq_equivp)
definition perm_add_raw where
- "perm_add_raw p q = map (map_pair id (perm_apply p)) q @ [a\<leftarrow>p. fst a \<notin> fst ` set q]"
+ "perm_add_raw p q = map (map_prod id (perm_apply p)) q @ [a\<leftarrow>p. fst a \<notin> fst ` set q]"
lemma perm_apply_del[simp]:
"e \<noteq> b \<Longrightarrow> perm_apply [a\<leftarrow>l. fst a \<noteq> b] e = perm_apply l e"
@@ -146,7 +146,7 @@
lemma valid_perm_add_minus: "valid_perm a \<Longrightarrow> perm_apply (map swap_pair a) (perm_apply a e) = e"
apply (auto simp add: filter_map_swap_pair filter_eq_nil filter_rev_eq_nil perm_apply_def split: list.split)
apply (metis filter_eq_nil(2) neq_Nil_conv valid_perm_def)
- apply (metis hd.simps hd_in_set image_eqI list.simps(2) member_project project_set snd_conv)
+ apply (metis list.sel(1) hd_in_set image_eqI list.simps(2) member_project project_set snd_conv)
apply (frule filter_fst_eq(1))
apply (frule filter_fst_eq(2))
apply (auto simp add: swap_pair_def)
@@ -162,9 +162,9 @@
"perm_eq x y \<Longrightarrow> perm_eq (map swap_pair x) (map swap_pair y)"
by (auto simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def)
-lemma fst_snd_map_pair[simp]:
- "fst ` map_pair f g ` set l = f ` fst ` set l"
- "snd ` map_pair f g ` set l = g ` snd ` set l"
+lemma fst_snd_map_prod[simp]:
+ "fst ` map_prod f g ` set l = f ` fst ` set l"
+ "snd ` map_prod f g ` set l = g ` snd ` set l"
by (induct l) auto
lemma fst_diff[simp]:
--- a/Nominal/Nominal2.thy Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/Nominal2.thy Thu Mar 13 09:21:31 2014 +0000
@@ -399,8 +399,8 @@
val qperm_bns = map #qconst qperm_bns_info
val _ = trace_msg (K "Lifting of theorems...")
- val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def
- prod.cases}
+ val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def rel_prod_def
+ prod.case}
val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts,
qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps,
@@ -747,6 +747,3 @@
end
-
-
-
--- a/Nominal/Nominal2_Abs.thy Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/Nominal2_Abs.thy Thu Mar 13 09:21:31 2014 +0000
@@ -479,14 +479,14 @@
shows "(op= ===> op= ===> alpha_abs_set) Pair Pair"
and "(op= ===> op= ===> alpha_abs_res) Pair Pair"
and "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
- unfolding fun_rel_def
+ unfolding rel_fun_def
by (auto intro: alphas_abs_refl)
lemma [quot_respect]:
shows "(op= ===> alpha_abs_set ===> alpha_abs_set) permute permute"
and "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute"
and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"
- unfolding fun_rel_def
+ unfolding rel_fun_def
by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
lemma Abs_eq_iff:
@@ -1045,18 +1045,18 @@
definition
prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"
where
- "prod_alpha = prod_rel"
+ "prod_alpha = rel_prod"
lemma [quot_respect]:
- shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
- unfolding fun_rel_def
- unfolding prod_rel_def
+ shows "((R1 ===> op =) ===> (R2 ===> op =) ===> rel_prod R1 R2 ===> op =) prod_fv prod_fv"
+ unfolding rel_fun_def
+ unfolding rel_prod_def
by auto
lemma [quot_preserve]:
assumes q1: "Quotient3 R1 abs1 rep1"
and q2: "Quotient3 R2 abs2 rep2"
- shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_pair rep1 rep2 ---> id) prod_fv = prod_fv"
+ shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_prod rep1 rep2 ---> id) prod_fv = prod_fv"
by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
lemma [mono]:
@@ -1067,7 +1067,7 @@
lemma [eqvt]:
shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
unfolding prod_alpha_def
- unfolding prod_rel_def
+ unfolding rel_prod_def
by (perm_simp) (rule refl)
lemma [eqvt]:
--- a/Nominal/Nominal2_Base.thy Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/Nominal2_Base.thy Thu Mar 13 09:21:31 2014 +0000
@@ -618,7 +618,7 @@
lemma permute_fset_rsp[quot_respect]:
shows "(op = ===> list_eq ===> list_eq) permute permute"
- unfolding fun_rel_def
+ unfolding rel_fun_def
by (simp add: set_eqvt[symmetric])
instantiation fset :: (pt) pt
@@ -1191,8 +1191,8 @@
subsubsection {* Equivariance for @{typ "'a option"} *}
-lemma option_map_eqvt[eqvt]:
- shows "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)"
+lemma map_option_eqvt[eqvt]:
+ shows "p \<bullet> (map_option f x) = map_option (p \<bullet> f) (p \<bullet> x)"
by (cases x) (simp_all)
@@ -1565,21 +1565,21 @@
proof -
{ assume "a \<notin> supp p" "a \<notin> supp q"
then have "(p + q) \<bullet> a = (q + p) \<bullet> a"
- by (simp add: supp_perm)
+ by (simp add: supp_perm)
}
moreover
{ assume a: "a \<in> supp p" "a \<notin> supp q"
then have "p \<bullet> a \<in> supp p" by (simp add: supp_perm)
then have "p \<bullet> a \<notin> supp q" using asm by auto
with a have "(p + q) \<bullet> a = (q + p) \<bullet> a"
- by (simp add: supp_perm)
+ by (simp add: supp_perm)
}
moreover
{ assume a: "a \<notin> supp p" "a \<in> supp q"
then have "q \<bullet> a \<in> supp q" by (simp add: supp_perm)
then have "q \<bullet> a \<notin> supp p" using asm by auto
with a have "(p + q) \<bullet> a = (q + p) \<bullet> a"
- by (simp add: supp_perm)
+ by (simp add: supp_perm)
}
ultimately show "(p + q) \<bullet> a = (q + p) \<bullet> a"
using asm by blast
@@ -2793,19 +2793,19 @@
by (auto simp: swap_atom)
moreover
{ have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
- using **
- apply (auto simp: supp_perm insert_eqvt)
- apply (subgoal_tac "q \<bullet> a \<in> bs \<union> p \<bullet> bs")
- apply(auto)[1]
- apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}")
- apply(blast)
- apply(simp)
- done
+ using **
+ apply (auto simp: supp_perm insert_eqvt)
+ apply (subgoal_tac "q \<bullet> a \<in> bs \<union> p \<bullet> bs")
+ apply(auto)[1]
+ apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}")
+ apply(blast)
+ apply(simp)
+ done
then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
unfolding supp_swap by auto
moreover
have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
- using ** by (auto simp: insert_eqvt)
+ using ** by (auto simp: insert_eqvt)
ultimately
have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
unfolding q'_def using supp_plus_perm by blast
@@ -2862,19 +2862,19 @@
unfolding q'_def using 2 * `a \<notin> set bs` by (auto simp: swap_atom)
moreover
{ have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
- using **
- apply (auto simp: supp_perm insert_eqvt)
- apply (subgoal_tac "q \<bullet> a \<in> set bs \<union> p \<bullet> set bs")
- apply(auto)[1]
- apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}")
- apply(blast)
- apply(simp)
- done
+ using **
+ apply (auto simp: supp_perm insert_eqvt)
+ apply (subgoal_tac "q \<bullet> a \<in> set bs \<union> p \<bullet> set bs")
+ apply(auto)[1]
+ apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}")
+ apply(blast)
+ apply(simp)
+ done
then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)"
unfolding supp_swap by auto
moreover
have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
- using ** by (auto simp: insert_eqvt)
+ using ** by (auto simp: insert_eqvt)
ultimately
have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
unfolding q'_def using supp_plus_perm by blast
--- a/Nominal/nominal_basics.ML Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/nominal_basics.ML Thu Mar 13 09:21:31 2014 +0000
@@ -35,8 +35,8 @@
val mk_All: (string * typ) -> term -> term
val mk_exists: (string * typ) -> term -> term
- val sum_case_const: typ -> typ -> typ -> term
- val mk_sum_case: term -> term -> term
+ val case_sum_const: typ -> typ -> typ -> term
+ val mk_case_sum: term -> term -> term
val mk_equiv: thm -> thm
val safe_mk_equiv: thm -> thm
@@ -148,15 +148,15 @@
fun mk_exists (a, T) t = HOLogic.exists_const T $ Abs (a, T, t)
-fun sum_case_const ty1 ty2 ty3 =
- Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)
+fun case_sum_const ty1 ty2 ty3 =
+ Const (@{const_name case_sum}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)
-fun mk_sum_case trm1 trm2 =
+fun mk_case_sum trm1 trm2 =
let
val ([ty1], ty3) = strip_type (fastype_of trm1)
val ty2 = domain_type (fastype_of trm2)
in
- sum_case_const ty1 ty2 ty3 $ trm1 $ trm2
+ case_sum_const ty1 ty2 ty3 $ trm1 $ trm2
end
fun mk_equiv r = r RS @{thm eq_reflection}
--- a/Nominal/nominal_dt_alpha.ML Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/nominal_dt_alpha.ML Thu Mar 13 09:21:31 2014 +0000
@@ -463,7 +463,7 @@
fun cases_tac intros ctxt =
let
- val prod_simps = @{thms split_conv prod_alpha_def prod_rel_def}
+ val prod_simps = @{thms split_conv prod_alpha_def rel_prod_def}
val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac
@@ -504,7 +504,7 @@
in
resolve_tac prems' 1
end) ctxt
- val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel_def alphas}
+ val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_def alphas}
in
EVERY'
[ etac exi_neg,
@@ -556,7 +556,7 @@
fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt =
let
- val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel_def}
+ val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_def}
in
resolve_tac intros
THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN'
@@ -570,7 +570,7 @@
eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
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 =
let
val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, alpha_cases, ...} = alpha_result
@@ -685,7 +685,7 @@
val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns
val simpset =
- put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps}
+ 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
@@ -706,8 +706,8 @@
val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys))
val simpset =
- put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def
- permute_prod_def prod.cases prod.recs})
+ put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_def
+ permute_prod_def prod.case prod.rec})
val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac simpset
in
@@ -719,9 +719,9 @@
fun raw_constr_rsp_tac ctxt alpha_intros simps =
let
- 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
+ val pre_simpset = put_simpset HOL_ss ctxt addsimps @{thms rel_fun_def}
+ val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def rel_prod_def
+ prod_fv.simps fresh_star_zero permute_zero prod.case} @ simps
in
asm_full_simp_tac pre_simpset
THEN' REPEAT o (resolve_tac @{thms allI impI})
@@ -738,15 +738,15 @@
NONE => HOLogic.eq_const ty
| SOME alpha => alpha
- fun fun_rel_app (t1, t2) =
- Const (@{const_name "fun_rel"}, dummyT) $ t1 $ t2
+ fun rel_fun_app (t1, t2) =
+ Const (@{const_name "rel_fun"}, dummyT) $ t1 $ t2
fun prep_goal trm =
trm
|> strip_type o fastype_of
|> (fn (tys, ty) => tys @ [ty])
|> map lookup
- |> foldr1 fun_rel_app
+ |> foldr1 rel_fun_app
|> (fn t => t $ trm $ trm)
|> Syntax.check_term ctxt
|> HOLogic.mk_Trueprop
@@ -762,7 +762,7 @@
val rsp_equivp =
@{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> op =) Q Q"
- by (simp only: fun_rel_def equivp_def, metis)}
+ by (simp only: rel_fun_def equivp_def, metis)}
(* we have to reorder the alpha_bn_imps theorems in order
@@ -791,7 +791,7 @@
(* rsp for permute_bn functions *)
val perm_bn_rsp = @{lemma "(!x y p. R x y --> R (f p x) (f p y)) ==> (op= ===> R ===> R) f f"
- by (simp add: fun_rel_def)}
+ by (simp add: rel_fun_def)}
fun raw_prove_perm_bn_tac alpha_result simps ctxt =
SUBPROOF (fn {prems, context, ...} =>
@@ -819,7 +819,7 @@
val perm_bn_ty = range_type o range_type o fastype_of
val ty_assoc = (alpha_tys @ alpha_bn_tys) ~~ (alpha_trms @ alpha_bn_trms)
- val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
+ val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
val p = Free (p, @{typ perm})
fun mk_prop t =
@@ -844,7 +844,7 @@
(* transformation of the natural rsp-lemmas into standard form *)
val fun_rsp = @{lemma
- "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: fun_rel_def)}
+ "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: rel_fun_def)}
fun mk_funs_rsp ctxt thm =
thm
@@ -855,7 +855,7 @@
val permute_rsp = @{lemma
"(!x y p. R x y --> R (permute p x) (permute p y))
- ==> ((op =) ===> R ===> R) permute permute" by (simp add: fun_rel_def)}
+ ==> ((op =) ===> R ===> R) permute permute" by (simp add: rel_fun_def)}
fun mk_alpha_permute_rsp ctxt thm =
thm
--- a/Nominal/nominal_dt_quot.ML Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/nominal_dt_quot.ML Thu Mar 13 09:21:31 2014 +0000
@@ -303,8 +303,8 @@
val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc}
val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un}
-val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def
- prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI}
+val thms3 = @{thms alphas prod_alpha_def prod_fv.simps rel_prod_def permute_prod_def
+ prod.rec prod.case prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI}
fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps
fv_bn_eqvts qinduct bclausess ctxt =
@@ -355,7 +355,7 @@
val props = map mk_goal qbns
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}))
+ @{thms set_simps set_append finite_insert finite.emptyI finite_Un}))
in
induct_prove qtys props qinduct (K ss_tac) ctxt
end
@@ -532,7 +532,7 @@
|> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))
|> HOLogic.mk_Trueprop
- val ss = fprops @ @{thms set.simps set_append union_eqvt}
+ val ss = fprops @ @{thms set_simps set_append union_eqvt}
@ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
fresh_star_set}
@@ -580,7 +580,7 @@
REPEAT o (etac @{thm conjE}),
REPEAT o (dtac setify),
full_simp_tac (put_simpset HOL_basic_ss ctxt''
- addsimps @{thms set_append set.simps})]) abs_eq_thms ctxt'
+ addsimps @{thms set_append set_simps})]) abs_eq_thms ctxt'
val (abs_eqs, peqs) = split_filter is_abs_eq eqs
--- a/Nominal/nominal_function_core.ML Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/nominal_function_core.ML Thu Mar 13 09:21:31 2014 +0000
@@ -91,14 +91,14 @@
(* Theory dependencies. *)
val acc_induct_rule = @{thm accp_induct_rule}
-val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}
-val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}
-val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff}
+val ex1_implies_ex = @{thm Fun_Def.fundef_ex1_existence}
+val ex1_implies_un = @{thm Fun_Def.fundef_ex1_uniqueness}
+val ex1_implies_iff = @{thm Fun_Def.fundef_ex1_iff}
val acc_downward = @{thm accp_downward}
val accI = @{thm accp.accI}
val case_split = @{thm HOL.case_split}
-val fundef_default_value = @{thm FunDef.fundef_default_value}
+val fundef_default_value = @{thm Fun_Def.fundef_default_value}
val not_acc_down = @{thm not_accp_down}
@@ -657,7 +657,7 @@
fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
let
val f_def =
- Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT)
+ Abs ("x", domT, Const (@{const_name Fun_Def.THE_default}, ranT --> (ranT --> boolT) --> ranT)
$ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
|> Syntax.check_term lthy
in
@@ -881,8 +881,8 @@
(** Termination rule **)
val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}
-val wf_in_rel = @{thm FunDef.wf_in_rel}
-val in_rel_def = @{thm FunDef.in_rel_def}
+val wf_in_rel = @{thm Fun_Def.wf_in_rel}
+val in_rel_def = @{thm Fun_Def.in_rel_def}
fun mk_nest_term_case thy globals R' ihyp clause =
let
@@ -943,7 +943,7 @@
val R' = Free ("R", fastype_of R)
val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
- val inrel_R = Const (@{const_name FunDef.in_rel},
+ val inrel_R = Const (@{const_name Fun_Def.in_rel},
HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},
--- a/Nominal/nominal_induct.ML Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/nominal_induct.ML Thu Mar 13 09:21:31 2014 +0000
@@ -66,7 +66,7 @@
let
val tune =
if internal then Name.internal
- else fn x => the_default x (try Name.dest_internal x);
+ else perhaps (try Name.dest_internal);
val n = length xs;
fun rename prem =
let
--- a/Nominal/nominal_library.ML Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/nominal_library.ML Thu Mar 13 09:21:31 2014 +0000
@@ -52,7 +52,7 @@
val supp_rel_ty: typ -> typ
val supp_rel_const: typ -> term
val mk_supp_rel_ty: typ -> term -> term -> term
- val mk_supp_rel: term -> term -> term
+ val mk_supp_rel: term -> term -> term
val supports_const: typ -> term
val mk_supports_ty: typ -> term -> term -> term
@@ -359,7 +359,7 @@
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
+ addsimps @{thms in_measure wf_measure sum.case add_Suc_right add.right_neutral
zero_less_Suc prod.size(1) mult_Suc_right})
val natT = @{typ nat}
@@ -374,7 +374,7 @@
end
fun snd_const T1 T2 =
- Const ("Product_Type.snd", HOLogic.mk_prodT (T1, T2) --> T2)
+ Const (@{const_name Product_Type.snd}, HOLogic.mk_prodT (T1, T2) --> T2)
fun mk_measure_trm f ctxt T =
@@ -390,7 +390,7 @@
fun mk_size_measure T =
case T of
(Type (@{type_name Sum_Type.sum}, [T1, T2])) =>
- SumTree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2)
+ Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2)
| (Type (@{type_name Product_Type.prod}, [T1, T2])) =>
HOLogic.mk_comp (mk_size_measure T2, snd_const T1 T2)
| _ => HOLogic.size_const T
@@ -406,7 +406,7 @@
fun mk_size_measure T =
case T of
(Type (@{type_name Sum_Type.sum}, [T1, T2])) =>
- SumTree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2)
+ Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2)
| (Type (@{type_name Product_Type.prod}, [T1, T2])) =>
prod_size_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2)
| _ => HOLogic.size_const T
@@ -512,4 +512,4 @@
end (* structure *)
-open Nominal_Library;
\ No newline at end of file
+open Nominal_Library;
--- a/Nominal/nominal_mutual.ML Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/nominal_mutual.ML Thu Mar 13 09:21:31 2014 +0000
@@ -13,7 +13,6 @@
signature NOMINAL_FUNCTION_MUTUAL =
sig
-
val prepare_nominal_function_mutual : Nominal_Function_Common.nominal_function_config
-> string (* defname *)
-> ((string * typ) * mixfix) list
@@ -22,10 +21,8 @@
-> ((thm (* goalstate *)
* (thm -> Nominal_Function_Common.nominal_function_result) (* proof continuation *)
) * local_theory)
-
end
-
structure Nominal_Function_Mutual: NOMINAL_FUNCTION_MUTUAL =
struct
@@ -95,8 +92,8 @@
val dresultTs = distinct (op =) resultTs
val n' = length dresultTs
- val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs
- val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs
+ val RST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) dresultTs
+ val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) argTs
val fsum_type = ST --> RST
@@ -108,7 +105,7 @@
val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1
- val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
+ val f_exp = Sum_Tree.mk_proj RST n' i' (Free fsum_var $ Sum_Tree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)
val rew = (n, fold_rev lambda vars f_exp)
@@ -124,8 +121,8 @@
val rhs' = rhs
|> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n) | t => t)
in
- (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
- Envir.beta_norm (SumTree.mk_inj RST n' i' rhs'))
+ (qs, gs, Sum_Tree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
+ Envir.beta_norm (Sum_Tree.mk_inj RST n' i' rhs'))
end
val qglrs = map convert_eqs fqgars
@@ -205,8 +202,8 @@
|> export
end
-val inl_perm = @{lemma "x = Inl y ==> Sum_Type.Projl (permute p x) = permute p (Sum_Type.Projl x)" by simp}
-val inr_perm = @{lemma "x = Inr y ==> Sum_Type.Projr (permute p x) = permute p (Sum_Type.Projr x)" by simp}
+val inl_perm = @{lemma "x = Inl y ==> projl (permute p x) = permute p (projl x)" by simp}
+val inr_perm = @{lemma "x = Inr y ==> projr (permute p x) = permute p (projr x)" by simp}
fun recover_mutual_eqvt eqvt_thm all_orig_fdefs parts ctxt (fname, _, _, args, _)
import (export : thm -> thm) sum_psimp_eq =
@@ -224,13 +221,12 @@
val ([p], ctxt'') = ctxt'
|> fold Variable.declare_term args
- |> Variable.variant_fixes ["p"]
+ |> Variable.variant_fixes ["p"]
val p = Free (p, @{typ perm})
val simpset =
put_simpset HOL_basic_ss ctxt'' addsimps
- @{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric]} @
- @{thms Projr.simps Projl.simps} @
+ @{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric] sum.sel} @
[(cond MRS eqvt_thm) RS @{thm sym}] @
[inl_perm, inr_perm, simp]
val goal_lhs = mk_perm p (list_comb (f, args))
@@ -272,21 +268,21 @@
end
val Ps = map2 mk_P parts newPs
- val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps
+ val case_exp = Sum_Tree.mk_sumcases HOLogic.boolT Ps
val induct_inst =
Thm.forall_elim (cert case_exp) induct
- |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt)
+ |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
|> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs)
fun project rule (MutualPart {cargTs, i, ...}) k =
let
val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *)
- val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
+ val inj = Sum_Tree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
in
(rule
|> Thm.forall_elim (cert inj)
- |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt)
+ |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
|> fold_rev (Thm.forall_intr o cert) (afs @ newPs),
k + length cargTs)
end
@@ -427,13 +423,13 @@
let
val (tys, ty) = strip_type T
val fun_var = Free (n ^ "_aux", HOLogic.mk_tupleT tys --> ty)
- val inj_fun = absdummy dummyT (SumTree.mk_inj RST n' i' (Bound 0))
+ val inj_fun = absdummy dummyT (Sum_Tree.mk_inj RST n' i' (Bound 0))
in
Syntax.check_term lthy'' (mk_comp_dummy inj_fun fun_var)
end
- val sum_case_exp = map mk_cases parts
- |> SumTree.mk_sumcases RST
+ val case_sum_exp = map mk_cases parts
+ |> Sum_Tree.mk_sumcases RST
val (G_name, G_type) = dest_Free G
val G_name_aux = G_name ^ "_aux"
@@ -441,7 +437,7 @@
val GIntros_aux = GIntro_thms
|> map prop_of
|> map (Term.subst_free subst)
- |> map (subst_all sum_case_exp)
+ |> map (subst_all case_sum_exp)
val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy''') =
Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy''
@@ -456,10 +452,10 @@
fun mk_inj_goal (MutualPart {i', ...}) =
let
- val injs = SumTree.mk_inj ST n' i' (Bound 0)
+ val injs = Sum_Tree.mk_inj ST n' i' (Bound 0)
val projs = y
- |> SumTree.mk_proj RST n' i'
- |> SumTree.mk_inj RST n' i'
+ |> Sum_Tree.mk_proj RST n' i'
+ |> Sum_Tree.mk_inj RST n' i'
in
Const (@{const_name "All"}, dummyT) $ absdummy dummyT
(HOLogic.mk_imp (HOLogic.mk_eq(x, injs), HOLogic.mk_eq(projs, y)))
@@ -474,7 +470,7 @@
val goal_iff2 = Logic.mk_implies (G_prem, G_aux_prem)
|> all x |> all y
- val simp_thms = @{thms Projl.simps Projr.simps sum.inject sum.cases sum.distinct o_apply}
+ val simp_thms = @{thms sum.sel sum.inject sum.case sum.distinct o_apply}
val simpset0 = put_simpset HOL_basic_ss lthy''' addsimps simp_thms
val simpset1 = put_simpset HOL_ss lthy''' addsimps simp_thms
--- a/Nominal/nominal_permeq.ML Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/nominal_permeq.ML Thu Mar 13 09:21:31 2014 +0000
@@ -22,8 +22,8 @@
val eqvt_rule: Proof.context -> eqvt_config -> thm -> thm
val eqvt_tac: Proof.context -> eqvt_config -> int -> tactic
- val perm_simp_meth: thm list * string list -> Proof.context -> Method.method
- val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method
+ val perm_simp_meth: thm list * string list -> Proof.context -> Proof.method
+ val perm_strict_simp_meth: thm list * string list -> Proof.context -> Proof.method
val args_parser: (thm list * string list) context_parser
val trace_eqvt: bool Config.T
@@ -219,9 +219,9 @@
Scan.repeat (unless_more_args Attrib.multi_thm) >> flat) [];
val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |--
- (Scan.repeat (Args.const true))) []
+ (Scan.repeat (Args.const {proper = true, strict = true}))) []
-val args_parser = add_thms_parser -- exclude_consts_parser
+val args_parser = add_thms_parser -- exclude_consts_parser
fun perm_simp_meth (thms, consts) ctxt =
SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt (eqvt_relaxed_config addpres thms addexcls consts)))