883 qed "hypreal_trichotomyE"; |
909 qed "hypreal_trichotomyE"; |
884 |
910 |
885 (*---------------------------------------------------------------------------- |
911 (*---------------------------------------------------------------------------- |
886 More properties of < |
912 More properties of < |
887 ----------------------------------------------------------------------------*) |
913 ----------------------------------------------------------------------------*) |
888 Goal "!!(A::hypreal). A < B ==> A + C < B + C"; |
|
889 by (res_inst_tac [("z","A")] eq_Abs_hypreal 1); |
|
890 by (res_inst_tac [("z","B")] eq_Abs_hypreal 1); |
|
891 by (res_inst_tac [("z","C")] eq_Abs_hypreal 1); |
|
892 by (auto_tac (claset() addSIs [exI],simpset() addsimps |
|
893 [hypreal_less_def,hypreal_add])); |
|
894 by (Ultra_tac 1); |
|
895 qed "hypreal_add_less_mono1"; |
|
896 |
|
897 Goal "!!(A::hypreal). A < B ==> C + A < C + B"; |
|
898 by (auto_tac (claset() addIs [hypreal_add_less_mono1], |
|
899 simpset() addsimps [hypreal_add_commute])); |
|
900 qed "hypreal_add_less_mono2"; |
|
901 |
914 |
902 Goal "((x::hypreal) < y) = (0 < y + -x)"; |
915 Goal "((x::hypreal) < y) = (0 < y + -x)"; |
903 by (Step_tac 1); |
916 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
904 by (dres_inst_tac [("C","-x")] hypreal_add_less_mono1 1); |
917 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
905 by (dres_inst_tac [("C","x")] hypreal_add_less_mono1 2); |
918 by (auto_tac (claset(),simpset() addsimps [hypreal_add, |
906 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
919 hypreal_zero_def,hypreal_minus,hypreal_less])); |
|
920 by (ALLGOALS(Ultra_tac)); |
907 qed "hypreal_less_minus_iff"; |
921 qed "hypreal_less_minus_iff"; |
908 |
922 |
909 Goal "((x::hypreal) < y) = (x + -y< 0)"; |
923 Goal "((x::hypreal) < y) = (x + -y < 0)"; |
910 by (Step_tac 1); |
924 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
911 by (dres_inst_tac [("C","-y")] hypreal_add_less_mono1 1); |
925 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
912 by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 2); |
926 by (auto_tac (claset(),simpset() addsimps [hypreal_add, |
913 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
927 hypreal_zero_def,hypreal_minus,hypreal_less])); |
|
928 by (ALLGOALS(Ultra_tac)); |
914 qed "hypreal_less_minus_iff2"; |
929 qed "hypreal_less_minus_iff2"; |
915 |
930 |
916 Goal "!!(y1 :: hypreal). [| z1 < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2"; |
|
917 by (dtac (hypreal_less_minus_iff RS iffD1) 1); |
|
918 by (dtac (hypreal_less_minus_iff RS iffD1) 1); |
|
919 by (dtac hypreal_add_order 1 THEN assume_tac 1); |
|
920 by (thin_tac "0 < y2 + - z2" 1); |
|
921 by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1); |
|
922 by (auto_tac (claset(),simpset() addsimps |
|
923 [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac)); |
|
924 qed "hypreal_add_less_mono"; |
|
925 |
|
926 Goal "((x::hypreal) = y) = (0 = x + - y)"; |
931 Goal "((x::hypreal) = y) = (0 = x + - y)"; |
927 by Auto_tac; |
932 by Auto_tac; |
928 by (res_inst_tac [("x1","-y")] (hypreal_add_right_cancel RS iffD1) 1); |
933 by (res_inst_tac [("x1","-y")] (hypreal_add_right_cancel RS iffD1) 1); |
929 by Auto_tac; |
934 by Auto_tac; |
930 qed "hypreal_eq_minus_iff"; |
935 qed "hypreal_eq_minus_iff"; |
1039 Goal "[| z <= w; w <= z |] ==> z = (w::hypreal)"; |
1072 Goal "[| z <= w; w <= z |] ==> z = (w::hypreal)"; |
1040 by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq, |
1073 by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq, |
1041 fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym])]); |
1074 fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym])]); |
1042 qed "hypreal_le_anti_sym"; |
1075 qed "hypreal_le_anti_sym"; |
1043 |
1076 |
1044 Goal "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y"; |
|
1045 by (auto_tac (claset() addDs [sym,hypreal_le_imp_less_or_eq] |
|
1046 addIs [hypreal_add_order],simpset())); |
|
1047 qed "hypreal_add_order_le"; |
|
1048 |
|
1049 (*------------------------------------------------------------------------ |
|
1050 ------------------------------------------------------------------------*) |
|
1051 |
|
1052 Goal "[| ~ y < x; y ~= x |] ==> x < (y::hypreal)"; |
1077 Goal "[| ~ y < x; y ~= x |] ==> x < (y::hypreal)"; |
1053 by (rtac not_hypreal_leE 1); |
1078 by (rtac not_hypreal_leE 1); |
1054 by (fast_tac (claset() addDs [hypreal_le_imp_less_or_eq]) 1); |
1079 by (fast_tac (claset() addDs [hypreal_le_imp_less_or_eq]) 1); |
1055 qed "not_less_not_eq_hypreal_less"; |
1080 qed "not_less_not_eq_hypreal_less"; |
1056 |
1081 |
|
1082 (* Axiom 'order_less_le' of class 'order': *) |
|
1083 Goal "(w::hypreal) < z = (w <= z & w ~= z)"; |
|
1084 by (simp_tac (simpset() addsimps [hypreal_le_def, hypreal_neq_iff]) 1); |
|
1085 by (blast_tac (claset() addIs [hypreal_less_asym]) 1); |
|
1086 qed "hypreal_less_le"; |
|
1087 |
1057 Goal "(0 < -R) = (R < (0::hypreal))"; |
1088 Goal "(0 < -R) = (R < (0::hypreal))"; |
1058 by (Step_tac 1); |
1089 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); |
1059 by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1); |
1090 by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def, |
1060 by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2); |
1091 hypreal_less,hypreal_minus])); |
1061 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
|
1062 qed "hypreal_minus_zero_less_iff"; |
1092 qed "hypreal_minus_zero_less_iff"; |
|
1093 Addsimps [hypreal_minus_zero_less_iff]; |
1063 |
1094 |
1064 Goal "(-R < 0) = ((0::hypreal) < R)"; |
1095 Goal "(-R < 0) = ((0::hypreal) < R)"; |
1065 by (Step_tac 1); |
1096 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); |
1066 by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1); |
1097 by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def, |
1067 by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2); |
1098 hypreal_less,hypreal_minus])); |
1068 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
1099 by (ALLGOALS(Ultra_tac)); |
1069 qed "hypreal_minus_zero_less_iff2"; |
1100 qed "hypreal_minus_zero_less_iff2"; |
1070 |
1101 |
1071 Goal "((x::hypreal) < y) = (-y < -x)"; |
1102 Goalw [hypreal_le_def] "((0::hypreal) <= -r) = (r <= (0::hypreal))"; |
1072 by (stac hypreal_less_minus_iff 1); |
1103 by (simp_tac (simpset() addsimps |
1073 by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1); |
1104 [hypreal_minus_zero_less_iff2]) 1); |
1074 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
1105 qed "hypreal_minus_zero_le_iff"; |
1075 qed "hypreal_less_swap_iff"; |
|
1076 |
|
1077 Goal "((0::hypreal) < x) = (-x < x)"; |
|
1078 by (Step_tac 1); |
|
1079 by (rtac ccontr 2 THEN forward_tac |
|
1080 [hypreal_leI RS hypreal_le_imp_less_or_eq] 2); |
|
1081 by (Step_tac 2); |
|
1082 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 2); |
|
1083 by (dres_inst_tac [("R2.0","-x")] hypreal_less_trans 2); |
|
1084 by (Auto_tac ); |
|
1085 by (ftac hypreal_add_order 1 THEN assume_tac 1); |
|
1086 by (dres_inst_tac [("C","-x"),("B","x + x")] hypreal_add_less_mono1 1); |
|
1087 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); |
|
1088 qed "hypreal_gt_zero_iff"; |
|
1089 |
|
1090 Goal "(x < (0::hypreal)) = (x < -x)"; |
|
1091 by (rtac (hypreal_minus_zero_less_iff RS subst) 1); |
|
1092 by (stac hypreal_gt_zero_iff 1); |
|
1093 by (Full_simp_tac 1); |
|
1094 qed "hypreal_lt_zero_iff"; |
|
1095 |
|
1096 Goalw [hypreal_le_def] "((0::hypreal) <= x) = (-x <= x)"; |
|
1097 by (auto_tac (claset(),simpset() addsimps [hypreal_lt_zero_iff RS sym])); |
|
1098 qed "hypreal_ge_zero_iff"; |
|
1099 |
|
1100 Goalw [hypreal_le_def] "(x <= (0::hypreal)) = (x <= -x)"; |
|
1101 by (auto_tac (claset(),simpset() addsimps [hypreal_gt_zero_iff RS sym])); |
|
1102 qed "hypreal_le_zero_iff"; |
|
1103 |
|
1104 Goal "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y"; |
|
1105 by (REPEAT(dtac (hypreal_minus_zero_less_iff RS iffD2) 1)); |
|
1106 by (dtac hypreal_mult_order 1 THEN assume_tac 1); |
|
1107 by (Asm_full_simp_tac 1); |
|
1108 qed "hypreal_mult_less_zero1"; |
|
1109 |
|
1110 Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x * y"; |
|
1111 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1)); |
|
1112 by (auto_tac (claset() addIs [hypreal_mult_order, |
|
1113 hypreal_less_imp_le],simpset())); |
|
1114 qed "hypreal_le_mult_order"; |
|
1115 |
|
1116 Goal "[| x <= 0; y <= 0 |] ==> (0::hypreal) <= x * y"; |
|
1117 by (rtac hypreal_less_or_eq_imp_le 1); |
|
1118 by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1); |
|
1119 by Auto_tac; |
|
1120 by (dtac hypreal_le_imp_less_or_eq 1); |
|
1121 by (auto_tac (claset() addDs [hypreal_mult_less_zero1],simpset())); |
|
1122 qed "real_mult_le_zero1"; |
|
1123 |
|
1124 Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::hypreal)"; |
|
1125 by (rtac hypreal_less_or_eq_imp_le 1); |
|
1126 by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1); |
|
1127 by Auto_tac; |
|
1128 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1); |
|
1129 by (rtac (hypreal_minus_zero_less_iff RS subst) 1); |
|
1130 by (blast_tac (claset() addDs [hypreal_mult_order] |
|
1131 addIs [hypreal_minus_mult_eq2 RS ssubst]) 1); |
|
1132 qed "hypreal_mult_le_zero"; |
|
1133 |
|
1134 Goal "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)"; |
|
1135 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1); |
|
1136 by (dtac hypreal_mult_order 1 THEN assume_tac 1); |
|
1137 by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1); |
|
1138 by (Asm_full_simp_tac 1); |
|
1139 qed "hypreal_mult_less_zero"; |
|
1140 |
|
1141 Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0 < 1hr"; |
|
1142 by (res_inst_tac [("x","%n. #0")] exI 1); |
|
1143 by (res_inst_tac [("x","%n. #1")] exI 1); |
|
1144 by (auto_tac (claset(),simpset() addsimps [real_zero_less_one, |
|
1145 FreeUltrafilterNat_Nat_set])); |
|
1146 qed "hypreal_zero_less_one"; |
|
1147 |
|
1148 Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y"; |
|
1149 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1)); |
|
1150 by (auto_tac (claset() addIs [hypreal_add_order, |
|
1151 hypreal_less_imp_le],simpset())); |
|
1152 qed "hypreal_le_add_order"; |
|
1153 |
|
1154 Goal "!!(q1::hypreal). q1 <= q2 ==> x + q1 <= x + q2"; |
|
1155 by (dtac hypreal_le_imp_less_or_eq 1); |
|
1156 by (Step_tac 1); |
|
1157 by (auto_tac (claset() addSIs [hypreal_le_refl, |
|
1158 hypreal_less_imp_le,hypreal_add_less_mono1], |
|
1159 simpset() addsimps [hypreal_add_commute])); |
|
1160 qed "hypreal_add_left_le_mono1"; |
|
1161 |
|
1162 Goal "!!(q1::hypreal). q1 <= q2 ==> q1 + x <= q2 + x"; |
|
1163 by (auto_tac (claset() addDs [hypreal_add_left_le_mono1], |
|
1164 simpset() addsimps [hypreal_add_commute])); |
|
1165 qed "hypreal_add_le_mono1"; |
|
1166 |
|
1167 Goal "!!k l::hypreal. [|i<=j; k<=l |] ==> i + k <= j + l"; |
|
1168 by (etac (hypreal_add_le_mono1 RS hypreal_le_trans) 1); |
|
1169 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
1170 (*j moves to the end because it is free while k, l are bound*) |
|
1171 by (etac hypreal_add_le_mono1 1); |
|
1172 qed "hypreal_add_le_mono"; |
|
1173 |
|
1174 Goal "!!k l::hypreal. [|i<j; k<=l |] ==> i + k < j + l"; |
|
1175 by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] |
|
1176 addIs [hypreal_add_less_mono1,hypreal_add_less_mono],simpset())); |
|
1177 qed "hypreal_add_less_le_mono"; |
|
1178 |
|
1179 Goal "!!k l::hypreal. [|i<=j; k<l |] ==> i + k < j + l"; |
|
1180 by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] |
|
1181 addIs [hypreal_add_less_mono2,hypreal_add_less_mono],simpset())); |
|
1182 qed "hypreal_add_le_less_mono"; |
|
1183 |
|
1184 Goal "(0*x<r)=((0::hypreal)<r)"; |
|
1185 by (Simp_tac 1); |
|
1186 qed "hypreal_mult_0_less"; |
|
1187 |
|
1188 Goal "[| (0::hypreal) < z; x < y |] ==> x*z < y*z"; |
|
1189 by (rotate_tac 1 1); |
|
1190 by (dtac (hypreal_less_minus_iff RS iffD1) 1); |
|
1191 by (rtac (hypreal_less_minus_iff RS iffD2) 1); |
|
1192 by (dtac hypreal_mult_order 1 THEN assume_tac 1); |
|
1193 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2, |
|
1194 hypreal_mult_commute ]) 1); |
|
1195 qed "hypreal_mult_less_mono1"; |
|
1196 |
|
1197 Goal "[| (0::hypreal)<z; x<y |] ==> z*x<z*y"; |
|
1198 by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,hypreal_mult_less_mono1]) 1); |
|
1199 qed "hypreal_mult_less_mono2"; |
|
1200 |
|
1201 Goal "[| (0::hypreal)<=z; x<y |] ==> x*z<=y*z"; |
|
1202 by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac hypreal_le_imp_less_or_eq]); |
|
1203 by (auto_tac (claset() addIs [hypreal_mult_less_mono1],simpset())); |
|
1204 qed "hypreal_mult_le_less_mono1"; |
|
1205 |
|
1206 Goal "[| (0::hypreal)<=z; x<y |] ==> z*x<=z*y"; |
|
1207 by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute, |
|
1208 hypreal_mult_le_less_mono1]) 1); |
|
1209 qed "hypreal_mult_le_less_mono2"; |
|
1210 |
|
1211 Goal "[| (0::hypreal)<=z; x<=y |] ==> z*x<=z*y"; |
|
1212 by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1); |
|
1213 by (auto_tac (claset() addIs [hypreal_mult_le_less_mono2,hypreal_le_refl],simpset())); |
|
1214 qed "hypreal_mult_le_le_mono1"; |
|
1215 |
|
1216 val prem1::prem2::prem3::rest = goal (the_context ()) |
|
1217 "[| (0::hypreal)<y; x<r; y*r<t*s |] ==> y*x<t*s"; |
|
1218 by (rtac ([([prem1,prem2] MRS hypreal_mult_less_mono2),prem3] MRS hypreal_less_trans) 1); |
|
1219 qed "hypreal_mult_less_trans"; |
|
1220 |
|
1221 Goal "[| 0<=y; x<r; y*r<t*s; (0::hypreal)<t*s|] ==> y*x<t*s"; |
|
1222 by (dtac hypreal_le_imp_less_or_eq 1); |
|
1223 by (fast_tac (HOL_cs addEs [(hypreal_mult_0_less RS iffD2),hypreal_mult_less_trans]) 1); |
|
1224 qed "hypreal_mult_le_less_trans"; |
|
1225 |
|
1226 Goal "[| 0 <= y; x <= r; y*r < t*s; (0::hypreal) < t*s|] ==> y*x < t*s"; |
|
1227 by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1); |
|
1228 by (fast_tac (claset() addIs [hypreal_mult_le_less_trans]) 1); |
|
1229 qed "hypreal_mult_le_le_trans"; |
|
1230 |
|
1231 Goal "[| 0 < r1; r1 <r2; (0::hypreal) < x; x < y|] \ |
|
1232 \ ==> r1 * x < r2 * y"; |
|
1233 by (dres_inst_tac [("x","x")] hypreal_mult_less_mono2 1); |
|
1234 by (dres_inst_tac [("R1.0","0")] hypreal_less_trans 2); |
|
1235 by (dres_inst_tac [("x","r1")] hypreal_mult_less_mono1 3); |
|
1236 by Auto_tac; |
|
1237 by (blast_tac (claset() addIs [hypreal_less_trans]) 1); |
|
1238 qed "hypreal_mult_less_mono"; |
|
1239 |
|
1240 Goal "[| 0 < r1; r1 <r2; 0 < y|] \ |
|
1241 \ ==> (0::hypreal) < r2 * y"; |
|
1242 by (dres_inst_tac [("R1.0","0")] hypreal_less_trans 1); |
|
1243 by (assume_tac 1); |
|
1244 by (blast_tac (claset() addIs [hypreal_mult_order]) 1); |
|
1245 qed "hypreal_mult_order_trans"; |
|
1246 |
|
1247 Goal "[| 0 < r1; r1 <= r2; (0::hypreal) <= x; x <= y |] \ |
|
1248 \ ==> r1 * x <= r2 * y"; |
|
1249 by (rtac hypreal_less_or_eq_imp_le 1); |
|
1250 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1)); |
|
1251 by (auto_tac (claset() addIs [hypreal_mult_less_mono, |
|
1252 hypreal_mult_less_mono1,hypreal_mult_less_mono2, |
|
1253 hypreal_mult_order_trans,hypreal_mult_order],simpset())); |
|
1254 qed "hypreal_mult_le_mono"; |
|
1255 |
1106 |
1256 (*---------------------------------------------------------- |
1107 (*---------------------------------------------------------- |
1257 hypreal_of_real preserves field and order properties |
1108 hypreal_of_real preserves field and order properties |
1258 -----------------------------------------------------------*) |
1109 -----------------------------------------------------------*) |
1259 Goalw [hypreal_of_real_def] |
1110 Goalw [hypreal_of_real_def] |
1344 |
1175 |
1345 Goal "x+x=x*(1hr+1hr)"; |
1176 Goal "x+x=x*(1hr+1hr)"; |
1346 by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1); |
1177 by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1); |
1347 qed "hypreal_add_self"; |
1178 qed "hypreal_add_self"; |
1348 |
1179 |
1349 Goal "1hr < 1hr + 1hr"; |
|
1350 by (rtac (hypreal_less_minus_iff RS iffD2) 1); |
|
1351 by (full_simp_tac (simpset() addsimps [hypreal_zero_less_one, |
|
1352 hypreal_add_assoc]) 1); |
|
1353 qed "hypreal_one_less_two"; |
|
1354 |
|
1355 Goal "0 < 1hr + 1hr"; |
|
1356 by (rtac ([hypreal_zero_less_one, |
|
1357 hypreal_one_less_two] MRS hypreal_less_trans) 1); |
|
1358 qed "hypreal_zero_less_two"; |
|
1359 |
|
1360 Goal "1hr + 1hr ~= 0"; |
|
1361 by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1); |
|
1362 qed "hypreal_two_not_zero"; |
|
1363 Addsimps [hypreal_two_not_zero]; |
|
1364 |
|
1365 Goal "x*hrinv(1hr + 1hr) + x*hrinv(1hr + 1hr) = x"; |
|
1366 by (stac hypreal_add_self 1); |
|
1367 by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1); |
|
1368 qed "hypreal_sum_of_halves"; |
|
1369 |
|
1370 Goal "z ~= 0 ==> x*y = (x*hrinv(z))*(z*y)"; |
1180 Goal "z ~= 0 ==> x*y = (x*hrinv(z))*(z*y)"; |
1371 by (asm_simp_tac (simpset() addsimps hypreal_mult_ac) 1); |
1181 by (asm_simp_tac (simpset() addsimps hypreal_mult_ac) 1); |
1372 qed "lemma_chain"; |
1182 qed "lemma_chain"; |
1373 |
|
1374 Goal "0 < r ==> 0 < r*hrinv(1hr+1hr)"; |
|
1375 by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero |
|
1376 RS hypreal_mult_less_mono1) 1); |
|
1377 by Auto_tac; |
|
1378 qed "hypreal_half_gt_zero"; |
|
1379 |
|
1380 (* TODO: remove redundant 0 < x *) |
|
1381 Goal "[| 0 < r; 0 < x; r < x |] ==> hrinv x < hrinv r"; |
|
1382 by (ftac hypreal_hrinv_gt_zero 1); |
|
1383 by (forw_inst_tac [("x","x")] hypreal_hrinv_gt_zero 1); |
|
1384 by (forw_inst_tac [("x","r"),("z","hrinv r")] hypreal_mult_less_mono1 1); |
|
1385 by (assume_tac 1); |
|
1386 by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS |
|
1387 not_sym RS hypreal_mult_hrinv]) 1); |
|
1388 by (ftac hypreal_hrinv_gt_zero 1); |
|
1389 by (forw_inst_tac [("x","1hr"),("z","hrinv x")] hypreal_mult_less_mono2 1); |
|
1390 by (assume_tac 1); |
|
1391 by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS |
|
1392 not_sym RS hypreal_mult_hrinv_left,hypreal_mult_assoc RS sym]) 1); |
|
1393 qed "hypreal_hrinv_less_swap"; |
|
1394 |
|
1395 Goal "[| 0 < r; 0 < x|] ==> (r < x) = (hrinv x < hrinv r)"; |
|
1396 by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],simpset())); |
|
1397 by (res_inst_tac [("t","r")] (hypreal_hrinv_hrinv RS subst) 1); |
|
1398 by (etac (hypreal_not_refl2 RS not_sym) 1); |
|
1399 by (res_inst_tac [("t","x")] (hypreal_hrinv_hrinv RS subst) 1); |
|
1400 by (etac (hypreal_not_refl2 RS not_sym) 1); |
|
1401 by (auto_tac (claset() addIs [hypreal_hrinv_less_swap], |
|
1402 simpset() addsimps [hypreal_hrinv_gt_zero])); |
|
1403 qed "hypreal_hrinv_less_iff"; |
|
1404 |
|
1405 Goal "[| 0 < z; x < y |] ==> x*hrinv(z) < y*hrinv(z)"; |
|
1406 by (blast_tac (claset() addSIs [hypreal_mult_less_mono1, |
|
1407 hypreal_hrinv_gt_zero]) 1); |
|
1408 qed "hypreal_mult_hrinv_less_mono1"; |
|
1409 |
|
1410 Goal "[| 0 < z; x < y |] ==> hrinv(z)*x < hrinv(z)*y"; |
|
1411 by (blast_tac (claset() addSIs [hypreal_mult_less_mono2, |
|
1412 hypreal_hrinv_gt_zero]) 1); |
|
1413 qed "hypreal_mult_hrinv_less_mono2"; |
|
1414 |
|
1415 Goal "[| (0::hypreal) < z; x*z < y*z |] ==> x < y"; |
|
1416 by (forw_inst_tac [("x","x*z")] hypreal_mult_hrinv_less_mono1 1); |
|
1417 by (dtac (hypreal_not_refl2 RS not_sym) 2); |
|
1418 by (auto_tac (claset() addSDs [hypreal_mult_hrinv], |
|
1419 simpset() addsimps hypreal_mult_ac)); |
|
1420 qed "hypreal_less_mult_right_cancel"; |
|
1421 |
|
1422 Goal "[| (0::hypreal) < z; z*x < z*y |] ==> x < y"; |
|
1423 by (auto_tac (claset() addIs [hypreal_less_mult_right_cancel], |
|
1424 simpset() addsimps [hypreal_mult_commute])); |
|
1425 qed "hypreal_less_mult_left_cancel"; |
|
1426 |
|
1427 Goal "[| 0 < r; (0::hypreal) < ra; \ |
|
1428 \ r < x; ra < y |] \ |
|
1429 \ ==> r*ra < x*y"; |
|
1430 by (forw_inst_tac [("R2.0","r")] hypreal_less_trans 1); |
|
1431 by (dres_inst_tac [("z","ra"),("x","r")] hypreal_mult_less_mono1 2); |
|
1432 by (dres_inst_tac [("z","x"),("x","ra")] hypreal_mult_less_mono2 3); |
|
1433 by (auto_tac (claset() addIs [hypreal_less_trans],simpset())); |
|
1434 qed "hypreal_mult_less_gt_zero"; |
|
1435 |
|
1436 Goal "[| 0 < r; (0::hypreal) < ra; \ |
|
1437 \ r <= x; ra <= y |] \ |
|
1438 \ ==> r*ra <= x*y"; |
|
1439 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1)); |
|
1440 by (rtac hypreal_less_or_eq_imp_le 1); |
|
1441 by (auto_tac (claset() addIs [hypreal_mult_less_mono1, |
|
1442 hypreal_mult_less_mono2,hypreal_mult_less_gt_zero], |
|
1443 simpset())); |
|
1444 qed "hypreal_mult_le_ge_zero"; |
|
1445 |
|
1446 Goal "EX (x::hypreal). x < y"; |
|
1447 by (rtac (hypreal_add_zero_right RS subst) 1); |
|
1448 by (res_inst_tac [("x","y + -1hr")] exI 1); |
|
1449 by (auto_tac (claset() addSIs [hypreal_add_less_mono2], |
|
1450 simpset() addsimps [hypreal_minus_zero_less_iff2, |
|
1451 hypreal_zero_less_one] delsimps [hypreal_add_zero_right])); |
|
1452 qed "hypreal_less_Ex"; |
|
1453 |
|
1454 Goal "!!(A::hypreal). A + C < B + C ==> A < B"; |
|
1455 by (dres_inst_tac [("C","-C")] hypreal_add_less_mono1 1); |
|
1456 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1); |
|
1457 qed "hypreal_less_add_right_cancel"; |
|
1458 |
|
1459 Goal "!!(A::hypreal). C + A < C + B ==> A < B"; |
|
1460 by (dres_inst_tac [("C","-C")] hypreal_add_less_mono2 1); |
|
1461 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
|
1462 qed "hypreal_less_add_left_cancel"; |
|
1463 |
|
1464 Goal "(0::hypreal) <= x*x"; |
|
1465 by (res_inst_tac [("x","0"),("y","x")] hypreal_linear_less2 1); |
|
1466 by (auto_tac (claset() addIs [hypreal_mult_order, |
|
1467 hypreal_mult_less_zero1,hypreal_less_imp_le], |
|
1468 simpset())); |
|
1469 qed "hypreal_le_square"; |
|
1470 Addsimps [hypreal_le_square]; |
|
1471 |
|
1472 Goalw [hypreal_le_def] "- (x*x) <= (0::hypreal)"; |
|
1473 by (auto_tac (claset() addSDs [(hypreal_le_square RS |
|
1474 hypreal_le_less_trans)],simpset() addsimps |
|
1475 [hypreal_minus_zero_less_iff,hypreal_less_not_refl])); |
|
1476 qed "hypreal_less_minus_square"; |
|
1477 Addsimps [hypreal_less_minus_square]; |
|
1478 |
1183 |
1479 Goal "[|x ~= 0; y ~= 0 |] ==> \ |
1184 Goal "[|x ~= 0; y ~= 0 |] ==> \ |
1480 \ hrinv(x) + hrinv(y) = (x + y)*hrinv(x*y)"; |
1185 \ hrinv(x) + hrinv(y) = (x + y)*hrinv(x*y)"; |
1481 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv_distrib, |
1186 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv_distrib, |
1482 hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1); |
1187 hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1); |
1550 by (asm_full_simp_tac (simpset() addsimps |
1253 by (asm_full_simp_tac (simpset() addsimps |
1551 [hypreal_add_assoc RS sym])1); |
1254 [hypreal_add_assoc RS sym])1); |
1552 qed "hypreal_add_self_minus_cancel2"; |
1255 qed "hypreal_add_self_minus_cancel2"; |
1553 Addsimps [hypreal_add_self_minus_cancel2]; |
1256 Addsimps [hypreal_add_self_minus_cancel2]; |
1554 |
1257 |
|
1258 (* of course, can prove this by "transfer" as well *) |
1555 Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))"; |
1259 Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))"; |
1556 by Auto_tac; |
1260 by Auto_tac; |
1557 by (dres_inst_tac [("x1","z")] |
1261 by (dres_inst_tac [("x1","z")] |
1558 (hypreal_add_right_cancel RS iffD2) 1); |
1262 (hypreal_add_right_cancel RS iffD2) 1); |
1559 by (asm_full_simp_tac (simpset() addsimps |
1263 by (asm_full_simp_tac (simpset() addsimps |
1560 [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac) 1); |
1264 [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac |
|
1265 delsimps [hypreal_minus_add_distrib]) 1); |
1561 by (asm_full_simp_tac (simpset() addsimps |
1266 by (asm_full_simp_tac (simpset() addsimps |
1562 [hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1); |
1267 [hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1); |
1563 qed "hypreal_add_self_minus_cancel3"; |
1268 qed "hypreal_add_self_minus_cancel3"; |
1564 Addsimps [hypreal_add_self_minus_cancel3]; |
1269 Addsimps [hypreal_add_self_minus_cancel3]; |
1565 |
1270 |
1566 (* check why this does not work without 2nd substiution anymore! *) |
|
1567 Goal "x < y ==> x < (x + y)*hrinv(1hr + 1hr)"; |
|
1568 by (dres_inst_tac [("C","x")] hypreal_add_less_mono2 1); |
|
1569 by (dtac (hypreal_add_self RS subst) 1); |
|
1570 by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS |
|
1571 hypreal_mult_less_mono1) 1); |
|
1572 by (auto_tac (claset() addDs [hypreal_two_not_zero RS |
|
1573 (hypreal_mult_hrinv RS subst)],simpset() |
|
1574 addsimps [hypreal_mult_assoc])); |
|
1575 qed "hypreal_less_half_sum"; |
|
1576 |
|
1577 (* check why this does not work without 2nd substiution anymore! *) |
|
1578 Goal "x < y ==> (x + y)*hrinv(1hr + 1hr) < y"; |
|
1579 by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 1); |
|
1580 by (dtac (hypreal_add_self RS subst) 1); |
|
1581 by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS |
|
1582 hypreal_mult_less_mono1) 1); |
|
1583 by (auto_tac (claset() addDs [hypreal_two_not_zero RS |
|
1584 (hypreal_mult_hrinv RS subst)],simpset() |
|
1585 addsimps [hypreal_mult_assoc])); |
|
1586 qed "hypreal_gt_half_sum"; |
|
1587 |
|
1588 Goal "!!(x::hypreal). x < y ==> EX r. x < r & r < y"; |
|
1589 by (blast_tac (claset() addSIs [hypreal_less_half_sum, |
|
1590 hypreal_gt_half_sum]) 1); |
|
1591 qed "hypreal_dense"; |
|
1592 |
|
1593 Goal "(x * x = 0) = (x = (0::hypreal))"; |
1271 Goal "(x * x = 0) = (x = (0::hypreal))"; |
1594 by Auto_tac; |
1272 by Auto_tac; |
1595 by (blast_tac (claset() addIs [hypreal_mult_not_0E]) 1); |
1273 by (blast_tac (claset() addIs [hypreal_mult_not_0E]) 1); |
1596 qed "hypreal_mult_self_eq_zero_iff"; |
1274 qed "hypreal_mult_self_eq_zero_iff"; |
1597 Addsimps [hypreal_mult_self_eq_zero_iff]; |
1275 Addsimps [hypreal_mult_self_eq_zero_iff]; |
1599 Goal "(0 = x * x) = (x = (0::hypreal))"; |
1277 Goal "(0 = x * x) = (x = (0::hypreal))"; |
1600 by (auto_tac (claset() addDs [sym],simpset())); |
1278 by (auto_tac (claset() addDs [sym],simpset())); |
1601 qed "hypreal_mult_self_eq_zero_iff2"; |
1279 qed "hypreal_mult_self_eq_zero_iff2"; |
1602 Addsimps [hypreal_mult_self_eq_zero_iff2]; |
1280 Addsimps [hypreal_mult_self_eq_zero_iff2]; |
1603 |
1281 |
1604 Goal "(x*x + y*y = 0) = (x = 0 & y = (0::hypreal))"; |
1282 Goalw [hypreal_diff_def] "(x<y) = (x-y < (0::hypreal))"; |
1605 by Auto_tac; |
1283 by (rtac hypreal_less_minus_iff2 1); |
1606 by (dtac (sym RS (hypreal_eq_minus_iff3 RS iffD1)) 1); |
1284 qed "hypreal_less_eq_diff"; |
1607 by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1)) 2); |
1285 |
1608 by (ALLGOALS(rtac ccontr)); |
1286 (*** Subtraction laws ***) |
1609 by (ALLGOALS(dtac hypreal_mult_self_not_zero)); |
1287 |
1610 by (cut_inst_tac [("x1","x")] (hypreal_le_square |
1288 Goal "x + (y - z) = (x + y) - (z::hypreal)"; |
1611 RS hypreal_le_imp_less_or_eq) 1); |
1289 by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
1612 by (cut_inst_tac [("x1","y")] (hypreal_le_square |
1290 qed "hypreal_add_diff_eq"; |
1613 RS hypreal_le_imp_less_or_eq) 2); |
1291 |
1614 by (auto_tac (claset() addDs [sym],simpset())); |
1292 Goal "(x - y) + z = (x + z) - (y::hypreal)"; |
1615 by (dres_inst_tac [("x1","y")] (hypreal_less_minus_square |
1293 by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
1616 RS hypreal_le_less_trans) 1); |
1294 qed "hypreal_diff_add_eq"; |
1617 by (dres_inst_tac [("x1","x")] (hypreal_less_minus_square |
1295 |
1618 RS hypreal_le_less_trans) 2); |
1296 Goal "(x - y) - z = x - (y + (z::hypreal))"; |
1619 by (auto_tac (claset(),simpset() addsimps |
1297 by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
1620 [hypreal_less_not_refl])); |
1298 qed "hypreal_diff_diff_eq"; |
1621 qed "hypreal_squares_add_zero_iff"; |
1299 |
1622 Addsimps [hypreal_squares_add_zero_iff]; |
1300 Goal "x - (y - z) = (x + z) - (y::hypreal)"; |
1623 |
1301 by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
1624 Goal "x * x ~= 0 ==> (0::hypreal) < x* x + y*y + z*z"; |
1302 qed "hypreal_diff_diff_eq2"; |
1625 by (cut_inst_tac [("x1","x")] (hypreal_le_square |
1303 |
1626 RS hypreal_le_imp_less_or_eq) 1); |
1304 Goal "(x-y < z) = (x < z + (y::hypreal))"; |
1627 by (auto_tac (claset() addSIs |
1305 by (stac hypreal_less_eq_diff 1); |
1628 [hypreal_add_order_le],simpset())); |
1306 by (res_inst_tac [("y1", "z")] (hypreal_less_eq_diff RS ssubst) 1); |
1629 qed "hypreal_sum_squares3_gt_zero"; |
1307 by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
1630 |
1308 qed "hypreal_diff_less_eq"; |
1631 Goal "x * x ~= 0 ==> (0::hypreal) < y*y + x*x + z*z"; |
1309 |
1632 by (dtac hypreal_sum_squares3_gt_zero 1); |
1310 Goal "(x < z-y) = (x + (y::hypreal) < z)"; |
1633 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac)); |
1311 by (stac hypreal_less_eq_diff 1); |
1634 qed "hypreal_sum_squares3_gt_zero2"; |
1312 by (res_inst_tac [("y1", "z-y")] (hypreal_less_eq_diff RS ssubst) 1); |
1635 |
1313 by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1); |
1636 Goal "x * x ~= 0 ==> (0::hypreal) < y*y + z*z + x*x"; |
1314 qed "hypreal_less_diff_eq"; |
1637 by (dtac hypreal_sum_squares3_gt_zero 1); |
1315 |
1638 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac)); |
1316 Goalw [hypreal_le_def] "(x-y <= z) = (x <= z + (y::hypreal))"; |
1639 qed "hypreal_sum_squares3_gt_zero3"; |
1317 by (simp_tac (simpset() addsimps [hypreal_less_diff_eq]) 1); |
1640 |
1318 qed "hypreal_diff_le_eq"; |
1641 Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"; |
1319 |
1642 by Auto_tac; |
1320 Goalw [hypreal_le_def] "(x <= z-y) = (x + (y::hypreal) <= z)"; |
1643 by (ALLGOALS(rtac ccontr)); |
1321 by (simp_tac (simpset() addsimps [hypreal_diff_less_eq]) 1); |
1644 by (ALLGOALS(dtac hypreal_mult_self_not_zero)); |
1322 qed "hypreal_le_diff_eq"; |
1645 by (auto_tac (claset() addDs [hypreal_not_refl2 RS not_sym, |
1323 |
1646 hypreal_sum_squares3_gt_zero3,hypreal_sum_squares3_gt_zero, |
1324 Goalw [hypreal_diff_def] "(x-y = z) = (x = z + (y::hypreal))"; |
1647 hypreal_sum_squares3_gt_zero2],simpset() delsimps |
1325 by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc])); |
1648 [hypreal_mult_self_eq_zero_iff])); |
1326 qed "hypreal_diff_eq_eq"; |
1649 qed "hypreal_three_squares_add_zero_iff"; |
1327 |
1650 Addsimps [hypreal_three_squares_add_zero_iff]; |
1328 Goalw [hypreal_diff_def] "(x = z-y) = (x + (y::hypreal) = z)"; |
1651 |
1329 by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc])); |
1652 Addsimps [rename_numerals real_le_square]; |
1330 qed "hypreal_eq_diff_eq"; |
1653 Goal "(x::hypreal)*x <= x*x + y*y"; |
1331 |
1654 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
1332 (*This list of rewrites simplifies (in)equalities by bringing subtractions |
1655 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
1333 to the top and then moving negative terms to the other side. |
1656 by (auto_tac (claset(),simpset() addsimps |
1334 Use with hypreal_add_ac*) |
1657 [hypreal_mult,hypreal_add,hypreal_le])); |
1335 val hypreal_compare_rls = |
1658 qed "hypreal_self_le_add_pos"; |
1336 [symmetric hypreal_diff_def, |
1659 Addsimps [hypreal_self_le_add_pos]; |
1337 hypreal_add_diff_eq, hypreal_diff_add_eq, hypreal_diff_diff_eq, hypreal_diff_diff_eq2, |
1660 |
1338 hypreal_diff_less_eq, hypreal_less_diff_eq, hypreal_diff_le_eq, hypreal_le_diff_eq, |
1661 Goal "(x::hypreal)*x <= x*x + y*y + z*z"; |
1339 hypreal_diff_eq_eq, hypreal_eq_diff_eq]; |
1662 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
1340 |
1663 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
1341 |
1664 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
1342 (** For the cancellation simproc. |
1665 by (auto_tac (claset(), |
1343 The idea is to cancel like terms on opposite sides by subtraction **) |
1666 simpset() addsimps [hypreal_mult, hypreal_add, hypreal_le, |
1344 |
1667 rename_numerals real_le_add_order])); |
1345 Goal "(x::hypreal) - y = x' - y' ==> (x<y) = (x'<y')"; |
1668 qed "hypreal_self_le_add_pos2"; |
1346 by (stac hypreal_less_eq_diff 1); |
1669 Addsimps [hypreal_self_le_add_pos2]; |
1347 by (res_inst_tac [("y1", "y")] (hypreal_less_eq_diff RS ssubst) 1); |
1670 |
1348 by (Asm_simp_tac 1); |
1671 (*--------------------------------------------------------------------------------- |
1349 qed "hypreal_less_eqI"; |
1672 Embedding of the naturals in the hyperreals |
1350 |
1673 ---------------------------------------------------------------------------------*) |
1351 Goal "(x::hypreal) - y = x' - y' ==> (y<=x) = (y'<=x')"; |
1674 Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 0 = 1hr"; |
1352 by (dtac hypreal_less_eqI 1); |
1675 by (full_simp_tac (simpset() addsimps |
1353 by (asm_simp_tac (simpset() addsimps [hypreal_le_def]) 1); |
1676 [pnat_one_iff RS sym,real_of_preal_def]) 1); |
1354 qed "hypreal_le_eqI"; |
1677 by (fold_tac [real_one_def]); |
1355 |
1678 by (simp_tac (simpset() addsimps [hypreal_of_real_one]) 1); |
1356 Goal "(x::hypreal) - y = x' - y' ==> (x=y) = (x'=y')"; |
1679 qed "hypreal_of_posnat_one"; |
1357 by Safe_tac; |
1680 |
1358 by (ALLGOALS |
1681 Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr"; |
1359 (asm_full_simp_tac |
1682 by (full_simp_tac (simpset() addsimps |
1360 (simpset() addsimps [hypreal_eq_diff_eq, hypreal_diff_eq_eq]))); |
1683 [real_of_preal_def, |
1361 qed "hypreal_eq_eqI"; |
1684 rename_numerals (real_one_def RS meta_eq_to_obj_eq), |
1362 |
1685 hypreal_add,hypreal_of_real_def,pnat_two_eq, |
|
1686 hypreal_one_def, real_add, |
|
1687 prat_of_pnat_add RS sym, preal_of_prat_add RS sym] @ |
|
1688 pnat_add_ac) 1); |
|
1689 qed "hypreal_of_posnat_two"; |
|
1690 |
|
1691 Goalw [hypreal_of_posnat_def] |
|
1692 "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \ |
|
1693 \ hypreal_of_posnat (n1 + n2) + 1hr"; |
|
1694 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one RS sym, |
|
1695 hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym, |
|
1696 preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1); |
|
1697 qed "hypreal_of_posnat_add"; |
|
1698 |
|
1699 Goal "hypreal_of_posnat (n + 1) = hypreal_of_posnat n + 1hr"; |
|
1700 by (res_inst_tac [("x1","1hr")] (hypreal_add_right_cancel RS iffD1) 1); |
|
1701 by (rtac (hypreal_of_posnat_add RS subst) 1); |
|
1702 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,hypreal_add_assoc]) 1); |
|
1703 qed "hypreal_of_posnat_add_one"; |
|
1704 |
|
1705 Goalw [real_of_posnat_def,hypreal_of_posnat_def] |
|
1706 "hypreal_of_posnat n = hypreal_of_real (real_of_posnat n)"; |
|
1707 by (rtac refl 1); |
|
1708 qed "hypreal_of_real_of_posnat"; |
|
1709 |
|
1710 Goalw [hypreal_of_posnat_def] |
|
1711 "(n < m) = (hypreal_of_posnat n < hypreal_of_posnat m)"; |
|
1712 by Auto_tac; |
|
1713 qed "hypreal_of_posnat_less_iff"; |
|
1714 |
|
1715 Addsimps [hypreal_of_posnat_less_iff RS sym]; |
|
1716 (*--------------------------------------------------------------------------------- |
|
1717 Existence of infinite hyperreal number |
|
1718 ---------------------------------------------------------------------------------*) |
|
1719 |
|
1720 Goal "hyprel^^{%n::nat. real_of_posnat n} : hypreal"; |
|
1721 by Auto_tac; |
|
1722 qed "hypreal_omega"; |
|
1723 |
|
1724 Goalw [omega_def] "Rep_hypreal(whr) : hypreal"; |
|
1725 by (rtac Rep_hypreal 1); |
|
1726 qed "Rep_hypreal_omega"; |
|
1727 |
|
1728 (* existence of infinite number not corresponding to any real number *) |
|
1729 (* use assumption that member FreeUltrafilterNat is not finite *) |
|
1730 (* a few lemmas first *) |
|
1731 |
|
1732 Goal "{n::nat. x = real_of_posnat n} = {} | \ |
|
1733 \ (EX y. {n::nat. x = real_of_posnat n} = {y})"; |
|
1734 by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset())); |
|
1735 qed "lemma_omega_empty_singleton_disj"; |
|
1736 |
|
1737 Goal "finite {n::nat. x = real_of_posnat n}"; |
|
1738 by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1); |
|
1739 by Auto_tac; |
|
1740 qed "lemma_finite_omega_set"; |
|
1741 |
|
1742 Goalw [omega_def,hypreal_of_real_def] |
|
1743 "~ (EX x. hypreal_of_real x = whr)"; |
|
1744 by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set |
|
1745 RS FreeUltrafilterNat_finite])); |
|
1746 qed "not_ex_hypreal_of_real_eq_omega"; |
|
1747 |
|
1748 Goal "hypreal_of_real x ~= whr"; |
|
1749 by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1); |
|
1750 by Auto_tac; |
|
1751 qed "hypreal_of_real_not_eq_omega"; |
|
1752 |
|
1753 (* existence of infinitesimal number also not *) |
|
1754 (* corresponding to any real number *) |
|
1755 |
|
1756 Goal "{n::nat. x = rinv(real_of_posnat n)} = {} | \ |
|
1757 \ (EX y. {n::nat. x = rinv(real_of_posnat n)} = {y})"; |
|
1758 by (Step_tac 1 THEN Step_tac 1); |
|
1759 by (auto_tac (claset() addIs [real_of_posnat_rinv_inj],simpset())); |
|
1760 qed "lemma_epsilon_empty_singleton_disj"; |
|
1761 |
|
1762 Goal "finite {n::nat. x = rinv(real_of_posnat n)}"; |
|
1763 by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1); |
|
1764 by Auto_tac; |
|
1765 qed "lemma_finite_epsilon_set"; |
|
1766 |
|
1767 Goalw [epsilon_def,hypreal_of_real_def] |
|
1768 "~ (EX x. hypreal_of_real x = ehr)"; |
|
1769 by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set |
|
1770 RS FreeUltrafilterNat_finite])); |
|
1771 qed "not_ex_hypreal_of_real_eq_epsilon"; |
|
1772 |
|
1773 Goal "hypreal_of_real x ~= ehr"; |
|
1774 by (cut_facts_tac [not_ex_hypreal_of_real_eq_epsilon] 1); |
|
1775 by Auto_tac; |
|
1776 qed "hypreal_of_real_not_eq_epsilon"; |
|
1777 |
|
1778 Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0"; |
|
1779 by (auto_tac (claset(), |
|
1780 simpset() addsimps [rename_numerals real_of_posnat_rinv_not_zero])); |
|
1781 qed "hypreal_epsilon_not_zero"; |
|
1782 |
|
1783 Addsimps [rename_numerals real_of_posnat_not_eq_zero]; |
|
1784 Goalw [omega_def,hypreal_zero_def] "whr ~= 0"; |
|
1785 by (Simp_tac 1); |
|
1786 qed "hypreal_omega_not_zero"; |
|
1787 |
|
1788 Goal "ehr = hrinv(whr)"; |
|
1789 by (asm_full_simp_tac (simpset() addsimps |
|
1790 [hypreal_hrinv,omega_def,epsilon_def] |
|
1791 addsplits [split_if]) 1); |
|
1792 qed "hypreal_epsilon_hrinv_omega"; |
|
1793 |
|
1794 (*---------------------------------------------------------------- |
|
1795 Another embedding of the naturals in the |
|
1796 hyperreals (see hypreal_of_posnat) |
|
1797 ----------------------------------------------------------------*) |
|
1798 Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0"; |
|
1799 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1); |
|
1800 qed "hypreal_of_nat_zero"; |
|
1801 |
|
1802 Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr"; |
|
1803 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two, |
|
1804 hypreal_add_assoc]) 1); |
|
1805 qed "hypreal_of_nat_one"; |
|
1806 |
|
1807 Goalw [hypreal_of_nat_def] |
|
1808 "hypreal_of_nat n1 + hypreal_of_nat n2 = \ |
|
1809 \ hypreal_of_nat (n1 + n2)"; |
|
1810 by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1); |
|
1811 by (simp_tac (simpset() addsimps [hypreal_of_posnat_add, |
|
1812 hypreal_add_assoc RS sym]) 1); |
|
1813 by (rtac (hypreal_add_commute RS subst) 1); |
|
1814 by (simp_tac (simpset() addsimps [hypreal_add_left_cancel, |
|
1815 hypreal_add_assoc]) 1); |
|
1816 qed "hypreal_of_nat_add"; |
|
1817 |
|
1818 Goal "hypreal_of_nat 2 = 1hr + 1hr"; |
|
1819 by (simp_tac (simpset() addsimps [hypreal_of_nat_one |
|
1820 RS sym,hypreal_of_nat_add]) 1); |
|
1821 qed "hypreal_of_nat_two"; |
|
1822 |
|
1823 Goalw [hypreal_of_nat_def] |
|
1824 "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)"; |
|
1825 by (auto_tac (claset() addIs [hypreal_add_less_mono1],simpset())); |
|
1826 by (dres_inst_tac [("C","1hr")] hypreal_add_less_mono1 1); |
|
1827 by (full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1); |
|
1828 qed "hypreal_of_nat_less_iff"; |
|
1829 Addsimps [hypreal_of_nat_less_iff RS sym]; |
|
1830 |
|
1831 (* naturals embedded in hyperreals is an hyperreal *) |
|
1832 Goalw [hypreal_of_nat_def,real_of_nat_def] |
|
1833 "hypreal_of_nat m = Abs_hypreal(hyprel^^{%n. real_of_nat m})"; |
|
1834 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def, |
|
1835 hypreal_of_real_of_posnat,hypreal_minus,hypreal_one_def,hypreal_add])); |
|
1836 qed "hypreal_of_nat_iff"; |
|
1837 |
|
1838 Goal "inj hypreal_of_nat"; |
|
1839 by (rtac injI 1); |
|
1840 by (auto_tac (claset() addSDs [FreeUltrafilterNat_P], |
|
1841 simpset() addsimps [split_if_mem1, hypreal_of_nat_iff, |
|
1842 real_add_right_cancel,inj_real_of_nat RS injD])); |
|
1843 qed "inj_hypreal_of_nat"; |
|
1844 |
|
1845 Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def, |
|
1846 real_of_posnat_def,hypreal_one_def,real_of_nat_def] |
|
1847 "hypreal_of_nat n = hypreal_of_real (real_of_nat n)"; |
|
1848 by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1); |
|
1849 qed "hypreal_of_nat_real_of_nat"; |
|