602 (ogl as ((Const (@{const_name "Ball"}, _)) $ |
602 (ogl as ((Const (@{const_name "Ball"}, _)) $ |
603 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => |
603 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => |
604 (let |
604 (let |
605 val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; |
605 val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; |
606 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
606 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
607 val _ = tracing (Syntax.string_of_term ctxt glc); |
607 (* val _ = tracing (Syntax.string_of_term ctxt glc);*) |
608 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
608 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
609 val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]); |
609 val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]); |
610 val R1c = cterm_of thy R1; |
610 val R1c = cterm_of thy R1; |
611 val thmi = Drule.instantiate' [] [SOME R1c] thm; |
611 val thmi = Drule.instantiate' [] [SOME R1c] thm; |
612 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *) |
612 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi));*) |
613 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl |
613 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl |
614 val _ = tracing "AAA"; |
|
615 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); |
614 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); |
616 val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); |
615 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); *) |
617 in |
616 in |
618 SOME thm2 |
617 SOME thm2 |
619 end |
618 end |
620 handle _ => NONE |
619 handle _ => NONE |
621 |
620 |
634 (ogl as ((Const (@{const_name "Bex"}, _)) $ |
633 (ogl as ((Const (@{const_name "Bex"}, _)) $ |
635 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => |
634 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => |
636 (let |
635 (let |
637 val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; |
636 val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; |
638 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
637 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
639 val _ = tracing (Syntax.string_of_term ctxt glc); |
638 (* val _ = tracing (Syntax.string_of_term ctxt glc); *) |
640 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
639 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
641 val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]); |
640 val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]); |
642 val R1c = cterm_of thy R1; |
641 val R1c = cterm_of thy R1; |
643 val thmi = Drule.instantiate' [] [SOME R1c] thm; |
642 val thmi = Drule.instantiate' [] [SOME R1c] thm; |
644 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *) |
643 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *) |
645 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl |
644 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl |
646 val _ = tracing "AAA"; |
|
647 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); |
645 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); |
648 val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); |
646 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));*) |
649 in |
647 in |
650 SOME thm2 |
648 SOME thm2 |
651 end |
649 end |
652 handle _ => NONE |
650 handle _ => NONE |
653 |
651 |