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