1 (* Title: Nominal2_Eqvt |
1 (* Title: Nominal2_Eqvt |
2 Authors: Brian Huffman, Christian Urban |
2 Authors: Brian Huffman, Christian Urban |
3 |
3 |
4 Equivariance, Supp and Fresh Lemmas for Operators. |
4 Equivariance, Supp and Fresh Lemmas for Operators. |
|
5 (Contains most, but not all such lemmas.) |
5 *) |
6 *) |
6 theory Nominal2_Eqvt |
7 theory Nominal2_Eqvt |
7 imports Nominal2_Base |
8 imports Nominal2_Base |
8 uses ("nominal_thmdecls.ML") |
9 uses ("nominal_thmdecls.ML") |
9 ("nominal_permeq.ML") |
10 ("nominal_permeq.ML") |
74 unfolding Ex1_def ex_eqvt2 conj_eqvt all_eqvt2 imp_eqvt eq_eqvt |
75 unfolding Ex1_def ex_eqvt2 conj_eqvt all_eqvt2 imp_eqvt eq_eqvt |
75 by simp |
76 by simp |
76 |
77 |
77 lemma the_eqvt: |
78 lemma the_eqvt: |
78 assumes unique: "\<exists>!x. P x" |
79 assumes unique: "\<exists>!x. P x" |
79 shows "p \<bullet> (THE x. P x) = (THE x. p \<bullet> P (- p \<bullet> x))" |
80 shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))" |
80 apply(rule the1_equality [symmetric]) |
81 apply(rule the1_equality [symmetric]) |
81 apply(simp add: ex1_eqvt2[symmetric]) |
82 apply(simp add: ex1_eqvt2[symmetric]) |
82 apply(simp add: permute_bool_def unique) |
83 apply(simp add: permute_bool_def unique) |
83 apply(simp add: permute_bool_def) |
84 apply(simp add: permute_bool_def) |
84 apply(rule theI'[OF unique]) |
85 apply(rule theI'[OF unique]) |
85 done |
86 done |
86 |
87 |
87 section {* Set Operations *} |
88 section {* Set Operations *} |
88 |
89 |
|
90 lemma mem_permute_iff: |
|
91 shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
|
92 unfolding mem_def permute_fun_def permute_bool_def |
|
93 by simp |
|
94 |
89 lemma mem_eqvt: |
95 lemma mem_eqvt: |
90 shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)" |
96 shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)" |
91 unfolding mem_def permute_fun_def by simp |
97 unfolding mem_permute_iff permute_bool_def by simp |
92 |
98 |
93 lemma not_mem_eqvt: |
99 lemma not_mem_eqvt: |
94 shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)" |
100 shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)" |
95 unfolding mem_def permute_fun_def by (simp add: Not_eqvt) |
101 unfolding mem_def permute_fun_def by (simp add: Not_eqvt) |
96 |
102 |
227 setup "Nominal_ThmDecls.setup" |
233 setup "Nominal_ThmDecls.setup" |
228 |
234 |
229 lemmas [eqvt] = |
235 lemmas [eqvt] = |
230 (* connectives *) |
236 (* connectives *) |
231 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
237 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
232 True_eqvt False_eqvt ex_eqvt all_eqvt |
238 True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt |
233 imp_eqvt [folded induct_implies_def] |
239 imp_eqvt [folded induct_implies_def] |
234 |
240 |
235 (* nominal *) |
241 (* nominal *) |
236 permute_eqvt supp_eqvt fresh_eqvt |
242 permute_eqvt supp_eqvt fresh_eqvt |
237 permute_pure |
243 permute_pure |
238 |
244 |
239 (* datatypes *) |
245 (* datatypes *) |
240 permute_prod.simps |
246 permute_prod.simps append_eqvt rev_eqvt set_eqvt |
241 fst_eqvt snd_eqvt |
247 fst_eqvt snd_eqvt |
242 |
248 |
243 (* sets *) |
249 (* sets *) |
244 empty_eqvt UNIV_eqvt union_eqvt inter_eqvt |
250 empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt |
245 Diff_eqvt Compl_eqvt insert_eqvt |
251 Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt |
246 |
252 |
247 thm eqvts |
253 thm eqvts |
248 thm eqvts_raw |
254 thm eqvts_raw |
249 |
255 |
250 text {* helper lemmas for the eqvt_tac *} |
256 text {* helper lemmas for the eqvt_tac *} |