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 (* Trying to use induction: *) |
138 lemma set_in_eq: "(\<forall>e. ((e \<in> A) = (e \<in> B))) \<equiv> A = B" |
139 lemma help1: "list_rel op \<approx>1 ba [] \<equiv> ba = []" |
139 apply (rule eq_reflection) |
140 apply(induct ba) |
140 apply auto |
141 apply (auto) |
141 done |
142 done |
142 |
143 lemma help2: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) (x # xs) [] \<equiv> False" |
143 lemma map_rep_ok: "b \<approx>1 ba \<Longrightarrow> map rep_fset b \<approx>1 map rep_fset ba" |
144 sorry |
144 unfolding erel1_def |
145 lemma help2a: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) [] (x # xs) \<equiv> False" |
145 apply(simp only: set_map set_in_eq) |
146 sorry |
146 done |
147 lemma help4: "abs_fset (a # b) = abs_fset [] \<equiv> False" |
147 |
148 sorry |
148 lemma map_abs_ok: "b \<approx>1 ba \<Longrightarrow> map abs_fset b \<approx>1 map abs_fset ba" |
149 lemma help4a: "abs_fset [] = abs_fset (a # b) \<equiv> False" |
149 unfolding erel1_def |
150 sorry |
150 apply(simp only: set_map set_in_eq) |
151 |
151 done |
152 lemma help5: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) x x" |
|
153 sorry |
|
154 |
|
155 lemma quotient_compose_list_pre_ind: |
|
156 "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s = |
|
157 ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and> |
|
158 (list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" |
|
159 apply(induct r s rule: list_induct2') |
|
160 apply(simp) |
|
161 apply(simp add: help2 help4 help5) |
|
162 apply(simp add: help2a help4a help5) |
|
163 apply(simp add: help5) |
|
164 apply rule |
|
165 apply (auto simp add: help2a help4a help5 help1 help2 help4 ) |
|
166 sorry |
|
167 |
|
168 (* Trying to solve it directly: *) |
|
169 |
152 |
170 lemma quotient_compose_list_pre: |
153 lemma quotient_compose_list_pre: |
171 "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s = |
154 "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s = |
172 ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and> |
155 ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and> |
173 (list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" |
156 (list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" |
195 prefer 2 |
178 prefer 2 |
196 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
179 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
197 apply (subgoal_tac "map abs_fset s = map abs_fset ba") |
180 apply (subgoal_tac "map abs_fset s = map abs_fset ba") |
198 prefer 2 |
181 prefer 2 |
199 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
182 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
200 apply simp |
183 apply (simp add: map_abs_ok) |
201 (* To solve first subgoal we just need: *) |
|
202 (* b \<approx> ba \<Longrightarrow> mapabs b \<approx> mapabs ba *) |
|
203 prefer 2 |
|
204 apply rule |
184 apply rule |
205 apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"]) |
185 apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"]) |
206 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
186 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
207 apply (rule list_rel_refl) |
187 apply (rule list_rel_refl) |
208 apply (metis equivp_def fset_equivp) |
188 apply (metis equivp_def fset_equivp) |
214 apply (metis equivp_def fset_equivp) |
194 apply (metis equivp_def fset_equivp) |
215 apply (erule conjE)+ |
195 apply (erule conjE)+ |
216 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s") |
196 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s") |
217 prefer 2 |
197 prefer 2 |
218 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp) |
198 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp) |
219 (* To solve this subgoal we just need: *) |
199 apply (rule map_rep_ok) |
220 (* x \<approx> y \<Longrightarrow> maprep x \<approx> maprep y *) |
200 apply (assumption) |
221 sorry |
201 done |
222 |
202 |
223 lemma quotient_compose_list: |
203 lemma quotient_compose_list: |
224 shows "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1)) |
204 shows "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1)) |
225 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
205 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
226 unfolding Quotient_def comp_def |
206 unfolding Quotient_def comp_def |
238 apply rule |
218 apply rule |
239 apply rule |
219 apply rule |
240 apply(rule quotient_compose_list_pre) |
220 apply(rule quotient_compose_list_pre) |
241 done |
221 done |
242 |
222 |
243 lemma quotient_compose_ok: |
223 lemma quotient_compose_list_gen: |
244 assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset" |
224 assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset" |
245 and a2: "Quotient r2 abs2 rep2" |
225 and a2: "Quotient r2 abs2 rep2" "equivp r2" |
246 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) |
226 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) |
247 (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
227 (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
248 unfolding Quotient_def comp_def |
228 unfolding Quotient_def comp_def |
249 apply (rule)+ |
229 apply (rule)+ |
250 apply (simp add: abs_o_rep[OF a2] id_simps Quotient_abs_rep[OF Quotient_fset]) |
230 apply (simp add: abs_o_rep[OF a2(1)] id_simps Quotient_abs_rep[OF Quotient_fset]) |
251 apply (rule) |
231 apply (rule) |
252 apply (rule) |
232 apply (rule) |
253 using a1 |
233 apply (rule) |
254 apply - |
234 apply (rule list_rel_refl) |
255 sorry |
235 apply (metis a2(2) equivp_def) |
|
236 apply (rule) |
|
237 apply (rule equivp_reflp[OF fset_equivp]) |
|
238 apply (rule list_rel_refl) |
|
239 apply (metis a2(2) equivp_def) |
|
240 apply rule |
|
241 apply rule |
|
242 apply(rule quotient_compose_list_gen_pre) |
|
243 done |
256 |
244 |
257 (* This is the general statement but the types are wrong as in following exanples *) |
245 (* This is the general statement but the types are wrong as in following exanples *) |
258 lemma quotient_compose_general: |
246 lemma quotient_compose_general: |
259 assumes a2: "Quotient r1 abs1 rep_fset" |
247 assumes a2: "Quotient r1 abs1 rep_fset" |
260 and "Quotient r2 abs2 rep2" |
248 and "Quotient r2 abs2 rep2" |