equal
deleted
inserted
replaced
1027 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm = |
1027 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm = |
1028 (FIRST' [ |
1028 (FIRST' [ |
1029 rtac @{thm FUN_QUOTIENT}, |
1029 rtac @{thm FUN_QUOTIENT}, |
1030 rtac quot_thm, |
1030 rtac quot_thm, |
1031 rtac @{thm IDENTITY_QUOTIENT}, |
1031 rtac @{thm IDENTITY_QUOTIENT}, |
1032 rtac @{thm card1_rsp}, |
1032 rtac @{thm ext}, |
1033 rtac @{thm ext}, |
1033 rtac trans_thm, |
1034 rtac trans_thm, |
|
1035 instantiate_tac @{thm REP_ABS_RSP(1)} ctxt, |
1034 instantiate_tac @{thm REP_ABS_RSP(1)} ctxt, |
1036 instantiate_tac @{thm APPLY_RSP} ctxt, |
1035 instantiate_tac @{thm APPLY_RSP} ctxt, |
1037 rtac reflex_thm, |
1036 rtac reflex_thm, |
1038 (* Cong_Tac.cong_tac @{thm cong},*) |
1037 (* Cong_Tac.cong_tac @{thm cong},*) |
1039 atac |
1038 atac |
1055 apply (simp only: id_def[symmetric]) |
1054 apply (simp only: id_def[symmetric]) |
1056 (* APPLY_RSP_TAC *) |
1055 (* APPLY_RSP_TAC *) |
1057 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1056 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1058 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1057 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1059 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1058 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1060 prefer 2 |
1059 apply (simp only: FUN_REL.simps) |
|
1060 apply (rule allI) |
|
1061 apply (rule allI) |
|
1062 apply (rule impI) |
|
1063 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *}) |
|
1064 apply (simp only: FUN_REL.simps) |
1061 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1065 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1062 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1066 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1063 (* LAMBDA_RES_TAC *) |
1067 (* LAMBDA_RES_TAC *) |
1064 apply (simp only: FUN_REL.simps) |
1068 apply (simp only: FUN_REL.simps) |
1065 apply (rule allI) |
1069 apply (rule allI) |
1085 apply (simp only: FUN_REL.simps) |
1089 apply (simp only: FUN_REL.simps) |
1086 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1090 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1087 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1091 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1088 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1092 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1089 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1093 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1090 (* TODO don't know how to handle ho_respects *) |
1094 (* ABS_REP_RSP *) |
1091 apply (simp only: FUN_REL.simps) |
1095 apply (simp only: FUN_REL.simps) |
1092 apply (rule allI) |
1096 apply (rule allI) |
1093 apply (rule allI) |
1097 apply (rule allI) |
1094 apply (rule impI) |
1098 apply (rule impI) |
1095 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *}) |
1099 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *}) |
1096 apply (simp only: FUN_REL.simps) |
1100 apply (simp only: FUN_REL.simps) |
1097 (* ABS_REP_RSP *) |
|
1098 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 *}) |
1099 (* LAMBDA_RSP *) |
1102 (* LAMBDA_RSP *) |
1100 apply (simp only: FUN_REL.simps) |
1103 apply (simp only: FUN_REL.simps) |
1101 apply (rule allI) |
1104 apply (rule allI) |
1102 apply (rule allI) |
1105 apply (rule allI) |
1162 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1165 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1163 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1166 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1164 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1167 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1165 apply (simp add: FUN_REL.simps) |
1168 apply (simp add: FUN_REL.simps) |
1166 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1169 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1167 apply (simp only: FUN_REL.simps) |
|
1168 apply (rule allI) |
|
1169 apply (rule allI) |
|
1170 apply (rule impI) |
|
1171 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *}) |
|
1172 apply (simp only: FUN_REL.simps) |
|
1173 done |
1170 done |
1174 |
1171 |
1175 prove list_induct_t: trm |
1172 prove list_induct_t: trm |
1176 apply (simp only: list_induct_tr[symmetric]) |
1173 apply (simp only: list_induct_tr[symmetric]) |
1177 apply (tactic {* rtac thm 1 *}) |
1174 apply (tactic {* rtac thm 1 *}) |