21 (*------------------------------------------------------------ |
21 (*------------------------------------------------------------ |
22 Properties of the absolute value function over the reals |
22 Properties of the absolute value function over the reals |
23 (adapted version of previously proved theorems about abs) |
23 (adapted version of previously proved theorems about abs) |
24 ------------------------------------------------------------*) |
24 ------------------------------------------------------------*) |
25 |
25 |
26 Goal "abs (0::hypreal) = 0"; |
|
27 by (simp_tac (simpset() addsimps [hrabs_def]) 1); |
|
28 qed "hrabs_zero"; |
|
29 Addsimps [hrabs_zero]; |
|
30 |
|
31 Goal "abs (1::hypreal) = 1"; |
|
32 by (simp_tac (simpset() addsimps [hrabs_def]) 1); |
|
33 qed "hrabs_one"; |
|
34 Addsimps [hrabs_one]; |
|
35 |
|
36 Goal "(0::hypreal)<=x ==> abs x = x"; |
26 Goal "(0::hypreal)<=x ==> abs x = x"; |
37 by (asm_simp_tac (simpset() addsimps [hrabs_def]) 1); |
27 by (asm_simp_tac (simpset() addsimps [hrabs_def]) 1); |
38 qed "hrabs_eqI1"; |
28 qed "hrabs_eqI1"; |
39 |
29 |
40 Goal "(0::hypreal)<x ==> abs x = x"; |
30 Goal "(0::hypreal)<x ==> abs x = x"; |
46 qed "hrabs_minus_eqI2"; |
36 qed "hrabs_minus_eqI2"; |
47 |
37 |
48 Goal "x<=(0::hypreal) ==> abs x = -x"; |
38 Goal "x<=(0::hypreal) ==> abs x = -x"; |
49 by (auto_tac (claset() addDs [order_antisym], simpset() addsimps [hrabs_def]));qed "hrabs_minus_eqI1"; |
39 by (auto_tac (claset() addDs [order_antisym], simpset() addsimps [hrabs_def]));qed "hrabs_minus_eqI1"; |
50 |
40 |
51 Goal "(0::hypreal)<= abs x"; |
41 Addsimps [abs_mult]; |
52 by (simp_tac (simpset() addsimps [hrabs_def]) 1); |
|
53 qed "hrabs_ge_zero"; |
|
54 |
|
55 Goal "abs(abs x) = abs (x::hypreal)"; |
|
56 by (simp_tac (simpset() addsimps [hrabs_def]) 1); |
|
57 qed "hrabs_idempotent"; |
|
58 Addsimps [hrabs_idempotent]; |
|
59 |
|
60 Goalw [hrabs_def] "(abs x = (0::hypreal)) = (x=0)"; |
|
61 by (Simp_tac 1); |
|
62 qed "hrabs_zero_iff"; |
|
63 AddIffs [hrabs_zero_iff]; |
|
64 |
|
65 Goalw [hrabs_def] "(x::hypreal) <= abs x"; |
|
66 by (Simp_tac 1); |
|
67 qed "hrabs_ge_self"; |
|
68 |
|
69 Goalw [hrabs_def] "-(x::hypreal) <= abs x"; |
|
70 by (Simp_tac 1); |
|
71 qed "hrabs_ge_minus_self"; |
|
72 |
|
73 (* proof by "transfer" *) |
|
74 Goal "abs(x*(y::hypreal)) = (abs x)*(abs y)"; |
|
75 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
76 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
77 by (auto_tac (claset(), |
|
78 simpset() addsimps [hypreal_hrabs, hypreal_mult,abs_mult])); |
|
79 qed "hrabs_mult"; |
|
80 Addsimps [hrabs_mult]; |
|
81 |
|
82 Goal "abs(inverse(x)) = inverse(abs(x::hypreal))"; |
|
83 by (simp_tac (simpset() addsimps [hypreal_minus_inverse, hrabs_def]) 1); |
|
84 qed "hrabs_inverse"; |
|
85 |
|
86 Goalw [hrabs_def] "abs(x+(y::hypreal)) <= abs x + abs y"; |
|
87 by (Simp_tac 1); |
|
88 qed "hrabs_triangle_ineq"; |
|
89 |
|
90 Goal "abs((w::hypreal) + x + y) <= abs(w) + abs(x) + abs(y)"; |
|
91 by (simp_tac (simpset() addsimps [hrabs_triangle_ineq RS order_trans]) 1); |
|
92 qed "hrabs_triangle_ineq_three"; |
|
93 |
|
94 Goalw [hrabs_def] "abs(-x) = abs((x::hypreal))"; |
|
95 by (Simp_tac 1); |
|
96 qed "hrabs_minus_cancel"; |
|
97 Addsimps [hrabs_minus_cancel]; |
|
98 |
42 |
99 Goalw [hrabs_def] "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"; |
43 Goalw [hrabs_def] "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"; |
100 by (asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1); |
44 by (asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1); |
101 qed "hrabs_add_less"; |
45 qed "hrabs_add_less"; |
102 |
46 |
103 Goal "[| abs x<r; abs y<s |] ==> abs x * abs y < r * (s::hypreal)"; |
|
104 by (subgoal_tac "0 < r" 1); |
|
105 by (asm_full_simp_tac (simpset() addsimps [hrabs_def] |
|
106 addsplits [split_if_asm]) 2); |
|
107 by (case_tac "y = 0" 1); |
|
108 by (asm_full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 1); |
|
109 by (rtac hypreal_mult_less_mono 1); |
|
110 by (auto_tac (claset(), |
|
111 simpset() addsimps [hrabs_def, linorder_neq_iff] |
|
112 addsplits [split_if_asm])); |
|
113 qed "hrabs_mult_less"; |
|
114 |
|
115 Goal "((0::hypreal) < abs x) = (x ~= 0)"; |
|
116 by (simp_tac (simpset() addsimps [hrabs_def]) 1); |
|
117 by (arith_tac 1); |
|
118 qed "hypreal_0_less_abs_iff"; |
|
119 Addsimps [hypreal_0_less_abs_iff]; |
|
120 |
|
121 Goal "abs x < r ==> (0::hypreal) < r"; |
47 Goal "abs x < r ==> (0::hypreal) < r"; |
122 by (blast_tac (claset() addSIs [order_le_less_trans, hrabs_ge_zero]) 1); |
48 by (blast_tac (claset() addSIs [order_le_less_trans, abs_ge_zero]) 1); |
123 qed "hrabs_less_gt_zero"; |
49 qed "hrabs_less_gt_zero"; |
124 |
50 |
125 Goal "abs x = (x::hypreal) | abs x = -x"; |
51 Goal "abs x = (x::hypreal) | abs x = -x"; |
126 by (simp_tac (simpset() addsimps [hrabs_def]) 1); |
52 by (simp_tac (simpset() addsimps [hrabs_def]) 1); |
127 qed "hrabs_disj"; |
53 qed "hrabs_disj"; |
129 Goal "abs x = (y::hypreal) ==> x = y | -x = y"; |
55 Goal "abs x = (y::hypreal) ==> x = y | -x = y"; |
130 by (asm_full_simp_tac (simpset() addsimps [hrabs_def] |
56 by (asm_full_simp_tac (simpset() addsimps [hrabs_def] |
131 addsplits [split_if_asm]) 1); |
57 addsplits [split_if_asm]) 1); |
132 qed "hrabs_eq_disj"; |
58 qed "hrabs_eq_disj"; |
133 |
59 |
134 Goalw [hrabs_def] "(abs x < (r::hypreal)) = (-r < x & x < r)"; |
|
135 by Auto_tac; |
|
136 qed "hrabs_interval_iff"; |
|
137 |
|
138 Goal "(abs x < (r::hypreal)) = (- x < r & x < r)"; |
|
139 by (auto_tac (claset(), simpset() addsimps [hrabs_interval_iff])); |
|
140 qed "hrabs_interval_iff2"; |
|
141 |
|
142 |
|
143 (* Needed in Geom.ML *) |
60 (* Needed in Geom.ML *) |
144 Goal "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"; |
61 Goal "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"; |
145 by (asm_full_simp_tac (simpset() addsimps [hrabs_def] |
62 by (asm_full_simp_tac (simpset() addsimps [hrabs_def] |
146 addsplits [split_if_asm]) 1); |
63 addsplits [split_if_asm]) 1); |
147 qed "hrabs_add_lemma_disj"; |
64 qed "hrabs_add_lemma_disj"; |
148 |
|
149 Goal "abs((x::hypreal) + -y) = abs (y + -x)"; |
|
150 by (simp_tac (simpset() addsimps [hrabs_def]) 1); |
|
151 qed "hrabs_minus_add_cancel"; |
|
152 |
65 |
153 (* Needed in Geom.ML?? *) |
66 (* Needed in Geom.ML?? *) |
154 Goal "(x::hypreal) + - y + (z + - y) = abs (x + - z) ==> y = z | x = y"; |
67 Goal "(x::hypreal) + - y + (z + - y) = abs (x + - z) ==> y = z | x = y"; |
155 by (asm_full_simp_tac (simpset() addsimps [hrabs_def] |
68 by (asm_full_simp_tac (simpset() addsimps [hrabs_def] |
156 addsplits [split_if_asm]) 1); |
69 addsplits [split_if_asm]) 1); |