equal
deleted
inserted
replaced
31 (* nominal *) |
31 (* nominal *) |
32 supp_eqvt fresh_eqvt fresh_star_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 *) |
38 (* sets *) |
39 mem_eqvt insert_eqvt |
39 mem_eqvt empty_eqvt insert_eqvt set_eqvt |
|
40 |
|
41 (* fsets *) |
|
42 permute_fset fset_eqvt |
40 |
43 |
41 text {* helper lemmas for the perm_simp *} |
44 text {* helper lemmas for the perm_simp *} |
42 |
45 |
43 definition |
46 definition |
44 "unpermute p = permute (- p)" |
47 "unpermute p = permute (- p)" |
77 apply(simp add: fun_eq_iff permute_fun_def) |
80 apply(simp add: fun_eq_iff permute_fun_def) |
78 apply(subst permute_eqvt) |
81 apply(subst permute_eqvt) |
79 apply(simp) |
82 apply(simp) |
80 done |
83 done |
81 |
84 |
82 section {* Logical Operators *} |
85 subsection {* Equivariance of Logical Operators *} |
83 |
86 |
84 lemma eq_eqvt[eqvt]: |
87 lemma eq_eqvt[eqvt]: |
85 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |
88 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |
86 unfolding permute_eq_iff permute_bool_def .. |
89 unfolding permute_eq_iff permute_bool_def .. |
87 |
90 |
126 apply(simp add: permute_bool_def unique) |
129 apply(simp add: permute_bool_def unique) |
127 apply(simp add: permute_bool_def) |
130 apply(simp add: permute_bool_def) |
128 apply(rule theI'[OF unique]) |
131 apply(rule theI'[OF unique]) |
129 done |
132 done |
130 |
133 |
131 section {* Set Operations *} |
134 subsection {* Equivariance Set Operations *} |
132 |
135 |
133 lemma not_mem_eqvt: |
136 lemma not_mem_eqvt: |
134 shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)" |
137 shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)" |
135 by (perm_simp) (rule refl) |
138 by (perm_simp) (rule refl) |
136 |
139 |
148 by (perm_simp) (rule refl) |
151 by (perm_simp) (rule refl) |
149 |
152 |
150 lemma Ball_eqvt[eqvt]: |
153 lemma Ball_eqvt[eqvt]: |
151 shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)" |
154 shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)" |
152 unfolding Ball_def |
155 unfolding Ball_def |
153 by (perm_simp) (rule refl) |
|
154 |
|
155 lemma empty_eqvt[eqvt]: |
|
156 shows "p \<bullet> {} = {}" |
|
157 unfolding empty_def |
|
158 by (perm_simp) (rule refl) |
156 by (perm_simp) (rule refl) |
159 |
157 |
160 lemma supp_set_empty: |
158 lemma supp_set_empty: |
161 shows "supp {} = {}" |
159 shows "supp {} = {}" |
162 unfolding supp_def |
160 unfolding supp_def |
221 lemma supp_set: |
219 lemma supp_set: |
222 fixes xs :: "('a::fs) list" |
220 fixes xs :: "('a::fs) list" |
223 shows "supp (set xs) = supp xs" |
221 shows "supp (set xs) = supp xs" |
224 apply(induct xs) |
222 apply(induct xs) |
225 apply(simp add: supp_set_empty supp_Nil) |
223 apply(simp add: supp_set_empty supp_Nil) |
226 apply(simp add: supp_Cons supp_of_fin_insert) |
224 apply(simp add: supp_Cons supp_of_finite_insert) |
227 done |
225 done |
228 |
226 |
229 |
227 |
230 section {* List Operations *} |
228 section {* List Operations *} |
231 |
229 |
251 |
249 |
252 lemma fresh_rev: |
250 lemma fresh_rev: |
253 shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs" |
251 shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs" |
254 by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil) |
252 by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil) |
255 |
253 |
256 lemma set_eqvt[eqvt]: |
|
257 shows "p \<bullet> (set xs) = set (p \<bullet> xs)" |
|
258 by (induct xs) (simp_all add: empty_eqvt insert_eqvt) |
|
259 |
|
260 (* needs finite support premise |
|
261 lemma supp_set: |
|
262 fixes x :: "'a::pt" |
|
263 shows "supp (set xs) = supp xs" |
|
264 *) |
|
265 |
|
266 lemma map_eqvt[eqvt]: |
254 lemma map_eqvt[eqvt]: |
267 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)" |
268 by (induct xs) (simp_all, simp only: permute_fun_app_eq) |
256 by (induct xs) (simp_all, simp only: permute_fun_app_eq) |
269 |
257 |
270 section {* Product Operations *} |
258 |
|
259 subsection {* Equivariance for fsets *} |
|
260 |
|
261 lemma map_fset_eqvt[eqvt]: |
|
262 shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)" |
|
263 by (lifting map_eqvt) |
|
264 |
|
265 |
|
266 subsection {* Product Operations *} |
271 |
267 |
272 lemma fst_eqvt[eqvt]: |
268 lemma fst_eqvt[eqvt]: |
273 "p \<bullet> (fst x) = fst (p \<bullet> x)" |
269 "p \<bullet> (fst x) = fst (p \<bullet> x)" |
274 by (cases x) simp |
270 by (cases x) simp |
275 |
271 |
377 thm eqvts_raw |
373 thm eqvts_raw |
378 |
374 |
379 ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *} |
375 ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *} |
380 |
376 |
381 |
377 |
382 section {* Automatic equivariance procedure for inductive definitions *} |
378 section {* automatic equivariance procedure for inductive definitions *} |
383 |
379 |
384 use "nominal_eqvt.ML" |
380 use "nominal_eqvt.ML" |
385 |
381 |
386 end |
382 end |