equal
deleted
inserted
replaced
1 theory Abs |
1 theory Abs |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Quotient" "Quotient_Product" |
3 begin |
3 begin |
4 |
4 |
5 lemma permute_boolI: |
5 lemma permute_boolI: |
6 fixes P::"bool" |
6 fixes P::"bool" |
7 shows "p \<bullet> P \<Longrightarrow> P" |
7 shows "p \<bullet> P \<Longrightarrow> P" |
270 apply(assumption) |
270 apply(assumption) |
271 apply(assumption) |
271 apply(assumption) |
272 apply(simp) |
272 apply(simp) |
273 done |
273 done |
274 |
274 |
275 term "alpha_abs_tst" |
|
276 |
|
277 quotient_type ('a,'b) abs_tst = "(('a \<Rightarrow>atom set) \<times> 'a::pt \<times> 'b::pt)" / "alpha_abs_tst" |
275 quotient_type ('a,'b) abs_tst = "(('a \<Rightarrow>atom set) \<times> 'a::pt \<times> 'b::pt)" / "alpha_abs_tst" |
278 apply(rule equivpI) |
276 apply(rule equivpI) |
279 unfolding reflp_def symp_def transp_def |
277 unfolding reflp_def symp_def transp_def |
280 apply(simp_all) |
278 apply(simp_all) |
281 (* refl *) |
279 (* refl *) |
296 apply(rule alpha_gen_trans_tst) |
294 apply(rule alpha_gen_trans_tst) |
297 apply(assumption) |
295 apply(assumption) |
298 apply(assumption) |
296 apply(assumption) |
299 apply(simp) |
297 apply(simp) |
300 done |
298 done |
301 |
|
302 |
299 |
303 quotient_definition |
300 quotient_definition |
304 "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs" |
301 "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs" |
305 is |
302 is |
306 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |
303 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |