133 shows "absf o repf = id" |
133 shows "absf o repf = id" |
134 apply(rule ext) |
134 apply(rule ext) |
135 apply(simp add: Quotient_abs_rep[OF a]) |
135 apply(simp add: Quotient_abs_rep[OF a]) |
136 done |
136 done |
137 |
137 |
138 lemma set_in_eq: "(\<forall>e. ((e \<in> A) = (e \<in> B))) \<equiv> A = B" |
138 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B" |
139 apply (rule eq_reflection) |
139 apply (rule eq_reflection) |
140 apply auto |
140 apply auto |
141 done |
141 done |
142 |
142 |
143 lemma map_rel_cong: "b \<approx>1 ba \<Longrightarrow> map f b \<approx>1 map f ba" |
143 lemma map_rel_cong: "b \<approx>1 ba \<Longrightarrow> map f b \<approx>1 map f ba" |
144 unfolding erel1_def |
144 unfolding erel1_def |
145 apply(simp only: set_map set_in_eq) |
145 apply(simp only: set_map set_in_eq) |
146 done |
146 done |
147 |
|
148 lemma quotient_compose_list_pre: |
|
149 "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s = |
|
150 ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and> |
|
151 (list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) s s \<and> |
|
152 abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" |
|
153 apply rule |
|
154 apply rule |
|
155 apply rule |
|
156 apply (rule list_rel_refl) |
|
157 apply (metis equivp_def fset_equivp) |
|
158 apply rule |
|
159 apply (rule equivp_reflp[OF fset_equivp]) |
|
160 apply (rule list_rel_refl) |
|
161 apply (metis equivp_def fset_equivp) |
|
162 apply(rule) |
|
163 apply rule |
|
164 apply (rule list_rel_refl) |
|
165 apply (metis equivp_def fset_equivp) |
|
166 apply rule |
|
167 apply (rule equivp_reflp[OF fset_equivp]) |
|
168 apply (rule list_rel_refl) |
|
169 apply (metis equivp_def fset_equivp) |
|
170 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s") |
|
171 apply (metis Quotient_rel[OF Quotient_fset]) |
|
172 apply (auto)[1] |
|
173 apply (subgoal_tac "map abs_fset r = map abs_fset b") |
|
174 prefer 2 |
|
175 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
|
176 apply (subgoal_tac "map abs_fset s = map abs_fset ba") |
|
177 prefer 2 |
|
178 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
|
179 apply (simp add: map_rel_cong) |
|
180 apply rule |
|
181 apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"]) |
|
182 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
|
183 apply (rule list_rel_refl) |
|
184 apply (metis equivp_def fset_equivp) |
|
185 apply rule |
|
186 prefer 2 |
|
187 apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"]) |
|
188 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
|
189 apply (rule list_rel_refl) |
|
190 apply (metis equivp_def fset_equivp) |
|
191 apply (erule conjE)+ |
|
192 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s") |
|
193 prefer 2 |
|
194 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp) |
|
195 apply (rule map_rel_cong) |
|
196 apply (assumption) |
|
197 done |
|
198 |
|
199 lemma quotient_compose_list: |
|
200 shows "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1)) |
|
201 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
|
202 unfolding Quotient_def comp_def |
|
203 apply (rule)+ |
|
204 apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset]) |
|
205 apply (rule) |
|
206 apply (rule) |
|
207 apply (rule) |
|
208 apply (rule list_rel_refl) |
|
209 apply (metis equivp_def fset_equivp) |
|
210 apply (rule) |
|
211 apply (rule equivp_reflp[OF fset_equivp]) |
|
212 apply (rule list_rel_refl) |
|
213 apply (metis equivp_def fset_equivp) |
|
214 apply rule |
|
215 apply rule |
|
216 apply(rule quotient_compose_list_pre) |
|
217 done |
|
218 |
147 |
219 lemma quotient_compose_list_gen_pre: |
148 lemma quotient_compose_list_gen_pre: |
220 assumes a: "equivp r2" |
149 assumes a: "equivp r2" |
221 and b: "Quotient r2 abs2 rep2" |
150 and b: "Quotient r2 abs2 rep2" |
222 shows "(list_rel r2 OO op \<approx>1 OO list_rel r2) r s = |
151 shows "(list_rel r2 OO op \<approx>1 OO list_rel r2) r s = |