1016 let |
1016 let |
1017 val pat = Drule.strip_imp_concl (cprop_of thm) |
1017 val pat = Drule.strip_imp_concl (cprop_of thm) |
1018 val insts = Thm.match (pat, concl) |
1018 val insts = Thm.match (pat, concl) |
1019 in |
1019 in |
1020 rtac (Drule.instantiate insts thm) 1 |
1020 rtac (Drule.instantiate insts thm) 1 |
1021 end) |
1021 end |
1022 *} |
1022 handle _ => no_tac |
1023 |
1023 ) |
|
1024 *} |
|
1025 |
|
1026 ML {* |
|
1027 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm = |
|
1028 (FIRST' [ |
|
1029 rtac @{thm FUN_QUOTIENT}, |
|
1030 rtac quot_thm, |
|
1031 rtac @{thm IDENTITY_QUOTIENT}, |
|
1032 rtac @{thm card1_rsp}, |
|
1033 rtac @{thm ext}, |
|
1034 rtac trans_thm, |
|
1035 instantiate_tac @{thm REP_ABS_RSP(1)} ctxt, |
|
1036 instantiate_tac @{thm APPLY_RSP} ctxt, |
|
1037 rtac reflex_thm, |
|
1038 Cong_Tac.cong_tac @{thm cong}, |
|
1039 atac |
|
1040 ]) |
|
1041 *} |
|
1042 |
|
1043 ML {* |
|
1044 fun r_mk_comb_tac_fset ctxt = |
|
1045 r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
|
1046 *} |
1024 |
1047 |
1025 |
1048 |
1026 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
1049 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
1027 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1050 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1028 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1051 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1029 |
1052 |
1030 prove list_induct_tr: trm_r |
1053 prove list_induct_tr: trm_r |
1031 apply (atomize(full)) |
1054 apply (atomize(full)) |
1032 apply (simp only: id_def[symmetric]) |
1055 apply (simp only: id_def[symmetric]) |
1033 (* APPLY_RSP_TAC *) |
1056 (* APPLY_RSP_TAC *) |
1034 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
1057 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1035 apply (rule FUN_QUOTIENT) |
1058 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1036 apply (rule FUN_QUOTIENT) |
1059 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1037 apply (rule QUOTIENT_fset) |
|
1038 apply (rule IDENTITY_QUOTIENT) |
|
1039 apply (rule IDENTITY_QUOTIENT) |
|
1040 apply (rule IDENTITY_QUOTIENT) |
|
1041 prefer 2 |
1060 prefer 2 |
1042 (* ABS_REP_RSP_TAC *) |
1061 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1043 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1062 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1044 apply (rule FUN_QUOTIENT) |
|
1045 apply (rule FUN_QUOTIENT) |
|
1046 apply (rule QUOTIENT_fset) |
|
1047 apply (rule IDENTITY_QUOTIENT) |
|
1048 apply (rule IDENTITY_QUOTIENT) |
|
1049 (* LAMBDA_RES_TAC *) |
1063 (* LAMBDA_RES_TAC *) |
1050 apply (simp only: FUN_REL.simps) |
1064 apply (simp only: FUN_REL.simps) |
1051 apply (rule allI) |
1065 apply (rule allI) |
1052 apply (rule allI) |
1066 apply (rule allI) |
1053 apply (rule impI) |
1067 apply (rule impI) |
1062 (* MK_COMB_TAC *) |
1076 (* MK_COMB_TAC *) |
1063 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1077 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1064 (* REFL_TAC *) |
1078 (* REFL_TAC *) |
1065 apply (simp) |
1079 apply (simp) |
1066 (* APPLY_RSP_TAC *) |
1080 (* APPLY_RSP_TAC *) |
1067 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
1081 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1068 apply (rule QUOTIENT_fset) |
1082 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1069 apply (rule IDENTITY_QUOTIENT) |
1083 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1070 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1084 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1071 apply (rule FUN_QUOTIENT) |
|
1072 apply (rule QUOTIENT_fset) |
|
1073 apply (rule IDENTITY_QUOTIENT) |
|
1074 apply (simp only: FUN_REL.simps) |
1085 apply (simp only: FUN_REL.simps) |
1075 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1086 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1076 apply (rule QUOTIENT_fset) |
1087 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1077 (* MINE *) |
1088 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1078 apply (rule list_eq_refl ) |
1089 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1079 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
|
1080 apply (rule FUN_QUOTIENT) |
|
1081 apply (rule QUOTIENT_fset) |
|
1082 apply (rule IDENTITY_QUOTIENT) |
|
1083 apply (rule IDENTITY_QUOTIENT) |
|
1084 (* TODO don't know how to handle ho_respects *) |
1090 (* TODO don't know how to handle ho_respects *) |
1085 prefer 2 |
1091 prefer 2 |
1086 (* ABS_REP_RSP *) |
1092 (* ABS_REP_RSP *) |
1087 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1093 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1088 apply (rule FUN_QUOTIENT) |
|
1089 apply (rule QUOTIENT_fset) |
|
1090 apply (rule IDENTITY_QUOTIENT) |
|
1091 (* LAMBDA_RSP *) |
1094 (* LAMBDA_RSP *) |
1092 apply (simp only: FUN_REL.simps) |
1095 apply (simp only: FUN_REL.simps) |
1093 apply (rule allI) |
1096 apply (rule allI) |
1094 apply (rule allI) |
1097 apply (rule allI) |
1095 apply (rule impI) |
1098 apply (rule impI) |
1098 (* MK_COMB_TAC *) |
1101 (* MK_COMB_TAC *) |
1099 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1102 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1100 (* REFL_TAC *) |
1103 (* REFL_TAC *) |
1101 apply (simp) |
1104 apply (simp) |
1102 (* APPLY_RSP *) |
1105 (* APPLY_RSP *) |
1103 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
1106 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1104 apply (rule QUOTIENT_fset) |
1107 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1105 apply (rule IDENTITY_QUOTIENT) |
1108 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1106 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1109 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1107 apply (rule FUN_QUOTIENT) |
|
1108 apply (rule QUOTIENT_fset) |
|
1109 apply (rule IDENTITY_QUOTIENT) |
|
1110 (* MINE *) |
1110 (* MINE *) |
1111 apply (simp only: FUN_REL.simps) |
1111 apply (simp only: FUN_REL.simps) |
1112 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1112 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1113 apply (rule QUOTIENT_fset) |
|
1114 (* FIRST_ASSUM MATCH_ACCEPT_TAC *) |
|
1115 apply (assumption) |
|
1116 (* MK_COMB_TAC *) |
1113 (* MK_COMB_TAC *) |
1117 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1114 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1118 (* REFL_TAC *) |
1115 (* REFL_TAC *) |
1119 apply (simp) |
1116 apply (simp) |
1120 (* W(C (curry op THEN) (G... *) |
1117 (* W(C (curry op THEN) (G... *) |
1121 apply (rule ext) |
1118 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1122 (* APPLY_RSP *) |
1119 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1123 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
1120 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1124 apply (rule QUOTIENT_fset) |
1121 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1125 apply (rule IDENTITY_QUOTIENT) |
1122 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1126 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
|
1127 apply (rule FUN_QUOTIENT) |
|
1128 apply (rule QUOTIENT_fset) |
|
1129 apply (rule IDENTITY_QUOTIENT) |
|
1130 apply (simp only: FUN_REL.simps) |
1123 apply (simp only: FUN_REL.simps) |
1131 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1124 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1132 apply (rule QUOTIENT_fset) |
1125 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1133 (* APPLY_RSP *) |
1126 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1134 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
1127 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1135 apply (rule QUOTIENT_fset) |
1128 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1136 apply (rule QUOTIENT_fset) |
1129 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1137 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
1130 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1138 apply (rule IDENTITY_QUOTIENT) |
1131 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1139 apply (rule FUN_QUOTIENT) |
|
1140 apply (rule QUOTIENT_fset) |
|
1141 apply (rule QUOTIENT_fset) |
|
1142 (* CONS respects *) |
1132 (* CONS respects *) |
1143 apply (simp add: FUN_REL.simps) |
1133 apply (simp add: FUN_REL.simps) |
1144 apply (rule allI) |
1134 apply (rule allI) |
1145 apply (rule allI) |
1135 apply (rule allI) |
1146 apply (rule allI) |
1136 apply (rule allI) |
1147 apply (rule impI) |
1137 apply (rule impI) |
1148 apply (rule cons_preserves) |
1138 apply (rule cons_preserves) |
1149 apply (assumption) |
1139 apply (assumption) |
1150 apply (simp) |
1140 apply (simp) |
1151 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1141 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1152 apply (rule QUOTIENT_fset) |
|
1153 apply (assumption) |
|
1154 prefer 2 |
1142 prefer 2 |
1155 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
1143 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1156 apply (rule FUN_QUOTIENT) |
1144 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1157 apply (rule QUOTIENT_fset) |
1145 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1158 apply (rule IDENTITY_QUOTIENT) |
|
1159 apply (rule IDENTITY_QUOTIENT) |
|
1160 prefer 2 |
1146 prefer 2 |
1161 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1147 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1162 apply (rule FUN_QUOTIENT) |
|
1163 apply (rule QUOTIENT_fset) |
|
1164 apply (rule IDENTITY_QUOTIENT) |
|
1165 apply (simp only: FUN_REL.simps) |
1148 apply (simp only: FUN_REL.simps) |
1166 apply (rule allI) |
1149 apply (rule allI) |
1167 apply (rule allI) |
1150 apply (rule allI) |
1168 apply (rule impI) |
1151 apply (rule impI) |
1169 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
1152 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1170 apply (rule QUOTIENT_fset) |
1153 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1171 apply (rule IDENTITY_QUOTIENT) |
1154 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1172 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1155 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1173 apply (rule FUN_QUOTIENT) |
|
1174 apply (rule QUOTIENT_fset) |
|
1175 apply (rule IDENTITY_QUOTIENT) |
|
1176 apply (simp add: FUN_REL.simps) |
1156 apply (simp add: FUN_REL.simps) |
1177 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
1157 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1178 apply (rule QUOTIENT_fset) |
|
1179 apply (assumption) |
|
1180 sorry |
1158 sorry |
1181 |
1159 |
1182 prove list_induct_t: trm |
1160 prove list_induct_t: trm |
1183 apply (simp only: list_induct_tr[symmetric]) |
1161 apply (simp only: list_induct_tr[symmetric]) |
1184 apply (tactic {* rtac thm 1 *}) |
1162 apply (tactic {* rtac thm 1 *}) |