375 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
375 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
376 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
376 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
377 |
377 |
378 thm list.recs(2) |
378 thm list.recs(2) |
379 ML {* val t_a = atomize_thm @{thm list_induct_part} *} |
379 ML {* val t_a = atomize_thm @{thm list_induct_part} *} |
|
380 |
|
381 |
380 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
382 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
381 ML_prf {* fun tac ctxt = FIRST' [ |
383 ML_prf {* fun tac ctxt = FIRST' [ |
382 rtac rel_refl, |
384 rtac rel_refl, |
383 atac, |
385 atac, |
384 rtac @{thm universal_twice}, |
386 rtac @{thm universal_twice}, |
385 (rtac @{thm impI} THEN' atac), |
387 (rtac @{thm impI} THEN' atac), |
386 rtac @{thm implication_twice}, |
388 rtac @{thm implication_twice}, |
387 (*rtac @{thm equality_twice},*) |
389 //comented out rtac @{thm equality_twice}, // |
388 EqSubst.eqsubst_tac ctxt [0] |
390 EqSubst.eqsubst_tac ctxt [0] |
389 [(@{thm equiv_res_forall} OF [rel_eqv]), |
391 [(@{thm equiv_res_forall} OF [rel_eqv]), |
390 (@{thm equiv_res_exists} OF [rel_eqv])], |
392 (@{thm equiv_res_exists} OF [rel_eqv])], |
391 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
393 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
392 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
394 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
393 ]; *} |
395 ]; *} |
394 apply (atomize(full)) |
396 apply (atomize(full)) |
395 apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) |
397 apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) |
396 done*) |
398 done *) |
397 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
399 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
398 ML {* |
400 ML {* |
399 val rt = build_repabs_term @{context} t_r consts rty qty |
401 val rt = build_repabs_term @{context} t_r consts rty qty |
400 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
402 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
401 *} |
403 *} |
587 ML {* prop_of t_a *} |
589 ML {* prop_of t_a *} |
588 ML {* term_of glac *} |
590 ML {* term_of glac *} |
589 ML {* val (tta, ttb) = (my_reg2 @{context} (prop_of t_a) (term_of glac)) *} |
591 ML {* val (tta, ttb) = (my_reg2 @{context} (prop_of t_a) (term_of glac)) *} |
590 |
592 |
591 (* Does not work. *) |
593 (* Does not work. *) |
592 (* ML {* val ttar = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *} *) |
594 ML {* |
|
595 prop_of t_a |
|
596 |> Syntax.string_of_term @{context} |
|
597 |> writeln |
|
598 *} |
|
599 |
|
600 ML {* |
|
601 (term_of glac) |
|
602 |> Syntax.string_of_term @{context} |
|
603 |> writeln |
|
604 *} |
|
605 |
|
606 ML {* val ttar = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *} |
593 |
607 |
594 ML {* val tt = Syntax.check_term @{context} tta *} |
608 ML {* val tt = Syntax.check_term @{context} tta *} |
|
609 ML {* val ttr = Syntax.check_term @{context} ttar *} |
|
610 |
|
611 |
595 |
612 |
596 prove t_r: {* Logic.mk_implies |
613 prove t_r: {* Logic.mk_implies |
597 ((prop_of t_a), tt) *} |
614 ((prop_of t_a), tt) *} |
598 ML_prf {* fun tac ctxt = FIRST' [ |
615 ML_prf {* fun tac ctxt = FIRST' [ |
599 rtac rel_refl, |
616 rtac rel_refl, |