equal
deleted
inserted
replaced
1033 rtac @{thm ext}, |
1033 rtac @{thm ext}, |
1034 rtac trans_thm, |
1034 rtac trans_thm, |
1035 instantiate_tac @{thm REP_ABS_RSP(1)} ctxt, |
1035 instantiate_tac @{thm REP_ABS_RSP(1)} ctxt, |
1036 instantiate_tac @{thm APPLY_RSP} ctxt, |
1036 instantiate_tac @{thm APPLY_RSP} ctxt, |
1037 rtac reflex_thm, |
1037 rtac reflex_thm, |
1038 Cong_Tac.cong_tac @{thm cong}, |
1038 (* Cong_Tac.cong_tac @{thm cong},*) |
1039 atac |
1039 atac |
1040 ]) |
1040 ]) |
1041 *} |
1041 *} |
1042 |
1042 |
1043 ML {* |
1043 ML {* |
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 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *}) |
1095 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *}) |
1096 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1097 apply (simp only: FUN_REL.simps) |
1096 apply (simp only: FUN_REL.simps) |
1098 (* ABS_REP_RSP *) |
1097 (* ABS_REP_RSP *) |
1099 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1098 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1100 (* LAMBDA_RSP *) |
1099 (* LAMBDA_RSP *) |
1101 apply (simp only: FUN_REL.simps) |
1100 apply (simp only: FUN_REL.simps) |
1151 apply (simp only: FUN_REL.simps) |
1150 apply (simp only: FUN_REL.simps) |
1152 apply (rule allI) |
1151 apply (rule allI) |
1153 apply (rule allI) |
1152 apply (rule allI) |
1154 apply (rule impI) |
1153 apply (rule impI) |
1155 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *}) |
1154 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) |
1155 apply (simp only: FUN_REL.simps) |
1158 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1156 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1159 apply (simp only: FUN_REL.simps) |
1157 apply (simp only: FUN_REL.simps) |
1160 apply (rule allI) |
1158 apply (rule allI) |
1161 apply (rule allI) |
1159 apply (rule allI) |
1169 apply (simp only: FUN_REL.simps) |
1167 apply (simp only: FUN_REL.simps) |
1170 apply (rule allI) |
1168 apply (rule allI) |
1171 apply (rule allI) |
1169 apply (rule allI) |
1172 apply (rule impI) |
1170 apply (rule impI) |
1173 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *}) |
1171 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) |
1172 apply (simp only: FUN_REL.simps) |
1176 done |
1173 done |
1177 |
1174 |
1178 prove list_induct_t: trm |
1175 prove list_induct_t: trm |
1179 apply (simp only: list_induct_tr[symmetric]) |
1176 apply (simp only: list_induct_tr[symmetric]) |