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 help1: "list_rel op \<approx>1 ba [] \<equiv> ba = []" |
139 lemma help1: "list_rel op \<approx>1 ba [] \<equiv> ba = []" |
139 apply(induct ba) |
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 help2: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) (x # xs) [] \<equiv> False" |
144 sorry |
144 sorry |
145 lemma help2a: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) [] (x # xs) \<equiv> False" |
145 lemma help2a: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) [] (x # xs) \<equiv> False" |
146 sorry |
146 sorry |
147 |
|
148 (* not used anymore *) |
|
149 lemma help3: "list_rel op \<approx>1 [] b \<equiv> b = []" |
|
150 apply (induct b) |
|
151 apply auto |
|
152 done |
|
153 |
|
154 lemma help4: "abs_fset (a # b) = abs_fset [] \<equiv> False" |
147 lemma help4: "abs_fset (a # b) = abs_fset [] \<equiv> False" |
155 sorry |
148 sorry |
156 lemma help4a: "abs_fset [] = abs_fset (a # b) \<equiv> False" |
149 lemma help4a: "abs_fset [] = abs_fset (a # b) \<equiv> False" |
157 sorry |
150 sorry |
158 |
151 |
159 lemma help5: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) x x" |
152 lemma help5: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) x x" |
160 sorry |
153 sorry |
161 |
154 |
162 lemma bla0pre: |
155 lemma quotient_compose_list_pre_ind: |
163 "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s = |
156 "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s = |
164 ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and> |
157 ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and> |
165 (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))" |
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))" |
166 apply(induct r s rule: list_induct2') |
159 apply(induct r s rule: list_induct2') |
167 apply(simp) |
160 apply(simp) |
170 apply(simp add: help5) |
163 apply(simp add: help5) |
171 apply rule |
164 apply rule |
172 apply (auto simp add: help2a help4a help5 help1 help2 help4 ) |
165 apply (auto simp add: help2a help4a help5 help1 help2 help4 ) |
173 sorry |
166 sorry |
174 |
167 |
175 lemma bla0: |
168 (* Trying to solve it directly: *) |
176 shows "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1)) |
169 |
|
170 lemma quotient_compose_list_pre: |
|
171 "(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> |
|
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))" |
|
174 apply rule |
|
175 apply rule |
|
176 apply rule |
|
177 apply (rule list_rel_refl) |
|
178 apply (metis equivp_def fset_equivp) |
|
179 apply rule |
|
180 apply (rule equivp_reflp[OF fset_equivp]) |
|
181 apply (rule list_rel_refl) |
|
182 apply (metis equivp_def fset_equivp) |
|
183 apply(rule) |
|
184 apply rule |
|
185 apply (rule list_rel_refl) |
|
186 apply (metis equivp_def fset_equivp) |
|
187 apply rule |
|
188 apply (rule equivp_reflp[OF fset_equivp]) |
|
189 apply (rule list_rel_refl) |
|
190 apply (metis equivp_def fset_equivp) |
|
191 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s") |
|
192 apply (metis Quotient_rel[OF Quotient_fset]) |
|
193 prefer 2 |
|
194 apply rule |
|
195 apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"]) |
|
196 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
|
197 apply (rule list_rel_refl) |
|
198 apply (metis equivp_def fset_equivp) |
|
199 apply rule |
|
200 prefer 2 |
|
201 apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"]) |
|
202 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
|
203 apply (rule list_rel_refl) |
|
204 apply (metis equivp_def fset_equivp) |
|
205 sorry |
|
206 |
|
207 lemma quotient_compose_list: |
|
208 shows "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1)) |
177 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
209 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
178 unfolding Quotient_def comp_def |
210 unfolding Quotient_def comp_def |
179 apply (rule)+ |
211 apply (rule)+ |
180 apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset]) |
212 apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset]) |
181 apply (rule) |
213 apply (rule) |
187 apply (rule equivp_reflp[OF fset_equivp]) |
219 apply (rule equivp_reflp[OF fset_equivp]) |
188 apply (rule list_rel_refl) |
220 apply (rule list_rel_refl) |
189 apply (metis equivp_def fset_equivp) |
221 apply (metis equivp_def fset_equivp) |
190 apply rule |
222 apply rule |
191 apply rule |
223 apply rule |
192 apply(rule bla0pre) |
224 apply(rule quotient_compose_list_pre) |
193 done |
225 done |
194 |
226 |
195 lemma bla0pre2: |
227 lemma quotient_compose_ok: |
196 "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s = |
|
197 ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and> |
|
198 (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))" |
|
199 apply rule |
|
200 apply rule |
|
201 apply rule |
|
202 apply (rule list_rel_refl) |
|
203 apply (metis equivp_def fset_equivp) |
|
204 apply rule |
|
205 apply (rule equivp_reflp[OF fset_equivp]) |
|
206 apply (rule list_rel_refl) |
|
207 apply (metis equivp_def fset_equivp) |
|
208 apply(rule) |
|
209 apply rule |
|
210 apply (rule list_rel_refl) |
|
211 apply (metis equivp_def fset_equivp) |
|
212 apply rule |
|
213 apply (rule equivp_reflp[OF fset_equivp]) |
|
214 apply (rule list_rel_refl) |
|
215 apply (metis equivp_def fset_equivp) |
|
216 thm pred_comp_def |
|
217 term "op OO" |
|
218 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s") |
|
219 apply (metis Quotient_rel[OF Quotient_fset]) |
|
220 prefer 2 |
|
221 apply rule |
|
222 thm rep_abs_rsp |
|
223 thm rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"] |
|
224 apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"]) |
|
225 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
|
226 apply (rule list_rel_refl) |
|
227 apply (metis equivp_def fset_equivp) |
|
228 apply rule |
|
229 prefer 2 |
|
230 apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"]) |
|
231 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
|
232 apply (rule list_rel_refl) |
|
233 apply (metis equivp_def fset_equivp) |
|
234 sorry |
|
235 |
|
236 lemma bla: |
|
237 assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset" |
228 assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset" |
238 and a2: "Quotient r2 abs2 rep2" |
229 and a2: "Quotient r2 abs2 rep2" |
239 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) |
230 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) |
240 (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
231 (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
241 unfolding Quotient_def comp_def |
232 unfolding Quotient_def comp_def |
242 apply (rule)+ |
233 apply (rule)+ |
243 apply (simp add: abs_o_rep[OF a2] id_simps Quotient_abs_rep[OF Quotient_fset]) |
234 apply (simp add: abs_o_rep[OF a2] id_simps Quotient_abs_rep[OF Quotient_fset]) |
244 apply (rule) |
235 apply (rule) |
245 apply (rule) |
236 apply (rule) |
246 using a1 |
237 using a1 |
247 apply - |
238 apply - |
248 sorry |
239 sorry |
249 |
240 |
250 lemma bla2: |
241 (* This is the general statement but the types are wrong as in following exanples *) |
|
242 lemma quotient_compose_general: |
251 assumes a2: "Quotient r1 abs1 rep_fset" |
243 assumes a2: "Quotient r1 abs1 rep_fset" |
252 and "Quotient r2 abs2 rep2" |
244 and "Quotient r2 abs2 rep2" |
253 shows "Quotient ((list_rel r2) OO r1 OO (list_rel r2)) (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
245 shows "Quotient ((list_rel r2) OO r1 OO (list_rel r2)) |
254 sorry |
246 (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
255 |
247 sorry |
256 thm bla [OF Quotient_fset] |
248 |
257 thm bla2[OF Quotient_fset] |
249 thm quotient_compose_ok [OF Quotient_fset] |
258 |
250 thm quotient_compose_general[OF Quotient_fset] |
259 thm bla [OF Quotient_fset Quotient_fset] |
251 |
|
252 thm quotient_compose_ok [OF Quotient_fset Quotient_fset] |
260 (* Doesn't work: *) |
253 (* Doesn't work: *) |
261 (* thm bla2[OF Quotient_fset Quotient_fset] *) |
254 (* thm quotient_compose_general[OF Quotient_fset Quotient_fset] *) |
262 |
255 |
263 end |
256 end |