equal
deleted
inserted
replaced
30 |
30 |
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 ("{||}") |
|
36 where |
|
37 "fempty :: 'a fset" |
36 is "[]::'a list" |
38 is "[]::'a list" |
37 |
39 |
38 quotient_definition |
40 quotient_definition |
39 "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
41 "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
40 is "op #" |
42 is "op #" |
50 memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" |
52 memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" |
51 where |
53 where |
52 "memb x xs \<equiv> x \<in> set xs" |
54 "memb x xs \<equiv> x \<in> set xs" |
53 |
55 |
54 quotient_definition |
56 quotient_definition |
55 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<in>| _" [50, 51] 50) |
57 fin ("_ |\<in>| _" [50, 51] 50) |
|
58 where |
|
59 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
56 is "memb" |
60 is "memb" |
57 |
61 |
58 abbreviation |
62 abbreviation |
59 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50) |
63 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50) |
60 where |
64 where |
133 by (lifting singleton_list_eq) |
137 by (lifting singleton_list_eq) |
134 |
138 |
135 section {* Union *} |
139 section {* Union *} |
136 |
140 |
137 quotient_definition |
141 quotient_definition |
138 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65) |
142 funion (infixl "|\<union>|" 65) |
|
143 where |
|
144 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
139 is |
145 is |
140 "op @" |
146 "op @" |
141 |
147 |
142 section {* Cardinality of finite sets *} |
148 section {* Cardinality of finite sets *} |
143 |
149 |
620 quotient_definition |
626 quotient_definition |
621 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" |
627 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" |
622 is "delete_raw" |
628 is "delete_raw" |
623 |
629 |
624 quotient_definition |
630 quotient_definition |
625 "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70) |
631 finter ("_ \<inter>f _" [70, 71] 70) |
|
632 where |
|
633 "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
626 is "inter_raw" |
634 is "inter_raw" |
627 |
635 |
628 quotient_definition |
636 quotient_definition |
629 "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" |
637 "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" |
630 is "fold_raw" |
638 is "fold_raw" |
701 |
709 |
702 lemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa" |
710 lemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa" |
703 apply (lifting list.cases(2)) |
711 apply (lifting list.cases(2)) |
704 done |
712 done |
705 |
713 |
706 thm quot_respect |
|
707 |
|
708 |
|
709 end |
714 end |