1225 by (asm_full_simp_tac (simpset() addsimps |
1225 by (asm_full_simp_tac (simpset() addsimps |
1226 [hypreal_minus_eq_swap]) 1); |
1226 [hypreal_minus_eq_swap]) 1); |
1227 qed "hypreal_minus_eq_cancel"; |
1227 qed "hypreal_minus_eq_cancel"; |
1228 Addsimps [hypreal_minus_eq_cancel]; |
1228 Addsimps [hypreal_minus_eq_cancel]; |
1229 |
1229 |
1230 Goal "x < x + 1hr"; |
|
1231 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1232 by (auto_tac (claset(), |
|
1233 simpset() addsimps [hypreal_add, hypreal_one_def,hypreal_less])); |
|
1234 qed "hypreal_less_self_add_one"; |
|
1235 Addsimps [hypreal_less_self_add_one]; |
|
1236 |
|
1237 (*??DELETE MOST OF THE FOLLOWING??*) |
|
1238 Goal "((x::hypreal) + x = y + y) = (x = y)"; |
|
1239 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1240 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1241 by (auto_tac (claset(),simpset() addsimps [hypreal_add])); |
|
1242 by (ALLGOALS(Ultra_tac)); |
|
1243 qed "hypreal_add_self_cancel"; |
|
1244 Addsimps [hypreal_add_self_cancel]; |
|
1245 |
|
1246 Goal "(y = x + - y + x) = (y = (x::hypreal))"; |
|
1247 by Auto_tac; |
|
1248 by (dres_inst_tac [("x1","y")] |
|
1249 (hypreal_add_right_cancel RS iffD2) 1); |
|
1250 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac)); |
|
1251 qed "hypreal_add_self_minus_cancel"; |
|
1252 Addsimps [hypreal_add_self_minus_cancel]; |
|
1253 |
|
1254 Goal "(y = x + (- y + x)) = (y = (x::hypreal))"; |
|
1255 by (asm_full_simp_tac (simpset() addsimps |
|
1256 [hypreal_add_assoc RS sym])1); |
|
1257 qed "hypreal_add_self_minus_cancel2"; |
|
1258 Addsimps [hypreal_add_self_minus_cancel2]; |
|
1259 |
|
1260 (* of course, can prove this by "transfer" as well *) |
|
1261 Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))"; |
|
1262 by Auto_tac; |
|
1263 by (dres_inst_tac [("x1","z")] |
|
1264 (hypreal_add_right_cancel RS iffD2) 1); |
|
1265 by (asm_full_simp_tac (simpset() addsimps |
|
1266 [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac |
|
1267 delsimps [hypreal_minus_add_distrib]) 1); |
|
1268 by (asm_full_simp_tac (simpset() addsimps |
|
1269 [hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1); |
|
1270 qed "hypreal_add_self_minus_cancel3"; |
|
1271 Addsimps [hypreal_add_self_minus_cancel3]; |
|
1272 |
|
1273 Goalw [hypreal_diff_def] "(x<y) = (x-y < (0::hypreal))"; |
1230 Goalw [hypreal_diff_def] "(x<y) = (x-y < (0::hypreal))"; |
1274 by (rtac hypreal_less_minus_iff2 1); |
1231 by (rtac hypreal_less_minus_iff2 1); |
1275 qed "hypreal_less_eq_diff"; |
1232 qed "hypreal_less_eq_diff"; |
1276 |
1233 |
1277 (*** Subtraction laws ***) |
1234 (*** Subtraction laws ***) |