equal
deleted
inserted
replaced
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 begin |
12 begin |
13 |
13 |
14 lemma r: "x = x" |
|
15 apply(auto) |
|
16 done |
|
17 |
|
18 ML {* |
|
19 prop_of @{thm r} |
|
20 *} |
|
21 |
14 |
22 section {* Logical Operators *} |
15 section {* Logical Operators *} |
23 |
16 |
24 lemma eq_eqvt: |
17 lemma eq_eqvt: |
25 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)" |
264 Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt |
257 Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt |
265 |
258 |
266 atom_eqvt add_perm_eqvt |
259 atom_eqvt add_perm_eqvt |
267 |
260 |
268 lemmas [eqvt_raw] = |
261 lemmas [eqvt_raw] = |
269 permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) |
262 permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) |
270 |
|
271 thm eqvts |
|
272 thm eqvts_raw |
|
273 |
263 |
274 text {* helper lemmas for the eqvt_tac *} |
264 text {* helper lemmas for the eqvt_tac *} |
275 |
265 |
276 definition |
266 definition |
277 "unpermute p = permute (- p)" |
267 "unpermute p = permute (- p)" |