1090 (* TODO don't know how to handle ho_respects *) |
1090 (* TODO don't know how to handle ho_respects *) |
1091 apply (simp only: FUN_REL.simps) |
1091 apply (simp only: FUN_REL.simps) |
1092 apply (rule allI) |
1092 apply (rule allI) |
1093 apply (rule allI) |
1093 apply (rule allI) |
1094 apply (rule impI) |
1094 apply (rule impI) |
1095 ML_prf {* |
|
1096 val concl = (#concl o fst) (Subgoal.focus @{context} 1 (Isar.goal ())); |
|
1097 val pat = Drule.strip_imp_concl (cprop_of @{thm RES_FORALL_RSP}); |
|
1098 val ((_,p),(_,c)) = (Thm.dest_comb pat, Thm.dest_comb concl); |
|
1099 val ((_,p),(_,c)) = (Thm.dest_comb p, Thm.dest_comb c); |
|
1100 *} |
|
1101 ML_prf {* |
|
1102 val ((_,pn),(_,cn)) = (Thm.dest_comb p, Thm.dest_comb c); |
|
1103 val (pnm, cnm) = (@{cpat "?a"}, @{cterm "b::('a List.list \<Rightarrow> bool)"}); |
|
1104 val (pp, cc) = (term_of pn, term_of cn); |
|
1105 val (ppt, cct) = (type_of pp, type_of cc); |
|
1106 val (ppm, ccm) = (term_of pnm, term_of cnm); |
|
1107 val i = Pattern.first_order_match @{theory} (ppm, ccm) (Vartab.empty, Vartab.empty); |
|
1108 val (ppmt, ccmt) = (type_of ppm, type_of ccm); |
|
1109 val ii = Sign.typ_match @{theory} (ppmt, cct) (Vartab.empty); |
|
1110 val ii = Sign.typ_match @{theory} (ppt, cct) (Vartab.empty); |
|
1111 *} |
|
1112 . |
|
1113 val pat = Drule.strip_imp_concl (cprop_of thm) |
|
1114 val insts = Thm.match (pat, concl) |
|
1115 |
|
1116 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *}) |
1095 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *}) |
1117 thm RES_FORALL_RSP |
1096 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1118 apply (rule_tac RES_FORALL_RSP) |
1097 apply (simp only: FUN_REL.simps) |
1119 |
|
1120 prefer 2 |
|
1121 (* ABS_REP_RSP *) |
1098 (* ABS_REP_RSP *) |
1122 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1099 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1123 (* LAMBDA_RSP *) |
1100 (* LAMBDA_RSP *) |
1124 apply (simp only: FUN_REL.simps) |
1101 apply (simp only: FUN_REL.simps) |
1125 apply (rule allI) |
1102 apply (rule allI) |
1166 apply (rule impI) |
1143 apply (rule impI) |
1167 apply (rule cons_preserves) |
1144 apply (rule cons_preserves) |
1168 apply (assumption) |
1145 apply (assumption) |
1169 apply (simp) |
1146 apply (simp) |
1170 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1147 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1171 prefer 2 |
1148 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1172 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1149 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1173 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1150 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1174 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1175 prefer 2 |
|
1176 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1177 apply (simp only: FUN_REL.simps) |
1151 apply (simp only: FUN_REL.simps) |
1178 apply (rule allI) |
1152 apply (rule allI) |
1179 apply (rule allI) |
1153 apply (rule allI) |
1180 apply (rule impI) |
1154 apply (rule impI) |
|
1155 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *}) |
|
1156 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1157 apply (simp only: FUN_REL.simps) |
|
1158 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1159 apply (simp only: FUN_REL.simps) |
|
1160 apply (rule allI) |
|
1161 apply (rule allI) |
|
1162 apply (rule impI) |
1181 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1163 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1182 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1164 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1183 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1165 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1184 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 *}) |
1185 apply (simp add: FUN_REL.simps) |
1167 apply (simp add: FUN_REL.simps) |
1186 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1168 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1187 sorry |
1169 apply (simp only: FUN_REL.simps) |
|
1170 apply (rule allI) |
|
1171 apply (rule allI) |
|
1172 apply (rule impI) |
|
1173 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *}) |
|
1174 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1175 apply (simp only: FUN_REL.simps) |
|
1176 done |
1188 |
1177 |
1189 prove list_induct_t: trm |
1178 prove list_induct_t: trm |
1190 apply (simp only: list_induct_tr[symmetric]) |
1179 apply (simp only: list_induct_tr[symmetric]) |
1191 apply (tactic {* rtac thm 1 *}) |
1180 apply (tactic {* rtac thm 1 *}) |
1192 done |
1181 done |