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