equal
deleted
inserted
replaced
18 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} |
18 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} |
19 |
19 |
20 use "nominal_thmdecls.ML" |
20 use "nominal_thmdecls.ML" |
21 setup "Nominal_ThmDecls.setup" |
21 setup "Nominal_ThmDecls.setup" |
22 |
22 |
|
23 |
|
24 section {* eqvt lemmas *} |
|
25 |
|
26 lemmas [eqvt] = |
|
27 conj_eqvt Not_eqvt ex_eqvt imp_eqvt |
|
28 imp_eqvt[folded induct_implies_def] |
|
29 |
|
30 (* nominal *) |
|
31 supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt uminus_eqvt |
|
32 |
|
33 (* datatypes *) |
|
34 Pair_eqvt permute_list.simps |
|
35 |
|
36 |
23 text {* helper lemmas for the perm_simp *} |
37 text {* helper lemmas for the perm_simp *} |
24 |
38 |
25 definition |
39 definition |
26 "unpermute p = permute (- p)" |
40 "unpermute p = permute (- p)" |
27 |
41 |
77 |
91 |
78 lemma False_eqvt[eqvt]: |
92 lemma False_eqvt[eqvt]: |
79 shows "p \<bullet> False = False" |
93 shows "p \<bullet> False = False" |
80 unfolding permute_bool_def .. |
94 unfolding permute_bool_def .. |
81 |
95 |
82 lemma imp_eqvt[eqvt]: |
|
83 shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))" |
|
84 by (simp add: permute_bool_def) |
|
85 |
|
86 lemma conj_eqvt[eqvt]: |
|
87 shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))" |
|
88 by (simp add: permute_bool_def) |
|
89 |
|
90 lemma disj_eqvt[eqvt]: |
96 lemma disj_eqvt[eqvt]: |
91 shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))" |
97 shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))" |
92 by (simp add: permute_bool_def) |
98 by (simp add: permute_bool_def) |
93 |
99 |
94 lemma Not_eqvt[eqvt]: |
100 lemma Not_eqvt[eqvt]: |
101 by (auto, drule_tac x="p \<bullet> x" in spec, simp) |
107 by (auto, drule_tac x="p \<bullet> x" in spec, simp) |
102 |
108 |
103 lemma all_eqvt2: |
109 lemma all_eqvt2: |
104 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))" |
110 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))" |
105 by (perm_simp add: permute_minus_cancel) (rule refl) |
111 by (perm_simp add: permute_minus_cancel) (rule refl) |
106 |
|
107 lemma ex_eqvt[eqvt]: |
|
108 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)" |
|
109 unfolding permute_fun_def permute_bool_def |
|
110 by (auto, rule_tac x="p \<bullet> x" in exI, simp) |
|
111 |
112 |
112 lemma ex_eqvt2: |
113 lemma ex_eqvt2: |
113 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))" |
114 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))" |
114 by (perm_simp add: permute_minus_cancel) (rule refl) |
115 by (perm_simp add: permute_minus_cancel) (rule refl) |
115 |
116 |
209 |
210 |
210 lemma insert_eqvt[eqvt]: |
211 lemma insert_eqvt[eqvt]: |
211 shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)" |
212 shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)" |
212 unfolding permute_set_eq_image image_insert .. |
213 unfolding permute_set_eq_image image_insert .. |
213 |
214 |
|
215 lemma image_eqvt: |
|
216 shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" |
|
217 unfolding permute_set_eq_image |
|
218 unfolding permute_fun_def [where f=f] |
|
219 by (simp add: image_image) |
|
220 |
214 lemma vimage_eqvt[eqvt]: |
221 lemma vimage_eqvt[eqvt]: |
215 shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)" |
222 shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)" |
216 unfolding vimage_def |
223 unfolding vimage_def |
217 by (perm_simp) (rule refl) |
224 by (perm_simp) (rule refl) |
218 |
225 |
227 using bij_permute by (rule finite_vimage_iff) |
234 using bij_permute by (rule finite_vimage_iff) |
228 |
235 |
229 lemma finite_eqvt[eqvt]: |
236 lemma finite_eqvt[eqvt]: |
230 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
237 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
231 unfolding finite_permute_iff permute_bool_def .. |
238 unfolding finite_permute_iff permute_bool_def .. |
|
239 |
|
240 lemma supp_set: |
|
241 fixes xs :: "('a::fs) list" |
|
242 shows "supp (set xs) = supp xs" |
|
243 apply(induct xs) |
|
244 apply(simp add: supp_set_empty supp_Nil) |
|
245 apply(simp add: supp_Cons supp_of_fin_insert) |
|
246 done |
|
247 |
232 |
248 |
233 section {* List Operations *} |
249 section {* List Operations *} |
234 |
250 |
235 lemma append_eqvt[eqvt]: |
251 lemma append_eqvt[eqvt]: |
236 shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)" |
252 shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)" |
293 |
309 |
294 lemma fresh_unit: |
310 lemma fresh_unit: |
295 shows "a \<sharp> ()" |
311 shows "a \<sharp> ()" |
296 by (simp add: fresh_def supp_unit) |
312 by (simp add: fresh_def supp_unit) |
297 |
313 |
298 section {* additional eqvt lemmas *} |
|
299 |
|
300 lemmas [eqvt] = |
|
301 imp_eqvt [folded induct_implies_def] |
|
302 |
|
303 (* nominal *) |
|
304 supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt uminus_eqvt |
|
305 |
|
306 (* datatypes *) |
|
307 Pair_eqvt permute_list.simps |
|
308 |
|
309 (* sets *) |
|
310 image_eqvt |
|
311 |
|
312 |
314 |
313 section {* Test cases *} |
315 section {* Test cases *} |
314 |
316 |
315 |
317 |
316 declare [[trace_eqvt = false]] |
318 declare [[trace_eqvt = false]] |