equal
deleted
inserted
replaced
8 uses ("nominal_thmdecls.ML") |
8 uses ("nominal_thmdecls.ML") |
9 ("nominal_permeq.ML") |
9 ("nominal_permeq.ML") |
10 begin |
10 begin |
11 |
11 |
12 section {* Logical Operators *} |
12 section {* Logical Operators *} |
|
13 |
13 |
14 |
14 lemma eq_eqvt: |
15 lemma eq_eqvt: |
15 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |
16 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |
16 unfolding permute_eq_iff permute_bool_def .. |
17 unfolding permute_eq_iff permute_bool_def .. |
17 |
18 |
231 True_eqvt False_eqvt ex_eqvt all_eqvt |
232 True_eqvt False_eqvt ex_eqvt all_eqvt |
232 imp_eqvt [folded induct_implies_def] |
233 imp_eqvt [folded induct_implies_def] |
233 |
234 |
234 (* nominal *) |
235 (* nominal *) |
235 permute_eqvt supp_eqvt fresh_eqvt |
236 permute_eqvt supp_eqvt fresh_eqvt |
|
237 permute_pure |
236 |
238 |
237 (* datatypes *) |
239 (* datatypes *) |
238 permute_prod.simps |
240 permute_prod.simps |
239 fst_eqvt snd_eqvt |
241 fst_eqvt snd_eqvt |
240 |
242 |
241 (* sets *) |
243 (* sets *) |
242 empty_eqvt UNIV_eqvt union_eqvt inter_eqvt |
244 empty_eqvt UNIV_eqvt union_eqvt inter_eqvt |
243 Diff_eqvt Compl_eqvt insert_eqvt |
245 Diff_eqvt Compl_eqvt insert_eqvt |
244 |
246 |
245 declare permute_pure [eqvt] |
247 thm eqvts |
246 |
248 thm eqvts_raw |
247 (* thm eqvts *) |
|
248 |
249 |
249 text {* helper lemmas for the eqvt_tac *} |
250 text {* helper lemmas for the eqvt_tac *} |
250 |
251 |
251 definition |
252 definition |
252 "unpermute p = permute (- p)" |
253 "unpermute p = permute (- p)" |