10 uses ("nominal_thmdecls.ML") |
10 uses ("nominal_thmdecls.ML") |
11 ("nominal_permeq.ML") |
11 ("nominal_permeq.ML") |
12 ("nominal_eqvt.ML") |
12 ("nominal_eqvt.ML") |
13 begin |
13 begin |
14 |
14 |
|
15 |
|
16 section {* Permsimp and Eqvt infrastructure *} |
|
17 |
|
18 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} |
|
19 |
|
20 use "nominal_thmdecls.ML" |
|
21 setup "Nominal_ThmDecls.setup" |
|
22 |
|
23 text {* helper lemmas for the perm_simp *} |
|
24 |
|
25 definition |
|
26 "unpermute p = permute (- p)" |
|
27 |
|
28 lemma eqvt_apply: |
|
29 fixes f :: "'a::pt \<Rightarrow> 'b::pt" |
|
30 and x :: "'a::pt" |
|
31 shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)" |
|
32 unfolding permute_fun_def by simp |
|
33 |
|
34 lemma eqvt_lambda: |
|
35 fixes f :: "'a::pt \<Rightarrow> 'b::pt" |
|
36 shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))" |
|
37 unfolding permute_fun_def unpermute_def by simp |
|
38 |
|
39 lemma eqvt_bound: |
|
40 shows "p \<bullet> unpermute p x \<equiv> x" |
|
41 unfolding unpermute_def by simp |
|
42 |
|
43 text {* provides perm_simp methods *} |
|
44 |
|
45 use "nominal_permeq.ML" |
|
46 setup Nominal_Permeq.setup |
|
47 |
|
48 method_setup perm_simp = |
|
49 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *} |
|
50 {* pushes permutations inside. *} |
|
51 |
|
52 method_setup perm_strict_simp = |
|
53 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} |
|
54 {* pushes permutations inside, raises an error if it cannot solve all permutations. *} |
|
55 |
|
56 (* the normal version of this lemma would cause loops *) |
|
57 lemma permute_eqvt_raw[eqvt_raw]: |
|
58 shows "p \<bullet> permute \<equiv> permute" |
|
59 apply(simp add: expand_fun_eq permute_fun_def) |
|
60 apply(subst permute_eqvt) |
|
61 apply(simp) |
|
62 done |
|
63 |
15 section {* Logical Operators *} |
64 section {* Logical Operators *} |
16 |
65 |
17 lemma eq_eqvt: |
66 lemma eq_eqvt[eqvt]: |
18 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |
67 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |
19 unfolding permute_eq_iff permute_bool_def .. |
68 unfolding permute_eq_iff permute_bool_def .. |
20 |
69 |
21 lemma if_eqvt: |
70 lemma if_eqvt[eqvt]: |
22 shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)" |
71 shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)" |
23 by (simp add: permute_fun_def permute_bool_def) |
72 by (simp add: permute_fun_def permute_bool_def) |
24 |
73 |
25 lemma True_eqvt: |
74 lemma True_eqvt[eqvt]: |
26 shows "p \<bullet> True = True" |
75 shows "p \<bullet> True = True" |
27 unfolding permute_bool_def .. |
76 unfolding permute_bool_def .. |
28 |
77 |
29 lemma False_eqvt: |
78 lemma False_eqvt[eqvt]: |
30 shows "p \<bullet> False = False" |
79 shows "p \<bullet> False = False" |
31 unfolding permute_bool_def .. |
80 unfolding permute_bool_def .. |
32 |
81 |
33 lemma imp_eqvt: |
82 lemma imp_eqvt[eqvt]: |
34 shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))" |
83 shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))" |
35 by (simp add: permute_bool_def) |
84 by (simp add: permute_bool_def) |
36 |
85 |
37 lemma conj_eqvt: |
86 lemma conj_eqvt[eqvt]: |
38 shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))" |
87 shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))" |
39 by (simp add: permute_bool_def) |
88 by (simp add: permute_bool_def) |
40 |
89 |
41 lemma disj_eqvt: |
90 lemma disj_eqvt[eqvt]: |
42 shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))" |
91 shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))" |
43 by (simp add: permute_bool_def) |
92 by (simp add: permute_bool_def) |
44 |
93 |
45 lemma Not_eqvt: |
94 lemma Not_eqvt[eqvt]: |
46 shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))" |
95 shows "p \<bullet> (\<not> A) \<longleftrightarrow> \<not> (p \<bullet> A)" |
47 by (simp add: permute_bool_def) |
96 by (simp add: permute_bool_def) |
48 |
97 |
49 lemma all_eqvt: |
98 lemma all_eqvt[eqvt]: |
50 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)" |
99 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)" |
51 unfolding permute_fun_def permute_bool_def |
100 unfolding permute_fun_def permute_bool_def |
52 by (auto, drule_tac x="p \<bullet> x" in spec, simp) |
101 by (auto, drule_tac x="p \<bullet> x" in spec, simp) |
53 |
102 |
54 lemma all_eqvt2: |
103 lemma all_eqvt2: |
55 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))" |
104 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))" |
56 unfolding permute_fun_def permute_bool_def |
105 by (perm_simp add: permute_minus_cancel) (rule refl) |
57 by (auto, drule_tac x="p \<bullet> x" in spec, simp) |
106 |
58 |
107 lemma ex_eqvt[eqvt]: |
59 lemma ex_eqvt: |
|
60 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)" |
108 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)" |
61 unfolding permute_fun_def permute_bool_def |
109 unfolding permute_fun_def permute_bool_def |
62 by (auto, rule_tac x="p \<bullet> x" in exI, simp) |
110 by (auto, rule_tac x="p \<bullet> x" in exI, simp) |
63 |
111 |
64 lemma ex_eqvt2: |
112 lemma ex_eqvt2: |
65 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))" |
113 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))" |
66 unfolding permute_fun_def permute_bool_def |
114 by (perm_simp add: permute_minus_cancel) (rule refl) |
67 by (auto, rule_tac x="p \<bullet> x" in exI, simp) |
115 |
68 |
116 lemma ex1_eqvt[eqvt]: |
69 lemma ex1_eqvt: |
|
70 shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)" |
117 shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)" |
71 unfolding Ex1_def |
118 unfolding Ex1_def |
72 by (simp add: ex_eqvt permute_fun_def conj_eqvt all_eqvt imp_eqvt eq_eqvt) |
119 by (perm_simp) (rule refl) |
73 |
120 |
74 lemma ex1_eqvt2: |
121 lemma ex1_eqvt2: |
75 shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))" |
122 shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))" |
76 unfolding Ex1_def ex_eqvt2 conj_eqvt all_eqvt2 imp_eqvt eq_eqvt |
123 by (perm_simp add: permute_minus_cancel) (rule refl) |
77 by simp |
|
78 |
124 |
79 lemma the_eqvt: |
125 lemma the_eqvt: |
80 assumes unique: "\<exists>!x. P x" |
126 assumes unique: "\<exists>!x. P x" |
81 shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))" |
127 shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))" |
82 apply(rule the1_equality [symmetric]) |
128 apply(rule the1_equality [symmetric]) |
88 |
134 |
89 section {* Set Operations *} |
135 section {* Set Operations *} |
90 |
136 |
91 lemma mem_permute_iff: |
137 lemma mem_permute_iff: |
92 shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
138 shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
93 unfolding mem_def permute_fun_def permute_bool_def |
139 unfolding mem_def permute_fun_def permute_bool_def |
94 by simp |
140 by simp |
95 |
141 |
96 lemma mem_eqvt: |
142 lemma mem_eqvt[eqvt]: |
97 shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)" |
143 shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)" |
98 unfolding mem_permute_iff permute_bool_def by simp |
144 unfolding mem_def |
|
145 by (perm_simp) (rule refl) |
99 |
146 |
100 lemma not_mem_eqvt: |
147 lemma not_mem_eqvt: |
101 shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)" |
148 shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)" |
102 unfolding mem_def permute_fun_def by (simp add: Not_eqvt) |
149 by (perm_simp) (rule refl) |
103 |
150 |
104 lemma Collect_eqvt: |
151 lemma Collect_eqvt[eqvt]: |
105 shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}" |
152 shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}" |
106 unfolding Collect_def permute_fun_def .. |
153 unfolding Collect_def permute_fun_def .. |
107 |
154 |
108 lemma Collect_eqvt2: |
155 lemma Collect_eqvt2: |
109 shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}" |
156 shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}" |
110 unfolding Collect_def permute_fun_def .. |
157 by (perm_simp add: permute_minus_cancel) (rule refl) |
111 |
158 |
112 lemma empty_eqvt: |
159 lemma empty_eqvt[eqvt]: |
113 shows "p \<bullet> {} = {}" |
160 shows "p \<bullet> {} = {}" |
114 unfolding empty_def Collect_eqvt2 False_eqvt .. |
161 unfolding empty_def |
|
162 by (perm_simp) (rule refl) |
115 |
163 |
116 lemma supp_set_empty: |
164 lemma supp_set_empty: |
117 shows "supp {} = {}" |
165 shows "supp {} = {}" |
118 by (simp add: supp_def empty_eqvt) |
166 unfolding supp_def |
|
167 by (simp add: empty_eqvt) |
119 |
168 |
120 lemma fresh_set_empty: |
169 lemma fresh_set_empty: |
121 shows "a \<sharp> {}" |
170 shows "a \<sharp> {}" |
122 by (simp add: fresh_def supp_set_empty) |
171 by (simp add: fresh_def supp_set_empty) |
123 |
172 |
124 lemma UNIV_eqvt: |
173 lemma UNIV_eqvt[eqvt]: |
125 shows "p \<bullet> UNIV = UNIV" |
174 shows "p \<bullet> UNIV = UNIV" |
126 unfolding UNIV_def Collect_eqvt2 True_eqvt .. |
175 unfolding UNIV_def |
127 |
176 by (perm_simp) (rule refl) |
128 lemma union_eqvt: |
177 |
|
178 lemma union_eqvt[eqvt]: |
129 shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)" |
179 shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)" |
130 unfolding Un_def Collect_eqvt2 disj_eqvt mem_eqvt by simp |
180 unfolding Un_def |
131 |
181 by (perm_simp) (rule refl) |
132 lemma inter_eqvt: |
182 |
|
183 lemma inter_eqvt[eqvt]: |
133 shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)" |
184 shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)" |
134 unfolding Int_def Collect_eqvt2 conj_eqvt mem_eqvt by simp |
185 unfolding Int_def |
135 |
186 by (perm_simp) (rule refl) |
136 lemma Diff_eqvt: |
187 |
|
188 lemma Diff_eqvt[eqvt]: |
137 fixes A B :: "'a::pt set" |
189 fixes A B :: "'a::pt set" |
138 shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B" |
190 shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B" |
139 unfolding set_diff_eq Collect_eqvt2 conj_eqvt Not_eqvt mem_eqvt by simp |
191 unfolding set_diff_eq |
140 |
192 by (perm_simp) (rule refl) |
141 lemma Compl_eqvt: |
193 |
|
194 lemma Compl_eqvt[eqvt]: |
142 fixes A :: "'a::pt set" |
195 fixes A :: "'a::pt set" |
143 shows "p \<bullet> (- A) = - (p \<bullet> A)" |
196 shows "p \<bullet> (- A) = - (p \<bullet> A)" |
144 unfolding Compl_eq_Diff_UNIV Diff_eqvt UNIV_eqvt .. |
197 unfolding Compl_eq_Diff_UNIV |
145 |
198 by (perm_simp) (rule refl) |
146 lemma insert_eqvt: |
199 |
|
200 lemma insert_eqvt[eqvt]: |
147 shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)" |
201 shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)" |
148 unfolding permute_set_eq_image image_insert .. |
202 unfolding permute_set_eq_image image_insert .. |
149 |
203 |
150 lemma vimage_eqvt: |
204 lemma vimage_eqvt[eqvt]: |
151 shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)" |
205 shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)" |
152 unfolding vimage_def permute_fun_def [where f=f] |
206 unfolding vimage_def |
153 unfolding Collect_eqvt2 mem_eqvt .. |
207 by (perm_simp) (rule refl) |
154 |
208 |
155 lemma finite_permute_iff: |
209 lemma finite_permute_iff: |
156 shows "finite (p \<bullet> A) \<longleftrightarrow> finite A" |
210 shows "finite (p \<bullet> A) \<longleftrightarrow> finite A" |
157 unfolding permute_set_eq_vimage |
211 unfolding permute_set_eq_vimage |
158 using bij_permute by (rule finite_vimage_iff) |
212 using bij_permute by (rule finite_vimage_iff) |
159 |
213 |
160 lemma finite_eqvt: |
214 lemma finite_eqvt[eqvt]: |
161 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
215 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
162 unfolding finite_permute_iff permute_bool_def .. |
216 unfolding finite_permute_iff permute_bool_def .. |
163 |
217 |
164 |
|
165 section {* List Operations *} |
218 section {* List Operations *} |
166 |
219 |
167 lemma append_eqvt: |
220 lemma append_eqvt[eqvt]: |
168 shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)" |
221 shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)" |
169 by (induct xs) auto |
222 by (induct xs) auto |
170 |
223 |
171 lemma supp_append: |
224 lemma supp_append: |
172 shows "supp (xs @ ys) = supp xs \<union> supp ys" |
225 shows "supp (xs @ ys) = supp xs \<union> supp ys" |
186 |
239 |
187 lemma fresh_rev: |
240 lemma fresh_rev: |
188 shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs" |
241 shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs" |
189 by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil) |
242 by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil) |
190 |
243 |
191 lemma set_eqvt: |
244 lemma set_eqvt[eqvt]: |
192 shows "p \<bullet> (set xs) = set (p \<bullet> xs)" |
245 shows "p \<bullet> (set xs) = set (p \<bullet> xs)" |
193 by (induct xs) (simp_all add: empty_eqvt insert_eqvt) |
246 by (induct xs) (simp_all add: empty_eqvt insert_eqvt) |
194 |
247 |
195 (* needs finite support premise |
248 (* needs finite support premise |
196 lemma supp_set: |
249 lemma supp_set: |
197 fixes x :: "'a::pt" |
250 fixes x :: "'a::pt" |
198 shows "supp (set xs) = supp xs" |
251 shows "supp (set xs) = supp xs" |
199 *) |
252 *) |
200 |
253 |
201 lemma map_eqvt: |
254 lemma map_eqvt[eqvt]: |
202 shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)" |
255 shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)" |
203 by (induct xs) (simp_all, simp only: permute_fun_app_eq) |
256 by (induct xs) (simp_all, simp only: permute_fun_app_eq) |
204 |
257 |
205 section {* Product Operations *} |
258 section {* Product Operations *} |
206 |
259 |
207 lemma fst_eqvt: |
260 lemma fst_eqvt[eqvt]: |
208 "p \<bullet> (fst x) = fst (p \<bullet> x)" |
261 "p \<bullet> (fst x) = fst (p \<bullet> x)" |
209 by (cases x) simp |
262 by (cases x) simp |
210 |
263 |
211 lemma snd_eqvt: |
264 lemma snd_eqvt[eqvt]: |
212 "p \<bullet> (snd x) = snd (p \<bullet> x)" |
265 "p \<bullet> (snd x) = snd (p \<bullet> x)" |
213 by (cases x) simp |
266 by (cases x) simp |
214 |
267 |
215 section {* Units *} |
268 section {* Units *} |
216 |
269 |
220 |
273 |
221 lemma fresh_unit: |
274 lemma fresh_unit: |
222 shows "a \<sharp> ()" |
275 shows "a \<sharp> ()" |
223 by (simp add: fresh_def supp_unit) |
276 by (simp add: fresh_def supp_unit) |
224 |
277 |
225 lemma permute_eqvt_raw: |
278 |
226 shows "p \<bullet> permute = permute" |
279 section {* additional lemmas *} |
227 apply(simp add: expand_fun_eq permute_fun_def) |
280 |
228 apply(subst permute_eqvt) |
281 ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "Pair"} *} |
229 apply(simp) |
282 |
230 done |
|
231 |
|
232 |
|
233 section {* Equivariance automation *} |
|
234 |
|
235 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} |
|
236 |
|
237 use "nominal_thmdecls.ML" |
|
238 setup "Nominal_ThmDecls.setup" |
|
239 |
|
240 ML {* Thm.full_rules *} |
|
241 lemmas [eqvt] = |
283 lemmas [eqvt] = |
242 (* connectives *) |
|
243 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
|
244 True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt |
|
245 imp_eqvt [folded induct_implies_def] |
284 imp_eqvt [folded induct_implies_def] |
246 |
285 |
247 (* nominal *) |
286 (* nominal *) |
248 supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt |
287 supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt |
249 |
288 |
250 (* datatypes *) |
289 (* datatypes *) |
251 permute_prod.simps append_eqvt rev_eqvt set_eqvt |
290 permute_prod.simps Pair_eqvt permute_list.simps |
252 map_eqvt fst_eqvt snd_eqvt Pair_eqvt permute_list.simps |
|
253 |
291 |
254 (* sets *) |
292 (* sets *) |
255 empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt |
293 image_eqvt |
256 Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt |
294 |
257 |
295 |
258 |
296 section {* Test cases *} |
259 lemmas [eqvt_raw] = |
297 |
260 permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) |
|
261 |
|
262 text {* helper lemmas for the eqvt_tac *} |
|
263 |
|
264 definition |
|
265 "unpermute p = permute (- p)" |
|
266 |
|
267 lemma eqvt_apply: |
|
268 fixes f :: "'a::pt \<Rightarrow> 'b::pt" |
|
269 and x :: "'a::pt" |
|
270 shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)" |
|
271 unfolding permute_fun_def by simp |
|
272 |
|
273 lemma eqvt_lambda: |
|
274 fixes f :: "'a::pt \<Rightarrow> 'b::pt" |
|
275 shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))" |
|
276 unfolding permute_fun_def unpermute_def by simp |
|
277 |
|
278 lemma eqvt_bound: |
|
279 shows "p \<bullet> unpermute p x \<equiv> x" |
|
280 unfolding unpermute_def by simp |
|
281 |
|
282 (* provides perm_simp methods *) |
|
283 use "nominal_permeq.ML" |
|
284 setup Nominal_Permeq.setup |
|
285 |
|
286 method_setup perm_simp = |
|
287 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *} |
|
288 {* pushes permutations inside. *} |
|
289 |
|
290 method_setup perm_strict_simp = |
|
291 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} |
|
292 {* pushes permutations inside, raises an error if it cannot solve all permutations. *} |
|
293 |
298 |
294 declare [[trace_eqvt = true]] |
299 declare [[trace_eqvt = true]] |
295 |
300 |
296 lemma |
301 lemma |
297 fixes B::"'a::pt" |
302 fixes B::"'a::pt" |