539 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
524 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
540 end |
525 end |
541 *} |
526 *} |
542 |
527 |
543 ML {* |
528 ML {* |
544 fun ball_reg_eqv_range_simproc ss redex = |
529 fun calculate_instance ctxt thm redex R1 R2 = |
545 let |
530 let |
546 val ctxt = Simplifier.the_context ss |
531 val thy = ProofContext.theory_of ctxt |
547 val thy = ProofContext.theory_of ctxt |
532 val goal = Const (@{const_name "equivp"}, dummyT) $ R2 |
548 in |
533 |> Syntax.check_term ctxt |
549 case redex of |
534 |> HOLogic.mk_Trueprop |
550 (ogl as ((Const (@{const_name "Ball"}, _)) $ |
535 val eqv_prem = Goal.prove ctxt [] [] goal (fn {context,...} => equiv_tac context 1) |
551 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) => |
536 val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]]) |
552 (let |
537 val R1c = cterm_of thy R1 |
553 val gl = Const (@{const_name "equivp"}, dummyT) $ R2; |
538 val thmi = Drule.instantiate' [] [SOME R1c] thm |
554 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
539 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex |
555 (* val _ = tracing (Syntax.string_of_term ctxt glc);*) |
540 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi) |
556 val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1) |
541 in |
557 val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]); |
542 SOME thm2 |
558 val R1c = cterm_of thy R1; |
543 end |
559 val thmi = Drule.instantiate' [] [SOME R1c] thm; |
544 handle _ => NONE |
560 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi));*) |
545 (* FIXME/TODO: what is the place where the exception can be raised: matching_prs? *) |
561 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl |
546 *} |
562 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); |
547 |
563 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); *) |
548 ML {* |
564 in |
549 fun ball_bex_range_simproc ss redex = |
565 SOME thm2 |
550 let |
566 end |
551 val ctxt = Simplifier.the_context ss |
567 handle _ => NONE |
552 in |
568 |
553 case redex of |
569 ) |
554 (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ |
|
555 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
|
556 calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2 |
|
557 | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ |
|
558 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
|
559 calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2 |
570 | _ => NONE |
560 | _ => NONE |
571 end |
561 end |
572 *} |
562 *} |
573 |
563 |
574 |
564 lemma eq_imp_rel: |
575 thm bex_reg_eqv_range |
565 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
576 thm ball_reg_eqv |
|
577 thm bex_reg_eqv |
|
578 |
|
579 ML {* |
|
580 fun bex_reg_eqv_range_simproc ss redex = |
|
581 let |
|
582 val ctxt = Simplifier.the_context ss |
|
583 val thy = ProofContext.theory_of ctxt |
|
584 in |
|
585 case redex of |
|
586 (ogl as ((Const (@{const_name "Bex"}, _)) $ |
|
587 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) => |
|
588 (let |
|
589 val gl = Const (@{const_name "equivp"}, dummyT) $ R2; |
|
590 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
|
591 (* val _ = tracing (Syntax.string_of_term ctxt glc); *) |
|
592 val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1) |
|
593 val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]); |
|
594 val R1c = cterm_of thy R1; |
|
595 val thmi = Drule.instantiate' [] [SOME R1c] thm; |
|
596 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *) |
|
597 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl |
|
598 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); |
|
599 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));*) |
|
600 in |
|
601 SOME thm2 |
|
602 end |
|
603 handle _ => NONE |
|
604 |
|
605 ) |
|
606 | _ => NONE |
|
607 end |
|
608 *} |
|
609 |
|
610 lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
|
611 by (simp add: equivp_reflp) |
566 by (simp add: equivp_reflp) |
612 |
567 |
|
568 (* FIXME/TODO: How does regularizing work? *) |
|
569 (* FIXME/TODO: needs to be adapted |
|
570 |
|
571 To prove that the raw theorem implies the regularised one, |
|
572 we try in order: |
|
573 |
|
574 - Reflexivity of the relation |
|
575 - Assumption |
|
576 - Elimnating quantifiers on both sides of toplevel implication |
|
577 - Simplifying implications on both sides of toplevel implication |
|
578 - Ball (Respects ?E) ?P = All ?P |
|
579 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q |
|
580 |
|
581 *) |
613 ML {* |
582 ML {* |
614 fun regularize_tac ctxt = |
583 fun regularize_tac ctxt = |
615 let |
584 let |
616 val pat1 = [@{term "Ball (Respects R) P"}]; |
585 val thy = ProofContext.theory_of ctxt |
617 val pat2 = [@{term "Bex (Respects R) P"}]; |
586 val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} |
618 val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}]; |
587 val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} |
619 val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}]; |
588 val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) |
620 val thy = ProofContext.theory_of ctxt |
589 val simpset = (mk_minimal_ss ctxt) |
621 val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc)) |
|
622 val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc)) |
|
623 val simp_set = (mk_minimal_ss ctxt) |
|
624 addsimps @{thms ball_reg_eqv bex_reg_eqv} |
590 addsimps @{thms ball_reg_eqv bex_reg_eqv} |
625 addsimprocs [simproc3, simproc4] |
591 addsimprocs [simproc] addSolver equiv_solver |
626 addSolver equiv_solver |
592 (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) |
627 (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) |
593 val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) |
628 val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) |
594 in |
629 in |
|
630 ObjectLogic.full_atomize_tac THEN' |
595 ObjectLogic.full_atomize_tac THEN' |
631 simp_tac simp_set THEN' |
596 simp_tac simpset THEN' |
632 REPEAT_ALL_NEW (FIRST' [ |
597 REPEAT_ALL_NEW (FIRST' [ |
633 rtac @{thm ball_reg_right}, |
598 rtac @{thm ball_reg_right}, |
634 rtac @{thm bex_reg_left}, |
599 rtac @{thm bex_reg_left}, |
635 resolve_tac (Inductive.get_monos ctxt), |
600 resolve_tac (Inductive.get_monos ctxt), |
636 rtac @{thm ball_all_comm}, |
601 rtac @{thm ball_all_comm}, |
637 rtac @{thm bex_ex_comm}, |
602 rtac @{thm bex_ex_comm}, |
638 resolve_tac eq_eqvs, |
603 resolve_tac eq_eqvs, |
639 simp_tac simp_set |
604 simp_tac simpset]) |
640 ]) |
605 end |
641 end |
|
642 *} |
606 *} |
643 |
607 |
644 section {* Injections of rep and abses *} |
608 section {* Injections of rep and abses *} |
645 |
609 |
646 (* |
610 (* |