117 test_funs absF @{context} |
117 test_funs absF @{context} |
118 (@{typ "('a list) list \<Rightarrow> 'a list"}, |
118 (@{typ "('a list) list \<Rightarrow> 'a list"}, |
119 @{typ "('a fset) fset \<Rightarrow> 'a fset"}) |
119 @{typ "('a fset) fset \<Rightarrow> 'a fset"}) |
120 *} |
120 *} |
121 |
121 |
122 lemma |
122 lemma OO_sym_inv: |
123 assumes sr: "symp r" |
123 assumes sr: "symp r" |
124 and ss: "symp s" |
124 and ss: "symp s" |
125 shows "(r OO s) x y = (s OO r) y x" |
125 shows "(r OO s) x y = (s OO r) y x" |
126 using sr ss |
126 using sr ss |
127 unfolding symp_def |
127 unfolding symp_def |
128 apply (metis pred_comp.intros pred_compE ss symp_def) |
128 apply (metis pred_comp.intros pred_compE ss symp_def) |
129 done |
129 done |
130 |
130 |
131 lemma abs_o_rep: |
131 lemma abs_o_rep: |
132 assumes a: "Quotient r absf repf" |
132 assumes a: "Quotient r absf repf" |
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) = (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_rep_ok: "b \<approx>1 ba \<Longrightarrow> map rep_fset b \<approx>1 map rep_fset 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 map_rep_ok_gen: "b \<approx>1 ba \<Longrightarrow> map rep2 b \<approx>1 map rep2 ba" |
|
149 unfolding erel1_def |
|
150 apply(simp only: set_map set_in_eq) |
|
151 done |
|
152 |
|
153 lemma map_abs_ok: "b \<approx>1 ba \<Longrightarrow> map abs_fset b \<approx>1 map abs_fset ba" |
|
154 unfolding erel1_def |
|
155 apply(simp only: set_map set_in_eq) |
|
156 done |
|
157 |
|
158 lemma map_abs_ok_gen: "b \<approx>1 ba \<Longrightarrow> map abs2 b \<approx>1 map abs2 ba" |
|
159 unfolding erel1_def |
|
160 apply(simp only: set_map set_in_eq) |
|
161 done |
|
162 |
147 |
163 lemma quotient_compose_list_pre: |
148 lemma quotient_compose_list_pre: |
164 "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s = |
149 "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s = |
165 ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and> |
150 ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and> |
166 (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))" |
151 (list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) s s \<and> |
167 apply rule |
152 abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" |
168 apply rule |
153 apply rule |
169 apply rule |
154 apply rule |
170 apply (rule list_rel_refl) |
155 apply rule |
171 apply (metis equivp_def fset_equivp) |
156 apply (rule list_rel_refl) |
172 apply rule |
157 apply (metis equivp_def fset_equivp) |
173 apply (rule equivp_reflp[OF fset_equivp]) |
158 apply rule |
174 apply (rule list_rel_refl) |
159 apply (rule equivp_reflp[OF fset_equivp]) |
175 apply (metis equivp_def fset_equivp) |
160 apply (rule list_rel_refl) |
176 apply(rule) |
161 apply (metis equivp_def fset_equivp) |
177 apply rule |
162 apply(rule) |
178 apply (rule list_rel_refl) |
163 apply rule |
179 apply (metis equivp_def fset_equivp) |
164 apply (rule list_rel_refl) |
180 apply rule |
165 apply (metis equivp_def fset_equivp) |
181 apply (rule equivp_reflp[OF fset_equivp]) |
166 apply rule |
182 apply (rule list_rel_refl) |
167 apply (rule equivp_reflp[OF fset_equivp]) |
183 apply (metis equivp_def fset_equivp) |
168 apply (rule list_rel_refl) |
184 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s") |
169 apply (metis equivp_def fset_equivp) |
185 apply (metis Quotient_rel[OF Quotient_fset]) |
170 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s") |
186 apply (auto)[1] |
171 apply (metis Quotient_rel[OF Quotient_fset]) |
187 apply (subgoal_tac "map abs_fset r = map abs_fset b") |
172 apply (auto)[1] |
188 prefer 2 |
173 apply (subgoal_tac "map abs_fset r = map abs_fset b") |
189 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
174 prefer 2 |
190 apply (subgoal_tac "map abs_fset s = map abs_fset ba") |
175 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
191 prefer 2 |
176 apply (subgoal_tac "map abs_fset s = map abs_fset ba") |
192 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
177 prefer 2 |
193 apply (simp add: map_abs_ok) |
178 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
194 apply rule |
179 apply (simp add: map_rel_cong) |
195 apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"]) |
180 apply rule |
196 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
181 apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"]) |
197 apply (rule list_rel_refl) |
182 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
198 apply (metis equivp_def fset_equivp) |
183 apply (rule list_rel_refl) |
199 apply rule |
184 apply (metis equivp_def fset_equivp) |
200 prefer 2 |
185 apply rule |
201 apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"]) |
186 prefer 2 |
202 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
187 apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"]) |
203 apply (rule list_rel_refl) |
188 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
204 apply (metis equivp_def fset_equivp) |
189 apply (rule list_rel_refl) |
205 apply (erule conjE)+ |
190 apply (metis equivp_def fset_equivp) |
206 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s") |
191 apply (erule conjE)+ |
207 prefer 2 |
192 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s") |
208 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp) |
193 prefer 2 |
209 apply (rule map_rep_ok) |
194 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp) |
210 apply (assumption) |
195 apply (rule map_rel_cong) |
211 done |
196 apply (assumption) |
|
197 done |
212 |
198 |
213 lemma quotient_compose_list: |
199 lemma quotient_compose_list: |
214 shows "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1)) |
200 shows "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1)) |
215 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
201 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
216 unfolding Quotient_def comp_def |
202 unfolding Quotient_def comp_def |
217 apply (rule)+ |
203 apply (rule)+ |
218 apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset]) |
204 apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset]) |
219 apply (rule) |
205 apply (rule) |
220 apply (rule) |
206 apply (rule) |
221 apply (rule) |
207 apply (rule) |
222 apply (rule list_rel_refl) |
208 apply (rule list_rel_refl) |
223 apply (metis equivp_def fset_equivp) |
209 apply (metis equivp_def fset_equivp) |
224 apply (rule) |
210 apply (rule) |
225 apply (rule equivp_reflp[OF fset_equivp]) |
211 apply (rule equivp_reflp[OF fset_equivp]) |
226 apply (rule list_rel_refl) |
212 apply (rule list_rel_refl) |
227 apply (metis equivp_def fset_equivp) |
213 apply (metis equivp_def fset_equivp) |
228 apply rule |
214 apply rule |
229 apply rule |
215 apply rule |
230 apply(rule quotient_compose_list_pre) |
216 apply(rule quotient_compose_list_pre) |
231 done |
217 done |
232 |
218 |
233 lemma quotient_compose_list_gen_pre: |
219 lemma quotient_compose_list_gen_pre: |
234 assumes a: "equivp r2" |
220 assumes a: "equivp r2" |
235 and b: "Quotient r2 abs2 rep2" |
221 and b: "Quotient r2 abs2 rep2" |
236 shows "(list_rel r2 OO op \<approx>1 OO list_rel r2) r s = |
222 shows "(list_rel r2 OO op \<approx>1 OO list_rel r2) r s = |
237 ((list_rel r2 OO op \<approx>1 OO list_rel r2) r r \<and> |
223 ((list_rel r2 OO op \<approx>1 OO list_rel r2) r r \<and> |
238 (list_rel r2 OO op \<approx>1 OO list_rel r2) s s \<and> |
224 (list_rel r2 OO op \<approx>1 OO list_rel r2) s s \<and> |
239 abs_fset (map abs2 r) = abs_fset (map abs2 s))" |
225 abs_fset (map abs2 r) = abs_fset (map abs2 s))" |
240 apply rule |
226 apply rule |
241 apply rule |
227 apply rule |
242 apply rule |
228 apply rule |
243 apply (rule list_rel_refl) |
229 apply (rule list_rel_refl) |
244 apply (metis equivp_def a) |
230 apply (metis equivp_def a) |
245 apply rule |
231 apply rule |
246 apply (rule equivp_reflp[OF fset_equivp]) |
232 apply (rule equivp_reflp[OF fset_equivp]) |
247 apply (rule list_rel_refl) |
233 apply (rule list_rel_refl) |
248 apply (metis equivp_def a) |
234 apply (metis equivp_def a) |
249 apply(rule) |
235 apply(rule) |
250 apply rule |
236 apply rule |
251 apply (rule list_rel_refl) |
237 apply (rule list_rel_refl) |
252 apply (metis equivp_def a) |
238 apply (metis equivp_def a) |
253 apply rule |
239 apply rule |
254 apply (rule equivp_reflp[OF fset_equivp]) |
240 apply (rule equivp_reflp[OF fset_equivp]) |
255 apply (rule list_rel_refl) |
241 apply (rule list_rel_refl) |
256 apply (metis equivp_def a) |
242 apply (metis equivp_def a) |
257 apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s") |
243 apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s") |
258 apply (metis Quotient_rel[OF Quotient_fset]) |
244 apply (metis Quotient_rel[OF Quotient_fset]) |
259 apply (auto)[1] |
245 apply (auto)[1] |
260 apply (subgoal_tac "map abs2 r = map abs2 b") |
246 apply (subgoal_tac "map abs2 r = map abs2 b") |
261 prefer 2 |
247 prefer 2 |
262 apply (metis Quotient_rel[OF list_quotient[OF b]]) |
248 apply (metis Quotient_rel[OF list_quotient[OF b]]) |
263 apply (subgoal_tac "map abs2 s = map abs2 ba") |
249 apply (subgoal_tac "map abs2 s = map abs2 ba") |
264 prefer 2 |
250 prefer 2 |
265 apply (metis Quotient_rel[OF list_quotient[OF b]]) |
251 apply (metis Quotient_rel[OF list_quotient[OF b]]) |
266 apply (simp add: map_abs_ok_gen) |
252 apply (simp add: map_rel_cong) |
267 apply rule |
253 apply rule |
268 apply (rule rep_abs_rsp[of "list_rel r2" "map abs2"]) |
254 apply (rule rep_abs_rsp[of "list_rel r2" "map abs2"]) |
269 apply (rule list_quotient) |
255 apply (rule list_quotient) |
270 apply (rule b) |
256 apply (rule b) |
271 apply (rule list_rel_refl) |
257 apply (rule list_rel_refl) |
272 apply (metis equivp_def a) |
258 apply (metis equivp_def a) |
273 apply rule |
259 apply rule |
274 prefer 2 |
260 prefer 2 |
275 apply (rule rep_abs_rsp_left[of "list_rel r2" "map abs2"]) |
261 apply (rule rep_abs_rsp_left[of "list_rel r2" "map abs2"]) |
276 apply (rule list_quotient) |
262 apply (rule list_quotient) |
277 apply (rule b) |
263 apply (rule b) |
278 apply (rule list_rel_refl) |
264 apply (rule list_rel_refl) |
279 apply (metis equivp_def a) |
265 apply (metis equivp_def a) |
280 apply (erule conjE)+ |
266 apply (erule conjE)+ |
281 apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s") |
267 apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s") |
282 apply (rule map_rep_ok_gen) |
268 apply (rule map_rel_cong) |
283 apply (assumption) |
269 apply (assumption) |
284 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp a b) |
270 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp a b) |
285 done |
271 done |
286 |
272 |
287 lemma quotient_compose_list_gen: |
273 lemma quotient_compose_list_gen: |
288 assumes a: "Quotient r2 abs2 rep2" |
274 assumes a: "Quotient r2 abs2 rep2" |
289 and b: "equivp r2" (* reflp should be enough... *) |
275 and b: "equivp r2" (* reflp should be enough... *) |
290 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) |
276 shows "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) |
291 (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
277 (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
292 unfolding Quotient_def comp_def |
278 unfolding Quotient_def comp_def |
293 apply (rule)+ |
279 apply (rule)+ |
294 apply (simp add: abs_o_rep[OF a] id_simps Quotient_abs_rep[OF Quotient_fset]) |
280 apply (simp add: abs_o_rep[OF a] id_simps Quotient_abs_rep[OF Quotient_fset]) |
295 apply (rule) |
281 apply (rule) |
296 apply (rule) |
282 apply (rule) |
297 apply (rule) |
283 apply (rule) |
298 apply (rule list_rel_refl) |
284 apply (rule list_rel_refl) |
299 apply (metis b equivp_def) |
285 apply (metis b equivp_def) |
300 apply (rule) |
286 apply (rule) |
301 apply (rule equivp_reflp[OF fset_equivp]) |
287 apply (rule equivp_reflp[OF fset_equivp]) |
302 apply (rule list_rel_refl) |
288 apply (rule list_rel_refl) |
303 apply (metis b equivp_def) |
289 apply (metis b equivp_def) |
304 apply rule |
290 apply rule |
305 apply rule |
291 apply rule |
306 apply(rule quotient_compose_list_gen_pre[OF b a]) |
292 apply(rule quotient_compose_list_gen_pre[OF b a]) |
307 done |
293 done |
308 |
294 |
309 (* This is the general statement but the types of abs2 and rep2 |
295 (* This is the general statement but the types of abs2 and rep2 |
310 are wrong as can be seen in following exanples *) |
296 are wrong as can be seen in following exanples *) |
311 |
|
312 lemma quotient_compose_general: |
297 lemma quotient_compose_general: |
313 assumes a2: "Quotient r1 abs1 rep1" |
298 assumes a2: "Quotient r1 abs1 rep1" |
314 and "Quotient r2 abs2 rep2" |
299 and "Quotient r2 abs2 rep2" |
315 shows "Quotient ((list_rel r2) OO r1 OO (list_rel r2)) |
300 shows "Quotient ((list_rel r2) OO r1 OO (list_rel r2)) |
316 (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep1)" |
301 (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep1)" |
317 sorry |
302 sorry |
318 |
303 |
319 thm quotient_compose_ok [OF Quotient_fset] |
304 thm quotient_compose_list_gen[OF Quotient_fset fset_equivp] |
320 thm quotient_compose_general[OF Quotient_fset] |
305 thm quotient_compose_general[OF Quotient_fset] |
321 |
|
322 thm quotient_compose_ok [OF Quotient_fset Quotient_fset] |
|
323 (* Doesn't work: *) |
306 (* Doesn't work: *) |
324 (* thm quotient_compose_general[OF Quotient_fset Quotient_fset] *) |
307 (* thm quotient_compose_general[OF Quotient_fset Quotient_fset] *) |
325 |
308 |
326 end |
309 end |