equal
deleted
inserted
replaced
31 |
31 |
32 section {* empty fset, finsert and membership *} |
32 section {* empty fset, finsert and membership *} |
33 |
33 |
34 quotient_definition |
34 quotient_definition |
35 "fempty :: 'a fset" ("{||}") |
35 "fempty :: 'a fset" ("{||}") |
36 as "[]::'a list" |
36 is "[]::'a list" |
37 |
37 |
38 quotient_definition |
38 quotient_definition |
39 "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
39 "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
40 as "op #" |
40 is "op #" |
41 |
41 |
42 syntax |
42 syntax |
43 "@Finset" :: "args => 'a fset" ("{|(_)|}") |
43 "@Finset" :: "args => 'a fset" ("{|(_)|}") |
44 |
44 |
45 translations |
45 translations |
51 where |
51 where |
52 "memb x xs \<equiv> x \<in> set xs" |
52 "memb x xs \<equiv> x \<in> set xs" |
53 |
53 |
54 quotient_definition |
54 quotient_definition |
55 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<in>| _" [50, 51] 50) |
55 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<in>| _" [50, 51] 50) |
56 as "memb" |
56 is "memb" |
57 |
57 |
58 abbreviation |
58 abbreviation |
59 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50) |
59 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50) |
60 where |
60 where |
61 "a |\<notin>| S \<equiv> \<not>(a |\<in>| S)" |
61 "a |\<notin>| S \<equiv> \<not>(a |\<in>| S)" |
147 fcard_raw_nil: "fcard_raw [] = 0" |
147 fcard_raw_nil: "fcard_raw [] = 0" |
148 | fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))" |
148 | fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))" |
149 |
149 |
150 quotient_definition |
150 quotient_definition |
151 "fcard :: 'a fset \<Rightarrow> nat" |
151 "fcard :: 'a fset \<Rightarrow> nat" |
152 as "fcard_raw" |
152 is "fcard_raw" |
153 |
153 |
154 text {* raw section *} |
154 text {* raw section *} |
155 |
155 |
156 lemma fcard_raw_ge_0: |
156 lemma fcard_raw_ge_0: |
157 assumes a: "x \<in> set xs" |
157 assumes a: "x \<in> set xs" |