954 (* TODO: Can this be done easier? *) |
954 (* TODO: Can this be done easier? *) |
955 ML {* |
955 ML {* |
956 fun unlam t = |
956 fun unlam t = |
957 case t of |
957 case t of |
958 (Abs a) => snd (Term.dest_abs a) |
958 (Abs a) => snd (Term.dest_abs a) |
959 | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) *} |
959 | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) |
960 |
|
961 |
|
962 ML {* |
|
963 fun inj_repabs_tac ctxt rel_refl trans2 = |
|
964 (FIRST' [ |
|
965 (* "cong" rule of the of the relation / transitivity*) |
|
966 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
|
967 NDT ctxt "1" (resolve_tac trans2 THEN' RANGE [ |
|
968 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]), |
|
969 |
|
970 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
|
971 NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam), |
|
972 |
|
973 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
|
974 NDT ctxt "3" (rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}), |
|
975 |
|
976 (* R2 is always equality *) |
|
977 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
|
978 NDT ctxt "4" (ball_rsp_tac THEN' quot_true_tac ctxt unlam), |
|
979 |
|
980 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
|
981 NDT ctxt "5" (rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}), |
|
982 |
|
983 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
|
984 NDT ctxt "6" (bex_rsp_tac THEN' dtac @{thm QT_ext}), |
|
985 |
|
986 (* respectfulness of constants *) |
|
987 NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)), |
|
988 |
|
989 (* reflexivity of operators arising from Cong_tac *) |
|
990 NDT ctxt "8" (rtac @{thm refl}), |
|
991 |
|
992 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
|
993 (* observe ---> *) |
|
994 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt |
|
995 THEN' (RANGE [SOLVES' (quotient_tac ctxt)]))), |
|
996 |
|
997 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
|
998 NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN' |
|
999 (RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt), |
|
1000 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
|
1001 |
|
1002 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
|
1003 (* merge with previous tactic *) |
|
1004 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
|
1005 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
|
1006 |
|
1007 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
|
1008 NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
|
1009 |
|
1010 (* reflexivity of the basic relations *) |
|
1011 (* R \<dots> \<dots> *) |
|
1012 NDT ctxt "D" (resolve_tac rel_refl), |
|
1013 |
|
1014 (* resolving with R x y assumptions *) |
|
1015 NDT ctxt "E" (atac) |
|
1016 |
|
1017 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
|
1018 (* global simplification *) |
|
1019 (*NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms FUN_REL_EQ LIST_REL_EQ})))*) |
|
1020 ]) |
|
1021 *} |
|
1022 |
|
1023 ML {* |
|
1024 fun all_inj_repabs_tac ctxt rel_refl trans2 = |
|
1025 REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) |
|
1026 *} |
960 *} |
1027 |
961 |
1028 ML {* |
962 ML {* |
1029 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
963 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
1030 | dest_fun_type _ = error "dest_fun_type" |
964 | dest_fun_type _ = error "dest_fun_type" |
1048 end |
982 end |
1049 handle _ => no_tac) |
983 handle _ => no_tac) |
1050 | _ => no_tac) |
984 | _ => no_tac) |
1051 *} |
985 *} |
1052 |
986 |
1053 (* A faster version *) |
987 ML {* |
1054 |
988 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => |
1055 ML {* |
|
1056 fun inj_repabs_tac_fast ctxt trans2 = SUBGOAL (fn (goal, i) => |
|
1057 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
989 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
|
990 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
1058 ((Const (@{const_name FUN_REL}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
991 ((Const (@{const_name FUN_REL}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
1059 => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam |
992 => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam |
|
993 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
1060 | (Const (@{const_name "op ="},_) $ |
994 | (Const (@{const_name "op ="},_) $ |
1061 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
995 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
1062 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
996 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
1063 => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} |
997 => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} |
|
998 (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *) |
1064 | (Const (@{const_name FUN_REL}, _) $ _ $ _) $ |
999 | (Const (@{const_name FUN_REL}, _) $ _ $ _) $ |
1065 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
1000 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
1066 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
1001 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
1067 => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam |
1002 => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam |
|
1003 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
1068 | Const (@{const_name "op ="},_) $ |
1004 | Const (@{const_name "op ="},_) $ |
1069 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
1005 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
1070 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
1006 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
1071 => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} |
1007 => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} |
|
1008 (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *) |
1072 | (Const (@{const_name FUN_REL}, _) $ _ $ _) $ |
1009 | (Const (@{const_name FUN_REL}, _) $ _ $ _) $ |
1073 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
1010 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
1074 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
1011 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
1075 => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam |
1012 => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam |
1076 | Const (@{const_name "op ="},_) $ _ $ _ => |
1013 | Const (@{const_name "op ="},_) $ _ $ _ => |
|
1014 (* reflexivity of operators arising from Cong_tac *) |
1077 rtac @{thm refl} ORELSE' |
1015 rtac @{thm refl} ORELSE' |
1078 (resolve_tac trans2 THEN' RANGE [ |
1016 (resolve_tac trans2 THEN' RANGE [ |
1079 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
1017 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
1080 | _ $ _ $ _ => |
1018 | _ $ _ $ _ => |
|
1019 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
|
1020 (* observe ---> *) |
1081 rep_abs_rsp_tac ctxt |
1021 rep_abs_rsp_tac ctxt |
1082 | _ => error "inj_repabs_tac not a relation" |
1022 | _ => error "inj_repabs_tac not a relation" |
1083 ) i) |
1023 ) i) |
1084 *} |
1024 *} |
1085 |
1025 |
1086 ML {* |
1026 ML {* |
1087 fun inj_repabs_tac' ctxt rel_refl trans2 = |
1027 fun inj_repabs_tac ctxt rel_refl trans2 = |
1088 (FIRST' [ |
1028 (FIRST' [ |
1089 inj_repabs_tac_fast ctxt trans2, |
1029 inj_repabs_tac_match ctxt trans2, |
|
1030 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
1090 NDT ctxt "A" (APPLY_RSP1_TAC' ctxt THEN' |
1031 NDT ctxt "A" (APPLY_RSP1_TAC' ctxt THEN' |
1091 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1032 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
|
1033 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
|
1034 (* merge with previous tactic *) |
1092 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
1035 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
1093 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1036 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
|
1037 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
1094 NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
1038 NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
|
1039 (* resolving with R x y assumptions *) |
1095 NDT ctxt "E" (atac), |
1040 NDT ctxt "E" (atac), |
|
1041 (* reflexivity of the basic relations *) |
|
1042 (* R \<dots> \<dots> *) |
1096 NDT ctxt "D" (resolve_tac rel_refl), |
1043 NDT ctxt "D" (resolve_tac rel_refl), |
|
1044 (* respectfulness of constants *) |
1097 NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)) |
1045 NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)) |
1098 (* NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms FUN_REL_EQ LIST_REL_EQ})))*) |
|
1099 ]) |
1046 ]) |
1100 *} |
1047 *} |
1101 |
1048 |
1102 ML {* |
1049 ML {* |
1103 fun all_inj_repabs_tac' ctxt rel_refl trans2 = |
1050 fun all_inj_repabs_tac ctxt rel_refl trans2 = |
1104 REPEAT_ALL_NEW (inj_repabs_tac' ctxt rel_refl trans2) |
1051 REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) |
1105 *} |
1052 *} |
1106 |
1053 |
1107 |
1054 |
1108 |
1055 |
1109 section {* Cleaning of the theorem *} |
1056 section {* Cleaning of the theorem *} |