58 |
58 |
59 (*17.9.02 aus SqRoot.thy------------------------------^^^---*) |
59 (*17.9.02 aus SqRoot.thy------------------------------^^^---*) |
60 |
60 |
61 axioms (*TODO: prove as theorems*) |
61 axioms (*TODO: prove as theorems*) |
62 |
62 |
63 radd_mult_distrib2 "(k::real) * (m + n) = k * m + k * n" |
63 radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n" |
64 rdistr_right_assoc "(k::real) + l * n + m * n = k + (l + m) * n" |
64 rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n" |
65 rdistr_right_assoc_p "l * n + (m * n + (k::real)) = (l + m) * n + k" |
65 rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k" |
66 rdistr_div_right "((k::real) + l) / n = k / n + l / n" |
66 rdistr_div_right: "((k::real) + l) / n = k / n + l / n" |
67 rcollect_right |
67 rcollect_right: |
68 "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" |
68 "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" |
69 rcollect_one_left |
69 rcollect_one_left: |
70 "m is_const ==> (n::real) + m * n = (1 + m) * n" |
70 "m is_const ==> (n::real) + m * n = (1 + m) * n" |
71 rcollect_one_left_assoc |
71 rcollect_one_left_assoc: |
72 "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" |
72 "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" |
73 rcollect_one_left_assoc_p |
73 rcollect_one_left_assoc_p: |
74 "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k" |
74 "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k" |
75 |
75 |
76 rtwo_of_the_same "a + a = 2 * a" |
76 rtwo_of_the_same: "a + a = 2 * a" |
77 rtwo_of_the_same_assoc "(x + a) + a = x + 2 * a" |
77 rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a" |
78 rtwo_of_the_same_assoc_p"a + (a + x) = 2 * a + x" |
78 rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" |
79 |
79 |
80 rcancel_den "not(a=0) ==> a * (b / a) = b" |
80 rcancel_den: "not(a=0) ==> a * (b / a) = b" |
81 rcancel_const "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" |
81 rcancel_const: "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" |
82 rshift_nominator "(a::real) * b / c = a / c * b" |
82 rshift_nominator: "(a::real) * b / c = a / c * b" |
83 |
83 |
84 exp_pow "(a ^^^ b) ^^^ c = a ^^^ (b * c)" |
84 exp_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" |
85 rsqare "(a::real) * a = a ^^^ 2" |
85 rsqare: "(a::real) * a = a ^^^ 2" |
86 power_1 "(a::real) ^^^ 1 = a" |
86 power_1: "(a::real) ^^^ 1 = a" |
87 rbinom_power_2 "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2" |
87 rbinom_power_2: "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2" |
88 |
88 |
89 rmult_1 "1 * k = (k::real)" |
89 rmult_1: "1 * k = (k::real)" |
90 rmult_1_right "k * 1 = (k::real)" |
90 rmult_1_right: "k * 1 = (k::real)" |
91 rmult_0 "0 * k = (0::real)" |
91 rmult_0: "0 * k = (0::real)" |
92 rmult_0_right "k * 0 = (0::real)" |
92 rmult_0_right: "k * 0 = (0::real)" |
93 radd_0 "0 + k = (k::real)" |
93 radd_0: "0 + k = (k::real)" |
94 radd_0_right "k + 0 = (k::real)" |
94 radd_0_right: "k + 0 = (k::real)" |
95 |
95 |
96 radd_real_const_eq |
96 radd_real_const_eq: |
97 "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" |
97 "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" |
98 radd_real_const |
98 radd_real_const: |
99 "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))" |
99 "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))" |
100 |
100 |
101 (*for AC-operators*) |
101 (*for AC-operators*) |
102 radd_commute "(m::real) + (n::real) = n + m" |
102 radd_commute: "(m::real) + (n::real) = n + m" |
103 radd_left_commute "(x::real) + (y + z) = y + (x + z)" |
103 radd_left_commute: "(x::real) + (y + z) = y + (x + z)" |
104 radd_assoc "(m::real) + n + k = m + (n + k)" |
104 radd_assoc: "(m::real) + n + k = m + (n + k)" |
105 rmult_commute "(m::real) * n = n * m" |
105 rmult_commute: "(m::real) * n = n * m" |
106 rmult_left_commute "(x::real) * (y * z) = y * (x * z)" |
106 rmult_left_commute: "(x::real) * (y * z) = y * (x * z)" |
107 rmult_assoc "(m::real) * n * k = m * (n * k)" |
107 rmult_assoc: "(m::real) * n * k = m * (n * k)" |
108 |
108 |
109 (*for equations: 'bdv' is a meta-constant*) |
109 (*for equations: 'bdv' is a meta-constant*) |
110 risolate_bdv_add "((k::real) + bdv = m) = (bdv = m + (-1)*k)" |
110 risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)" |
111 risolate_bdv_mult_add "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" |
111 risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" |
112 risolate_bdv_mult "((n::real) * bdv = m) = (bdv = m / n)" |
112 risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)" |
113 |
113 |
114 rnorm_equation_add |
114 rnorm_equation_add: |
115 "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" |
115 "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" |
116 |
116 |
117 (*17.9.02 aus SqRoot.thy------------------------------vvv---*) |
117 (*17.9.02 aus SqRoot.thy------------------------------vvv---*) |
118 root_ge0 "0 <= a ==> 0 <= sqrt a" |
118 root_ge0: "0 <= a ==> 0 <= sqrt a" |
119 (*should be dropped with better simplification in eval_rls ...*) |
119 (*should be dropped with better simplification in eval_rls ...*) |
120 root_add_ge0 |
120 root_add_ge0: |
121 "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" |
121 "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" |
122 root_ge0_1 |
122 root_ge0_1: |
123 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" |
123 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" |
124 root_ge0_2 |
124 root_ge0_2: |
125 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" |
125 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" |
126 |
126 |
127 |
127 |
128 rroot_square_inv "(sqrt a)^^^ 2 = a" |
128 rroot_square_inv: "(sqrt a)^^^ 2 = a" |
129 rroot_times_root "sqrt a * sqrt b = sqrt(a*b)" |
129 rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)" |
130 rroot_times_root_assoc "(a * sqrt b) * sqrt c = a * sqrt(b*c)" |
130 rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)" |
131 rroot_times_root_assoc_p "sqrt b * (sqrt c * a)= sqrt(b*c) * a" |
131 rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a" |
132 |
132 |
133 |
133 |
134 (*for root-equations*) |
134 (*for root-equations*) |
135 square_equation_left |
135 square_equation_left: |
136 "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))" |
136 "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))" |
137 square_equation_right |
137 square_equation_right: |
138 "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))" |
138 "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))" |
139 (*causes frequently non-termination:*) |
139 (*causes frequently non-termination:*) |
140 square_equation |
140 square_equation: |
141 "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))" |
141 "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))" |
142 |
142 |
143 risolate_root_add "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)" |
143 risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)" |
144 risolate_root_mult "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" |
144 risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" |
145 risolate_root_div "(a * sqrt c = d) = ( sqrt c = d / a)" |
145 risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)" |
146 |
146 |
147 (*for polynomial equations of degree 2; linear case in RatArith*) |
147 (*for polynomial equations of degree 2; linear case in RatArith*) |
148 mult_square "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)" |
148 mult_square: "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)" |
149 constant_square "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)" |
149 constant_square: "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)" |
150 constant_mult_square "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)" |
150 constant_mult_square: "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)" |
151 |
151 |
152 square_equality |
152 square_equality: |
153 "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" |
153 "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" |
154 square_equality_0 |
154 square_equality_0: |
155 "(x^^^2 = 0) = (x = 0)" |
155 "(x^^^2 = 0) = (x = 0)" |
156 |
156 |
157 (*isolate root on the LEFT hand side of the equation |
157 (*isolate root on the LEFT hand side of the equation |
158 otherwise shuffling from left to right would not terminate*) |
158 otherwise shuffling from left to right would not terminate*) |
159 |
159 |
160 rroot_to_lhs |
160 rroot_to_lhs: |
161 "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" |
161 "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" |
162 rroot_to_lhs_mult |
162 rroot_to_lhs_mult: |
163 "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" |
163 "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" |
164 rroot_to_lhs_add_mult |
164 rroot_to_lhs_add_mult: |
165 "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)" |
165 "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)" |
166 (*17.9.02 aus SqRoot.thy------------------------------^^^---*) |
166 (*17.9.02 aus SqRoot.thy------------------------------^^^---*) |
167 |
167 |
168 ML {* |
168 ML {* |
169 val thy = @{theory}; |
169 val thy = @{theory}; |