equal
deleted
inserted
replaced
1022 handle _ => no_tac |
1022 handle _ => no_tac |
1023 ) |
1023 ) |
1024 *} |
1024 *} |
1025 |
1025 |
1026 ML {* |
1026 ML {* |
|
1027 fun res_forall_rsp_tac ctxt = |
|
1028 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
1029 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
1030 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
|
1031 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
1032 *} |
|
1033 |
|
1034 |
|
1035 ML {* |
1027 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm = |
1036 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm = |
1028 (FIRST' [ |
1037 (FIRST' [ |
1029 rtac @{thm FUN_QUOTIENT}, |
1038 rtac @{thm FUN_QUOTIENT}, |
1030 rtac quot_thm, |
1039 rtac quot_thm, |
1031 rtac @{thm IDENTITY_QUOTIENT}, |
1040 rtac @{thm IDENTITY_QUOTIENT}, |
1032 rtac @{thm ext}, |
1041 rtac @{thm ext}, |
1033 rtac trans_thm, |
1042 rtac trans_thm, |
|
1043 res_forall_rsp_tac ctxt, |
1034 instantiate_tac @{thm REP_ABS_RSP(1)} ctxt, |
1044 instantiate_tac @{thm REP_ABS_RSP(1)} ctxt, |
1035 instantiate_tac @{thm APPLY_RSP} ctxt, |
1045 instantiate_tac @{thm APPLY_RSP} ctxt, |
1036 rtac reflex_thm, |
1046 rtac reflex_thm, |
1037 (* Cong_Tac.cong_tac @{thm cong},*) |
1047 (* Cong_Tac.cong_tac @{thm cong},*) |
1038 atac |
1048 atac |
1054 apply (simp only: id_def[symmetric]) |
1064 apply (simp only: id_def[symmetric]) |
1055 (* APPLY_RSP_TAC *) |
1065 (* APPLY_RSP_TAC *) |
1056 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1066 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1057 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1067 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1058 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1068 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1059 apply (simp only: FUN_REL.simps) |
1069 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
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) |
|
1065 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1070 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1066 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1071 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1067 (* LAMBDA_RES_TAC *) |
1072 (* LAMBDA_RES_TAC *) |
1068 apply (simp only: FUN_REL.simps) |
1073 apply (simp only: FUN_REL.simps) |
1069 apply (rule allI) |
1074 apply (rule allI) |
1090 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1095 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1091 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1096 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1092 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1097 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1093 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1098 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1094 (* ABS_REP_RSP *) |
1099 (* ABS_REP_RSP *) |
1095 apply (simp only: FUN_REL.simps) |
1100 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1096 apply (rule allI) |
|
1097 apply (rule allI) |
|
1098 apply (rule impI) |
|
1099 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *}) |
|
1100 apply (simp only: FUN_REL.simps) |
|
1101 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 *}) |
1102 (* LAMBDA_RSP *) |
1102 (* LAMBDA_RSP *) |
1103 apply (simp only: FUN_REL.simps) |
1103 apply (simp only: FUN_REL.simps) |
1104 apply (rule allI) |
1104 apply (rule allI) |
1105 apply (rule allI) |
1105 apply (rule allI) |
1148 apply (simp) |
1148 apply (simp) |
1149 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 *}) |
1150 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1150 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1151 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1151 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1152 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1152 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1153 apply (simp only: FUN_REL.simps) |
1153 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1154 apply (rule allI) |
|
1155 apply (rule allI) |
|
1156 apply (rule impI) |
|
1157 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *}) |
|
1158 apply (simp only: FUN_REL.simps) |
|
1159 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1154 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1160 apply (simp only: FUN_REL.simps) |
1155 apply (simp only: FUN_REL.simps) |
1161 apply (rule allI) |
1156 apply (rule allI) |
1162 apply (rule allI) |
1157 apply (rule allI) |
1163 apply (rule impI) |
1158 apply (rule impI) |