31 |
31 |
32 quotient_type |
32 quotient_type |
33 'a fset = "'a list" / "list_eq" |
33 'a fset = "'a list" / "list_eq" |
34 by (rule list_eq_equivp) |
34 by (rule list_eq_equivp) |
35 |
35 |
|
36 lemma sub_list_rsp1: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list xs zs = sub_list ys zs" |
|
37 by (simp add: sub_list_def) |
|
38 |
|
39 lemma sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys" |
|
40 by (simp add: sub_list_def) |
|
41 |
|
42 lemma [quot_respect]: |
|
43 "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
|
44 by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2) |
|
45 |
|
46 lemma sub_list_not_eq: |
|
47 "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)" |
|
48 by (auto simp add: sub_list_def) |
|
49 |
|
50 lemma sub_list_refl: |
|
51 "sub_list x x" |
|
52 by (simp add: sub_list_def) |
|
53 |
|
54 lemma sub_list_trans: |
|
55 "sub_list x y \<Longrightarrow> sub_list y z \<Longrightarrow> sub_list x z" |
|
56 by (simp add: sub_list_def) |
|
57 |
|
58 lemma sub_list_empty: |
|
59 "sub_list [] x" |
|
60 by (simp add: sub_list_def) |
|
61 |
|
62 instantiation fset :: (type) bot |
|
63 begin |
|
64 |
|
65 quotient_definition |
|
66 "bot :: 'a fset" is "[] :: 'a list" |
|
67 |
|
68 abbreviation |
|
69 fempty ("{||}") |
|
70 where |
|
71 "{||} \<equiv> bot :: 'a fset" |
|
72 |
|
73 quotient_definition |
|
74 "less_eq_fset \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)" |
|
75 is |
|
76 "sub_list \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> bool)" |
|
77 |
|
78 abbreviation |
|
79 f_subset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50) |
|
80 where |
|
81 "xs |\<subseteq>| ys \<equiv> xs \<le> ys" |
|
82 |
|
83 definition |
|
84 less_fset: |
|
85 "(xs :: 'a fset) < ys \<equiv> xs \<le> ys \<and> xs \<noteq> ys" |
|
86 |
|
87 abbreviation |
|
88 f_subset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50) |
|
89 where |
|
90 "xs |\<subset>| ys \<equiv> xs < ys" |
|
91 |
|
92 instance |
|
93 proof |
|
94 fix x y z :: "'a fset" |
|
95 show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)" |
|
96 unfolding less_fset by (lifting sub_list_not_eq) |
|
97 show "x |\<subseteq>| x" by (lifting sub_list_refl) |
|
98 show "{||} |\<subseteq>| x" by (lifting sub_list_empty) |
|
99 next |
|
100 fix x y z :: "'a fset" |
|
101 assume a: "x |\<subseteq>| y" |
|
102 assume b: "y |\<subseteq>| z" |
|
103 show "x |\<subseteq>| z" using a b by (lifting sub_list_trans) |
|
104 qed |
|
105 |
|
106 end |
|
107 |
36 section {* Empty fset, Finsert and Membership *} |
108 section {* Empty fset, Finsert and Membership *} |
37 |
109 |
38 quotient_definition |
110 quotient_definition |
39 fempty ("{||}") |
111 "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
40 where |
|
41 "fempty :: 'a fset" |
|
42 is "[]::'a list" |
|
43 |
|
44 quotient_definition |
|
45 "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
46 is "op #" |
112 is "op #" |
47 |
113 |
48 syntax |
114 syntax |
49 "@Finset" :: "args => 'a fset" ("{|(_)|}") |
115 "@Finset" :: "args => 'a fset" ("{|(_)|}") |
50 |
116 |
127 section {* sub_list *} |
193 section {* sub_list *} |
128 |
194 |
129 lemma sub_list_cons: |
195 lemma sub_list_cons: |
130 "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)" |
196 "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)" |
131 by (auto simp add: memb_def sub_list_def) |
197 by (auto simp add: memb_def sub_list_def) |
132 |
|
133 lemma sub_list_rsp1: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list xs zs = sub_list ys zs" |
|
134 by (simp add: sub_list_def) |
|
135 |
|
136 lemma sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys" |
|
137 by (simp add: sub_list_def) |
|
138 |
|
139 lemma [quot_respect]: |
|
140 "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
|
141 by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2) |
|
142 |
198 |
143 section {* Cardinality of finite sets *} |
199 section {* Cardinality of finite sets *} |
144 |
200 |
145 fun |
201 fun |
146 fcard_raw :: "'a list \<Rightarrow> nat" |
202 fcard_raw :: "'a list \<Rightarrow> nat" |
770 |
826 |
771 lemma fin_finter: |
827 lemma fin_finter: |
772 "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T" |
828 "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T" |
773 by (lifting memb_finter_raw) |
829 by (lifting memb_finter_raw) |
774 |
830 |
|
831 lemma fsubset_finsert: |
|
832 "(finsert x xs |\<subseteq>| ys) = (x |\<in>| ys \<and> xs |\<subseteq>| ys)" |
|
833 by (lifting sub_list_cons) |
|
834 |
|
835 thm sub_list_def[simplified memb_def[symmetric], quot_lifted, no_vars] |
|
836 |
|
837 lemma fsubset_fin: "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)" |
|
838 by (rule meta_eq_to_obj_eq) |
|
839 (lifting sub_list_def[simplified memb_def[symmetric]]) |
|
840 |
775 lemma expand_fset_eq: |
841 lemma expand_fset_eq: |
776 "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))" |
842 "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))" |
777 by (lifting list_eq.simps[simplified memb_def[symmetric]]) |
843 by (lifting list_eq.simps[simplified memb_def[symmetric]]) |
778 |
844 |
779 (* We cannot write it as "assumes .. shows" since Isabelle changes |
845 (* We cannot write it as "assumes .. shows" since Isabelle changes |