equal
deleted
inserted
replaced
25 'a fset = "'a list" / "list_eq" |
25 'a fset = "'a list" / "list_eq" |
26 by (rule equivp_list_eq) |
26 by (rule equivp_list_eq) |
27 |
27 |
28 quotient_definition |
28 quotient_definition |
29 "fempty :: 'a fset" ("{||}") |
29 "fempty :: 'a fset" ("{||}") |
30 as |
30 is |
31 "[]" |
31 "[]" |
32 |
32 |
33 quotient_definition |
33 quotient_definition |
34 "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
34 "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
35 as |
35 is |
36 "(op #)" |
36 "(op #)" |
37 |
37 |
38 lemma finsert_rsp[quot_respect]: |
38 lemma finsert_rsp[quot_respect]: |
39 shows "(op = ===> op \<approx> ===> op \<approx>) (op #) (op #)" |
39 shows "(op = ===> op \<approx> ===> op \<approx>) (op #) (op #)" |
40 by (auto intro: list_eq.intros) |
40 by (auto intro: list_eq.intros) |
41 |
41 |
42 quotient_definition |
42 quotient_definition |
43 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65) |
43 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65) |
44 as |
44 is |
45 "(op @)" |
45 "(op @)" |
46 |
46 |
47 lemma append_rsp_aux1: |
47 lemma append_rsp_aux1: |
48 assumes a : "l2 \<approx> r2 " |
48 assumes a : "l2 \<approx> r2 " |
49 shows "(h @ l2) \<approx> (h @ r2)" |
49 shows "(h @ l2) \<approx> (h @ r2)" |
66 by (auto simp add: append_rsp_aux2) |
66 by (auto simp add: append_rsp_aux2) |
67 |
67 |
68 |
68 |
69 quotient_definition |
69 quotient_definition |
70 "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50) |
70 "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50) |
71 as |
71 is |
72 "(op mem)" |
72 "(op mem)" |
73 |
73 |
74 lemma memb_rsp_aux: |
74 lemma memb_rsp_aux: |
75 assumes a: "x \<approx> y" |
75 assumes a: "x \<approx> y" |
76 shows "(z mem x) = (z mem y)" |
76 shows "(z mem x) = (z mem y)" |
90 where |
90 where |
91 "inter_list X Y \<equiv> [x \<leftarrow> X. x\<in>set Y]" |
91 "inter_list X Y \<equiv> [x \<leftarrow> X. x\<in>set Y]" |
92 |
92 |
93 quotient_definition |
93 quotient_definition |
94 "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70) |
94 "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70) |
95 as |
95 is |
96 "inter_list" |
96 "inter_list" |
97 |
97 |
98 no_syntax |
98 no_syntax |
99 "@Finset" :: "args => 'a fset" ("{|(_)|}") |
99 "@Finset" :: "args => 'a fset" ("{|(_)|}") |
100 syntax |
100 syntax |