1.1 --- a/src/sml/IsacKnowledge/PolyMinus.ML Fri Jan 04 19:00:50 2008 +0100
1.2 +++ b/src/sml/IsacKnowledge/PolyMinus.ML Sun Jan 06 18:56:55 2008 +0100
1.3 @@ -120,12 +120,31 @@
1.4 Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r),
1.5 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
1.6
1.7 +
1.8 + Thm ("subtrahiere",num_str subtrahiere),
1.9 + (*"[| l is_const; m is_const |] ==> \
1.10 + \m * v - l * v = (m - l) * v"*)
1.11 +
1.12 Thm ("subtrahiere_x_plus_minus",num_str subtrahiere_x_plus_minus),
1.13 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
1.14 + Thm ("subtrahiere_x_plus1_minus",num_str subtrahiere_x_plus1_minus),
1.15 + (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*)
1.16 + Thm ("subtrahiere_x_plus_minus1",num_str subtrahiere_x_plus_minus1),
1.17 + (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*)
1.18 +
1.19 Thm ("subtrahiere_x_minus_plus",num_str subtrahiere_x_minus_plus),
1.20 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
1.21 + Thm ("subtrahiere_x_minus1_plus",num_str subtrahiere_x_minus1_plus),
1.22 + (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
1.23 + Thm ("subtrahiere_x_minus_plus1",num_str subtrahiere_x_minus_plus1),
1.24 + (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
1.25 +
1.26 Thm ("subtrahiere_x_minus_minus",num_str subtrahiere_x_minus_minus),
1.27 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
1.28 + Thm ("subtrahiere_x_minus1_minus",num_str subtrahiere_x_minus1_minus),
1.29 + (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
1.30 + Thm ("subtrahiere_x_minus_minus1",num_str subtrahiere_x_minus_minus1),
1.31 + (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
1.32
1.33 Calc ("op +", eval_binop "#add_"),
1.34 Calc ("op -", eval_binop "#subtr_"),
1.35 @@ -161,8 +180,23 @@
1.36 (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
1.37 Thm ("vorzeichen_minus_weg4",num_str vorzeichen_minus_weg4),
1.38 (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
1.39 - Calc ("op *", eval_binop "#mult_")
1.40 - ], scr = EmptyScr}:rls;
1.41 +
1.42 + Calc ("op *", eval_binop "#mult_"),
1.43 +
1.44 + Thm ("real_mult_0",num_str real_mult_0),
1.45 + (*"0 * z = 0"*)
1.46 + Thm ("real_mult_1",num_str real_mult_1),
1.47 + (*"1 * z = z"*)
1.48 + Thm ("real_add_zero_left",num_str real_add_zero_left),
1.49 + (*"0 + z = z"*)
1.50 + Thm ("null_minus",num_str null_minus),
1.51 + (*"0 - a = -a"*)
1.52 + Thm ("vor_minus_mal",num_str vor_minus_mal)
1.53 + (*"- a * b = (-a) * b"*)
1.54 +
1.55 + (*Thm ("",num_str ),*)
1.56 + (**)
1.57 + ], scr = EmptyScr}:rls (*end verschoenere*);
1.58
1.59 val klammern_aufloesen =
1.60 Rls{id = "klammern_aufloesen", preconds = [],
1.61 @@ -205,8 +239,10 @@
1.62 (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*)
1.63 Thm ("tausche_vor_mal",num_str tausche_vor_mal),
1.64 (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*)
1.65 - Thm ("tausche_mal_mal",num_str tausche_mal_mal)
1.66 + Thm ("tausche_mal_mal",num_str tausche_mal_mal),
1.67 (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*)
1.68 + Thm ("x_quadrat",num_str x_quadrat)
1.69 + (*"(x * a) * a = x * a ^^^ 2"*)
1.70
1.71 (*Thm ("",num_str ),
1.72 (*""*)*)
1.73 @@ -249,6 +285,11 @@
1.74 store_pbt
1.75 (prep_pbt PolyMinus.thy "pbl_vereinf_poly" [] e_pblID
1.76 (["polynom","vereinfachen"],
1.77 + [], Erls, None, []));
1.78 +
1.79 +store_pbt
1.80 + (prep_pbt PolyMinus.thy "pbl_vereinf_poly_minus" [] e_pblID
1.81 + (["plus_minus","polynom","vereinfachen"],
1.82 [("#Given" ,["term t_"]),
1.83 ("#Where" ,["t_ is_polyexp",
1.84 "Not (matchsub (?a + (?b + ?c)) t_ | \
1.85 @@ -285,7 +326,7 @@
1.86
1.87 store_pbt
1.88 (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
1.89 - (["mal","klammer","polynom","vereinfachen"],
1.90 + (["binom_klammer","polynom","vereinfachen"],
1.91 [("#Given" ,["term t_"]),
1.92 ("#Where" ,["t_ is_polyexp"]),
1.93 ("#Find" ,["normalform n_"])
1.94 @@ -371,11 +412,11 @@
1.95 [(*for preds in where_*)
1.96 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
1.97 crls = e_rls, nrls = rls_p_34},
1.98 -"Script SimplifyScript (t_::real) = \
1.99 -\ (((Try (Rewrite_Set klammern_aufloesen False)) @@ \
1.100 -\ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \
1.101 -\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
1.102 -\ (Try (Rewrite_Set verschoenere False))) t_)"
1.103 +"Script SimplifyScript (t_::real) = \
1.104 +\ ((Repeat((Try (Rewrite_Set klammern_aufloesen False)) @@ \
1.105 +\ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \
1.106 +\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
1.107 +\ (Try (Rewrite_Set verschoenere False)))) t_)"
1.108 ));
1.109
1.110 store_met
1.111 @@ -391,13 +432,13 @@
1.112 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
1.113 crls = e_rls, nrls = rls_p_34},
1.114 "Script SimplifyScript (t_::real) = \
1.115 -\ (((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ \
1.116 -\ (Try (Rewrite_Set discard_parentheses False)) @@ \
1.117 -\ (Try (Rewrite_Set ordne_monome False)) @@ \
1.118 -\ (Try (Rewrite_Set klammern_aufloesen False)) @@ \
1.119 -\ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \
1.120 -\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
1.121 -\ (Try (Rewrite_Set verschoenere False))) t_)"
1.122 +\ ((Repeat((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ \
1.123 +\ (Try (Rewrite_Set discard_parentheses False)) @@ \
1.124 +\ (Try (Rewrite_Set ordne_monome False)) @@ \
1.125 +\ (Try (Rewrite_Set klammern_aufloesen False)) @@ \
1.126 +\ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \
1.127 +\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
1.128 +\ (Try (Rewrite_Set verschoenere False)))) t_)"
1.129 ));
1.130
1.131 store_met
2.1 --- a/src/sml/IsacKnowledge/PolyMinus.thy Fri Jan 04 19:00:50 2008 +0100
2.2 +++ b/src/sml/IsacKnowledge/PolyMinus.thy Sun Jan 06 18:56:55 2008 +0100
2.3 @@ -30,6 +30,9 @@
2.4
2.5 rules
2.6
2.7 + null_minus "0 - a = -a"
2.8 + vor_minus_mal "- a * b = (-a) * b"
2.9 +
2.10 (*commute with invariant (a.b).c -association*)
2.11 tausche_plus "[| b ist_monom; a kleiner b |] ==> \
2.12 \(b + a) = (a + b)"
2.13 @@ -51,17 +54,33 @@
2.14 \(-b * a) = (-a * b)"
2.15 tausche_mal_mal "[| c is_atom; b kleiner c |] ==> \
2.16 \(x * c * b) = (x * b * c)"
2.17 -(*WN080104^^^ _x_ umbenannt, vvv neu:
2.18 - tausche_mal_mal "[| c is_atom; b kleiner c |] ==> \
2.19 - \(b * a * c) = (a * b * c)"
2.20 -*)
2.21 + x_quadrat "(x * a) * a = x * a ^^^ 2"
2.22
2.23 +
2.24 + subtrahiere "[| l is_const; m is_const |] ==> \
2.25 + \m * v - l * v = (m - l) * v"
2.26 subtrahiere_x_plus_minus "[| l is_const; m is_const |] ==> \
2.27 \(x + m * v) - l * v = x + (m - l) * v"
2.28 + subtrahiere_x_plus1_minus "[| l is_const |] ==> \
2.29 + \(x + v) - l * v = x + (1 - l) * v"
2.30 + subtrahiere_x_plus_minus1 "[| m is_const |] ==> \
2.31 + \(x + m * v) - v = x + (m - 1) * v"
2.32 +
2.33 subtrahiere_x_minus_plus "[| l is_const; m is_const |] ==> \
2.34 \(x - m * v) + l * v = x + (-m + l) * v"
2.35 + subtrahiere_x_minus1_plus "[| l is_const |] ==> \
2.36 + \(x - v) + l * v = x + (-1 + l) * v"
2.37 + subtrahiere_x_minus_plus1 "[| m is_const |] ==> \
2.38 + \(x - m * v) + v = x + (-m + 1) * v"
2.39 +
2.40 subtrahiere_x_minus_minus "[| l is_const; m is_const |] ==> \
2.41 \(x - m * v) - l * v = x + (-m - l) * v"
2.42 + subtrahiere_x_minus1_minus"[| l is_const |] ==> \
2.43 + \(x - v) - l * v = x + (-1 - l) * v"
2.44 + subtrahiere_x_minus_minus1"[| m is_const |] ==> \
2.45 + \(x - m * v) - v = x + (-m - 1) * v"
2.46 +
2.47 +
2.48 addiere_vor_minus "[| l is_const; m is_const |] ==> \
2.49 \- (l * v) + m * v = (-l + m) * v"
2.50 addiere_eins_vor_minus "[| m is_const |] ==> \
3.1 --- a/src/smltest/IsacKnowledge/polyminus.sml Fri Jan 04 19:00:50 2008 +0100
3.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml Sun Jan 06 18:56:55 2008 +0100
3.3 @@ -16,7 +16,7 @@
3.4 "----------- build fasse_zusammen --------------------------------";
3.5 "----------- build verschoenere ----------------------------------";
3.6 "----------- met simplification for_polynomials with_minus -------";
3.7 -"----------- pbl polynom vereinfachen ----------------------------";
3.8 +"----------- pbl polynom vereinfachen p.33 -----------------------";
3.9 "----------- met probe fuer_polynom ------------------------------";
3.10 "----------- pbl polynom probe -----------------------------------";
3.11 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
3.12 @@ -191,21 +191,75 @@
3.13 atomty sc;
3.14
3.15
3.16 -"----------- pbl polynom vereinfachen ----------------------------";
3.17 -"----------- pbl polynom vereinfachen ----------------------------";
3.18 -"----------- pbl polynom vereinfachen ----------------------------";
3.19 +"----------- pbl polynom vereinfachen p.33 -----------------------";
3.20 +"----------- pbl polynom vereinfachen p.33 -----------------------";
3.21 +"----------- pbl polynom vereinfachen p.33 -----------------------";
3.22 +"----------- 140 c ---";
3.23 states:=[];
3.24 CalcTree [(["term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
3.25 "normalform N"],
3.26 - ("PolyMinus.thy",["polynom","vereinfachen"],
3.27 + ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
3.28 ["simplification","for_polynomials","with_minus"]))];
3.29 moveActiveRoot 1;
3.30 autoCalculate 1 CompleteCalc;
3.31 -val ((pt,p),_) = get_calc 1;
3.32 +val ((pt,p),_) = get_calc 1; show_pt pt;
3.33 if p = ([], Res) andalso
3.34 term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"
3.35 then () else raise error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f...";
3.36 -show_pt pt;
3.37 +
3.38 +"----------- 140 d ---";
3.39 +states:=[];
3.40 +CalcTree [(["term (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)",
3.41 + "normalform N"],
3.42 + ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
3.43 + ["simplification","for_polynomials","with_minus"]))];
3.44 +moveActiveRoot 1;
3.45 +autoCalculate 1 CompleteCalc;
3.46 +val ((pt,p),_) = get_calc 1; show_pt pt;
3.47 +if p = ([], Res) andalso
3.48 + term2str (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
3.49 +then () else raise error "polyminus.sml: Vereinfache 140 d)";
3.50 +
3.51 +
3.52 +"----------- 139 c ---";
3.53 +states:=[];
3.54 +CalcTree [(["term (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)",
3.55 + "normalform N"],
3.56 + ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
3.57 + ["simplification","for_polynomials","with_minus"]))];
3.58 +moveActiveRoot 1;
3.59 +autoCalculate 1 CompleteCalc;
3.60 +val ((pt,p),_) = get_calc 1; show_pt pt;
3.61 +if p = ([], Res) andalso
3.62 + term2str (get_obj g_res pt (fst p)) = "- (3 * f)"
3.63 +then () else raise error "polyminus.sml: Vereinfache 139 c)";
3.64 +
3.65 +"----------- 139 b ---";
3.66 +states:=[];
3.67 +CalcTree [(["term (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)",
3.68 + "normalform N"],
3.69 + ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
3.70 + ["simplification","for_polynomials","with_minus"]))];
3.71 +moveActiveRoot 1;
3.72 +autoCalculate 1 CompleteCalc;
3.73 +val ((pt,p),_) = get_calc 1; show_pt pt;
3.74 +if p = ([], Res) andalso
3.75 + term2str (get_obj g_res pt (fst p)) = "-3 * u - v"
3.76 +then () else raise error "polyminus.sml: Vereinfache 139 b)";
3.77 +
3.78 +"----------- 138 a ---";
3.79 +states:=[];
3.80 +CalcTree [(["term (2*u - 3*v - 6*u + 5*v)",
3.81 + "normalform N"],
3.82 + ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
3.83 + ["simplification","for_polynomials","with_minus"]))];
3.84 +moveActiveRoot 1;
3.85 +autoCalculate 1 CompleteCalc;
3.86 +val ((pt,p),_) = get_calc 1; show_pt pt;
3.87 +if p = ([], Res) andalso
3.88 + term2str (get_obj g_res pt (fst p)) = "-4 * u + 2 * v"
3.89 +then () else raise error "polyminus.sml: Vereinfache 138 a)";
3.90 +
3.91
3.92 "----------- met probe fuer_polynom ------------------------------";
3.93 "----------- met probe fuer_polynom ------------------------------";
3.94 @@ -276,7 +330,7 @@
3.95 states:=[];
3.96 CalcTree [(["term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
3.97 "normalform N"],
3.98 - ("PolyMinus.thy",["polynom","vereinfachen"],
3.99 + ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
3.100 ["simplification","for_polynomials","with_minus"]))];
3.101 moveActiveRoot 1;
3.102 autoCalculate 1 CompleteCalcHead;
3.103 @@ -336,7 +390,7 @@
3.104 states:=[];
3.105 CalcTree [(["term (- (8 * g) + 10 * g + h)",
3.106 "normalform N"],
3.107 - ("PolyMinus.thy",["polynom","vereinfachen"],
3.108 + ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
3.109 ["simplification","for_polynomials","with_minus"]))];
3.110 moveActiveRoot 1;
3.111 autoCalculate 1 CompleteCalc;
3.112 @@ -348,7 +402,7 @@
3.113 states:=[];
3.114 CalcTree [(["term (- (8 * g) + 10 * g + f)",
3.115 "normalform N"],
3.116 - ("PolyMinus.thy",["polynom","vereinfachen"],
3.117 + ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
3.118 ["simplification","for_polynomials","with_minus"]))];
3.119 moveActiveRoot 1;
3.120 autoCalculate 1 CompleteCalc;
3.121 @@ -397,7 +451,7 @@
3.122 states:=[];
3.123 CalcTree [(["term ((3*a + 2) * (4*a - 1))",
3.124 "normalform N"],
3.125 - ("PolyMinus.thy",["mal","klammer","polynom","vereinfachen"],
3.126 + ("PolyMinus.thy",["binom_klammer","polynom","vereinfachen"],
3.127 ["simplification","for_polynomials","with_parentheses_mult"]))];
3.128 moveActiveRoot 1;
3.129 autoCalculate 1 CompleteCalc;