equal
deleted
inserted
replaced
1 (* Title: Nominal2_Eqvt |
1 (* Title: Nominal2_Eqvt |
2 Authors: Brian Huffman, Christian Urban |
2 Author: Brian Huffman, |
|
3 Author: Christian Urban |
3 |
4 |
4 Equivariance, Supp and Fresh Lemmas for Operators. |
5 Equivariance, Supp and Fresh Lemmas for Operators. |
5 (Contains most, but not all such lemmas.) |
6 (Contains many, but not all such lemmas.) |
6 *) |
7 *) |
7 theory Nominal2_Eqvt |
8 theory Nominal2_Eqvt |
8 imports Nominal2_Base Nominal2_Atoms |
9 imports Nominal2_Base Nominal2_Atoms |
9 uses ("nominal_thmdecls.ML") |
10 uses ("nominal_thmdecls.ML") |
10 ("nominal_permeq.ML") |
11 ("nominal_permeq.ML") |
11 begin |
12 begin |
|
13 |
|
14 lemma r: "x = x" |
|
15 apply(auto) |
|
16 done |
|
17 |
|
18 ML {* |
|
19 prop_of @{thm r} |
|
20 *} |
12 |
21 |
13 section {* Logical Operators *} |
22 section {* Logical Operators *} |
14 |
23 |
15 lemma eq_eqvt: |
24 lemma eq_eqvt: |
16 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |
25 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |