305 |
305 |
306 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
306 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
307 |
307 |
308 thm m2 |
308 thm m2 |
309 |
309 |
310 thm append_assoc |
310 thm neq_Nil_conv |
311 (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *) |
311 term REP_fset |
|
312 term "op --->" |
|
313 thm INSERT_def |
|
314 ML {* val defs_sym = flat (map (add_lower_defs @{context}) @{thms INSERT_def}) *} |
|
315 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*) |
312 ML {* lift_thm_fset @{context} @{thm m1} *} |
316 ML {* lift_thm_fset @{context} @{thm m1} *} |
313 ML {* lift_thm_fset @{context} @{thm m2} *} |
317 ML {* lift_thm_fset @{context} @{thm m2} *} |
314 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
318 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
315 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
319 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
316 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
320 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
396 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
400 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
397 *} |
401 *} |
398 prove {* Syntax.check_term @{context} rg *} |
402 prove {* Syntax.check_term @{context} rg *} |
399 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
403 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
400 apply(atomize(full)) |
404 apply(atomize(full)) |
401 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
|
402 apply (rule FUN_QUOTIENT) |
|
403 apply (rule FUN_QUOTIENT) |
|
404 apply (rule QUOTIENT_fset) |
|
405 apply (rule FUN_QUOTIENT) |
|
406 apply (rule QUOTIENT_fset) |
|
407 apply (rule IDENTITY_QUOTIENT) |
|
408 apply (rule IDENTITY_QUOTIENT) |
|
409 apply (rule IDENTITY_QUOTIENT) |
|
410 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
411 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
405 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
412 done |
406 done |
413 ML {* |
407 ML {* |
414 val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms |
408 val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms |
415 *} |
409 *} |
458 Term.absfree (x2', T2, s2)) |
452 Term.absfree (x2', T2, s2)) |
459 end |
453 end |
460 | _ => f trm trm2 |
454 | _ => f trm trm2 |
461 *} |
455 *} |
462 |
456 |
|
457 (*ML_prf {* |
|
458 val concl = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) |
|
459 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP2}) |
|
460 val insts = Thm.first_order_match (pat, concl) |
|
461 val t = Drule.instantiate insts @{thm APPLY_RSP2} |
|
462 *}*) |
|
463 |
463 ML {* |
464 ML {* |
464 fun tyRel2 lthy ty gty = |
465 fun tyRel2 lthy ty gty = |
465 if ty = gty then HOLogic.eq_const ty else |
466 if ty = gty then HOLogic.eq_const ty else |
466 |
467 |
467 case find_first (fn x => Sign.typ_instance (ProofContext.theory_of lthy) (gty, (#qtyp x))) (quotdata_lookup lthy) of |
468 case quotdata_lookup lthy (fst (dest_Type gty)) of |
468 SOME quotdata => |
469 SOME quotdata => |
469 if Sign.typ_instance (ProofContext.theory_of lthy) (ty, #rtyp quotdata) then |
470 if Sign.typ_instance (ProofContext.theory_of lthy) (ty, #rtyp quotdata) then |
470 case #rel quotdata of |
471 case #rel quotdata of |
471 Const(s, _) => Const(s, dummyT) |
472 Const(s, _) => Const(s, dummyT) |
472 | _ => error "tyRel2 fail: relation is not a constant" |
473 | _ => error "tyRel2 fail: relation is not a constant" |
710 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
711 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
711 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
712 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
712 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
713 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
713 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
714 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
714 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
715 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
715 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
716 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
716 apply (rule QUOTIENT_fset) |
717 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
717 apply (rule IDENTITY_QUOTIENT) |
718 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) |
718 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
719 apply assumption |
719 apply (rule IDENTITY_QUOTIENT) |
720 apply (rule refl) |
720 apply (rule FUN_QUOTIENT) |
721 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
721 apply (rule QUOTIENT_fset) |
722 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
722 apply (rule IDENTITY_QUOTIENT) |
723 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
723 |
724 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
724 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
725 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) |
725 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
726 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
727 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
728 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
729 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
|
730 apply (rule QUOTIENT_fset) |
|
731 apply (rule IDENTITY_QUOTIENT) |
|
732 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
|
733 apply (rule IDENTITY_QUOTIENT) |
|
734 apply (rule FUN_QUOTIENT) |
|
735 apply (rule QUOTIENT_fset) |
|
736 apply (rule IDENTITY_QUOTIENT) |
|
737 |
|
738 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
739 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
740 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
726 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
741 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
727 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
742 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
728 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
743 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
729 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
744 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
730 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
745 apply (rule IDENTITY_QUOTIENT) |
731 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) |
746 apply (rule FUN_QUOTIENT) |
|
747 apply (rule QUOTIENT_fset) |
|
748 apply (rule IDENTITY_QUOTIENT) |
|
749 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
750 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
732 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
751 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
733 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
752 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
734 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
753 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
735 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
754 done |
736 done |