293 lemma map_append : |
291 lemma map_append : |
294 "(map f (a @ b)) \<approx> |
292 "(map f (a @ b)) \<approx> |
295 (map f a) @ (map f b)" |
293 (map f a) @ (map f b)" |
296 by simp (rule list_eq_refl) |
294 by simp (rule list_eq_refl) |
297 |
295 |
|
296 lemma op_eq_twice: "(op = ===> op =) = (op =)" |
|
297 apply (rule ext) |
|
298 apply (rule ext) |
|
299 apply (simp add: FUN_REL.simps) |
|
300 apply auto |
|
301 apply (rule ext) |
|
302 apply simp |
|
303 done |
|
304 |
|
305 |
|
306 |
|
307 lemma ho_fold_rsp: |
|
308 "((op = ===> op = ===> op =) ===> (op = ===> op =) ===> op = ===> op \<approx> ===> op =) fold1 fold1" |
|
309 apply (auto simp add: op_eq_twice) |
|
310 sorry |
298 |
311 |
299 print_quotients |
312 print_quotients |
300 |
313 |
301 |
314 |
302 ML {* val qty = @{typ "'a fset"} *} |
315 ML {* val qty = @{typ "'a fset"} *} |
303 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
|
304 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
|
305 |
|
306 ML {* val rsp_thms = |
316 ML {* val rsp_thms = |
307 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} |
317 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} |
308 @ @{thms ho_all_prs ho_ex_prs} *} |
318 @ @{thms ho_all_prs ho_ex_prs} *} |
309 |
319 |
310 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
320 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
311 |
321 |
312 (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *) |
322 (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *) |
|
323 |
|
324 |
|
325 |
313 ML {* lift_thm_fset @{context} @{thm m1} *} |
326 ML {* lift_thm_fset @{context} @{thm m1} *} |
314 ML {* lift_thm_fset @{context} @{thm m2} *} |
327 ML {* lift_thm_fset @{context} @{thm m2} *} |
315 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
328 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
316 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
329 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
317 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
330 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
318 (*ML {* lift_thm_fset @{context} @{thm map_append} *}*) |
331 (*ML {* lift_thm_fset @{context} @{thm map_append} *}*) |
319 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
332 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
320 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
333 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
321 |
334 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *} |
322 thm fold1.simps(2) |
335 |
|
336 term list_rec |
|
337 |
|
338 quotient_def |
|
339 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'b" |
|
340 where |
|
341 "fset_rec \<equiv> list_rec" |
|
342 |
323 thm list.recs(2) |
343 thm list.recs(2) |
324 thm list.cases |
344 thm list.cases |
325 |
345 |
326 ML {* val ind_r_a = atomize_thm @{thm list.induct} *} |
346 |
|
347 |
|
348 |
|
349 |
|
350 |
|
351 ML {* val consts = lookup_quot_consts defs *} |
|
352 ML {* val defs_sym = add_lower_defs @{context} defs *} |
|
353 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
|
354 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
|
355 |
|
356 |
|
357 ML {* val ind_r_a = atomize_thm @{thm card1_suc} *} |
327 (* prove {* build_regularize_goal ind_r_a rty rel @{context} *} |
358 (* prove {* build_regularize_goal ind_r_a rty rel @{context} *} |
328 ML_prf {* fun tac ctxt = |
359 ML_prf {* fun tac ctxt = |
329 (FIRST' [ |
360 (FIRST' [ |
330 rtac rel_refl, |
361 rtac rel_refl, |
331 atac, |
362 atac, |
339 ]); |
370 ]); |
340 *} |
371 *} |
341 apply (atomize(full)) |
372 apply (atomize(full)) |
342 apply (tactic {* tac @{context} 1 *}) *) |
373 apply (tactic {* tac @{context} 1 *}) *) |
343 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *} |
374 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *} |
344 (*ML {* |
375 ML {* |
345 val rt = build_repabs_term @{context} ind_r_r consts rty qty |
376 val rt = build_repabs_term @{context} ind_r_r consts rty qty |
346 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
377 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
347 *} |
378 *} |
348 prove rg |
379 prove rg |
349 apply(atomize(full)) |
380 apply(atomize(full)) |
350 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
381 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
351 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
382 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
352 done*) |
383 done |
353 ML {* val ind_r_t = |
384 ML {* val ind_r_t = |
354 Toplevel.program (fn () => |
385 Toplevel.program (fn () => |
355 repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms |
386 repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms |
356 ) |
387 ) |
357 *} |
388 *} |