92 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
92 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
93 by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs, |
93 by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs, |
94 hypreal_mult,abs_mult])); |
94 hypreal_mult,abs_mult])); |
95 qed "hrabs_mult"; |
95 qed "hrabs_mult"; |
96 |
96 |
97 Goal "x~= (0::hypreal) ==> abs(inverse(x)) = inverse(abs(x))"; |
97 Goal "abs(inverse(x)) = inverse(abs(x::hypreal))"; |
98 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
98 by (hypreal_div_undefined_case_tac "x=0" 1); |
99 by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs, |
99 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
100 hypreal_inverse,hypreal_zero_def])); |
100 by (auto_tac (claset(), |
101 by (ultra_tac (claset(),simpset() addsimps [abs_inverse]) 1); |
101 simpset() addsimps [hypreal_hrabs, |
102 by (arith_tac 1); |
102 hypreal_inverse,hypreal_zero_def])); |
|
103 by (ultra_tac (claset(), simpset() addsimps [abs_inverse]) 1); |
103 qed "hrabs_inverse"; |
104 qed "hrabs_inverse"; |
104 |
|
105 (* old version of proof: |
|
106 Goalw [hrabs_def] |
|
107 "x~= (0::hypreal) ==> abs(inverse(x)) = inverse(abs(x))"; |
|
108 by (auto_tac (claset(),simpset() addsimps [hypreal_minus_inverse])); |
|
109 by (ALLGOALS(dtac not_hypreal_leE)); |
|
110 by (etac hypreal_less_asym 1); |
|
111 by (blast_tac (claset() addDs [hypreal_le_imp_less_or_eq, |
|
112 hypreal_inverse_gt_zero]) 1); |
|
113 by (dtac (hreal_inverse_not_zero RS not_sym) 1); |
|
114 by (rtac (hypreal_inverse_less_zero RSN (2,hypreal_less_asym)) 1); |
|
115 by (assume_tac 2); |
|
116 by (blast_tac (claset() addSDs [hypreal_le_imp_less_or_eq]) 1); |
|
117 qed "hrabs_inverse"; |
|
118 *) |
|
119 |
|
120 val [prem] = goal thy "y ~= (0::hypreal) ==> \ |
|
121 \ abs(x*inverse(y)) = abs(x)*inverse(abs(y))"; |
|
122 by (res_inst_tac [("c1","abs y")] (hypreal_mult_left_cancel RS subst) 1); |
|
123 by (simp_tac (simpset() addsimps [(hrabs_not_zero_iff RS sym), prem]) 1); |
|
124 by (simp_tac (simpset() addsimps [(hrabs_mult RS sym), prem, |
|
125 hrabs_not_zero_iff RS sym] @ hypreal_mult_ac) 1); |
|
126 qed "hrabs_mult_inverse"; |
|
127 |
105 |
128 Goal "abs(x+(y::hypreal)) <= abs x + abs y"; |
106 Goal "abs(x+(y::hypreal)) <= abs x + abs y"; |
129 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
107 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
130 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
108 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
131 by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs, |
109 by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs, |