author | bauerg |
Wed, 06 Dec 2000 12:34:40 +0100 | |
changeset 10607 | 352f6f209775 |
parent 10045 | c76b73e16711 |
child 10677 | 36625483213f |
permissions | -rw-r--r-- |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
1 |
(* Title: Real/Hyperreal/HyperOrd.ML |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
2 |
Author: Jacques D. Fleuriot |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
3 |
Copyright: 1998 University of Cambridge |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
4 |
2000 University of Edinburgh |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
5 |
Description: Type "hypreal" is a linear order and also |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
6 |
satisfies plus_ac0: + is an AC-operator with zero |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
7 |
*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
8 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
9 |
(**** The simproc abel_cancel ****) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
10 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
11 |
(*** Two lemmas needed for the simprocs ***) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
12 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
13 |
(*Deletion of other terms in the formula, seeking the -x at the front of z*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
14 |
Goal "((x::hypreal) + (y + z) = y + u) = ((x + z) = u)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
15 |
by (stac hypreal_add_left_commute 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
16 |
by (rtac hypreal_add_left_cancel 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
17 |
qed "hypreal_add_cancel_21"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
18 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
19 |
(*A further rule to deal with the case that |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
20 |
everything gets cancelled on the right.*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
21 |
Goal "((x::hypreal) + (y + z) = y) = (x = -z)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
22 |
by (stac hypreal_add_left_commute 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
23 |
by (res_inst_tac [("t", "y")] (hypreal_add_zero_right RS subst) 1 |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
24 |
THEN stac hypreal_add_left_cancel 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
25 |
by (simp_tac (simpset() addsimps [hypreal_eq_diff_eq RS sym]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
26 |
qed "hypreal_add_cancel_end"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
27 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
28 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
29 |
structure Hyperreal_Cancel_Data = |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
30 |
struct |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
31 |
val ss = HOL_ss |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
32 |
val eq_reflection = eq_reflection |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
33 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
34 |
val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
35 |
val T = Type("HyperDef.hypreal",[]) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
36 |
val zero = Const ("0", T) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
37 |
val restrict_to_left = restrict_to_left |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
38 |
val add_cancel_21 = hypreal_add_cancel_21 |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
39 |
val add_cancel_end = hypreal_add_cancel_end |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
40 |
val add_left_cancel = hypreal_add_left_cancel |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
41 |
val add_assoc = hypreal_add_assoc |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
42 |
val add_commute = hypreal_add_commute |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
43 |
val add_left_commute = hypreal_add_left_commute |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
44 |
val add_0 = hypreal_add_zero_left |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
45 |
val add_0_right = hypreal_add_zero_right |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
46 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
47 |
val eq_diff_eq = hypreal_eq_diff_eq |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
48 |
val eqI_rules = [hypreal_less_eqI, hypreal_eq_eqI, hypreal_le_eqI] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
49 |
fun dest_eqI th = |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
50 |
#1 (HOLogic.dest_bin "op =" HOLogic.boolT |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
51 |
(HOLogic.dest_Trueprop (concl_of th))) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
52 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
53 |
val diff_def = hypreal_diff_def |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
54 |
val minus_add_distrib = hypreal_minus_add_distrib |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
55 |
val minus_minus = hypreal_minus_minus |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
56 |
val minus_0 = hypreal_minus_zero |
10607 | 57 |
val add_inverses = [hypreal_add_minus, hypreal_add_minus_left] |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
58 |
val cancel_simps = [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
59 |
end; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
60 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
61 |
structure Hyperreal_Cancel = Abel_Cancel (Hyperreal_Cancel_Data); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
62 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
63 |
Addsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
64 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
65 |
Goal "- (z - y) = y - (z::hypreal)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
66 |
by (Simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
67 |
qed "hypreal_minus_diff_eq"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
68 |
Addsimps [hypreal_minus_diff_eq]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
69 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
70 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
71 |
Goal "((x::hypreal) < y) = (-y < -x)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
72 |
by (stac hypreal_less_minus_iff 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
73 |
by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
74 |
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
75 |
qed "hypreal_less_swap_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
76 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
77 |
Goalw [hypreal_zero_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
78 |
"((0::hypreal) < x) = (-x < x)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
79 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
80 |
by (auto_tac (claset(),simpset() addsimps [hypreal_less, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
81 |
hypreal_minus])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
82 |
by (ALLGOALS(Ultra_tac)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
83 |
qed "hypreal_gt_zero_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
84 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
85 |
Goal "(A::hypreal) < B ==> A + C < B + C"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
86 |
by (res_inst_tac [("z","A")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
87 |
by (res_inst_tac [("z","B")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
88 |
by (res_inst_tac [("z","C")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
89 |
by (auto_tac (claset() addSIs [exI],simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
90 |
[hypreal_less_def,hypreal_add])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
91 |
by (Ultra_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
92 |
qed "hypreal_add_less_mono1"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
93 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
94 |
Goal "!!(A::hypreal). A < B ==> C + A < C + B"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
95 |
by (auto_tac (claset() addIs [hypreal_add_less_mono1], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
96 |
simpset() addsimps [hypreal_add_commute])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
97 |
qed "hypreal_add_less_mono2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
98 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
99 |
Goal "(x < (0::hypreal)) = (x < -x)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
100 |
by (rtac (hypreal_minus_zero_less_iff RS subst) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
101 |
by (stac hypreal_gt_zero_iff 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
102 |
by (Full_simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
103 |
qed "hypreal_lt_zero_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
104 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
105 |
Goalw [hypreal_le_def] "((0::hypreal) <= x) = (-x <= x)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
106 |
by (auto_tac (claset(),simpset() addsimps [hypreal_lt_zero_iff RS sym])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
107 |
qed "hypreal_ge_zero_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
108 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
109 |
Goalw [hypreal_le_def] "(x <= (0::hypreal)) = (x <= -x)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
110 |
by (auto_tac (claset(),simpset() addsimps [hypreal_gt_zero_iff RS sym])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
111 |
qed "hypreal_le_zero_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
112 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
113 |
Goalw [hypreal_zero_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
114 |
"[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
115 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
116 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
117 |
by (auto_tac (claset(),simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
118 |
[hypreal_less_def,hypreal_add])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
119 |
by (auto_tac (claset() addSIs [exI],simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
120 |
[hypreal_less_def,hypreal_add])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
121 |
by (ultra_tac (claset() addIs [real_add_order],simpset()) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
122 |
qed "hypreal_add_order"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
123 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
124 |
Goal "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
125 |
by (auto_tac (claset() addDs [sym,hypreal_le_imp_less_or_eq] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
126 |
addIs [hypreal_add_order],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
127 |
qed "hypreal_add_order_le"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
128 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
129 |
Goalw [hypreal_zero_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
130 |
"[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
131 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
132 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
133 |
by (auto_tac (claset() addSIs [exI],simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
134 |
[hypreal_less_def,hypreal_mult])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
135 |
by (ultra_tac (claset() addIs [rename_numerals real_mult_order], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
136 |
simpset()) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
137 |
qed "hypreal_mult_order"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
138 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
139 |
Goal "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
140 |
by (REPEAT(dtac (hypreal_minus_zero_less_iff RS iffD2) 1)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
141 |
by (dtac hypreal_mult_order 1 THEN assume_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
142 |
by (Asm_full_simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
143 |
qed "hypreal_mult_less_zero1"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
144 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
145 |
Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x * y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
146 |
by (REPEAT(dtac hypreal_le_imp_less_or_eq 1)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
147 |
by (auto_tac (claset() addIs [hypreal_mult_order, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
148 |
hypreal_less_imp_le],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
149 |
qed "hypreal_le_mult_order"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
150 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
151 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
152 |
Goal "[| x <= 0; y <= 0 |] ==> (0::hypreal) <= x * y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
153 |
by (rtac hypreal_less_or_eq_imp_le 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
154 |
by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
155 |
by Auto_tac; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
156 |
by (dtac hypreal_le_imp_less_or_eq 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
157 |
by (auto_tac (claset() addDs [hypreal_mult_less_zero1],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
158 |
qed "hypreal_mult_le_zero1"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
159 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
160 |
Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::hypreal)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
161 |
by (rtac hypreal_less_or_eq_imp_le 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
162 |
by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
163 |
by Auto_tac; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
164 |
by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
165 |
by (rtac (hypreal_minus_zero_less_iff RS subst) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
166 |
by (blast_tac (claset() addDs [hypreal_mult_order] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
167 |
addIs [hypreal_minus_mult_eq2 RS ssubst]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
168 |
qed "hypreal_mult_le_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
169 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
170 |
Goal "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
171 |
by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
172 |
by (dtac hypreal_mult_order 1 THEN assume_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
173 |
by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
174 |
by (Asm_full_simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
175 |
qed "hypreal_mult_less_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
176 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
177 |
Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0 < 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
178 |
by (res_inst_tac [("x","%n. #0")] exI 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
179 |
by (res_inst_tac [("x","%n. #1")] exI 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
180 |
by (auto_tac (claset(),simpset() addsimps [real_zero_less_one, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
181 |
FreeUltrafilterNat_Nat_set])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
182 |
qed "hypreal_zero_less_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
183 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
184 |
Goal "1hr < 1hr + 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
185 |
by (rtac (hypreal_less_minus_iff RS iffD2) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
186 |
by (full_simp_tac (simpset() addsimps [hypreal_zero_less_one, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
187 |
hypreal_add_assoc]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
188 |
qed "hypreal_one_less_two"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
189 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
190 |
Goal "0 < 1hr + 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
191 |
by (rtac ([hypreal_zero_less_one, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
192 |
hypreal_one_less_two] MRS hypreal_less_trans) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
193 |
qed "hypreal_zero_less_two"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
194 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
195 |
Goal "1hr + 1hr ~= 0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
196 |
by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
197 |
qed "hypreal_two_not_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
198 |
Addsimps [hypreal_two_not_zero]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
199 |
|
10607 | 200 |
Goal "x*inverse(1hr + 1hr) + x*inverse(1hr + 1hr) = x"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
201 |
by (stac hypreal_add_self 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
202 |
by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc, |
10607 | 203 |
hypreal_two_not_zero RS hypreal_mult_inverse_left]) 1); |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
204 |
qed "hypreal_sum_of_halves"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
205 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
206 |
Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
207 |
by (REPEAT(dtac hypreal_le_imp_less_or_eq 1)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
208 |
by (auto_tac (claset() addIs [hypreal_add_order, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
209 |
hypreal_less_imp_le],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
210 |
qed "hypreal_le_add_order"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
211 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
212 |
(*** Monotonicity results ***) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
213 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
214 |
Goal "(v+z < w+z) = (v < (w::hypreal))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
215 |
by (Simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
216 |
qed "hypreal_add_right_cancel_less"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
217 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
218 |
Goal "(z+v < z+w) = (v < (w::hypreal))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
219 |
by (Simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
220 |
qed "hypreal_add_left_cancel_less"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
221 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
222 |
Addsimps [hypreal_add_right_cancel_less, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
223 |
hypreal_add_left_cancel_less]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
224 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
225 |
Goal "(v+z <= w+z) = (v <= (w::hypreal))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
226 |
by (Simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
227 |
qed "hypreal_add_right_cancel_le"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
228 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
229 |
Goal "(z+v <= z+w) = (v <= (w::hypreal))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
230 |
by (Simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
231 |
qed "hypreal_add_left_cancel_le"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
232 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
233 |
Addsimps [hypreal_add_right_cancel_le, hypreal_add_left_cancel_le]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
234 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
235 |
Goal "[| (z1::hypreal) < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
236 |
by (dtac (hypreal_less_minus_iff RS iffD1) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
237 |
by (dtac (hypreal_less_minus_iff RS iffD1) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
238 |
by (dtac hypreal_add_order 1 THEN assume_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
239 |
by (thin_tac "0 < y2 + - z2" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
240 |
by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
241 |
by (auto_tac (claset(),simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
242 |
[hypreal_minus_add_distrib RS sym] @ hypreal_add_ac |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
243 |
delsimps [hypreal_minus_add_distrib])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
244 |
qed "hypreal_add_less_mono"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
245 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
246 |
Goal "(q1::hypreal) <= q2 ==> x + q1 <= x + q2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
247 |
by (dtac hypreal_le_imp_less_or_eq 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
248 |
by (Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
249 |
by (auto_tac (claset() addSIs [hypreal_le_refl, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
250 |
hypreal_less_imp_le,hypreal_add_less_mono1], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
251 |
simpset() addsimps [hypreal_add_commute])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
252 |
qed "hypreal_add_left_le_mono1"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
253 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
254 |
Goal "(q1::hypreal) <= q2 ==> q1 + x <= q2 + x"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
255 |
by (auto_tac (claset() addDs [hypreal_add_left_le_mono1], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
256 |
simpset() addsimps [hypreal_add_commute])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
257 |
qed "hypreal_add_le_mono1"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
258 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
259 |
Goal "[|(i::hypreal)<=j; k<=l |] ==> i + k <= j + l"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
260 |
by (etac (hypreal_add_le_mono1 RS hypreal_le_trans) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
261 |
by (Simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
262 |
qed "hypreal_add_le_mono"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
263 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
264 |
Goal "[|(i::hypreal)<j; k<=l |] ==> i + k < j + l"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
265 |
by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
266 |
addIs [hypreal_add_less_mono1,hypreal_add_less_mono], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
267 |
simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
268 |
qed "hypreal_add_less_le_mono"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
269 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
270 |
Goal "[|(i::hypreal)<=j; k<l |] ==> i + k < j + l"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
271 |
by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
272 |
addIs [hypreal_add_less_mono2,hypreal_add_less_mono],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
273 |
qed "hypreal_add_le_less_mono"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
274 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
275 |
Goal "(A::hypreal) + C < B + C ==> A < B"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
276 |
by (Full_simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
277 |
qed "hypreal_less_add_right_cancel"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
278 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
279 |
Goal "(C::hypreal) + A < C + B ==> A < B"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
280 |
by (Full_simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
281 |
qed "hypreal_less_add_left_cancel"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
282 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
283 |
Goal "[|r < x; (0::hypreal) <= y|] ==> r < x + y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
284 |
by (auto_tac (claset() addDs [hypreal_add_less_le_mono], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
285 |
simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
286 |
qed "hypreal_add_zero_less_le_mono"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
287 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
288 |
Goal "!!(A::hypreal). A + C <= B + C ==> A <= B"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
289 |
by (dres_inst_tac [("x","-C")] hypreal_add_le_mono1 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
290 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
291 |
qed "hypreal_le_add_right_cancel"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
292 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
293 |
Goal "!!(A::hypreal). C + A <= C + B ==> A <= B"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
294 |
by (dres_inst_tac [("x","-C")] hypreal_add_left_le_mono1 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
295 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
296 |
qed "hypreal_le_add_left_cancel"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
297 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
298 |
Goal "(0::hypreal) <= x*x"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
299 |
by (res_inst_tac [("x","0"),("y","x")] hypreal_linear_less2 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
300 |
by (auto_tac (claset() addIs [hypreal_mult_order, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
301 |
hypreal_mult_less_zero1,hypreal_less_imp_le], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
302 |
simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
303 |
qed "hypreal_le_square"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
304 |
Addsimps [hypreal_le_square]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
305 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
306 |
Goalw [hypreal_le_def] "- (x*x) <= (0::hypreal)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
307 |
by (auto_tac (claset() addSDs [(hypreal_le_square RS |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
308 |
hypreal_le_less_trans)],simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
309 |
[hypreal_minus_zero_less_iff,hypreal_less_not_refl])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
310 |
qed "hypreal_less_minus_square"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
311 |
Addsimps [hypreal_less_minus_square]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
312 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
313 |
Goal "(0*x<r)=((0::hypreal)<r)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
314 |
by (Simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
315 |
qed "hypreal_mult_0_less"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
316 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
317 |
Goal "[| (0::hypreal) < z; x < y |] ==> x*z < y*z"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
318 |
by (rotate_tac 1 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
319 |
by (dtac (hypreal_less_minus_iff RS iffD1) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
320 |
by (rtac (hypreal_less_minus_iff RS iffD2) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
321 |
by (dtac hypreal_mult_order 1 THEN assume_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
322 |
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
323 |
hypreal_mult_commute ]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
324 |
qed "hypreal_mult_less_mono1"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
325 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
326 |
Goal "[| (0::hypreal)<z; x<y |] ==> z*x<z*y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
327 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,hypreal_mult_less_mono1]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
328 |
qed "hypreal_mult_less_mono2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
329 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
330 |
Goal "[| (0::hypreal)<=z; x<y |] ==> x*z<=y*z"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
331 |
by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac hypreal_le_imp_less_or_eq]); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
332 |
by (auto_tac (claset() addIs [hypreal_mult_less_mono1],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
333 |
qed "hypreal_mult_le_less_mono1"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
334 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
335 |
Goal "[| (0::hypreal)<=z; x<y |] ==> z*x<=z*y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
336 |
by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
337 |
hypreal_mult_le_less_mono1]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
338 |
qed "hypreal_mult_le_less_mono2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
339 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
340 |
Goal "[| (0::hypreal)<=z; x<=y |] ==> z*x<=z*y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
341 |
by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
342 |
by (auto_tac (claset() addIs [hypreal_mult_le_less_mono2,hypreal_le_refl],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
343 |
qed "hypreal_mult_le_le_mono1"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
344 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
345 |
val prem1::prem2::prem3::rest = goal thy |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
346 |
"[| (0::hypreal)<y; x<r; y*r<t*s |] ==> y*x<t*s"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
347 |
by (rtac ([([prem1,prem2] MRS hypreal_mult_less_mono2),prem3] MRS hypreal_less_trans) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
348 |
qed "hypreal_mult_less_trans"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
349 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
350 |
Goal "[| 0<=y; x<r; y*r<t*s; (0::hypreal)<t*s|] ==> y*x<t*s"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
351 |
by (dtac hypreal_le_imp_less_or_eq 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
352 |
by (fast_tac (HOL_cs addEs [(hypreal_mult_0_less RS iffD2),hypreal_mult_less_trans]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
353 |
qed "hypreal_mult_le_less_trans"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
354 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
355 |
Goal "[| 0 <= y; x <= r; y*r < t*s; (0::hypreal) < t*s|] ==> y*x < t*s"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
356 |
by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
357 |
by (fast_tac (claset() addIs [hypreal_mult_le_less_trans]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
358 |
qed "hypreal_mult_le_le_trans"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
359 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
360 |
Goal "[| 0 < r1; r1 <r2; (0::hypreal) < x; x < y|] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
361 |
\ ==> r1 * x < r2 * y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
362 |
by (dres_inst_tac [("x","x")] hypreal_mult_less_mono2 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
363 |
by (dres_inst_tac [("R1.0","0")] hypreal_less_trans 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
364 |
by (dres_inst_tac [("x","r1")] hypreal_mult_less_mono1 3); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
365 |
by Auto_tac; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
366 |
by (blast_tac (claset() addIs [hypreal_less_trans]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
367 |
qed "hypreal_mult_less_mono"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
368 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
369 |
Goal "[| 0 < r1; r1 <r2; 0 < y|] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
370 |
\ ==> (0::hypreal) < r2 * y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
371 |
by (dres_inst_tac [("R1.0","0")] hypreal_less_trans 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
372 |
by (assume_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
373 |
by (blast_tac (claset() addIs [hypreal_mult_order]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
374 |
qed "hypreal_mult_order_trans"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
375 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
376 |
Goal "[| 0 < r1; r1 <= r2; (0::hypreal) <= x; x <= y |] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
377 |
\ ==> r1 * x <= r2 * y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
378 |
by (rtac hypreal_less_or_eq_imp_le 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
379 |
by (REPEAT(dtac hypreal_le_imp_less_or_eq 1)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
380 |
by (auto_tac (claset() addIs [hypreal_mult_less_mono, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
381 |
hypreal_mult_less_mono1,hypreal_mult_less_mono2, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
382 |
hypreal_mult_order_trans,hypreal_mult_order],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
383 |
qed "hypreal_mult_le_mono"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
384 |
|
10607 | 385 |
Goal "0 < x ==> 0 < inverse (x::hypreal)"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
386 |
by (EVERY1[rtac ccontr, dtac hypreal_leI]); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
387 |
by (forward_tac [hypreal_minus_zero_less_iff2 RS iffD2] 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
388 |
by (forward_tac [hypreal_not_refl2 RS not_sym] 1); |
10607 | 389 |
by (dtac (hypreal_not_refl2 RS not_sym RS hypreal_inverse_not_zero) 1); |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
390 |
by (EVERY1[dtac hypreal_le_imp_less_or_eq, Step_tac]); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
391 |
by (dtac hypreal_mult_less_zero1 1 THEN assume_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
392 |
by (auto_tac (claset() addIs [hypreal_zero_less_one RS hypreal_less_asym], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
393 |
simpset() addsimps [hypreal_minus_zero_less_iff])); |
10607 | 394 |
qed "hypreal_inverse_gt_zero"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
395 |
|
10607 | 396 |
Goal "x < 0 ==> inverse (x::hypreal) < 0"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
397 |
by (ftac hypreal_not_refl2 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
398 |
by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
399 |
by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1); |
10607 | 400 |
by (dtac (hypreal_minus_inverse RS sym) 1); |
401 |
by (auto_tac (claset() addIs [hypreal_inverse_gt_zero], |
|
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
402 |
simpset())); |
10607 | 403 |
qed "hypreal_inverse_less_zero"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
404 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
405 |
(* check why this does not work without 2nd substitution anymore! *) |
10607 | 406 |
Goal "x < y ==> x < (x + y)*inverse(1hr + 1hr)"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
407 |
by (dres_inst_tac [("C","x")] hypreal_add_less_mono2 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
408 |
by (dtac (hypreal_add_self RS subst) 1); |
10607 | 409 |
by (dtac (hypreal_zero_less_two RS hypreal_inverse_gt_zero RS |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
410 |
hypreal_mult_less_mono1) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
411 |
by (auto_tac (claset() addDs [hypreal_two_not_zero RS |
10607 | 412 |
(hypreal_mult_inverse RS subst)],simpset() |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
413 |
addsimps [hypreal_mult_assoc])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
414 |
qed "hypreal_less_half_sum"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
415 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
416 |
(* check why this does not work without 2nd substitution anymore! *) |
10607 | 417 |
Goal "x < y ==> (x + y)*inverse(1hr + 1hr) < y"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
418 |
by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
419 |
by (dtac (hypreal_add_self RS subst) 1); |
10607 | 420 |
by (dtac (hypreal_zero_less_two RS hypreal_inverse_gt_zero RS |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
421 |
hypreal_mult_less_mono1) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
422 |
by (auto_tac (claset() addDs [hypreal_two_not_zero RS |
10607 | 423 |
(hypreal_mult_inverse RS subst)],simpset() |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
424 |
addsimps [hypreal_mult_assoc])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
425 |
qed "hypreal_gt_half_sum"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
426 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
427 |
Goal "!!(x::hypreal). x < y ==> EX r. x < r & r < y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
428 |
by (blast_tac (claset() addSIs [hypreal_less_half_sum, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
429 |
hypreal_gt_half_sum]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
430 |
qed "hypreal_dense"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
431 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
432 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
433 |
Goal "(x*x + y*y = 0) = (x = 0 & y = (0::hypreal))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
434 |
by Auto_tac; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
435 |
by (dtac (sym RS (hypreal_eq_minus_iff3 RS iffD1)) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
436 |
by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1)) 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
437 |
by (ALLGOALS(rtac ccontr)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
438 |
by (ALLGOALS(dtac hypreal_mult_self_not_zero)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
439 |
by (cut_inst_tac [("x1","x")] (hypreal_le_square |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
440 |
RS hypreal_le_imp_less_or_eq) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
441 |
by (cut_inst_tac [("x1","y")] (hypreal_le_square |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
442 |
RS hypreal_le_imp_less_or_eq) 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
443 |
by (auto_tac (claset() addDs [sym],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
444 |
by (dres_inst_tac [("x1","y")] (hypreal_less_minus_square |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
445 |
RS hypreal_le_less_trans) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
446 |
by (dres_inst_tac [("x1","x")] (hypreal_less_minus_square |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
447 |
RS hypreal_le_less_trans) 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
448 |
by (auto_tac (claset(),simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
449 |
[hypreal_less_not_refl])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
450 |
qed "hypreal_squares_add_zero_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
451 |
Addsimps [hypreal_squares_add_zero_iff]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
452 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
453 |
Goal "x * x ~= 0 ==> (0::hypreal) < x* x + y*y + z*z"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
454 |
by (cut_inst_tac [("x1","x")] (hypreal_le_square |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
455 |
RS hypreal_le_imp_less_or_eq) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
456 |
by (auto_tac (claset() addSIs |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
457 |
[hypreal_add_order_le],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
458 |
qed "hypreal_sum_squares3_gt_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
459 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
460 |
Goal "x * x ~= 0 ==> (0::hypreal) < y*y + x*x + z*z"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
461 |
by (dtac hypreal_sum_squares3_gt_zero 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
462 |
by (auto_tac (claset(),simpset() addsimps hypreal_add_ac)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
463 |
qed "hypreal_sum_squares3_gt_zero2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
464 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
465 |
Goal "x * x ~= 0 ==> (0::hypreal) < y*y + z*z + x*x"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
466 |
by (dtac hypreal_sum_squares3_gt_zero 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
467 |
by (auto_tac (claset(),simpset() addsimps hypreal_add_ac)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
468 |
qed "hypreal_sum_squares3_gt_zero3"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
469 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
470 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
471 |
Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
472 |
by Auto_tac; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
473 |
by (ALLGOALS(rtac ccontr)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
474 |
by (ALLGOALS(dtac hypreal_mult_self_not_zero)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
475 |
by (auto_tac (claset() addDs [hypreal_not_refl2 RS not_sym, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
476 |
hypreal_sum_squares3_gt_zero3,hypreal_sum_squares3_gt_zero, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
477 |
hypreal_sum_squares3_gt_zero2],simpset() delsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
478 |
[hypreal_mult_self_eq_zero_iff])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
479 |
qed "hypreal_three_squares_add_zero_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
480 |
Addsimps [hypreal_three_squares_add_zero_iff]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
481 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
482 |
Addsimps [rename_numerals real_le_square]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
483 |
Goal "(x::hypreal)*x <= x*x + y*y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
484 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
485 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
486 |
by (auto_tac (claset(),simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
487 |
[hypreal_mult,hypreal_add,hypreal_le])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
488 |
qed "hypreal_self_le_add_pos"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
489 |
Addsimps [hypreal_self_le_add_pos]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
490 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
491 |
Goal "(x::hypreal)*x <= x*x + y*y + z*z"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
492 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
493 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
494 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
495 |
by (auto_tac (claset(), |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
496 |
simpset() addsimps [hypreal_mult, hypreal_add, hypreal_le, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
497 |
rename_numerals real_le_add_order])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
498 |
qed "hypreal_self_le_add_pos2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
499 |
Addsimps [hypreal_self_le_add_pos2]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
500 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
501 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
502 |
(*--------------------------------------------------------------------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
503 |
Embedding of the naturals in the hyperreals |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
504 |
---------------------------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
505 |
Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 0 = 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
506 |
by (full_simp_tac (simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
507 |
[pnat_one_iff RS sym,real_of_preal_def]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
508 |
by (fold_tac [real_one_def]); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
509 |
by (simp_tac (simpset() addsimps [hypreal_of_real_one]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
510 |
qed "hypreal_of_posnat_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
511 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
512 |
Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
513 |
by (full_simp_tac (simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
514 |
[real_of_preal_def, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
515 |
rename_numerals (real_one_def RS meta_eq_to_obj_eq), |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
516 |
hypreal_add,hypreal_of_real_def,pnat_two_eq, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
517 |
hypreal_one_def, real_add, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
518 |
prat_of_pnat_add RS sym, preal_of_prat_add RS sym] @ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
519 |
pnat_add_ac) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
520 |
qed "hypreal_of_posnat_two"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
521 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
522 |
Goalw [hypreal_of_posnat_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
523 |
"hypreal_of_posnat n1 + hypreal_of_posnat n2 = \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
524 |
\ hypreal_of_posnat (n1 + n2) + 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
525 |
by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one RS sym, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
526 |
hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
527 |
preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
528 |
qed "hypreal_of_posnat_add"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
529 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
530 |
Goal "hypreal_of_posnat (n + 1) = hypreal_of_posnat n + 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
531 |
by (res_inst_tac [("x1","1hr")] (hypreal_add_right_cancel RS iffD1) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
532 |
by (rtac (hypreal_of_posnat_add RS subst) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
533 |
by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,hypreal_add_assoc]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
534 |
qed "hypreal_of_posnat_add_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
535 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
536 |
Goalw [real_of_posnat_def,hypreal_of_posnat_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
537 |
"hypreal_of_posnat n = hypreal_of_real (real_of_posnat n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
538 |
by (rtac refl 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
539 |
qed "hypreal_of_real_of_posnat"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
540 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
541 |
Goalw [hypreal_of_posnat_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
542 |
"(n < m) = (hypreal_of_posnat n < hypreal_of_posnat m)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
543 |
by Auto_tac; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
544 |
qed "hypreal_of_posnat_less_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
545 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
546 |
Addsimps [hypreal_of_posnat_less_iff RS sym]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
547 |
(*--------------------------------------------------------------------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
548 |
Existence of infinite hyperreal number |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
549 |
---------------------------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
550 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
551 |
Goal "hyprel^^{%n::nat. real_of_posnat n} : hypreal"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
552 |
by Auto_tac; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
553 |
qed "hypreal_omega"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
554 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
555 |
Goalw [omega_def] "Rep_hypreal(whr) : hypreal"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
556 |
by (rtac Rep_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
557 |
qed "Rep_hypreal_omega"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
558 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
559 |
(* existence of infinite number not corresponding to any real number *) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
560 |
(* use assumption that member FreeUltrafilterNat is not finite *) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
561 |
(* a few lemmas first *) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
562 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
563 |
Goal "{n::nat. x = real_of_posnat n} = {} | \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
564 |
\ (EX y. {n::nat. x = real_of_posnat n} = {y})"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
565 |
by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
566 |
qed "lemma_omega_empty_singleton_disj"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
567 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
568 |
Goal "finite {n::nat. x = real_of_posnat n}"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
569 |
by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
570 |
by Auto_tac; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
571 |
qed "lemma_finite_omega_set"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
572 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
573 |
Goalw [omega_def,hypreal_of_real_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
574 |
"~ (EX x. hypreal_of_real x = whr)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
575 |
by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
576 |
RS FreeUltrafilterNat_finite])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
577 |
qed "not_ex_hypreal_of_real_eq_omega"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
578 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
579 |
Goal "hypreal_of_real x ~= whr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
580 |
by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
581 |
by Auto_tac; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
582 |
qed "hypreal_of_real_not_eq_omega"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
583 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
584 |
(* existence of infinitesimal number also not *) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
585 |
(* corresponding to any real number *) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
586 |
|
10607 | 587 |
Goal "{n::nat. x = inverse(real_of_posnat n)} = {} | \ |
588 |
\ (EX y. {n::nat. x = inverse(real_of_posnat n)} = {y})"; |
|
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
589 |
by (Step_tac 1 THEN Step_tac 1); |
10607 | 590 |
by (auto_tac (claset() addIs [real_of_posnat_inverse_inj],simpset())); |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
591 |
qed "lemma_epsilon_empty_singleton_disj"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
592 |
|
10607 | 593 |
Goal "finite {n::nat. x = inverse(real_of_posnat n)}"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
594 |
by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
595 |
by Auto_tac; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
596 |
qed "lemma_finite_epsilon_set"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
597 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
598 |
Goalw [epsilon_def,hypreal_of_real_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
599 |
"~ (EX x. hypreal_of_real x = ehr)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
600 |
by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
601 |
RS FreeUltrafilterNat_finite])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
602 |
qed "not_ex_hypreal_of_real_eq_epsilon"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
603 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
604 |
Goal "hypreal_of_real x ~= ehr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
605 |
by (cut_facts_tac [not_ex_hypreal_of_real_eq_epsilon] 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
606 |
by Auto_tac; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
607 |
qed "hypreal_of_real_not_eq_epsilon"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
608 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
609 |
Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
610 |
by (auto_tac (claset(), |
10607 | 611 |
simpset() addsimps [rename_numerals real_of_posnat_inverse_not_zero])); |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
612 |
qed "hypreal_epsilon_not_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
613 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
614 |
Addsimps [rename_numerals real_of_posnat_not_eq_zero]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
615 |
Goalw [omega_def,hypreal_zero_def] "whr ~= 0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
616 |
by (Simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
617 |
qed "hypreal_omega_not_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
618 |
|
10607 | 619 |
Goal "ehr = inverse(whr)"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
620 |
by (asm_full_simp_tac (simpset() addsimps |
10607 | 621 |
[hypreal_inverse,omega_def,epsilon_def]) 1); |
622 |
qed "hypreal_epsilon_inverse_omega"; |
|
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
623 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
624 |
(*---------------------------------------------------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
625 |
Another embedding of the naturals in the |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
626 |
hyperreals (see hypreal_of_posnat) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
627 |
----------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
628 |
Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
629 |
by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
630 |
qed "hypreal_of_nat_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
631 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
632 |
Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
633 |
by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
634 |
hypreal_add_assoc]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
635 |
qed "hypreal_of_nat_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
636 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
637 |
Goalw [hypreal_of_nat_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
638 |
"hypreal_of_nat n1 + hypreal_of_nat n2 = \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
639 |
\ hypreal_of_nat (n1 + n2)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
640 |
by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
641 |
by (simp_tac (simpset() addsimps [hypreal_of_posnat_add, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
642 |
hypreal_add_assoc RS sym]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
643 |
qed "hypreal_of_nat_add"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
644 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
645 |
Goal "hypreal_of_nat 2 = 1hr + 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
646 |
by (simp_tac (simpset() addsimps [hypreal_of_nat_one |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
647 |
RS sym,hypreal_of_nat_add]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
648 |
qed "hypreal_of_nat_two"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
649 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
650 |
Goalw [hypreal_of_nat_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
651 |
"(n < m) = (hypreal_of_nat n < hypreal_of_nat m)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
652 |
by (auto_tac (claset() addIs [hypreal_add_less_mono1],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
653 |
qed "hypreal_of_nat_less_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
654 |
Addsimps [hypreal_of_nat_less_iff RS sym]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
655 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
656 |
(*------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
657 |
(* naturals embedded in hyperreals *) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
658 |
(* is a hyperreal c.f. NS extension *) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
659 |
(*------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
660 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
661 |
Goalw [hypreal_of_nat_def,real_of_nat_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
662 |
"hypreal_of_nat m = Abs_hypreal(hyprel^^{%n. real_of_nat m})"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
663 |
by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
664 |
hypreal_of_real_of_posnat,hypreal_minus,hypreal_one_def,hypreal_add])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
665 |
qed "hypreal_of_nat_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
666 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
667 |
Goal "inj hypreal_of_nat"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
668 |
by (rtac injI 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
669 |
by (auto_tac (claset() addSDs [FreeUltrafilterNat_P], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
670 |
simpset() addsimps [split_if_mem1, hypreal_of_nat_iff, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
671 |
real_add_right_cancel,inj_real_of_nat RS injD])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
672 |
qed "inj_hypreal_of_nat"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
673 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
674 |
Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
675 |
real_of_posnat_def,hypreal_one_def,real_of_nat_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
676 |
"hypreal_of_nat n = hypreal_of_real (real_of_nat n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
677 |
by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
678 |
qed "hypreal_of_nat_real_of_nat"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
679 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
680 |
Goal "hypreal_of_posnat (Suc n) = hypreal_of_posnat n + 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
681 |
by (stac (hypreal_of_posnat_add_one RS sym) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
682 |
by (Simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
683 |
qed "hypreal_of_posnat_Suc"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
684 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
685 |
Goalw [hypreal_of_nat_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
686 |
"hypreal_of_nat (Suc n) = hypreal_of_nat n + 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
687 |
by (simp_tac (simpset() addsimps [hypreal_of_posnat_Suc] @ hypreal_add_ac) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
688 |
qed "hypreal_of_nat_Suc"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
689 |
|
10607 | 690 |
Goal "0 < r ==> 0 < r*inverse(1hr+1hr)"; |
691 |
by (dtac (hypreal_zero_less_two RS hypreal_inverse_gt_zero |
|
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
692 |
RS hypreal_mult_less_mono1) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
693 |
by Auto_tac; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
694 |
qed "hypreal_half_gt_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
695 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
696 |
(* this proof is so much simpler than one for reals!! *) |
10607 | 697 |
Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
698 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
699 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
10607 | 700 |
by (auto_tac (claset(),simpset() addsimps [hypreal_inverse, |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
701 |
hypreal_less,hypreal_zero_def])); |
10607 | 702 |
by (ultra_tac (claset() addIs [real_inverse_less_swap],simpset()) 1); |
703 |
qed "hypreal_inverse_less_swap"; |
|
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
704 |
|
10607 | 705 |
Goal "[| 0 < r; 0 < x|] ==> (r < x) = (inverse x < inverse (r::hypreal))"; |
706 |
by (auto_tac (claset() addIs [hypreal_inverse_less_swap],simpset())); |
|
707 |
by (res_inst_tac [("t","r")] (hypreal_inverse_inverse RS subst) 1); |
|
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
708 |
by (etac (hypreal_not_refl2 RS not_sym) 1); |
10607 | 709 |
by (res_inst_tac [("t","x")] (hypreal_inverse_inverse RS subst) 1); |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
710 |
by (etac (hypreal_not_refl2 RS not_sym) 1); |
10607 | 711 |
by (auto_tac (claset() addIs [hypreal_inverse_less_swap], |
712 |
simpset() addsimps [hypreal_inverse_gt_zero])); |
|
713 |
qed "hypreal_inverse_less_iff"; |
|
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
714 |
|
10607 | 715 |
Goal "[| 0 < z; x < y |] ==> x * inverse z < y * inverse (z::hypreal)"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
716 |
by (blast_tac (claset() addSIs [hypreal_mult_less_mono1, |
10607 | 717 |
hypreal_inverse_gt_zero]) 1); |
718 |
qed "hypreal_mult_inverse_less_mono1"; |
|
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
719 |
|
10607 | 720 |
Goal "[| 0 < z; x < y |] ==> inverse z * x < inverse (z::hypreal) * y"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
721 |
by (blast_tac (claset() addSIs [hypreal_mult_less_mono2, |
10607 | 722 |
hypreal_inverse_gt_zero]) 1); |
723 |
qed "hypreal_mult_inverse_less_mono2"; |
|
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
724 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
725 |
Goal "[| (0::hypreal) < z; x*z < y*z |] ==> x < y"; |
10607 | 726 |
by (forw_inst_tac [("x","x*z")] hypreal_mult_inverse_less_mono1 1); |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
727 |
by (dtac (hypreal_not_refl2 RS not_sym) 2); |
10607 | 728 |
by (auto_tac (claset() addSDs [hypreal_mult_inverse], |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
729 |
simpset() addsimps hypreal_mult_ac)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
730 |
qed "hypreal_less_mult_right_cancel"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
731 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
732 |
Goal "[| (0::hypreal) < z; z*x < z*y |] ==> x < y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
733 |
by (auto_tac (claset() addIs [hypreal_less_mult_right_cancel], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
734 |
simpset() addsimps [hypreal_mult_commute])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
735 |
qed "hypreal_less_mult_left_cancel"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
736 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
737 |
Goal "[| 0 < r; (0::hypreal) < ra; \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
738 |
\ r < x; ra < y |] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
739 |
\ ==> r*ra < x*y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
740 |
by (forw_inst_tac [("R2.0","r")] hypreal_less_trans 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
741 |
by (dres_inst_tac [("z","ra"),("x","r")] hypreal_mult_less_mono1 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
742 |
by (dres_inst_tac [("z","x"),("x","ra")] hypreal_mult_less_mono2 3); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
743 |
by (auto_tac (claset() addIs [hypreal_less_trans],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
744 |
qed "hypreal_mult_less_gt_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
745 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
746 |
Goal "[| 0 < r; (0::hypreal) < ra; \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
747 |
\ r <= x; ra <= y |] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
748 |
\ ==> r*ra <= x*y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
749 |
by (REPEAT(dtac hypreal_le_imp_less_or_eq 1)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
750 |
by (rtac hypreal_less_or_eq_imp_le 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
751 |
by (auto_tac (claset() addIs [hypreal_mult_less_mono1, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
752 |
hypreal_mult_less_mono2,hypreal_mult_less_gt_zero], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
753 |
simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
754 |
qed "hypreal_mult_le_ge_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
755 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
756 |
(*---------------------------------------------------------------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
757 |
Some convenient biconditionals for products of signs |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
758 |
----------------------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
759 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
760 |
Goal "((0::hypreal) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
761 |
by (auto_tac (claset(), simpset() addsimps [order_le_less, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
762 |
linorder_not_less, hypreal_mult_order, hypreal_mult_less_zero1])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
763 |
by (ALLGOALS (rtac ccontr)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
764 |
by (auto_tac (claset(), simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
765 |
[order_le_less, linorder_not_less])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
766 |
by (ALLGOALS (etac rev_mp)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
767 |
by (ALLGOALS (dtac hypreal_mult_less_zero THEN' assume_tac)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
768 |
by (auto_tac (claset() addDs [order_less_not_sym], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
769 |
simpset() addsimps [hypreal_mult_commute])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
770 |
qed "hypreal_zero_less_mult_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
771 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
772 |
Goal "((0::hypreal) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
773 |
by (auto_tac (claset() addDs [sym RS hypreal_mult_zero_disj], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
774 |
simpset() addsimps [order_le_less, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
775 |
linorder_not_less,hypreal_zero_less_mult_iff])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
776 |
qed "hypreal_zero_le_mult_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
777 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
778 |
Goal "(x*y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
779 |
by (auto_tac (claset(), |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
780 |
simpset() addsimps [hypreal_zero_le_mult_iff, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
781 |
linorder_not_le RS sym])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
782 |
by (auto_tac (claset() addDs [order_less_not_sym], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
783 |
simpset() addsimps [linorder_not_le])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
784 |
qed "hypreal_mult_less_zero_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
785 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
786 |
Goal "(x*y <= (0::hypreal)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
787 |
by (auto_tac (claset() addDs [order_less_not_sym], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
788 |
simpset() addsimps [hypreal_zero_less_mult_iff, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
789 |
linorder_not_less RS sym])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
790 |
qed "hypreal_mult_le_zero_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
791 |