1.1 --- a/src/Tools/isac/Knowledge/Poly.thy Tue Aug 31 15:36:57 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Aug 31 16:00:13 2010 +0200
1.3 @@ -391,7 +391,7 @@
1.4 val Poly_erls =
1.5 append_rls "Poly_erls" Atools_erls
1.6 [ Calc ("op =",eval_equal "#equal_"),
1.7 - Thm ("real_unari_minus",num_str real_unari_minus),
1.8 + Thm ("real_unari_minus",num_str @{real_unari_minus),
1.9 Calc ("op +",eval_binop "#add_"),
1.10 Calc ("op -",eval_binop "#sub_"),
1.11 Calc ("op *",eval_binop "#mult_"),
1.12 @@ -401,7 +401,7 @@
1.13 val poly_crls =
1.14 append_rls "poly_crls" Atools_crls
1.15 [ Calc ("op =",eval_equal "#equal_"),
1.16 - Thm ("real_unari_minus",num_str real_unari_minus),
1.17 + Thm ("real_unari_minus",num_str @{real_unari_minus),
1.18 Calc ("op +",eval_binop "#add_"),
1.19 Calc ("op -",eval_binop "#sub_"),
1.20 Calc ("op *",eval_binop "#mult_"),
1.21 @@ -505,9 +505,9 @@
1.22 erls = e_rls,srls = Erls,
1.23 calc = [],
1.24 (*asm_thm = [],*)
1.25 - rules = [Thm ("real_diff_minus",num_str real_diff_minus),
1.26 + rules = [Thm ("real_diff_minus",num_str @{real_diff_minus),
1.27 (*"a - b = a + -1 * b"*)
1.28 - Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym))
1.29 + Thm ("sym_real_mult_minus1",num_str @{(real_mult_minus1 RS sym))
1.30 (*- ?z = "-1 * ?z"*)
1.31 ], scr = EmptyScr}:rls;
1.32 val expand_poly_ =
1.33 @@ -516,23 +516,23 @@
1.34 erls = e_rls,srls = Erls,
1.35 calc = [],
1.36 (*asm_thm = [],*)
1.37 - rules = [Thm ("real_plus_binom_pow4",num_str real_plus_binom_pow4),
1.38 + rules = [Thm ("real_plus_binom_pow4",num_str @{real_plus_binom_pow4),
1.39 (*"(a + b)^^^4 = ... "*)
1.40 - Thm ("real_plus_binom_pow5",num_str real_plus_binom_pow5),
1.41 + Thm ("real_plus_binom_pow5",num_str @{real_plus_binom_pow5),
1.42 (*"(a + b)^^^5 = ... "*)
1.43 - Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),
1.44 + Thm ("real_plus_binom_pow3",num_str @{real_plus_binom_pow3),
1.45 (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
1.46
1.47 (*WN071229 changed/removed for Schaerding -----vvv*)
1.48 - (*Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),*)
1.49 + (*Thm ("real_plus_binom_pow2",num_str @{real_plus_binom_pow2),*)
1.50 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
1.51 - Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),
1.52 + Thm ("real_plus_binom_pow2",num_str @{real_plus_binom_pow2),
1.53 (*"(a + b)^^^2 = (a + b) * (a + b)"*)
1.54 (*Thm ("real_plus_minus_binom1_p_p",
1.55 - num_str real_plus_minus_binom1_p_p),*)
1.56 + num_str @{real_plus_minus_binom1_p_p),*)
1.57 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
1.58 (*Thm ("real_plus_minus_binom2_p_p",
1.59 - num_str real_plus_minus_binom2_p_p),*)
1.60 + num_str @{real_plus_minus_binom2_p_p),*)
1.61 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
1.62 (*WN071229 changed/removed for Schaerding -----^^^*)
1.63
1.64 @@ -541,9 +541,9 @@
1.65 Thm ("left_distrib2",num_str @{thm left_distrib}2),
1.66 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.67
1.68 - Thm ("realpow_multI", num_str realpow_multI),
1.69 + Thm ("realpow_multI", num_str @{realpow_multI),
1.70 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.71 - Thm ("realpow_pow",num_str realpow_pow)
1.72 + Thm ("realpow_pow",num_str @{realpow_pow)
1.73 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.74 ], scr = EmptyScr}:rls;
1.75
1.76 @@ -586,19 +586,19 @@
1.77 calc = [],
1.78 (*asm_thm = [],*)
1.79 rules =
1.80 - [Thm ("real_plus_binom_pow4_poly", num_str real_plus_binom_pow4_poly),
1.81 + [Thm ("real_plus_binom_pow4_poly", num_str @{real_plus_binom_pow4_poly),
1.82 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^4 = ... "*)
1.83 - Thm ("real_plus_binom_pow5_poly", num_str real_plus_binom_pow5_poly),
1.84 + Thm ("real_plus_binom_pow5_poly", num_str @{real_plus_binom_pow5_poly),
1.85 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^5 = ... "*)
1.86 - Thm ("real_plus_binom_pow2_poly",num_str real_plus_binom_pow2_poly),
1.87 + Thm ("real_plus_binom_pow2_poly",num_str @{real_plus_binom_pow2_poly),
1.88 (*"[| a is_polyexp; b is_polyexp |] ==>
1.89 (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
1.90 - Thm ("real_plus_binom_pow3_poly",num_str real_plus_binom_pow3_poly),
1.91 + Thm ("real_plus_binom_pow3_poly",num_str @{real_plus_binom_pow3_poly),
1.92 (*"[| a is_polyexp; b is_polyexp |] ==>
1.93 (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
1.94 - Thm ("real_plus_minus_binom1_p_p",num_str real_plus_minus_binom1_p_p),
1.95 + Thm ("real_plus_minus_binom1_p_p",num_str @{real_plus_minus_binom1_p_p),
1.96 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
1.97 - Thm ("real_plus_minus_binom2_p_p",num_str real_plus_minus_binom2_p_p),
1.98 + Thm ("real_plus_minus_binom2_p_p",num_str @{real_plus_minus_binom2_p_p),
1.99 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
1.100
1.101 Thm ("left_distrib_poly" ,num_str @{thm left_distrib}_poly),
1.102 @@ -606,10 +606,10 @@
1.103 Thm("left_distrib2_poly",num_str @{thm left_distrib}2_poly),
1.104 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.105
1.106 - Thm ("realpow_multI_poly", num_str realpow_multI_poly),
1.107 + Thm ("realpow_multI_poly", num_str @{realpow_multI_poly),
1.108 (*"[| r is_polyexp; s is_polyexp |] ==>
1.109 (r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.110 - Thm ("realpow_pow",num_str realpow_pow)
1.111 + Thm ("realpow_pow",num_str @{realpow_pow)
1.112 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.113 ], scr = EmptyScr}:rls;
1.114
1.115 @@ -621,27 +621,27 @@
1.116 (*asm_thm = [],*)
1.117 rules = [(*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
1.118 a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *)
1.119 - Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.120 + Thm ("sym_realpow_twoI",num_str @{(realpow_twoI RS sym)),
1.121 (*"r * r = r ^^^ 2"*)
1.122 - Thm ("realpow_twoI_assoc_l",num_str realpow_twoI_assoc_l),
1.123 + Thm ("realpow_twoI_assoc_l",num_str @{realpow_twoI_assoc_l),
1.124 (*"r * (r * s) = r ^^^ 2 * s"*)
1.125
1.126 - Thm ("realpow_plus_1",num_str realpow_plus_1),
1.127 + Thm ("realpow_plus_1",num_str @{realpow_plus_1),
1.128 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.129 - Thm ("realpow_plus_1_assoc_l", num_str realpow_plus_1_assoc_l),
1.130 + Thm ("realpow_plus_1_assoc_l", num_str @{realpow_plus_1_assoc_l),
1.131 (*"r * (r ^^^ m * s) = r ^^^ (1 + m) * s"*)
1.132 (*MG 9.7.03: neues Thm wegen a*(a*(a*b)) --> a^^^2*(a*b) *)
1.133 - Thm ("realpow_plus_1_assoc_l2", num_str realpow_plus_1_assoc_l2),
1.134 + Thm ("realpow_plus_1_assoc_l2", num_str @{realpow_plus_1_assoc_l2),
1.135 (*"r ^^^ m * (r * s) = r ^^^ (1 + m) * s"*)
1.136
1.137 - Thm ("sym_realpow_addI",num_str (realpow_addI RS sym)),
1.138 + Thm ("sym_realpow_addI",num_str @{(realpow_addI RS sym)),
1.139 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
1.140 - Thm ("realpow_addI_assoc_l", num_str realpow_addI_assoc_l),
1.141 + Thm ("realpow_addI_assoc_l", num_str @{realpow_addI_assoc_l),
1.142 (*"r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"*)
1.143
1.144 (* ist in expand_poly - wird hier aber auch gebraucht, wegen:
1.145 "r * r = r ^^^ 2" wenn r=a^^^b*)
1.146 - Thm ("realpow_pow",num_str realpow_pow)
1.147 + Thm ("realpow_pow",num_str @{realpow_pow)
1.148 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.149 ], scr = EmptyScr}:rls;
1.150
1.151 @@ -668,11 +668,11 @@
1.152 rules = [(* MG: folgende Thm müssen hier stehen bleiben: *)
1.153 Thm ("mult_1_right",num_str @{thm mult_1_right}),
1.154 (*"z * 1 = z"*) (*wegen "a * b * b^^^(-1) + a"*)
1.155 - Thm ("realpow_zeroI",num_str realpow_zeroI),
1.156 + Thm ("realpow_zeroI",num_str @{realpow_zeroI),
1.157 (*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)
1.158 - Thm ("realpow_oneI",num_str realpow_oneI),
1.159 + Thm ("realpow_oneI",num_str @{realpow_oneI),
1.160 (*"r ^^^ 1 = r"*)
1.161 - Thm ("realpow_eq_oneI",num_str realpow_eq_oneI)
1.162 + Thm ("realpow_eq_oneI",num_str @{realpow_eq_oneI)
1.163 (*"1 ^^^ n = 1"*)
1.164 ], scr = EmptyScr}:rls;
1.165
1.166 @@ -683,23 +683,23 @@
1.167 calc = [("PLUS" , ("op +", eval_binop "#add_"))
1.168 ],
1.169 rules =
1.170 - [Thm ("real_num_collect",num_str real_num_collect),
1.171 + [Thm ("real_num_collect",num_str @{real_num_collect),
1.172 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.173 - Thm ("real_num_collect_assoc_r",num_str real_num_collect_assoc_r),
1.174 + Thm ("real_num_collect_assoc_r",num_str @{real_num_collect_assoc_r),
1.175 (*"[| l is_const; m is_const |] ==> \
1.176 \(k + m * n) + l * n = k + (l + m)*n"*)
1.177 - Thm ("real_one_collect",num_str real_one_collect),
1.178 + Thm ("real_one_collect",num_str @{real_one_collect),
1.179 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.180 - Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r),
1.181 + Thm ("real_one_collect_assoc_r",num_str @{real_one_collect_assoc_r),
1.182 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
1.183
1.184 Calc ("op +", eval_binop "#add_"),
1.185
1.186 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
1.187 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
1.188 - Thm ("real_mult_2_assoc_r",num_str real_mult_2_assoc_r),
1.189 + Thm ("real_mult_2_assoc_r",num_str @{real_mult_2_assoc_r),
1.190 (*"(k + z1) + z1 = k + 2 * z1"*)
1.191 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym))
1.192 + Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym))
1.193 (*"z1 + z1 = 2 * z1"*)
1.194 ], scr = EmptyScr}:rls;
1.195
1.196 @@ -720,7 +720,7 @@
1.197 Thm ("add_0_right",num_str @{thm add_0_right}),
1.198 (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
1.199
1.200 - (*Thm ("realpow_oneI",num_str realpow_oneI)*)
1.201 + (*Thm ("realpow_oneI",num_str @{realpow_oneI)*)
1.202 (*"?r ^^^ 1 = ?r"*)
1.203 Thm ("divide_zero_left",num_str @{thm divide_zero_left})(*WN060914*)
1.204 (*"0 / ?x = 0"*)
1.205 @@ -729,9 +729,9 @@
1.206 (*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
1.207 val discard_parentheses_ =
1.208 append_rls "discard_parentheses_" e_rls
1.209 - [Thm ("sym_real_mult_assoc", num_str (real_mult_assoc RS sym))
1.210 + [Thm ("sym_real_mult_assoc", num_str @{(real_mult_assoc RS sym))
1.211 (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
1.212 - (*Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym))*)
1.213 + (*Thm ("sym_real_add_assoc",num_str @{(real_add_assoc RS sym))*)
1.214 (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)
1.215 ];
1.216
1.217 @@ -747,22 +747,22 @@
1.218 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.219 ],
1.220 (*asm_thm = [],*)
1.221 - rules = [Thm ("real_num_collect",num_str real_num_collect),
1.222 + rules = [Thm ("real_num_collect",num_str @{real_num_collect),
1.223 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.224 - Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.225 + Thm ("real_num_collect_assoc",num_str @{real_num_collect_assoc),
1.226 (*"[| l is_const; m is_const |] ==>
1.227 l * n + (m * n + k) = (l + m) * n + k"*)
1.228 - Thm ("real_one_collect",num_str real_one_collect),
1.229 + Thm ("real_one_collect",num_str @{real_one_collect),
1.230 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.231 - Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.232 + Thm ("real_one_collect_assoc",num_str @{real_one_collect_assoc),
1.233 (*"m is_const ==> n + (m * n + k) = (1 + m) * n + k"*)
1.234
1.235 Calc ("op +", eval_binop "#add_"),
1.236
1.237 (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*)
1.238 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.239 + Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
1.240 (*"z1 + z1 = 2 * z1"*)
1.241 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc)
1.242 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc)
1.243 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.244 ], scr = EmptyScr}:rls;*)
1.245
1.246 @@ -779,31 +779,31 @@
1.247 (*Thm ("left_distrib1",num_str @{thm left_distrib}1),
1.248 ....... 18.3.03 undefined???*)
1.249
1.250 - Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),
1.251 + Thm ("real_plus_binom_pow2",num_str @{real_plus_binom_pow2),
1.252 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
1.253 - Thm ("real_minus_binom_pow2_p",num_str real_minus_binom_pow2_p),
1.254 + Thm ("real_minus_binom_pow2_p",num_str @{real_minus_binom_pow2_p),
1.255 (*"(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"*)
1.256 Thm ("real_plus_minus_binom1_p",
1.257 - num_str real_plus_minus_binom1_p),
1.258 + num_str @{real_plus_minus_binom1_p),
1.259 (*"(a + b)*(a - b) = a^^^2 + -1*b^^^2"*)
1.260 Thm ("real_plus_minus_binom2_p",
1.261 - num_str real_plus_minus_binom2_p),
1.262 + num_str @{real_plus_minus_binom2_p),
1.263 (*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*)
1.264
1.265 Thm ("minus_minus",num_str @{thm minus_minus}),
1.266 (*"- (- ?z) = ?z"*)
1.267 - Thm ("real_diff_minus",num_str real_diff_minus),
1.268 + Thm ("real_diff_minus",num_str @{real_diff_minus),
1.269 (*"a - b = a + -1 * b"*)
1.270 - Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym))
1.271 + Thm ("sym_real_mult_minus1",num_str @{(real_mult_minus1 RS sym))
1.272 (*- ?z = "-1 * ?z"*)
1.273
1.274 - (*Thm ("",num_str ),
1.275 - Thm ("",num_str ),
1.276 - Thm ("",num_str ),*)
1.277 + (*Thm ("",num_str @{),
1.278 + Thm ("",num_str @{),
1.279 + Thm ("",num_str @{),*)
1.280 (*Thm ("real_minus_add_distrib",
1.281 - num_str real_minus_add_distrib),*)
1.282 + num_str @{real_minus_add_distrib),*)
1.283 (*"- (?x + ?y) = - ?x + - ?y"*)
1.284 - (*Thm ("real_diff_plus",num_str real_diff_plus)*)
1.285 + (*Thm ("real_diff_plus",num_str @{real_diff_plus)*)
1.286 (*"a - b = a + -b"*)
1.287 ], scr = EmptyScr}:rls;
1.288
1.289 @@ -813,20 +813,20 @@
1.290 erls = e_rls, srls = Erls,
1.291 calc = [],
1.292 (*asm_thm = [],*)
1.293 - rules = [Thm ("realpow_multI", num_str realpow_multI),
1.294 + rules = [Thm ("realpow_multI", num_str @{realpow_multI),
1.295 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.296
1.297 - Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.298 + Thm ("sym_realpow_twoI",num_str @{(realpow_twoI RS sym)),
1.299 (*"r1 * r1 = r1 ^^^ 2"*)
1.300 - Thm ("realpow_plus_1",num_str realpow_plus_1),
1.301 + Thm ("realpow_plus_1",num_str @{realpow_plus_1),
1.302 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.303 - Thm ("realpow_pow",num_str realpow_pow),
1.304 + Thm ("realpow_pow",num_str @{realpow_pow),
1.305 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.306 - Thm ("sym_realpow_addI",num_str (realpow_addI RS sym)),
1.307 + Thm ("sym_realpow_addI",num_str @{(realpow_addI RS sym)),
1.308 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
1.309 - Thm ("realpow_oneI",num_str realpow_oneI),
1.310 + Thm ("realpow_oneI",num_str @{realpow_oneI),
1.311 (*"r ^^^ 1 = r"*)
1.312 - Thm ("realpow_eq_oneI",num_str realpow_eq_oneI)
1.313 + Thm ("realpow_eq_oneI",num_str @{realpow_eq_oneI)
1.314 (*"1 ^^^ n = 1"*)
1.315 ], scr = EmptyScr}:rls;
1.316 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
1.317 @@ -837,11 +837,11 @@
1.318 erls = e_rls,srls = Erls,
1.319 calc = [],
1.320 (*asm_thm = [],*)
1.321 - rules = [Thm ("real_mult_commute",num_str real_mult_commute),
1.322 + rules = [Thm ("real_mult_commute",num_str @{real_mult_commute),
1.323 (* z * w = w * z *)
1.324 - Thm ("real_mult_left_commute",num_str real_mult_left_commute),
1.325 + Thm ("real_mult_left_commute",num_str @{real_mult_left_commute),
1.326 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.327 - Thm ("real_mult_assoc",num_str real_mult_assoc),
1.328 + Thm ("real_mult_assoc",num_str @{real_mult_assoc),
1.329 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.330 Thm ("add_commute",num_str @{thm add_commute}),
1.331 (*z + w = w + z*)
1.332 @@ -858,11 +858,11 @@
1.333 erls = e_rls,srls = Erls,
1.334 calc = [],
1.335 (*asm_thm = [],*)
1.336 - rules = [Thm ("real_mult_commute",num_str real_mult_commute),
1.337 + rules = [Thm ("real_mult_commute",num_str @{real_mult_commute),
1.338 (* z * w = w * z *)
1.339 - Thm ("real_mult_left_commute",num_str real_mult_left_commute),
1.340 + Thm ("real_mult_left_commute",num_str @{real_mult_left_commute),
1.341 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.342 - Thm ("real_mult_assoc",num_str real_mult_assoc)
1.343 + Thm ("real_mult_assoc",num_str @{real_mult_assoc)
1.344 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.345 ], scr = EmptyScr}:rls;
1.346 val collect_numerals =
1.347 @@ -874,14 +874,14 @@
1.348 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.349 ],
1.350 (*asm_thm = [],*)
1.351 - rules = [Thm ("real_num_collect",num_str real_num_collect),
1.352 + rules = [Thm ("real_num_collect",num_str @{real_num_collect),
1.353 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.354 - Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.355 + Thm ("real_num_collect_assoc",num_str @{real_num_collect_assoc),
1.356 (*"[| l is_const; m is_const |] ==>
1.357 l * n + (m * n + k) = (l + m) * n + k"*)
1.358 - Thm ("real_one_collect",num_str real_one_collect),
1.359 + Thm ("real_one_collect",num_str @{real_one_collect),
1.360 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.361 - Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.362 + Thm ("real_one_collect_assoc",num_str @{real_one_collect_assoc),
1.363 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.364 Calc ("op +", eval_binop "#add_"),
1.365 Calc ("op *", eval_binop "#mult_"),
1.366 @@ -895,12 +895,12 @@
1.367 (*asm_thm = [],*)
1.368 rules = [Thm ("mult_1_left",num_str @{thm mult_1_left}),
1.369 (*"1 * z = z"*)
1.370 - (*Thm ("real_mult_minus1",num_str real_mult_minus1),14.3.03*)
1.371 + (*Thm ("real_mult_minus1",num_str @{real_mult_minus1),14.3.03*)
1.372 (*"-1 * z = - z"*)
1.373 Thm ("minus_mult_left",
1.374 - num_str (real_mult_minus_eq1 RS sym)),
1.375 + num_str @{(real_mult_minus_eq1 RS sym)),
1.376 (*- (?x * ?y) = "- ?x * ?y"*)
1.377 - (*Thm ("real_minus_mult_cancel",num_str real_minus_mult_cancel),
1.378 + (*Thm ("real_minus_mult_cancel",num_str @{real_minus_mult_cancel),
1.379 (*"- ?x * - ?y = ?x * ?y"*)---*)
1.380 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
1.381 (*"0 * z = 0"*)
1.382 @@ -908,16 +908,16 @@
1.383 (*"0 + z = z"*)
1.384 Thm ("right_minus",num_str @{thm right_minus}),
1.385 (*"?z + - ?z = 0"*)
1.386 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.387 + Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
1.388 (*"z1 + z1 = 2 * z1"*)
1.389 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc)
1.390 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc)
1.391 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.392 ], scr = EmptyScr}:rls;
1.393 (*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
1.394 val discard_parentheses =
1.395 append_rls "discard_parentheses" e_rls
1.396 - [Thm ("sym_real_mult_assoc", num_str (real_mult_assoc RS sym)),
1.397 - Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym))];
1.398 + [Thm ("sym_real_mult_assoc", num_str @{(real_mult_assoc RS sym)),
1.399 + Thm ("sym_real_add_assoc",num_str @{(real_add_assoc RS sym))];
1.400
1.401 val scr_make_polynomial =
1.402 "Script Expand_binoms t_ = " ^
1.403 @@ -967,7 +967,7 @@
1.404 Rls_ simplify_power, (*realpow_eq_oneI, eg. x^1 --> x *)
1.405 Rls_ collect_numerals, (*eg. x^(2+ -1) --> x^1 *)
1.406 Rls_ reduce_012,
1.407 - Thm ("realpow_oneI",num_str realpow_oneI),(*in --^*)
1.408 + Thm ("realpow_oneI",num_str @{realpow_oneI),(*in --^*)
1.409 Rls_ discard_parentheses
1.410 ],
1.411 scr = EmptyScr
1.412 @@ -1015,32 +1015,32 @@
1.413 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.414 ],
1.415 (*asm_thm = [],*)
1.416 - rules = [Thm ("real_plus_binom_pow2" ,num_str real_plus_binom_pow2),
1.417 + rules = [Thm ("real_plus_binom_pow2" ,num_str @{real_plus_binom_pow2),
1.418 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1.419 - Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
1.420 + Thm ("real_plus_binom_times" ,num_str @{real_plus_binom_times),
1.421 (*"(a + b)*(a + b) = ...*)
1.422 - Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2),
1.423 + Thm ("real_minus_binom_pow2" ,num_str @{real_minus_binom_pow2),
1.424 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1.425 - Thm ("real_minus_binom_times",num_str real_minus_binom_times),
1.426 + Thm ("real_minus_binom_times",num_str @{real_minus_binom_times),
1.427 (*"(a - b)*(a - b) = ...*)
1.428 - Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1),
1.429 + Thm ("real_plus_minus_binom1",num_str @{real_plus_minus_binom1),
1.430 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1.431 - Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2),
1.432 + Thm ("real_plus_minus_binom2",num_str @{real_plus_minus_binom2),
1.433 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1.434 (*RL 020915*)
1.435 - Thm ("real_pp_binom_times",num_str real_pp_binom_times),
1.436 + Thm ("real_pp_binom_times",num_str @{real_pp_binom_times),
1.437 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1.438 - Thm ("real_pm_binom_times",num_str real_pm_binom_times),
1.439 + Thm ("real_pm_binom_times",num_str @{real_pm_binom_times),
1.440 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1.441 - Thm ("real_mp_binom_times",num_str real_mp_binom_times),
1.442 + Thm ("real_mp_binom_times",num_str @{real_mp_binom_times),
1.443 (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
1.444 - Thm ("real_mm_binom_times",num_str real_mm_binom_times),
1.445 + Thm ("real_mm_binom_times",num_str @{real_mm_binom_times),
1.446 (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
1.447 - Thm ("realpow_multI",num_str realpow_multI),
1.448 + Thm ("realpow_multI",num_str @{realpow_multI),
1.449 (*(a*b)^^^n = a^^^n * b^^^n*)
1.450 - Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),
1.451 + Thm ("real_plus_binom_pow3",num_str @{real_plus_binom_pow3),
1.452 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1.453 - Thm ("real_minus_binom_pow3",num_str real_minus_binom_pow3),
1.454 + Thm ("real_minus_binom_pow3",num_str @{real_minus_binom_pow3),
1.455 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1.456
1.457
1.458 @@ -1062,30 +1062,30 @@
1.459 Calc ("op *", eval_binop "#mult_"),
1.460 Calc ("Atools.pow", eval_binop "#power_"),
1.461 (*
1.462 - Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*)
1.463 - Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**)
1.464 - Thm ("real_mult_assoc",num_str real_mult_assoc), (**)
1.465 + Thm ("real_mult_commute",num_str @{real_mult_commute), (*AC-rewriting*)
1.466 + Thm ("real_mult_left_commute",num_str @{real_mult_left_commute), (**)
1.467 + Thm ("real_mult_assoc",num_str @{real_mult_assoc), (**)
1.468 Thm ("add_commute",num_str @{thm add_commute}), (**)
1.469 Thm ("add_left_commute",num_str @{thm add_left_commute}), (**)
1.470 Thm ("add_assoc",num_str @{thm add_assoc}), (**)
1.471 *)
1.472
1.473 - Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.474 + Thm ("sym_realpow_twoI",num_str @{(realpow_twoI RS sym)),
1.475 (*"r1 * r1 = r1 ^^^ 2"*)
1.476 - Thm ("realpow_plus_1",num_str realpow_plus_1),
1.477 + Thm ("realpow_plus_1",num_str @{realpow_plus_1),
1.478 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.479 - (*Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.480 + (*Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
1.481 (*"z1 + z1 = 2 * z1"*)*)
1.482 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
1.483 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc),
1.484 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.485
1.486 - Thm ("real_num_collect",num_str real_num_collect),
1.487 + Thm ("real_num_collect",num_str @{real_num_collect),
1.488 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
1.489 - Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.490 + Thm ("real_num_collect_assoc",num_str @{real_num_collect_assoc),
1.491 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1.492 - Thm ("real_one_collect",num_str real_one_collect),
1.493 + Thm ("real_one_collect",num_str @{real_one_collect),
1.494 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.495 - Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.496 + Thm ("real_one_collect_assoc",num_str @{real_one_collect_assoc),
1.497 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.498
1.499 Calc ("op +", eval_binop "#add_"),
1.500 @@ -1475,11 +1475,11 @@
1.501 ("TIMES" , ("op *", eval_binop "#mult_")),
1.502 ("POWER", ("Atools.pow", eval_binop "#power_"))*)
1.503 ],
1.504 - rules = [Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
1.505 + rules = [Thm ("real_plus_binom_times" ,num_str @{real_plus_binom_times),
1.506 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
1.507 - Thm ("real_plus_binom_times1" ,num_str real_plus_binom_times1),
1.508 + Thm ("real_plus_binom_times1" ,num_str @{real_plus_binom_times1),
1.509 (*"(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"*)
1.510 - Thm ("real_plus_binom_times2" ,num_str real_plus_binom_times2),
1.511 + Thm ("real_plus_binom_times2" ,num_str @{real_plus_binom_times2),
1.512 (*"(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"*)
1.513
1.514 Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*)
1.515 @@ -1489,7 +1489,7 @@
1.516 Thm ("left_distrib2",num_str @{thm left_distrib}2),
1.517 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.518
1.519 - Thm ("real_mult_assoc", num_str real_mult_assoc),
1.520 + Thm ("real_mult_assoc", num_str @{real_mult_assoc),
1.521 (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
1.522 Rls_ order_mult_rls_,
1.523 (*Rls_ order_add_rls_,*)
1.524 @@ -1498,24 +1498,24 @@
1.525 Calc ("op *", eval_binop "#mult_"),
1.526 Calc ("Atools.pow", eval_binop "#power_"),
1.527
1.528 - Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.529 + Thm ("sym_realpow_twoI",num_str @{(realpow_twoI RS sym)),
1.530 (*"r1 * r1 = r1 ^^^ 2"*)
1.531 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.532 + Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
1.533 (*"z1 + z1 = 2 * z1"*)
1.534 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
1.535 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc),
1.536 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.537
1.538 - Thm ("real_num_collect",num_str real_num_collect),
1.539 + Thm ("real_num_collect",num_str @{real_num_collect),
1.540 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.541 - Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.542 + Thm ("real_num_collect_assoc",num_str @{real_num_collect_assoc),
1.543 (*"[| l is_const; m is_const |] ==>
1.544 l * n + (m * n + k) = (l + m) * n + k"*)
1.545 - Thm ("real_one_collect",num_str real_one_collect),
1.546 + Thm ("real_one_collect",num_str @{real_one_collect),
1.547 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.548 - Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.549 + Thm ("real_one_collect_assoc",num_str @{real_one_collect_assoc),
1.550 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.551
1.552 - Thm ("realpow_multI", num_str realpow_multI),
1.553 + Thm ("realpow_multI", num_str @{realpow_multI),
1.554 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.555
1.556 Calc ("op +", eval_binop "#add_"),