796 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
796 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
797 shows "(R1 ===> R2) f g" |
797 shows "(R1 ===> R2) f g" |
798 using a by simp |
798 using a by simp |
799 |
799 |
800 ML {* |
800 ML {* |
801 val lambda_res_tac = |
801 val lambda_rsp_tac = |
802 SUBGOAL (fn (goal, i) => |
802 SUBGOAL (fn (goal, i) => |
803 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
803 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
804 (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i |
804 (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i |
805 | _ => no_tac) |
805 | _ => no_tac) |
806 *} |
806 *} |
807 |
807 |
808 ML {* |
808 ML {* |
809 val weak_lambda_res_tac = |
809 val weak_lambda_rsp_tac = |
810 SUBGOAL (fn (goal, i) => |
810 SUBGOAL (fn (goal, i) => |
811 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
811 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
812 (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} i |
812 (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} i |
813 | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} i |
813 | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} i |
814 | _ => no_tac) |
814 | _ => no_tac) |
866 (* |
866 (* |
867 To prove that the regularised theorem implies the abs/rep injected, |
867 To prove that the regularised theorem implies the abs/rep injected, |
868 we try: |
868 we try: |
869 |
869 |
870 1) theorems 'trans2' from the appropriate QUOT_TYPE |
870 1) theorems 'trans2' from the appropriate QUOT_TYPE |
871 2) remove lambdas from both sides: lambda_res_tac |
871 2) remove lambdas from both sides: lambda_rsp_tac |
872 3) remove Ball/Bex from the right hand side |
872 3) remove Ball/Bex from the right hand side |
873 4) use user-supplied RSP theorems |
873 4) use user-supplied RSP theorems |
874 5) remove rep_abs from the right side |
874 5) remove rep_abs from the right side |
875 6) reflexivity of equality |
875 6) reflexivity of equality |
876 7) split applications of lifted type (apply_rsp) |
876 7) split applications of lifted type (apply_rsp) |
889 definition |
889 definition |
890 "QUOT_TRUE x \<equiv> True" |
890 "QUOT_TRUE x \<equiv> True" |
891 |
891 |
892 lemma quot_true_dests: |
892 lemma quot_true_dests: |
893 shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
893 shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
894 and QT_appL: "QUOT_TRUE (A B) \<Longrightarrow> QUOT_TRUE A" |
894 and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P" |
895 and QT_appR: "QUOT_TRUE (A B) \<Longrightarrow> QUOT_TRUE B" |
|
896 and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
895 and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
897 apply(simp_all add: QUOT_TRUE_def) |
896 and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)" |
|
897 apply(simp_all add: QUOT_TRUE_def ext) |
898 done |
898 done |
899 |
899 |
900 lemma QUOT_TRUE_i: "(QUOT_TRUE a \<Longrightarrow> P) \<Longrightarrow> P" |
900 lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P" |
901 by (simp add: QUOT_TRUE_def) |
901 by (simp add: QUOT_TRUE_def) |
902 |
902 |
903 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<Longrightarrow> QUOT_TRUE b" |
903 lemma QUOT_TRUE_imp: "QUOT_TRUE a" |
904 by (simp add: QUOT_TRUE_def) |
904 by (simp add: QUOT_TRUE_def) |
905 |
905 |
906 ML {* |
906 ML {* |
907 fun quot_true_tac ctxt fnctn = |
907 fun quot_true_tac ctxt fnctn = |
908 SUBGOAL (fn (gl, i) => |
908 CSUBGOAL (fn (cgl, i) => |
909 let |
909 let |
|
910 val gl = term_of cgl; |
910 val thy = ProofContext.theory_of ctxt; |
911 val thy = ProofContext.theory_of ctxt; |
911 fun find_fun trm = |
912 fun find_fun trm = |
912 case trm of |
913 case trm of |
913 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true |
914 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true |
914 | _ => false |
915 | _ => false |
915 in |
916 in |
916 case find_first find_fun (Logic.strip_assums_hyp gl) of |
917 case find_first find_fun (Logic.strip_assums_hyp gl) of |
917 SOME (_ $ (_ $ x)) => |
918 SOME (_ $ (_ $ x)) => |
918 let |
919 let |
|
920 val thm' = Thm.lift_rule cgl @{thm QUOT_TRUE_imp} |
|
921 val ps = Logic.strip_params (Thm.concl_of thm'); |
919 val fx = fnctn x; |
922 val fx = fnctn x; |
920 val ctrm1 = cterm_of thy x; |
923 val (_ $ (_ $ fx')) = Logic.strip_assums_concl (prop_of thm'); |
921 val cty1 = ctyp_of thy (fastype_of x); |
924 val insts = [(fx', fx)] |
922 val ctrm2 = cterm_of thy fx; |
925 |> map (fn (t, u) => (cterm_of thy (Term.head_of t), cterm_of thy (Term.list_abs (ps, u)))); |
923 val cty2 = ctyp_of thy (fastype_of fx); |
926 val thm_i = Drule.cterm_instantiate insts thm' |
924 val thm = Drule.instantiate' [SOME cty1, SOME cty2] [SOME ctrm1, SOME ctrm2] @{thm QUOT_TRUE_imp} |
927 val thm_j = Thm.forall_elim_vars 1 thm_i |
925 in |
928 in |
926 dtac thm i |
929 dtac thm_j i |
927 end |
930 end |
928 | NONE => error "quot_true_tac!" |
931 | NONE => error "quot_true_tac!" |
929 | _ => error "quot_true_tac!!" |
932 | _ => error "quot_true_tac!!" |
930 end) |
933 end) |
931 *} |
934 *} |
|
935 |
|
936 |
|
937 ML {* fun dest_comb (f $ a) = (f, a) *} |
|
938 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *} |
|
939 ML {* fun unlam (Abs a) = snd (Term.dest_abs a) *} |
932 |
940 |
933 ML {* |
941 ML {* |
934 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
942 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
935 (FIRST' [ |
943 (FIRST' [ |
936 (* "cong" rule of the of the relation / transitivity*) |
944 (* "cong" rule of the of the relation / transitivity*) |
937 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
945 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
938 DT ctxt "1" (resolve_tac trans2), |
946 DT ctxt "1" (resolve_tac trans2), |
939 |
947 |
940 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
948 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
941 NDT ctxt "2" (lambda_res_tac), |
949 NDT ctxt "2" (lambda_rsp_tac), |
942 |
950 |
943 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
951 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
944 NDT ctxt "3" (rtac @{thm ball_rsp}), |
952 NDT ctxt "3" (rtac @{thm ball_rsp}), |
945 |
953 |
946 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
954 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
985 (* global simplification *) |
993 (* global simplification *) |
986 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
994 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
987 *} |
995 *} |
988 |
996 |
989 ML {* |
997 ML {* |
|
998 fun inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 = |
|
999 (FIRST' [ |
|
1000 (* "cong" rule of the of the relation / transitivity*) |
|
1001 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
|
1002 DT ctxt "1" (resolve_tac trans2), |
|
1003 |
|
1004 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
|
1005 NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam), |
|
1006 |
|
1007 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
|
1008 NDT ctxt "3" (rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}), |
|
1009 |
|
1010 (* R2 is always equality *) |
|
1011 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
|
1012 NDT ctxt "4" (ball_rsp_tac THEN' quot_true_tac ctxt unlam), |
|
1013 |
|
1014 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
|
1015 NDT ctxt "5" (rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}), |
|
1016 |
|
1017 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
|
1018 NDT ctxt "6" (bex_rsp_tac THEN' dtac @{thm QT_ext}), |
|
1019 |
|
1020 (* respectfulness of constants *) |
|
1021 NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)), |
|
1022 |
|
1023 (* reflexivity of operators arising from Cong_tac *) |
|
1024 NDT ctxt "8" (rtac @{thm refl}), |
|
1025 |
|
1026 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
|
1027 (* observe ---> *) |
|
1028 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt |
|
1029 THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))), |
|
1030 |
|
1031 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
|
1032 NDT ctxt "A" (APPLY_RSP_TAC rty ctxt THEN' |
|
1033 (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms), |
|
1034 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
|
1035 |
|
1036 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
|
1037 (* merge with previous tactic *) |
|
1038 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
|
1039 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
|
1040 |
|
1041 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
|
1042 NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
|
1043 |
|
1044 (* reflexivity of the basic relations *) |
|
1045 (* R \<dots> \<dots> *) |
|
1046 NDT ctxt "D" (resolve_tac rel_refl), |
|
1047 |
|
1048 (* resolving with R x y assumptions *) |
|
1049 NDT ctxt "E" (atac), |
|
1050 |
|
1051 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
|
1052 (* global simplification *) |
|
1053 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
|
1054 *} |
|
1055 |
|
1056 ML {* |
990 fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
1057 fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
991 REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2) |
1058 REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2) |
992 *} |
1059 *} |
993 |
|
994 |
1060 |
995 section {* Cleaning of the theorem *} |
1061 section {* Cleaning of the theorem *} |
996 |
1062 |
997 |
1063 |
998 (* TODO: This is slow *) |
1064 (* TODO: This is slow *) |
1204 THEN' gen_frees_tac lthy |
1270 THEN' gen_frees_tac lthy |
1205 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1271 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1206 let |
1272 let |
1207 val rthm' = atomize_thm rthm |
1273 val rthm' = atomize_thm rthm |
1208 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1274 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
|
1275 val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i} |
1209 in |
1276 in |
1210 EVERY1 [rtac rule, rtac rthm'] |
1277 EVERY1 [rtac rule, rtac rthm'] THEN RANGE [(fn _ => all_tac), rtac thm] 1 |
1211 end) lthy |
1278 end) lthy |
1212 *} |
1279 *} |
1213 |
|
1214 thm EQUIV_REFL |
|
1215 thm equiv_trans2 |
|
1216 |
1280 |
1217 ML {* |
1281 ML {* |
1218 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1282 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1219 fun lift_tac lthy rthm rel_eqv rty quot defs = |
1283 fun lift_tac lthy rthm rel_eqv rty quot defs = |
1220 ObjectLogic.full_atomize_tac |
1284 ObjectLogic.full_atomize_tac |