1035 |
1035 |
1036 ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) THEN' (fn _ => no_tac)) |
1036 ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) THEN' (fn _ => no_tac)) |
1037 *} |
1037 *} |
1038 |
1038 |
1039 ML {* ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) THEN_ALL_NEW (fn _ => no_tac)) *} |
1039 ML {* ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) THEN_ALL_NEW (fn _ => no_tac)) *} |
|
1040 ML {* RANGE *} |
|
1041 |
|
1042 ML {* |
|
1043 fun quotient_tac quot_thm = |
|
1044 REPEAT_ALL_NEW (FIRST' [ |
|
1045 rtac @{thm FUN_QUOTIENT}, |
|
1046 rtac quot_thm, |
|
1047 rtac @{thm IDENTITY_QUOTIENT} |
|
1048 ]) |
|
1049 *} |
1040 |
1050 |
1041 ML {* |
1051 ML {* |
1042 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm = |
1052 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm = |
1043 (FIRST' [ |
1053 (FIRST' [ |
1044 rtac @{thm FUN_QUOTIENT}, |
1054 rtac @{thm FUN_QUOTIENT}, |
1045 rtac quot_thm, |
1055 rtac quot_thm, |
1046 rtac @{thm IDENTITY_QUOTIENT}, |
1056 rtac @{thm IDENTITY_QUOTIENT}, |
1047 rtac @{thm ext}, |
1057 rtac @{thm ext}, |
1048 rtac trans_thm, |
1058 rtac trans_thm, |
1049 res_forall_rsp_tac ctxt, |
1059 res_forall_rsp_tac ctxt, |
1050 instantiate_tac @{thm REP_ABS_RSP(1)} ctxt, |
1060 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
1051 instantiate_tac @{thm APPLY_RSP} ctxt, |
1061 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
1052 rtac reflex_thm, |
1062 rtac reflex_thm, |
1053 (* Cong_Tac.cong_tac @{thm cong},*) |
|
1054 atac, |
1063 atac, |
1055 ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) THEN_ALL_NEW (fn _ => no_tac)) |
1064 ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) THEN_ALL_NEW (fn _ => no_tac)) |
1056 ]) |
1065 ]) |
1057 *} |
1066 *} |
1058 |
1067 |
1069 prove list_induct_tr: trm_r |
1078 prove list_induct_tr: trm_r |
1070 apply (atomize(full)) |
1079 apply (atomize(full)) |
1071 apply (simp only: id_def[symmetric]) |
1080 apply (simp only: id_def[symmetric]) |
1072 (* APPLY_RSP_TAC *) |
1081 (* APPLY_RSP_TAC *) |
1073 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1082 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1074 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1075 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1083 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1076 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1084 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1077 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1078 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1079 (* LAMBDA_RES_TAC *) |
1085 (* LAMBDA_RES_TAC *) |
1080 apply (simp only: FUN_REL.simps) |
1086 apply (simp only: FUN_REL.simps) |
1081 apply (rule allI) |
1087 apply (rule allI) |
1082 apply (rule allI) |
1088 apply (rule allI) |
1083 apply (rule impI) |
1089 apply (rule impI) |
1094 (* REFL_TAC *) |
1100 (* REFL_TAC *) |
1095 apply (simp) |
1101 apply (simp) |
1096 (* APPLY_RSP_TAC *) |
1102 (* APPLY_RSP_TAC *) |
1097 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1103 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1098 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1104 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1099 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1100 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1105 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1101 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1106 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1102 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1103 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1104 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1105 (* ABS_REP_RSP *) |
|
1106 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1107 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1108 (* LAMBDA_RSP *) |
|
1109 apply (simp only: FUN_REL.simps) |
1107 apply (simp only: FUN_REL.simps) |
1110 apply (rule allI) |
1108 apply (rule allI) |
1111 apply (rule allI) |
1109 apply (rule allI) |
1112 apply (rule impI) |
1110 apply (rule impI) |
1113 (* MK_COMB_TAC *) |
1111 (* MK_COMB_TAC *) |
1117 (* REFL_TAC *) |
1115 (* REFL_TAC *) |
1118 apply (simp) |
1116 apply (simp) |
1119 (* APPLY_RSP *) |
1117 (* APPLY_RSP *) |
1120 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1118 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1121 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1119 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1122 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1123 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1124 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1120 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1125 (* MK_COMB_TAC *) |
1121 (* MK_COMB_TAC *) |
1126 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1122 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1127 (* REFL_TAC *) |
1123 (* REFL_TAC *) |
1128 apply (simp) |
1124 apply (simp) |
1129 (* W(C (curry op THEN) (G... *) |
1125 (* W(C (curry op THEN) (G... *) |
1130 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1126 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1131 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1127 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1132 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1128 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1133 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1129 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1134 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1135 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1130 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1136 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1131 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1137 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1138 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1139 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1140 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1141 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1142 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1143 (* CONS respects *) |
1132 (* CONS respects *) |
1144 apply (simp add: FUN_REL.simps) |
1133 apply (simp add: FUN_REL.simps) |
1145 apply (rule allI) |
1134 apply (rule allI) |
1146 apply (rule allI) |
1135 apply (rule allI) |
1147 apply (rule allI) |
1136 apply (rule allI) |
1151 apply (simp) |
1140 apply (simp) |
1152 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1141 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1153 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1142 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1154 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1143 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1155 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1144 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1156 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1157 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1158 apply (simp only: FUN_REL.simps) |
1145 apply (simp only: FUN_REL.simps) |
1159 apply (rule allI) |
1146 apply (rule allI) |
1160 apply (rule allI) |
1147 apply (rule allI) |
1161 apply (rule impI) |
1148 apply (rule impI) |
1162 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1163 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1164 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1165 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1166 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1149 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1167 done |
1150 done |
1168 |
1151 |
1169 prove list_induct_t: trm |
1152 prove list_induct_t: trm |
1170 apply (simp only: list_induct_tr[symmetric]) |
1153 apply (simp only: list_induct_tr[symmetric]) |