equal
deleted
inserted
replaced
134 |
134 |
135 section {* Union *} |
135 section {* Union *} |
136 |
136 |
137 quotient_definition |
137 quotient_definition |
138 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65) |
138 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65) |
139 as |
139 is |
140 "op @" |
140 "op @" |
141 |
141 |
142 section {* Cardinality of finite sets *} |
142 section {* Cardinality of finite sets *} |
143 |
143 |
144 fun |
144 fun |
225 |
225 |
226 section {* fmap and fset comprehension *} |
226 section {* fmap and fset comprehension *} |
227 |
227 |
228 quotient_definition |
228 quotient_definition |
229 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
229 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
230 as |
230 is |
231 "map" |
231 "map" |
232 |
232 |
233 quotient_definition |
233 quotient_definition |
234 "fconcat :: ('a fset) fset => 'a fset" |
234 "fconcat :: ('a fset) fset => 'a fset" |
235 as |
235 is |
236 "concat" |
236 "concat" |
237 |
237 |
238 (*lemma fconcat_rsp[quot_respect]: |
238 (*lemma fconcat_rsp[quot_respect]: |
239 shows "((list_rel op \<approx>) ===> op \<approx>) concat concat" |
239 shows "((list_rel op \<approx>) ===> op \<approx>) concat concat" |
240 apply(auto) |
240 apply(auto) |
617 section {* Constants on the Quotient Type *} |
617 section {* Constants on the Quotient Type *} |
618 |
618 |
619 |
619 |
620 quotient_definition |
620 quotient_definition |
621 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" |
621 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" |
622 as "delete_raw" |
622 is "delete_raw" |
623 |
623 |
624 quotient_definition |
624 quotient_definition |
625 "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70) |
625 "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70) |
626 as "inter_raw" |
626 is "inter_raw" |
627 |
627 |
628 quotient_definition |
628 quotient_definition |
629 "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" |
629 "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" |
630 as "fold_raw" |
630 is "fold_raw" |
631 |
631 |
632 quotient_definition |
632 quotient_definition |
633 "fset_to_set :: 'a fset \<Rightarrow> 'a set" |
633 "fset_to_set :: 'a fset \<Rightarrow> 'a set" |
634 as "set" |
634 is "set" |
635 |
635 |
636 |
636 |
637 section {* Lifted Theorems *} |
637 section {* Lifted Theorems *} |
638 |
638 |
639 thm list.cases (* ??? *) |
639 thm list.cases (* ??? *) |
688 lemma "funion (funion x xa) xb = funion x (funion xa xb)" |
688 lemma "funion (funion x xa) xb = funion x (funion xa xb)" |
689 by (lifting append_assoc) |
689 by (lifting append_assoc) |
690 |
690 |
691 quotient_definition |
691 quotient_definition |
692 "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
692 "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
693 as |
693 is |
694 "list_case" |
694 "list_case" |
695 |
695 |
696 (* NOT SURE IF TRUE *) |
696 (* NOT SURE IF TRUE *) |
697 lemma list_case_rsp[quot_respect]: |
697 lemma list_case_rsp[quot_respect]: |
698 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
698 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |