114 Thm ("real_one_collect",num_str real_one_collect), |
114 Thm ("real_one_collect",num_str real_one_collect), |
115 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
115 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
116 Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r), |
116 Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r), |
117 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*) |
117 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*) |
118 |
118 |
119 Thm ("addiere_x_plus_minus",num_str addiere_x_plus_minus), |
119 Thm ("subtrahiere_x_plus_minus",num_str subtrahiere_x_plus_minus), |
120 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*) |
120 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*) |
121 Thm ("addiere_x_minus_plus",num_str addiere_x_minus_plus), |
121 Thm ("subtrahiere_x_minus_plus",num_str subtrahiere_x_minus_plus), |
122 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*) |
122 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*) |
123 Thm ("addiere_x_minus_minus",num_str addiere_x_minus_minus), |
123 Thm ("subtrahiere_x_minus_minus",num_str subtrahiere_x_minus_minus), |
124 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*) |
124 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*) |
125 |
125 |
126 Calc ("op +", eval_binop "#add_"), |
126 Calc ("op +", eval_binop "#add_"), |
127 Calc ("op -", eval_binop "#subtr_"), |
127 Calc ("op -", eval_binop "#subtr_"), |
128 |
128 |
207 store_pbt |
207 store_pbt |
208 (prep_pbt PolyMinus.thy "pbl_vereinf_poly" [] e_pblID |
208 (prep_pbt PolyMinus.thy "pbl_vereinf_poly" [] e_pblID |
209 (["polynom","vereinfachen"], |
209 (["polynom","vereinfachen"], |
210 [("#Given" ,["term t_"]), |
210 [("#Given" ,["term t_"]), |
211 ("#Where" ,["t_ is_polyexp", |
211 ("#Where" ,["t_ is_polyexp", |
212 "Not (matchsub (?a + (?b + ?c)) t_ & \ |
212 "Not (matchsub (?a + (?b + ?c)) t_ | \ |
213 \ matchsub (?a + (?b - ?c)) t_ & \ |
213 \ matchsub (?a + (?b - ?c)) t_ | \ |
214 \ matchsub (?a - (?b + ?c)) t_ & \ |
214 \ matchsub (?a - (?b + ?c)) t_ | \ |
215 \ matchsub (?a + (?b - ?c)) t_ )"]), |
215 \ matchsub (?a + (?b - ?c)) t_ )"]), |
216 ("#Find" ,["normalform n_"]) |
216 ("#Find" ,["normalform n_"]) |
217 ], |
217 ], |
218 append_rls "prls_pbl_vereinf_poly" e_rls |
218 append_rls "prls_pbl_vereinf_poly" e_rls |
219 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""), |
219 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""), |
278 store_met |
278 store_met |
279 (prep_met PolyMinus.thy "met_simp_poly_minus" [] e_metID |
279 (prep_met PolyMinus.thy "met_simp_poly_minus" [] e_metID |
280 (["simplification","for_polynomials","with_minus"], |
280 (["simplification","for_polynomials","with_minus"], |
281 [("#Given" ,["term t_"]), |
281 [("#Given" ,["term t_"]), |
282 ("#Where" ,["t_ is_polyexp", |
282 ("#Where" ,["t_ is_polyexp", |
283 "Not (matchsub (?a + (?b + ?c)) t_ & \ |
283 "Not (matchsub (?a + (?b + ?c)) t_ | \ |
284 \ matchsub (?a + (?b - ?c)) t_ & \ |
284 \ matchsub (?a + (?b - ?c)) t_ | \ |
285 \ matchsub (?a - (?b + ?c)) t_ & \ |
285 \ matchsub (?a - (?b + ?c)) t_ | \ |
286 \ matchsub (?a + (?b - ?c)) t_ )"]), |
286 \ matchsub (?a + (?b - ?c)) t_ )"]), |
287 ("#Find" ,["normalform n_"]) |
287 ("#Find" ,["normalform n_"]) |
288 ], |
288 ], |
289 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, |
289 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, |
290 prls = append_rls "prls_met_simp_poly_minus" e_rls |
290 prls = append_rls "prls_met_simp_poly_minus" e_rls |