301 ML {* val qty = @{typ "'a fset"} *} |
299 ML {* val qty = @{typ "'a fset"} *} |
302 ML {* val rsp_thms = |
300 ML {* val rsp_thms = |
303 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} |
301 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} |
304 @ @{thms ho_all_prs ho_ex_prs} *} |
302 @ @{thms ho_all_prs ho_ex_prs} *} |
305 |
303 |
306 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
|
307 ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *} |
|
308 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
304 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
309 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
305 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
310 ML {* val consts = lookup_quot_consts defs *} |
306 ML {* val consts = lookup_quot_consts defs *} |
311 ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} |
307 ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} |
312 |
308 |
376 apply (auto simp add: FUN_REL_EQ) |
372 apply (auto simp add: FUN_REL_EQ) |
377 sorry |
373 sorry |
378 |
374 |
379 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
375 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
380 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} |
376 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} |
381 |
|
382 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
|
383 ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *} |
|
384 ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} |
377 ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} |
385 |
378 |
386 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.recs(2)})) *} |
379 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.recs(2)})) *} |
387 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
380 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
388 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
381 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
415 apply (rule b) |
405 apply (rule b) |
416 apply (assumption) |
406 apply (assumption) |
417 done |
407 done |
418 |
408 |
419 |
409 |
|
410 ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
|
411 |
|
412 |
420 |
413 |
421 (* Construction site starts here *) |
414 (* Construction site starts here *) |
422 |
415 lemma "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
423 |
416 apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *}) |
424 ML {* val consts = lookup_quot_consts defs *} |
417 apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
425 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
|
426 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
|
427 |
|
428 ML {* val t_a = atomize_thm @{thm list_induct_part} *} |
|
429 |
|
430 |
|
431 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
|
432 ML_prf {* fun tac ctxt = FIRST' [ |
|
433 rtac rel_refl, |
|
434 atac, |
|
435 rtac @{thm universal_twice}, |
|
436 (rtac @{thm impI} THEN' atac), |
|
437 rtac @{thm implication_twice}, |
|
438 //comented out rtac @{thm equality_twice}, // |
|
439 EqSubst.eqsubst_tac ctxt [0] |
|
440 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
441 (@{thm equiv_res_exists} OF [rel_eqv])], |
|
442 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
|
443 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
444 ]; *} |
|
445 apply (atomize(full)) |
|
446 apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) |
|
447 done *) |
|
448 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
|
449 ML {* |
|
450 val rt = build_repabs_term @{context} t_r consts rty qty |
|
451 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
|
452 *} |
|
453 prove {* Syntax.check_term @{context} rg *} |
|
454 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
|
455 apply(atomize(full)) |
|
456 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
457 done |
|
458 ML {* |
|
459 val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms |
|
460 *} |
|
461 |
|
462 ML {* val abs = findabs rty (prop_of (t_a)) *} |
|
463 ML {* val aps = findaps rty (prop_of (t_a)) *} |
|
464 ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
|
465 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
|
466 ML {* val lam_prs_thms = map Thm.varifyT lam_prs_thms *} |
|
467 ML {* t_t *} |
|
468 ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *} |
|
469 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
|
470 ML {* val t_l0 = repeat_eqsubst_thm @{context} (app_prs_thms) t_t *} |
|
471 ML app_prs_thms |
|
472 ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_l0 *} |
|
473 ML lam_prs_thms |
|
474 ML {* val t_id = simp_ids @{context} t_l *} |
|
475 thm INSERT_def |
|
476 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
|
477 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *} |
|
478 ML allthms |
|
479 thm FORALL_PRS |
|
480 ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *} |
|
481 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *} |
|
482 ML {* ObjectLogic.rulify t_s *} |
|
483 |
|
484 ML {* val gl = @{term "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"} *} |
|
485 ML {* val gla = atomize_goal @{theory} gl *} |
|
486 |
|
487 prove t_r: {* mk_REGULARIZE_goal @{context} (prop_of t_a) gla *} |
|
488 |
|
489 ML_prf {* fun tac ctxt = FIRST' [ |
|
490 rtac rel_refl, |
|
491 atac, |
|
492 rtac @{thm universal_twice}, |
|
493 (rtac @{thm impI} THEN' atac), |
|
494 rtac @{thm implication_twice}, |
|
495 (*rtac @{thm equality_twice},*) |
|
496 EqSubst.eqsubst_tac ctxt [0] |
|
497 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
498 (@{thm equiv_res_exists} OF [rel_eqv])], |
|
499 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
|
500 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
501 ]; *} |
|
502 |
|
503 apply (atomize(full)) |
|
504 apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) |
|
505 done |
|
506 |
|
507 ML {* val t_r = @{thm t_r} OF [t_a] *} |
|
508 |
|
509 ML {* val ttt = mk_inj_REPABS_goal @{context} (prop_of t_r, gla) *} |
|
510 ML {* val si = simp_ids_trm (cterm_of @{theory} ttt) *} |
|
511 prove t_t: {* term_of si *} |
|
512 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
|
513 apply(atomize(full)) |
|
514 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
418 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
515 apply (rule FUN_QUOTIENT) |
419 apply (rule FUN_QUOTIENT) |
516 apply (rule FUN_QUOTIENT) |
420 apply (rule FUN_QUOTIENT) |
517 apply (rule IDENTITY_QUOTIENT) |
421 apply (rule IDENTITY_QUOTIENT) |
518 apply (rule FUN_QUOTIENT) |
422 apply (rule FUN_QUOTIENT) |
577 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) |
481 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) |
578 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
482 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
579 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
483 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
580 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
484 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
581 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
485 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
582 done |
486 apply (tactic {* clean_tac @{context} quot defs reps_same 1 *}) |
583 |
487 done |
584 thm t_t |
|
585 ML {* val t_t = @{thm Pure.equal_elim_rule1} OF [@{thm t_t}, t_r] *} |
|
586 ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_t *} |
|
587 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *} |
|
588 ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *} |
|
589 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *} |
|
590 |
488 |
591 end |
489 end |