769 end |
768 end |
770 end |
769 end |
771 *} |
770 *} |
772 |
771 |
773 section {* RepAbs Injection Tactic *} |
772 section {* RepAbs Injection Tactic *} |
774 (* |
773 |
775 To prove that the regularised theorem implies the abs/rep injected, we first |
774 ML {* |
776 atomize it and then try: |
775 fun stripped_term_of ct = |
777 |
776 ct |> term_of |> HOLogic.dest_Trueprop |
778 1) theorems 'trans2' from the appropriate QUOT_TYPE |
777 *} |
779 2) remove lambdas from both sides (LAMBDA_RES_TAC) |
|
780 3) remove Ball/Bex from the right hand side |
|
781 4) use user-supplied RSP theorems |
|
782 5) remove rep_abs from the right side |
|
783 6) reflexivity of equality |
|
784 7) split applications of lifted type (apply_rsp) |
|
785 8) split applications of non-lifted type (cong_tac) |
|
786 9) apply extentionality |
|
787 10) reflexivity of the relation |
|
788 11) assumption |
|
789 (Lambdas under respects may have left us some assumptions) |
|
790 12) proving obvious higher order equalities by simplifying fun_rel |
|
791 (not sure if it is still needed?) |
|
792 13) unfolding lambda on one side |
|
793 14) simplifying (= ===> =) for simpler respectfullness |
|
794 |
|
795 *) |
|
796 |
778 |
797 ML {* |
779 ML {* |
798 fun instantiate_tac thm = |
780 fun instantiate_tac thm = |
799 Subgoal.FOCUS (fn {concl, ...} => |
781 Subgoal.FOCUS (fn {concl, ...} => |
800 let |
782 let |
824 using a by (simp add: FUN_REL.simps) |
806 using a by (simp add: FUN_REL.simps) |
825 |
807 |
826 ML {* |
808 ML {* |
827 val lambda_res_tac = |
809 val lambda_res_tac = |
828 Subgoal.FOCUS (fn {concl, ...} => |
810 Subgoal.FOCUS (fn {concl, ...} => |
829 case (term_of concl) of |
811 case (stripped_term_of concl) of |
830 (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
812 (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} 1 |
831 | _ => no_tac) |
813 | _ => no_tac) |
832 *} |
814 *} |
833 |
815 |
834 ML {* |
816 ML {* |
835 val weak_lambda_res_tac = |
817 val weak_lambda_res_tac = |
836 Subgoal.FOCUS (fn {concl, ...} => |
818 Subgoal.FOCUS (fn {concl, ...} => |
837 case (term_of concl) of |
819 case (stripped_term_of concl) of |
838 (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
820 (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} 1 |
839 | (_ $ (_ $ (Abs _) $ _)) => rtac @{thm FUN_REL_I} 1 |
821 | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} 1 |
840 | _ => no_tac) |
822 | _ => no_tac) |
841 *} |
823 *} |
842 |
824 |
843 ML {* |
825 ML {* |
844 val ball_rsp_tac = |
826 val ball_rsp_tac = |
845 Subgoal.FOCUS (fn {concl, ...} => |
827 Subgoal.FOCUS (fn {concl, ...} => |
846 case (term_of concl) of |
828 case (stripped_term_of concl) of |
847 (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) |
829 (_ $ (Const (@{const_name Ball}, _) $ _) |
848 $ (Const (@{const_name Ball}, _) $ _))) => rtac @{thm FUN_REL_I} 1 |
830 $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} 1 |
849 |_ => no_tac) |
831 |_ => no_tac) |
850 *} |
832 *} |
851 |
833 |
852 ML {* |
834 ML {* |
853 val bex_rsp_tac = |
835 val bex_rsp_tac = |
854 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
836 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
855 case (term_of concl) of |
837 case (stripped_term_of concl) of |
856 (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) |
838 (_ $ (Const (@{const_name Bex}, _) $ _) |
857 $ (Const (@{const_name Bex}, _) $ _))) => rtac @{thm FUN_REL_I} 1 |
839 $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} 1 |
858 | _ => no_tac) |
840 | _ => no_tac) |
859 *} |
841 *} |
860 |
842 |
861 ML {* (* Legacy *) |
843 ML {* (* Legacy *) |
862 fun needs_lift (rty as Type (rty_s, _)) ty = |
844 fun needs_lift (rty as Type (rty_s, _)) ty = |
863 case ty of |
845 case ty of |
864 Type (s, tys) => |
846 Type (s, tys) => (s = rty_s) orelse (exists (needs_lift rty) tys) |
865 (s = rty_s) orelse (exists (needs_lift rty) tys) |
|
866 | _ => false |
847 | _ => false |
867 |
848 |
868 *} |
849 *} |
869 |
850 |
870 ML {* |
851 ML {* |
871 fun APPLY_RSP_TAC rty = |
852 fun APPLY_RSP_TAC rty = |
872 Subgoal.FOCUS (fn {concl, ...} => |
853 Subgoal.FOCUS (fn {concl, ...} => |
873 case (term_of concl) of |
854 case (stripped_term_of concl) of |
874 (_ $ (R $ (f $ _) $ (_ $ _))) => |
855 (_ $ (f $ _) $ (_ $ _)) => |
875 let |
856 let |
876 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
857 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
877 val insts = Thm.match (pat, concl) |
858 val insts = Thm.match (pat, concl) |
878 in |
859 in |
879 if needs_lift rty (fastype_of f) |
860 if needs_lift rty (fastype_of f) |
919 |
900 |
920 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
901 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
921 NDT ctxt "2" (lambda_res_tac ctxt), |
902 NDT ctxt "2" (lambda_res_tac ctxt), |
922 |
903 |
923 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
904 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
924 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
905 NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
925 |
906 |
926 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
907 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
927 DT ctxt "4" (ball_rsp_tac ctxt), |
908 NDT ctxt "4" (ball_rsp_tac ctxt), |
928 |
909 |
929 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
910 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
930 NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
911 NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
931 |
912 |
932 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
913 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
962 |
943 |
963 (* seems not necessay:: NDT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*) |
944 (* seems not necessay:: NDT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*) |
964 |
945 |
965 (* (R1 ===> R2) (\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
946 (* (R1 ===> R2) (\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
966 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
947 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
967 NDT ctxt "G" (weak_lambda_res_tac ctxt), |
948 (*NDT ctxt "G" (weak_lambda_res_tac ctxt),*) |
968 |
949 |
969 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
950 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
970 (* global simplification *) |
951 (* global simplification *) |
971 NDT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
952 NDT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
972 *} |
953 *} |