equal
deleted
inserted
replaced
1029 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
1029 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
1030 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
1030 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
1031 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
1031 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
1032 *} |
1032 *} |
1033 |
1033 |
|
1034 ML {* |
|
1035 |
|
1036 ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) THEN' (fn _ => no_tac)) |
|
1037 *} |
|
1038 |
|
1039 ML {* ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) THEN_ALL_NEW (fn _ => no_tac)) *} |
1034 |
1040 |
1035 ML {* |
1041 ML {* |
1036 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm = |
1042 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm = |
1037 (FIRST' [ |
1043 (FIRST' [ |
1038 rtac @{thm FUN_QUOTIENT}, |
1044 rtac @{thm FUN_QUOTIENT}, |
1043 res_forall_rsp_tac ctxt, |
1049 res_forall_rsp_tac ctxt, |
1044 instantiate_tac @{thm REP_ABS_RSP(1)} ctxt, |
1050 instantiate_tac @{thm REP_ABS_RSP(1)} ctxt, |
1045 instantiate_tac @{thm APPLY_RSP} ctxt, |
1051 instantiate_tac @{thm APPLY_RSP} ctxt, |
1046 rtac reflex_thm, |
1052 rtac reflex_thm, |
1047 (* Cong_Tac.cong_tac @{thm cong},*) |
1053 (* Cong_Tac.cong_tac @{thm cong},*) |
1048 atac |
1054 atac, |
|
1055 ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) THEN_ALL_NEW (fn _ => no_tac)) |
1049 ]) |
1056 ]) |
1050 *} |
1057 *} |
1051 |
1058 |
1052 ML {* |
1059 ML {* |
1053 fun r_mk_comb_tac_fset ctxt = |
1060 fun r_mk_comb_tac_fset ctxt = |
1089 (* APPLY_RSP_TAC *) |
1096 (* APPLY_RSP_TAC *) |
1090 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1097 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1091 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 *}) |
1092 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1099 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1093 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1100 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1094 apply (simp only: FUN_REL.simps) |
|
1095 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 *}) |
1096 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1102 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1097 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1103 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1098 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1104 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1099 (* ABS_REP_RSP *) |
1105 (* ABS_REP_RSP *) |
1113 (* APPLY_RSP *) |
1119 (* APPLY_RSP *) |
1114 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1120 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1115 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1121 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1116 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1122 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1117 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1123 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1118 (* MINE *) |
|
1119 apply (simp only: FUN_REL.simps) |
|
1120 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 *}) |
1121 (* MK_COMB_TAC *) |
1125 (* MK_COMB_TAC *) |
1122 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1126 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1123 (* REFL_TAC *) |
1127 (* REFL_TAC *) |
1124 apply (simp) |
1128 apply (simp) |
1126 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1130 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1127 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1131 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1128 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1132 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1129 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1133 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1130 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1134 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1131 apply (simp only: FUN_REL.simps) |
|
1132 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1135 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1133 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1136 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1134 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1137 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1135 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1138 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1136 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1139 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1158 apply (rule impI) |
1161 apply (rule impI) |
1159 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1162 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1160 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1163 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1161 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1164 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
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 (simp add: FUN_REL.simps) |
|
1164 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 *}) |
1165 done |
1167 done |
1166 |
1168 |
1167 prove list_induct_t: trm |
1169 prove list_induct_t: trm |
1168 apply (simp only: list_induct_tr[symmetric]) |
1170 apply (simp only: list_induct_tr[symmetric]) |