602 (******************************************) |
602 (******************************************) |
603 (******************************************) |
603 (******************************************) |
604 |
604 |
605 |
605 |
606 ML {* |
606 ML {* |
607 (* builds the relation for respects *) |
607 (* |
|
608 Regularizing an rtrm means: |
|
609 - quantifiers over a type that needs lifting are replaced by |
|
610 bounded quantifiers, for example: |
|
611 \<forall>x. P \<Longrightarrow> \<forall>x \<in> (Respects R). P / All (Respects R) P |
|
612 |
|
613 the relation R is given by the rty and qty; |
608 |
614 |
|
615 - abstractions over a type that needs lifting are replaced |
|
616 by bounded abstractions: |
|
617 \<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P) |
|
618 |
|
619 - equalities over the type being lifted are replaced by |
|
620 corresponding relations: |
|
621 A = B \<Longrightarrow> A \<approx> B |
|
622 |
|
623 example with more complicated types of A, B: |
|
624 A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B |
|
625 *) |
|
626 |
|
627 |
|
628 (* builds the relation that is the argument of respects *) |
609 fun mk_resp_arg lthy (rty, qty) = |
629 fun mk_resp_arg lthy (rty, qty) = |
610 let |
630 let |
611 val thy = ProofContext.theory_of lthy |
631 val thy = ProofContext.theory_of lthy |
612 in |
632 in |
613 if rty = qty |
633 if rty = qty |
657 | _ => f trm1 trm2 |
677 | _ => f trm1 trm2 |
658 |
678 |
659 (* the major type of All and Ex quantifiers *) |
679 (* the major type of All and Ex quantifiers *) |
660 fun qnt_typ ty = domain_type (domain_type ty) |
680 fun qnt_typ ty = domain_type (domain_type ty) |
661 *} |
681 *} |
662 |
|
663 (* |
|
664 Regularizing an rtrm means: |
|
665 - quantifiers over a type that needs lifting are replaced by |
|
666 bounded quantifiers, for example: |
|
667 \<forall>x. P \<Longrightarrow> \<forall>x \<in> (Respects R). P / All (Respects R) P |
|
668 |
|
669 the relation R is given by the rty and qty; |
|
670 |
|
671 - abstractions over a type that needs lifting are replaced |
|
672 by bounded abstractions: |
|
673 \<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P) |
|
674 |
|
675 - equalities over the type being lifted are replaced by |
|
676 corresponding relations: |
|
677 A = B \<Longrightarrow> A \<approx> B |
|
678 |
|
679 example with more complicated types of A, B: |
|
680 A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B |
|
681 *) |
|
682 |
682 |
683 ML {* |
683 ML {* |
684 (* produces a regularized version of rtm *) |
684 (* produces a regularized version of rtm *) |
685 (* - the result is still not completely typed *) |
685 (* - the result is still not completely typed *) |
686 (* - does not need any special treatment of *) |
686 (* - does not need any special treatment of *) |
744 fun mk_REGULARIZE_goal lthy rtrm qtrm = |
744 fun mk_REGULARIZE_goal lthy rtrm qtrm = |
745 Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm)) |
745 Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm)) |
746 *} |
746 *} |
747 |
747 |
748 (* |
748 (* |
749 To prove that the old theorem implies the new one, we first |
749 To prove that the raw theorem implies the regularised one, |
750 atomize it and then try: |
750 we try in order: |
751 |
751 |
752 - Reflexivity of the relation |
752 - Reflexivity of the relation |
753 - Assumption |
753 - Assumption |
754 - Elimnating quantifiers on both sides of toplevel implication |
754 - Elimnating quantifiers on both sides of toplevel implication |
755 - Simplifying implications on both sides of toplevel implication |
755 - Simplifying implications on both sides of toplevel implication |
833 DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
833 DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
834 DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})] |
834 DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})] |
835 *} |
835 *} |
836 |
836 |
837 ML {* |
837 ML {* |
838 fun REGULARIZE_prove rtrm qtrm rel_eqv rel_refl lthy = |
838 fun regularize_tac ctxt rel_eqv rel_refl = |
839 let |
839 (ObjectLogic.full_atomize_tac) THEN' |
840 val goal = mk_REGULARIZE_goal lthy rtrm qtrm |
840 REPEAT_ALL_NEW (FIRST' [ |
841 in |
841 rtac rel_refl, |
842 Goal.prove lthy [] [] goal |
842 atac, |
843 (fn {context, ...} => REGULARIZE_tac' context rel_refl rel_eqv) |
843 rtac @{thm universal_twice}, |
844 end |
844 (rtac @{thm impI} THEN' atac), |
845 *} |
845 rtac @{thm implication_twice}, |
|
846 EqSubst.eqsubst_tac ctxt [0] |
|
847 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
848 (@{thm equiv_res_exists} OF [rel_eqv])], |
|
849 (* For a = b \<longrightarrow> a \<approx> b *) |
|
850 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
|
851 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
852 ]); |
|
853 *} |
|
854 |
846 |
855 |
847 (* |
856 (* |
|
857 Injections of REP and Abses |
|
858 *************************** |
|
859 |
848 Injecting REPABS means: |
860 Injecting REPABS means: |
849 |
861 |
850 For abstractions: |
862 For abstractions: |
851 * If the type of the abstraction doesn't need lifting we recurse. |
863 * If the type of the abstraction doesn't need lifting we recurse. |
852 * If it does we add RepAbs around the whole term and check if the |
864 * If it does we add RepAbs around the whole term and check if the |
864 (if it is not applied we treated it in Abs branch) then we |
876 (if it is not applied we treated it in Abs branch) then we |
865 put RepAbs and recurse |
877 put RepAbs and recurse |
866 * Otherwise just recurse. |
878 * Otherwise just recurse. |
867 *) |
879 *) |
868 |
880 |
869 (* rep-abs injection *) |
|
870 |
|
871 ML {* |
881 ML {* |
872 fun mk_repabs lthy (T, T') trm = |
882 fun mk_repabs lthy (T, T') trm = |
873 Quotient_Def.get_fun repF lthy (T, T') |
883 Quotient_Def.get_fun repF lthy (T, T') |
874 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
884 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
875 *} |
885 *} |
876 |
|
877 |
886 |
878 ML {* |
887 ML {* |
879 (* bound variables need to be treated properly, *) |
888 (* bound variables need to be treated properly, *) |
880 (* as the type of subterms need to be calculated *) |
889 (* as the type of subterms need to be calculated *) |
881 |
890 |
937 fun mk_inj_REPABS_goal lthy (rtrm, qtrm) = |
946 fun mk_inj_REPABS_goal lthy (rtrm, qtrm) = |
938 Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm))) |
947 Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm))) |
939 *} |
948 *} |
940 |
949 |
941 |
950 |
942 |
951 (* Genralisation of free variables in a goal *) |
943 (* |
|
944 To prove that the old theorem implies the new one, we first |
|
945 atomize it and then try: |
|
946 - Reflexivity of the relation |
|
947 - Assumption |
|
948 - Elimnating quantifiers on both sides of toplevel implication |
|
949 - Simplifying implications on both sides of toplevel implication |
|
950 - Ball (Respects ?E) ?P = All ?P |
|
951 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q |
|
952 *) |
|
953 |
|
954 ML {* |
|
955 fun regularize_tac ctxt rel_eqv rel_refl = |
|
956 (ObjectLogic.full_atomize_tac) THEN' |
|
957 REPEAT_ALL_NEW (FIRST' [ |
|
958 rtac rel_refl, |
|
959 atac, |
|
960 rtac @{thm universal_twice}, |
|
961 (rtac @{thm impI} THEN' atac), |
|
962 rtac @{thm implication_twice}, |
|
963 EqSubst.eqsubst_tac ctxt [0] |
|
964 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
965 (@{thm equiv_res_exists} OF [rel_eqv])], |
|
966 (* For a = b \<longrightarrow> a \<approx> b *) |
|
967 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
|
968 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
969 ]); |
|
970 *} |
|
971 |
952 |
972 ML {* |
953 ML {* |
973 fun inst_spec ctrm = |
954 fun inst_spec ctrm = |
974 let |
955 let |
975 val cty = ctyp_of_term ctrm |
956 val cty = ctyp_of_term ctrm |
996 (K ((inst_spec_tac (rev cvrs) THEN' atac) 1)) |
977 (K ((inst_spec_tac (rev cvrs) THEN' atac) 1)) |
997 in |
978 in |
998 rtac rule i |
979 rtac rule i |
999 end) |
980 end) |
1000 *} |
981 *} |
|
982 |
|
983 (* General outline of the lifting procedure *) |
|
984 (* **************************************** *) |
|
985 (* *) |
|
986 (* - A is the original raw theorem *) |
|
987 (* - B is the regularized theorem *) |
|
988 (* - C is the rep/abs injected version of B *) |
|
989 (* - D is the lifted theorem *) |
|
990 (* *) |
|
991 (* - b is the regularization step *) |
|
992 (* - c is the rep/abs injection step *) |
|
993 (* - d is the cleaning part *) |
1001 |
994 |
1002 lemma procedure: |
995 lemma procedure: |
1003 assumes a: "A" |
996 assumes a: "A" |
1004 and b: "A \<Longrightarrow> B" |
997 and b: "A \<Longrightarrow> B" |
1005 and c: "B = C" |
998 and c: "B = C" |
1024 fun procedure_inst ctxt rtrm qtrm = |
1017 fun procedure_inst ctxt rtrm qtrm = |
1025 let |
1018 let |
1026 val thy = ProofContext.theory_of ctxt |
1019 val thy = ProofContext.theory_of ctxt |
1027 val rtrm' = HOLogic.dest_Trueprop rtrm |
1020 val rtrm' = HOLogic.dest_Trueprop rtrm |
1028 val qtrm' = HOLogic.dest_Trueprop qtrm |
1021 val qtrm' = HOLogic.dest_Trueprop qtrm |
1029 val reg_goal = Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm') |
1022 val reg_goal = |
1030 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm |
1023 Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm') |
1031 val inj_goal = Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm')) |
1024 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm |
1032 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm |
1025 val inj_goal = |
|
1026 Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm')) |
|
1027 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm |
1033 in |
1028 in |
1034 Drule.instantiate' [] |
1029 Drule.instantiate' [] |
1035 [SOME (cterm_of thy rtrm'), |
1030 [SOME (cterm_of thy rtrm'), |
1036 SOME (cterm_of thy reg_goal), |
1031 SOME (cterm_of thy reg_goal), |
1037 SOME (cterm_of thy inj_goal)] |
1032 SOME (cterm_of thy inj_goal)] |