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 (* FIXME: they should be in in the new Isabelle *) |
491 lemma [mono]: |
492 lemma [mono]: |
492 "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)" |
493 "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)" |
493 by blast |
494 by blast |
494 |
495 |
495 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P" |
496 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P" |
809 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
810 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
810 shows "(R1 ===> R2) f g" |
811 shows "(R1 ===> R2) f g" |
811 using a by (simp add: FUN_REL.simps) |
812 using a by (simp add: FUN_REL.simps) |
812 |
813 |
813 ML {* |
814 ML {* |
814 val LAMBDA_RES_TAC = |
815 val lambda_res_tac = |
815 Subgoal.FOCUS (fn {concl, ...} => |
816 Subgoal.FOCUS (fn {concl, ...} => |
816 case (term_of concl) of |
817 case (term_of concl) of |
817 (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
818 (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
818 | _ => no_tac) |
819 | _ => no_tac) |
819 *} |
820 *} |
820 |
821 |
821 ML {* |
822 ML {* |
822 val WEAK_LAMBDA_RES_TAC = |
823 val weak_lambda_res_tac = |
823 Subgoal.FOCUS (fn {concl, ...} => |
824 Subgoal.FOCUS (fn {concl, ...} => |
824 case (term_of concl) of |
825 case (term_of concl) of |
825 (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
826 (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
826 | (_ $ (_ $ (Abs _) $ _)) => rtac @{thm FUN_REL_I} 1 |
827 | (_ $ (_ $ (Abs _) $ _)) => rtac @{thm FUN_REL_I} 1 |
827 | _ => no_tac) |
828 | _ => no_tac) |
829 |
830 |
830 ML {* |
831 ML {* |
831 val ball_rsp_tac = |
832 val ball_rsp_tac = |
832 Subgoal.FOCUS (fn {concl, ...} => |
833 Subgoal.FOCUS (fn {concl, ...} => |
833 case (term_of concl) of |
834 case (term_of concl) of |
834 (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) => |
835 (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) |
|
836 $ (Const (@{const_name Ball}, _) $ _))) => |
835 rtac @{thm FUN_REL_I} 1 |
837 rtac @{thm FUN_REL_I} 1 |
836 |_ => no_tac) |
838 |_ => no_tac) |
837 *} |
839 *} |
838 |
840 |
839 ML {* |
841 ML {* |
840 val bex_rsp_tac = |
842 val bex_rsp_tac = |
841 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
843 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
842 case (term_of concl) of |
844 case (term_of concl) of |
843 (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) => |
845 (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) |
|
846 $ (Const (@{const_name Bex}, _) $ _))) => |
844 rtac @{thm FUN_REL_I} 1 |
847 rtac @{thm FUN_REL_I} 1 |
845 | _ => no_tac) |
848 | _ => no_tac) |
846 *} |
849 *} |
847 |
850 |
848 ML {* (* Legacy *) |
851 ML {* (* Legacy *) |
875 *} |
878 *} |
876 |
879 |
877 ML {* |
880 ML {* |
878 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
881 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
879 (FIRST' [resolve_tac trans2, |
882 (FIRST' [resolve_tac trans2, |
880 LAMBDA_RES_TAC ctxt, |
883 lambda_res_tac ctxt, |
881 rtac @{thm RES_FORALL_RSP}, |
884 rtac @{thm RES_FORALL_RSP}, |
882 ball_rsp_tac ctxt, |
885 ball_rsp_tac ctxt, |
883 rtac @{thm RES_EXISTS_RSP}, |
886 rtac @{thm RES_EXISTS_RSP}, |
884 bex_rsp_tac ctxt, |
887 bex_rsp_tac ctxt, |
885 resolve_tac rsp_thms, |
888 resolve_tac rsp_thms, |
890 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])), |
893 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])), |
891 Cong_Tac.cong_tac @{thm cong}, |
894 Cong_Tac.cong_tac @{thm cong}, |
892 rtac @{thm ext}, |
895 rtac @{thm ext}, |
893 resolve_tac rel_refl, |
896 resolve_tac rel_refl, |
894 atac, |
897 atac, |
895 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
898 (*seems not necessary:: SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),*) |
896 WEAK_LAMBDA_RES_TAC ctxt, |
899 weak_lambda_res_tac ctxt, |
897 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))]) |
900 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))]) |
898 |
901 |
899 fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
902 fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
900 REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms) |
903 REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms) |
901 *} |
904 *} |
903 (* |
906 (* |
904 To prove that the regularised theorem implies the abs/rep injected, |
907 To prove that the regularised theorem implies the abs/rep injected, |
905 we try: |
908 we try: |
906 |
909 |
907 1) theorems 'trans2' from the appropriate QUOT_TYPE |
910 1) theorems 'trans2' from the appropriate QUOT_TYPE |
908 2) remove lambdas from both sides: LAMBDA_RES_TAC |
911 2) remove lambdas from both sides: lambda_res_tac |
909 3) remove Ball/Bex from the right hand side |
912 3) remove Ball/Bex from the right hand side |
910 4) use user-supplied RSP theorems |
913 4) use user-supplied RSP theorems |
911 5) remove rep_abs from the right side |
914 5) remove rep_abs from the right side |
912 6) reflexivity of equality |
915 6) reflexivity of equality |
913 7) split applications of lifted type (apply_rsp) |
916 7) split applications of lifted type (apply_rsp) |
927 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 = |
928 (FIRST' [ |
931 (FIRST' [ |
929 (K (print_tac "start")) THEN' (K no_tac), |
932 (K (print_tac "start")) THEN' (K no_tac), |
930 |
933 |
931 (* "cong" rule of the of the relation *) |
934 (* "cong" rule of the of the relation *) |
932 (* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> (a \<approx> b) = (c \<approx> d) *) |
935 (* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> a \<approx> b = c \<approx> d *) |
933 DT ctxt "1" (resolve_tac trans2), |
936 DT ctxt "1" (resolve_tac trans2), |
934 |
937 |
935 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
938 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
936 DT ctxt "2" (LAMBDA_RES_TAC ctxt), |
939 DT ctxt "2" (lambda_res_tac ctxt), |
937 |
940 |
938 (* = (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *) |
941 (* = (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *) |
939 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
942 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
940 |
943 |
941 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
944 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
945 DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
948 DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
946 |
949 |
947 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
950 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
948 DT ctxt "6" (bex_rsp_tac ctxt), |
951 DT ctxt "6" (bex_rsp_tac ctxt), |
949 |
952 |
950 (* respectfulness of ops *) |
953 (* respectfulness of constants *) |
951 DT ctxt "7" (resolve_tac rsp_thms), |
954 DT ctxt "7" (resolve_tac rsp_thms), |
952 |
955 |
953 (* reflexivity of operators arising from Cong_tac *) |
956 (* reflexivity of operators arising from Cong_tac *) |
954 DT ctxt "8" (rtac @{thm refl}), |
957 DT ctxt "8" (rtac @{thm refl}), |
955 |
958 |
972 DT ctxt "D" (resolve_tac rel_refl), |
975 DT ctxt "D" (resolve_tac rel_refl), |
973 |
976 |
974 (* resolving with R x y assumptions *) |
977 (* resolving with R x y assumptions *) |
975 DT ctxt "E" (atac), |
978 DT ctxt "E" (atac), |
976 |
979 |
977 DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
980 (* seems not necessay:: DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*) |
978 DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt), |
981 DT ctxt "G" (weak_lambda_res_tac ctxt), |
|
982 |
|
983 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed to apply respectfulness theorems *) |
|
984 (* works globally *) |
979 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
985 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
980 |
986 |
981 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
987 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
982 REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms) |
988 REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms) |
983 *} |
989 *} |
984 |
990 |
985 ML {* |
|
986 fun get_inj_repabs_tac ctxt rel lhs rhs = |
|
987 let |
|
988 val _ = tracing "input" |
|
989 val _ = tracing ("rel: " ^ Syntax.string_of_term ctxt rel) |
|
990 val _ = tracing ("lhs: " ^ Syntax.string_of_term ctxt lhs) |
|
991 val _ = tracing ("rhs: " ^ Syntax.string_of_term ctxt rhs) |
|
992 in |
|
993 case (rel, lhs, rhs) of |
|
994 (_, l, Const _ $ (Const _ $ r)) (* FIXME: not right_match *) |
|
995 => rtac @{thm REP_ABS_RSP(1)} |
|
996 | (_, Const (@{const_name "Ball"}, _) $ _, |
|
997 Const (@{const_name "Ball"}, _) $ _) |
|
998 => rtac @{thm RES_FORALL_RSP} |
|
999 | _ => K no_tac |
|
1000 end |
|
1001 *} |
|
1002 |
|
1003 ML {* |
|
1004 fun inj_repabs_tac ctxt = |
|
1005 SUBGOAL (fn (goal, i) => |
|
1006 (case (HOLogic.dest_Trueprop goal) of |
|
1007 (rel $ lhs $ rhs) => get_inj_repabs_tac ctxt rel lhs rhs |
|
1008 | _ => K no_tac) i) |
|
1009 *} |
|
1010 |
991 |
1011 section {* Cleaning of the theorem *} |
992 section {* Cleaning of the theorem *} |
1012 |
993 |
1013 ML {* |
994 ML {* |
1014 fun applic_prs lthy absrep (rty, qty) = |
995 fun applic_prs lthy absrep (rty, qty) = |