equal
deleted
inserted
replaced
32 |
32 |
33 typ "'a fset" |
33 typ "'a fset" |
34 thm "Rep_fset" |
34 thm "Rep_fset" |
35 thm "ABS_fset_def" |
35 thm "ABS_fset_def" |
36 |
36 |
37 quotient_def (for "'a fset") |
37 quotient_def |
38 EMPTY :: "'a fset" |
38 EMPTY :: "'a fset" |
39 where |
39 where |
40 "EMPTY \<equiv> ([]::'a list)" |
40 "EMPTY \<equiv> ([]::'a list)" |
41 |
41 |
42 term Nil |
42 term Nil |
43 term EMPTY |
43 term EMPTY |
44 thm EMPTY_def |
44 thm EMPTY_def |
45 |
45 |
46 quotient_def (for "'a fset") |
46 quotient_def |
47 INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
47 INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
48 where |
48 where |
49 "INSERT \<equiv> op #" |
49 "INSERT \<equiv> op #" |
50 |
50 |
51 term Cons |
51 term Cons |
52 term INSERT |
52 term INSERT |
53 thm INSERT_def |
53 thm INSERT_def |
54 |
54 |
55 quotient_def (for "'a fset") |
55 quotient_def |
56 FUNION :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
56 FUNION :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
57 where |
57 where |
58 "FUNION \<equiv> (op @)" |
58 "FUNION \<equiv> (op @)" |
59 |
59 |
60 term append |
60 term append |
76 card1 :: "'a list \<Rightarrow> nat" |
76 card1 :: "'a list \<Rightarrow> nat" |
77 where |
77 where |
78 card1_nil: "(card1 []) = 0" |
78 card1_nil: "(card1 []) = 0" |
79 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" |
79 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" |
80 |
80 |
81 quotient_def (for "'a fset") |
81 quotient_def |
82 CARD :: "'a fset \<Rightarrow> nat" |
82 CARD :: "'a fset \<Rightarrow> nat" |
83 where |
83 where |
84 "CARD \<equiv> card1" |
84 "CARD \<equiv> card1" |
85 |
85 |
86 term card1 |
86 term card1 |
142 apply (induct X) |
142 apply (induct X) |
143 apply (simp) |
143 apply (simp) |
144 apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1) |
144 apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1) |
145 done |
145 done |
146 |
146 |
147 quotient_def (for "'a fset") |
147 quotient_def |
148 IN :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
148 IN :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
149 where |
149 where |
150 "IN \<equiv> membship" |
150 "IN \<equiv> membship" |
151 |
151 |
152 term membship |
152 term membship |
166 term fold1 |
166 term fold1 |
167 term fold |
167 term fold |
168 thm fold_def |
168 thm fold_def |
169 |
169 |
170 (* FIXME: does not work yet for all types*) |
170 (* FIXME: does not work yet for all types*) |
171 quotient_def (for "'a fset" "'b fset") |
171 quotient_def |
172 fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
172 fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
173 where |
173 where |
174 "fmap \<equiv> map" |
174 "fmap \<equiv> map" |
175 |
175 |
176 term map |
176 term map |