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_type fset = "'a list" / "list_eq" |
24 quotient_type fset = "'a list" / "list_eq" |
25 by (rule equivp_list_eq) |
25 by (rule equivp_list_eq) |
26 |
26 |
27 quotient_def |
27 quotient_definition |
28 "fempty :: 'a fset" ("{||}") |
28 "fempty :: 'a fset" ("{||}") |
29 as |
29 as |
30 "[]" |
30 "[]" |
31 |
31 |
32 quotient_def |
32 quotient_definition |
33 "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
33 "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
34 as |
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_definition |
42 "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 as |
43 as |
44 "(op @)" |
44 "(op @)" |
45 |
45 |
46 lemma append_rsp_aux1: |
46 lemma append_rsp_aux1: |
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_definition |
69 "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 as |
70 as |
71 "(op mem)" |
71 "(op mem)" |
72 |
72 |
73 lemma memb_rsp_aux: |
73 lemma memb_rsp_aux: |
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_definition |
93 "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 as |
94 as |
95 "inter_list" |
95 "inter_list" |
96 |
96 |
97 no_syntax |
97 no_syntax |