equal
deleted
inserted
replaced
188 apply (rule equivp_reflp[OF fset_equivp]) |
188 apply (rule equivp_reflp[OF fset_equivp]) |
189 apply (rule list_rel_refl) |
189 apply (rule list_rel_refl) |
190 apply (metis equivp_def fset_equivp) |
190 apply (metis equivp_def fset_equivp) |
191 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s") |
191 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s") |
192 apply (metis Quotient_rel[OF Quotient_fset]) |
192 apply (metis Quotient_rel[OF Quotient_fset]) |
|
193 apply (auto)[1] |
|
194 apply (subgoal_tac "map abs_fset r = map abs_fset b") |
|
195 prefer 2 |
|
196 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
|
197 apply (subgoal_tac "map abs_fset s = map abs_fset ba") |
|
198 prefer 2 |
|
199 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
|
200 apply simp |
|
201 (* To solve first subgoal we just need: *) |
|
202 (* b \<approx> ba \<Longrightarrow> mapabs b \<approx> mapabs ba *) |
193 prefer 2 |
203 prefer 2 |
194 apply rule |
204 apply rule |
195 apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"]) |
205 apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"]) |
196 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
206 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
197 apply (rule list_rel_refl) |
207 apply (rule list_rel_refl) |
200 prefer 2 |
210 prefer 2 |
201 apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"]) |
211 apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"]) |
202 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
212 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
203 apply (rule list_rel_refl) |
213 apply (rule list_rel_refl) |
204 apply (metis equivp_def fset_equivp) |
214 apply (metis equivp_def fset_equivp) |
|
215 apply (erule conjE)+ |
|
216 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s") |
|
217 prefer 2 |
|
218 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp) |
|
219 (* To solve this subgoal we just need: *) |
|
220 (* x \<approx> y \<Longrightarrow> maprep x \<approx> maprep y *) |
205 sorry |
221 sorry |
206 |
222 |
207 lemma quotient_compose_list: |
223 lemma quotient_compose_list: |
208 shows "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1)) |
224 shows "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1)) |
209 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
225 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |