| changeset 1546 | dbdce626c925 |
| parent 1544 | c6849a634582 |
| child 1557 | fee2389789ad |
| 1545:f32981105089 | 1546:dbdce626c925 |
|---|---|
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" "Nominal2_FSet" |
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" |
747 "distinct_perms [] = True" |
747 "distinct_perms [] = True" |
748 | "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)" |
748 | "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)" |
749 |
749 |
750 (* support of concrete atom sets *) |
750 (* support of concrete atom sets *) |
751 |
751 |
752 lemma atom_eqvt_raw: |
|
753 fixes p::"perm" |
|
754 shows "(p \<bullet> atom) = atom" |
|
755 by (simp add: expand_fun_eq permute_fun_def atom_eqvt) |
|
756 |
|
757 lemma atom_image_cong: |
|
758 shows "(atom ` X = atom ` Y) = (X = Y)" |
|
759 apply(rule inj_image_eq_iff) |
|
760 apply(simp add: inj_on_def) |
|
761 done |
|
762 |
|
763 lemma supp_atom_image: |
752 lemma supp_atom_image: |
764 fixes as::"'a::at_base set" |
753 fixes as::"'a::at_base set" |
765 shows "supp (atom ` as) = supp as" |
754 shows "supp (atom ` as) = supp as" |
766 apply(simp add: supp_def) |
755 apply(simp add: supp_def) |
767 apply(simp add: image_eqvt) |
756 apply(simp add: image_eqvt) |
791 "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) = |
780 "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) = |
792 (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 |
781 (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 |
793 \<and> pi \<bullet> bs = cs)" |
782 \<and> pi \<bullet> bs = cs)" |
794 by (simp add: alpha_gen) |
783 by (simp add: alpha_gen) |
795 |
784 |
785 (* maybe should be added to Infinite.thy *) |
|
786 lemma infinite_Un: |
|
787 shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
|
788 by simp |
|
789 |
|
796 end |
790 end |
797 |
791 |