equal
deleted
inserted
replaced
1 (* Title: Nominal2_Eqvt |
1 (* Title: Nominal2_Eqvt |
2 Author: Brian Huffman, |
2 Author: Brian Huffman, |
3 Author: Christian Urban |
3 Author: Christian Urban |
4 |
4 |
5 Equivariance, Supp and Fresh Lemmas for Operators. |
5 Equivariance, supp and freshness lemmas for various operators |
6 (Contains many, but not all such lemmas.) |
6 (contains many, but not all such lemmas). |
7 *) |
7 *) |
8 theory Nominal2_Eqvt |
8 theory Nominal2_Eqvt |
9 imports Nominal2_Base Nominal2_Atoms |
9 imports Nominal2_Base Nominal2_Atoms |
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 |
|
15 |
14 |
16 section {* Logical Operators *} |
15 section {* Logical Operators *} |
17 |
16 |
18 lemma eq_eqvt: |
17 lemma eq_eqvt: |
19 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |
18 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |
236 apply(simp) |
235 apply(simp) |
237 done |
236 done |
238 |
237 |
239 section {* Equivariance automation *} |
238 section {* Equivariance automation *} |
240 |
239 |
241 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *} |
240 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} |
|
241 |
|
242 ML {* Thm.declaration_attribute *} |
242 |
243 |
243 use "nominal_thmdecls.ML" |
244 use "nominal_thmdecls.ML" |
244 setup "Nominal_ThmDecls.setup" |
245 setup "Nominal_ThmDecls.setup" |
245 |
246 |
246 lemmas [eqvt] = |
247 lemmas [eqvt] = |