486 - Ball (Respects ?E) ?P = All ?P |
486 - Ball (Respects ?E) ?P = All ?P |
487 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q |
487 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q |
488 |
488 |
489 *) |
489 *) |
490 |
490 |
491 lemma universal_twice: |
|
492 assumes *: "\<And>x. (P x \<longrightarrow> Q x)" |
|
493 shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)" |
|
494 using * by auto |
|
495 |
|
496 lemma implication_twice: |
|
497 assumes a: "c \<longrightarrow> a" |
|
498 assumes b: "b \<longrightarrow> d" |
|
499 shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)" |
|
500 using a b by auto |
|
501 |
|
502 (* version of regularize_tac including debugging information *) |
|
503 ML {* |
|
504 fun regularize_tac ctxt rel_eqv rel_refl = |
|
505 (ObjectLogic.full_atomize_tac) THEN' |
|
506 REPEAT_ALL_NEW (FIRST' |
|
507 [(K (print_tac "start")) THEN' (K no_tac), |
|
508 DT ctxt "1" (resolve_tac rel_refl), |
|
509 DT ctxt "2" atac, |
|
510 DT ctxt "3" (rtac @{thm universal_twice}), |
|
511 DT ctxt "4" (rtac @{thm impI} THEN' atac), |
|
512 DT ctxt "5" (rtac @{thm implication_twice}), |
|
513 DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0] |
|
514 [(@{thm ball_reg_eqv} OF [rel_eqv]), |
|
515 (@{thm ball_reg_eqv} OF [rel_eqv])]), |
|
516 (* For a = b \<longrightarrow> a \<approx> b *) |
|
517 DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl)), |
|
518 DT ctxt "8" (rtac @{thm ball_reg_right}) |
|
519 ]); |
|
520 *} |
|
521 |
|
522 lemma move_forall: |
|
523 "(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))" |
|
524 by auto |
|
525 |
|
526 lemma move_exists: |
|
527 "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))" |
|
528 by auto |
|
529 |
|
530 lemma [mono]: |
491 lemma [mono]: |
531 "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)" |
492 "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)" |
532 by blast |
493 by blast |
533 |
494 |
534 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P" |
495 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P" |
542 rtac @{thm IDENTITY_EQUIV}, |
503 rtac @{thm IDENTITY_EQUIV}, |
543 rtac @{thm LIST_EQUIV}]) |
504 rtac @{thm LIST_EQUIV}]) |
544 *} |
505 *} |
545 |
506 |
546 ML {* |
507 ML {* |
547 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
508 fun ball_reg_eqv_simproc rel_eqvs ss redex = |
548 *} |
509 let |
549 |
510 val ctxt = Simplifier.the_context ss |
550 (* |
511 val thy = ProofContext.theory_of ctxt |
551 ML {* |
512 in |
552 fun regularize_tac ctxt rel_eqvs rel_refl = |
513 case redex of |
553 let |
514 (ogl as ((Const (@{const_name "Ball"}, _)) $ |
554 val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs |
515 ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => |
555 val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs |
516 (let |
556 val subs = map (fn x => @{thm eq_reflection} OF [x]) (subs1 @ subs2) |
517 val gl = Const (@{const_name "EQUIV"}, dummyT) $ R; |
557 in |
518 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
558 (ObjectLogic.full_atomize_tac) THEN' |
519 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
559 (simp_tac ((Simplifier.context ctxt empty_ss) addsimps subs)) |
520 val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]); |
560 THEN' |
521 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) |
561 REPEAT_ALL_NEW (FIRST' |
522 in |
562 [(rtac @{thm RIGHT_RES_FORALL_REGULAR}), |
523 SOME thm |
563 (rtac @{thm LEFT_RES_EXISTS_REGULAR}), |
524 end |
564 (resolve_tac (Inductive.get_monos ctxt)), |
525 handle _ => NONE |
565 (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
526 ) |
566 (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
527 | _ => NONE |
567 rtac @{thm move_forall}, |
528 end |
568 rtac @{thm move_exists}, |
529 *} |
569 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl))]) |
530 |
570 end |
531 ML {* |
571 *} |
532 fun bex_reg_eqv_simproc rel_eqvs ss redex = |
572 *) |
533 let |
|
534 val ctxt = Simplifier.the_context ss |
|
535 val thy = ProofContext.theory_of ctxt |
|
536 in |
|
537 case redex of |
|
538 (ogl as ((Const (@{const_name "Bex"}, _)) $ |
|
539 ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => |
|
540 (let |
|
541 val gl = Const (@{const_name "EQUIV"}, dummyT) $ R; |
|
542 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
|
543 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
|
544 val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]); |
|
545 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) |
|
546 in |
|
547 SOME thm |
|
548 end |
|
549 handle _ => NONE |
|
550 ) |
|
551 | _ => NONE |
|
552 end |
|
553 *} |
|
554 |
|
555 ML {* |
|
556 fun prep_trm thy (x, (T, t)) = |
|
557 (cterm_of thy (Var (x, T)), cterm_of thy t) |
|
558 |
|
559 fun prep_ty thy (x, (S, ty)) = |
|
560 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
|
561 *} |
|
562 |
|
563 ML {* |
|
564 fun matching_prs thy pat trm = |
|
565 let |
|
566 val univ = Unify.matchers thy [(pat, trm)] |
|
567 val SOME (env, _) = Seq.pull univ |
|
568 val tenv = Vartab.dest (Envir.term_env env) |
|
569 val tyenv = Vartab.dest (Envir.type_env env) |
|
570 in |
|
571 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
|
572 end |
|
573 *} |
|
574 |
|
575 ML {* |
|
576 fun ball_reg_eqv_range_simproc rel_eqvs ss redex = |
|
577 let |
|
578 val ctxt = Simplifier.the_context ss |
|
579 val thy = ProofContext.theory_of ctxt |
|
580 in |
|
581 case redex of |
|
582 (ogl as ((Const (@{const_name "Ball"}, _)) $ |
|
583 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => |
|
584 (let |
|
585 val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; |
|
586 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
|
587 val _ = tracing (Syntax.string_of_term ctxt glc); |
|
588 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
|
589 val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]); |
|
590 val R1c = cterm_of thy R1; |
|
591 val thmi = Drule.instantiate' [] [SOME R1c] thm; |
|
592 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *) |
|
593 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl |
|
594 val _ = tracing "AAA"; |
|
595 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); |
|
596 val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); |
|
597 in |
|
598 SOME thm2 |
|
599 end |
|
600 handle _ => NONE |
|
601 |
|
602 ) |
|
603 | _ => NONE |
|
604 end |
|
605 *} |
|
606 |
|
607 ML {* |
|
608 fun bex_reg_eqv_range_simproc rel_eqvs ss redex = |
|
609 let |
|
610 val ctxt = Simplifier.the_context ss |
|
611 val thy = ProofContext.theory_of ctxt |
|
612 in |
|
613 case redex of |
|
614 (ogl as ((Const (@{const_name "Bex"}, _)) $ |
|
615 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => |
|
616 (let |
|
617 val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; |
|
618 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
|
619 val _ = tracing (Syntax.string_of_term ctxt glc); |
|
620 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
|
621 val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]); |
|
622 val R1c = cterm_of thy R1; |
|
623 val thmi = Drule.instantiate' [] [SOME R1c] thm; |
|
624 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *) |
|
625 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl |
|
626 val _ = tracing "AAA"; |
|
627 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); |
|
628 val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); |
|
629 in |
|
630 SOME thm2 |
|
631 end |
|
632 handle _ => NONE |
|
633 |
|
634 ) |
|
635 | _ => NONE |
|
636 end |
|
637 *} |
|
638 |
|
639 lemma eq_imp_rel: "EQUIV R \<Longrightarrow> a = b \<longrightarrow> R a b" |
|
640 by (simp add: EQUIV_REFL) |
|
641 |
|
642 ML {* |
|
643 fun regularize_tac ctxt rel_eqvs = |
|
644 let |
|
645 val pat1 = [@{term "Ball (Respects R) P"}]; |
|
646 val pat2 = [@{term "Bex (Respects R) P"}]; |
|
647 val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}]; |
|
648 val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}]; |
|
649 val thy = ProofContext.theory_of ctxt |
|
650 val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs)) |
|
651 val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs)) |
|
652 val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs)) |
|
653 val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs)) |
|
654 val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4] |
|
655 (* TODO: Make sure that there are no LIST_REL, PAIR_REL etc involved *) |
|
656 val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs |
|
657 in |
|
658 ObjectLogic.full_atomize_tac THEN' |
|
659 simp_tac simp_ctxt THEN' |
|
660 REPEAT_ALL_NEW (FIRST' [ |
|
661 rtac @{thm ball_reg_right}, |
|
662 rtac @{thm bex_reg_left}, |
|
663 resolve_tac (Inductive.get_monos ctxt), |
|
664 rtac @{thm ball_all_comm}, |
|
665 rtac @{thm bex_ex_comm}, |
|
666 resolve_tac eq_eqvs, |
|
667 simp_tac simp_ctxt |
|
668 ]) |
|
669 end |
|
670 *} |
573 |
671 |
574 section {* Injections of REP and ABSes *} |
672 section {* Injections of REP and ABSes *} |
575 |
673 |
576 (* |
674 (* |
577 Injecting REPABS means: |
675 Injecting REPABS means: |
771 end |
869 end |
772 | _ => no_tac) |
870 | _ => no_tac) |
773 *} |
871 *} |
774 |
872 |
775 ML {* |
873 ML {* |
|
874 <<<<<<< variant A |
|
875 >>>>>>> variant B |
|
876 val ball_rsp_tac = |
|
877 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
878 case (term_of concl) of |
|
879 (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) => |
|
880 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
|
881 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
882 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
|
883 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
|
884 |_ => no_tac) |
|
885 *} |
|
886 |
|
887 ML {* |
|
888 val bex_rsp_tac = |
|
889 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
890 case (term_of concl) of |
|
891 (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) => |
|
892 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
|
893 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
894 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
|
895 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
|
896 | _ => no_tac) |
|
897 *} |
|
898 |
|
899 ML {* |
|
900 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
|
901 *} |
|
902 |
|
903 ML {* |
|
904 ####### Ancestor |
|
905 val ball_rsp_tac = |
|
906 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
907 case (term_of concl) of |
|
908 (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) => |
|
909 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
|
910 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
911 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
|
912 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
|
913 |_ => no_tac) |
|
914 *} |
|
915 |
|
916 ML {* |
|
917 val bex_rsp_tac = |
|
918 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
919 case (term_of concl) of |
|
920 (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) => |
|
921 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
|
922 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
923 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
|
924 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
|
925 | _ => no_tac) |
|
926 *} |
|
927 |
|
928 ML {* |
|
929 ======= end |
776 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
930 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
777 (FIRST' [resolve_tac trans2, |
931 (FIRST' [resolve_tac trans2, |
778 LAMBDA_RES_TAC ctxt, |
932 LAMBDA_RES_TAC ctxt, |
779 rtac @{thm RES_FORALL_RSP}, |
933 rtac @{thm RES_FORALL_RSP}, |
780 ball_rsp_tac ctxt, |
934 ball_rsp_tac ctxt, |
878 |
1032 |
879 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
1033 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
880 REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms) |
1034 REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms) |
881 *} |
1035 *} |
882 |
1036 |
|
1037 ML {* |
|
1038 fun get_inj_repabs_tac ctxt rel lhs rhs = |
|
1039 let |
|
1040 val _ = tracing "input" |
|
1041 val _ = tracing ("rel: " ^ Syntax.string_of_term ctxt rel) |
|
1042 val _ = tracing ("lhs: " ^ Syntax.string_of_term ctxt lhs) |
|
1043 val _ = tracing ("rhs: " ^ Syntax.string_of_term ctxt rhs) |
|
1044 in |
|
1045 case (rel, lhs, rhs) of |
|
1046 (_, l, Const _ $ (Const _ $ r)) (* FIXME: not right_match *) |
|
1047 => rtac @{thm REP_ABS_RSP(1)} |
|
1048 | (_, Const (@{const_name "Ball"}, _) $ _, |
|
1049 Const (@{const_name "Ball"}, _) $ _) |
|
1050 => rtac @{thm RES_FORALL_RSP} |
|
1051 | _ => K no_tac |
|
1052 end |
|
1053 *} |
|
1054 |
|
1055 ML {* |
|
1056 fun inj_repabs_tac ctxt = |
|
1057 SUBGOAL (fn (goal, i) => |
|
1058 (case (HOLogic.dest_Trueprop goal) of |
|
1059 (rel $ lhs $ rhs) => get_inj_repabs_tac ctxt rel lhs rhs |
|
1060 | _ => K no_tac) i) |
|
1061 *} |
883 |
1062 |
884 section {* Cleaning of the theorem *} |
1063 section {* Cleaning of the theorem *} |
885 |
1064 |
886 ML {* |
1065 ML {* |
887 fun applic_prs lthy absrep (rty, qty) = |
1066 fun applic_prs lthy absrep (rty, qty) = |