equal
deleted
inserted
replaced
22 |
22 |
23 |
23 |
24 section {* eqvt lemmas *} |
24 section {* eqvt lemmas *} |
25 |
25 |
26 lemmas [eqvt] = |
26 lemmas [eqvt] = |
27 conj_eqvt Not_eqvt ex_eqvt imp_eqvt |
27 conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt |
28 imp_eqvt[folded induct_implies_def] |
28 imp_eqvt[folded induct_implies_def] |
29 uminus_eqvt |
29 uminus_eqvt |
30 |
30 |
31 (* nominal *) |
31 (* nominal *) |
32 supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt |
32 supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt |
33 swap_eqvt flip_eqvt |
33 swap_eqvt flip_eqvt |
34 |
34 |
35 (* datatypes *) |
35 (* datatypes *) |
36 Pair_eqvt permute_list.simps |
36 Pair_eqvt permute_list.simps |
37 |
37 |
|
38 (* sets *) |
|
39 mem_eqvt insert_eqvt |
38 |
40 |
39 text {* helper lemmas for the perm_simp *} |
41 text {* helper lemmas for the perm_simp *} |
40 |
42 |
41 definition |
43 definition |
42 "unpermute p = permute (- p)" |
44 "unpermute p = permute (- p)" |
96 unfolding permute_bool_def .. |
98 unfolding permute_bool_def .. |
97 |
99 |
98 lemma disj_eqvt[eqvt]: |
100 lemma disj_eqvt[eqvt]: |
99 shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))" |
101 shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))" |
100 by (simp add: permute_bool_def) |
102 by (simp add: permute_bool_def) |
101 |
|
102 lemma Not_eqvt[eqvt]: |
|
103 shows "p \<bullet> (\<not> A) \<longleftrightarrow> \<not> (p \<bullet> A)" |
|
104 by (simp add: permute_bool_def) |
|
105 |
|
106 lemma all_eqvt[eqvt]: |
|
107 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)" |
|
108 unfolding permute_fun_def permute_bool_def |
|
109 by (auto, drule_tac x="p \<bullet> x" in spec, simp) |
|
110 |
103 |
111 lemma all_eqvt2: |
104 lemma all_eqvt2: |
112 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))" |
105 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))" |
113 by (perm_simp add: permute_minus_cancel) (rule refl) |
106 by (perm_simp add: permute_minus_cancel) (rule refl) |
114 |
107 |
135 apply(rule theI'[OF unique]) |
128 apply(rule theI'[OF unique]) |
136 done |
129 done |
137 |
130 |
138 section {* Set Operations *} |
131 section {* Set Operations *} |
139 |
132 |
140 lemma mem_permute_iff: |
|
141 shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
|
142 unfolding mem_def permute_fun_def permute_bool_def |
|
143 by simp |
|
144 |
|
145 lemma mem_eqvt[eqvt]: |
|
146 shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)" |
|
147 unfolding mem_def |
|
148 by (perm_simp) (rule refl) |
|
149 |
|
150 lemma not_mem_eqvt: |
133 lemma not_mem_eqvt: |
151 shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)" |
134 shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)" |
152 by (perm_simp) (rule refl) |
135 by (perm_simp) (rule refl) |
153 |
136 |
154 lemma Collect_eqvt[eqvt]: |
137 lemma Collect_eqvt[eqvt]: |
207 lemma Compl_eqvt[eqvt]: |
190 lemma Compl_eqvt[eqvt]: |
208 fixes A :: "'a::pt set" |
191 fixes A :: "'a::pt set" |
209 shows "p \<bullet> (- A) = - (p \<bullet> A)" |
192 shows "p \<bullet> (- A) = - (p \<bullet> A)" |
210 unfolding Compl_eq_Diff_UNIV |
193 unfolding Compl_eq_Diff_UNIV |
211 by (perm_simp) (rule refl) |
194 by (perm_simp) (rule refl) |
212 |
|
213 lemma insert_eqvt[eqvt]: |
|
214 shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)" |
|
215 unfolding permute_set_eq_image image_insert .. |
|
216 |
195 |
217 lemma image_eqvt: |
196 lemma image_eqvt: |
218 shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" |
197 shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" |
219 unfolding permute_set_eq_image |
198 unfolding permute_set_eq_image |
220 unfolding permute_fun_def [where f=f] |
199 unfolding permute_fun_def [where f=f] |
301 lemma split_eqvt[eqvt]: |
280 lemma split_eqvt[eqvt]: |
302 shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)" |
281 shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)" |
303 unfolding split_def |
282 unfolding split_def |
304 by (perm_simp) (rule refl) |
283 by (perm_simp) (rule refl) |
305 |
284 |
306 section {* Units *} |
|
307 |
|
308 lemma supp_unit: |
|
309 shows "supp () = {}" |
|
310 by (simp add: supp_def) |
|
311 |
|
312 lemma fresh_unit: |
|
313 shows "a \<sharp> ()" |
|
314 by (simp add: fresh_def supp_unit) |
|
315 |
|
316 |
285 |
317 section {* Test cases *} |
286 section {* Test cases *} |
318 |
287 |
319 |
288 |
320 declare [[trace_eqvt = false]] |
289 declare [[trace_eqvt = false]] |