1.1 --- a/src/sml/IsacKnowledge/PolyMinus.ML Fri Jan 04 16:08:52 2008 +0100
1.2 +++ b/src/sml/IsacKnowledge/PolyMinus.ML Fri Jan 04 19:00:50 2008 +0100
1.3 @@ -90,6 +90,10 @@
1.4 (*"b kleiner a ==> (b + a) = (a + b)"*)
1.5 Thm ("tausche_minus",num_str tausche_minus),
1.6 (*"b kleiner a ==> (b - a) = (-a + b)"*)
1.7 + Thm ("tausche_vor_plus",num_str tausche_vor_plus),
1.8 + (*"[| b ist_monom; a kleiner b |] ==> (- b + a) = (a - b)"*)
1.9 + Thm ("tausche_vor_minus",num_str tausche_vor_minus),
1.10 + (*"[| b ist_monom; a kleiner b |] ==> (- b - a) = (-a - b)"*)
1.11 Thm ("tausche_plus_plus",num_str tausche_plus_plus),
1.12 (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
1.13 Thm ("tausche_plus_minus",num_str tausche_plus_minus),
1.14 @@ -130,8 +134,17 @@
1.15 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
1.16 Thm ("real_mult_2_assoc_r",num_str real_mult_2_assoc_r),
1.17 (*"(k + z1) + z1 = k + 2 * z1"*)
1.18 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym))
1.19 + Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.20 (*"z1 + z1 = 2 * z1"*)
1.21 +
1.22 + Thm ("addiere_vor_minus",num_str addiere_vor_minus),
1.23 + (*"[| l is_const; m is_const |] ==> -(l * v) + m * v = (-l + m) *v"*)
1.24 + Thm ("addiere_eins_vor_minus",num_str addiere_eins_vor_minus),
1.25 + (*"[| m is_const |] ==> - v + m * v = (-1 + m) * v"*)
1.26 + Thm ("subtrahiere_vor_minus",num_str subtrahiere_vor_minus),
1.27 + (*"[| l is_const; m is_const |] ==> -(l * v) - m * v = (-l - m) *v"*)
1.28 + Thm ("subtrahiere_eins_vor_minus",num_str subtrahiere_eins_vor_minus)
1.29 + (*"[| m is_const |] ==> - v - m * v = (-1 - m) * v"*)
1.30
1.31 ], scr = EmptyScr}:rls;
1.32
1.33 @@ -151,8 +164,8 @@
1.34 Calc ("op *", eval_binop "#mult_")
1.35 ], scr = EmptyScr}:rls;
1.36
1.37 -val klammern_ausmultiplizieren =
1.38 - Rls{id = "klammern_ausmultiplizieren", preconds = [],
1.39 +val klammern_aufloesen =
1.40 + Rls{id = "klammern_aufloesen", preconds = [],
1.41 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
1.42 rules = [Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym)),
1.43 (*"a + (b + c) = (a + b) + c"*)
1.44 @@ -164,14 +177,42 @@
1.45 (*"a - (b - c) = (a - b) + c"*)
1.46 ], scr = EmptyScr}:rls;
1.47
1.48 -val multipliziere_aus =
1.49 - Rls{id = "multipliziere_aus", preconds = [],
1.50 +val klammern_ausmultiplizieren =
1.51 + Rls{id = "klammern_ausmultiplizieren", preconds = [],
1.52 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
1.53 - rules = [Rls_ ordne_alphabetisch,
1.54 - Rls_ fasse_zusammen,
1.55 - Rls_ verschoenere
1.56 + rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.57 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.58 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.59 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.60 +
1.61 + Thm ("klammer_mult_minus",num_str klammer_mult_minus),
1.62 + (*"a * (b - c) = a * b - a * c"*)
1.63 + Thm ("klammer_minus_mult",num_str klammer_minus_mult)
1.64 + (*"(b - c) * a = b * a - c * a"*)
1.65 +
1.66 + (*Thm ("",num_str ),
1.67 + (*""*)*)
1.68 ], scr = EmptyScr}:rls;
1.69
1.70 +val ordne_monome =
1.71 + Rls{id = "ordne_monome", preconds = [],
1.72 + rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
1.73 + erls = append_rls "erls_ordne_monome" e_rls
1.74 + [Calc ("PolyMinus.kleiner", eval_kleiner ""),
1.75 + Calc ("Atools.is'_atom", eval_is_atom "")
1.76 + ],
1.77 + rules = [Thm ("tausche_mal",num_str tausche_mal),
1.78 + (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*)
1.79 + Thm ("tausche_vor_mal",num_str tausche_vor_mal),
1.80 + (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*)
1.81 + Thm ("tausche_mal_mal",num_str tausche_mal_mal)
1.82 + (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*)
1.83 +
1.84 + (*Thm ("",num_str ),
1.85 + (*""*)*)
1.86 + ], scr = EmptyScr}:rls;
1.87 +
1.88 +
1.89 val rls_p_33 =
1.90 append_rls "rls_p_33" e_rls
1.91 [Rls_ ordne_alphabetisch,
1.92 @@ -180,7 +221,7 @@
1.93 ];
1.94 val rls_p_34 =
1.95 append_rls "rls_p_34" e_rls
1.96 - [Rls_ klammern_ausmultiplizieren,
1.97 + [Rls_ klammern_aufloesen,
1.98 Rls_ ordne_alphabetisch,
1.99 Rls_ fasse_zusammen,
1.100 Rls_ verschoenere
1.101 @@ -197,9 +238,10 @@
1.102 [("ordne_alphabetisch", prep_rls ordne_alphabetisch),
1.103 ("fasse_zusammen", prep_rls fasse_zusammen),
1.104 ("verschoenere", prep_rls verschoenere),
1.105 + ("ordne_monome", prep_rls ordne_monome),
1.106 + ("klammern_aufloesen", prep_rls klammern_aufloesen),
1.107 ("klammern_ausmultiplizieren",
1.108 - prep_rls klammern_ausmultiplizieren),
1.109 - ("multipliziere_aus", prep_rls multipliziere_aus)
1.110 + prep_rls klammern_ausmultiplizieren)
1.111 ]);
1.112
1.113 (** problems **)
1.114 @@ -242,6 +284,18 @@
1.115 [["simplification","for_polynomials","with_parentheses"]]));
1.116
1.117 store_pbt
1.118 + (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
1.119 + (["mal","klammer","polynom","vereinfachen"],
1.120 + [("#Given" ,["term t_"]),
1.121 + ("#Where" ,["t_ is_polyexp"]),
1.122 + ("#Find" ,["normalform n_"])
1.123 + ],
1.124 + append_rls "e_rls" e_rls [(*for preds in where_*)
1.125 + Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1.126 + Some "Vereinfache t_",
1.127 + [["simplification","for_polynomials","with_parentheses_mult"]]));
1.128 +
1.129 +store_pbt
1.130 (prep_pbt PolyMinus.thy "pbl_probe" [] e_pblID
1.131 (["probe"],
1.132 [], Erls, None, []));
1.133 @@ -318,9 +372,31 @@
1.134 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
1.135 crls = e_rls, nrls = rls_p_34},
1.136 "Script SimplifyScript (t_::real) = \
1.137 -\ (((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ \
1.138 -\ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \
1.139 -\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
1.140 +\ (((Try (Rewrite_Set klammern_aufloesen False)) @@ \
1.141 +\ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \
1.142 +\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
1.143 +\ (Try (Rewrite_Set verschoenere False))) t_)"
1.144 + ));
1.145 +
1.146 +store_met
1.147 + (prep_met PolyMinus.thy "met_simp_poly_parenth_mult" [] e_metID
1.148 + (["simplification","for_polynomials","with_parentheses_mult"],
1.149 + [("#Given" ,["term t_"]),
1.150 + ("#Where" ,["t_ is_polyexp"]),
1.151 + ("#Find" ,["normalform n_"])
1.152 + ],
1.153 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
1.154 + prls = append_rls "simplification_for_polynomials_prls" e_rls
1.155 + [(*for preds in where_*)
1.156 + Calc("Poly.is'_polyexp",eval_is_polyexp"")],
1.157 + crls = e_rls, nrls = rls_p_34},
1.158 +"Script SimplifyScript (t_::real) = \
1.159 +\ (((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ \
1.160 +\ (Try (Rewrite_Set discard_parentheses False)) @@ \
1.161 +\ (Try (Rewrite_Set ordne_monome False)) @@ \
1.162 +\ (Try (Rewrite_Set klammern_aufloesen False)) @@ \
1.163 +\ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \
1.164 +\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
1.165 \ (Try (Rewrite_Set verschoenere False))) t_)"
1.166 ));
1.167
2.1 --- a/src/sml/IsacKnowledge/PolyMinus.thy Fri Jan 04 16:08:52 2008 +0100
2.2 +++ b/src/sml/IsacKnowledge/PolyMinus.thy Fri Jan 04 19:00:50 2008 +0100
2.3 @@ -6,7 +6,7 @@
2.4 use_thy"IsacKnowledge/Isac";
2.5 *)
2.6
2.7 -PolyMinus = (*Poly// due to "is_ratpolyexp"..*) Rational +
2.8 +PolyMinus = (*Poly// due to "is_ratpolyexp" in...*) Rational +
2.9
2.10 consts
2.11
2.12 @@ -35,17 +35,41 @@
2.13 \(b + a) = (a + b)"
2.14 tausche_minus "[| b ist_monom; a kleiner b |] ==> \
2.15 \(b - a) = (-a + b)"
2.16 + tausche_vor_plus "[| b ist_monom; a kleiner b |] ==> \
2.17 + \(- b + a) = (a - b)"
2.18 + tausche_vor_minus "[| b ist_monom; a kleiner b |] ==> \
2.19 + \(- b - a) = (-a - b)"
2.20 tausche_plus_plus "b kleiner c ==> (a + c + b) = (a + b + c)"
2.21 tausche_plus_minus "b kleiner c ==> (a + c - b) = (a - b + c)"
2.22 tausche_minus_plus "b kleiner c ==> (a - c + b) = (a + b - c)"
2.23 tausche_minus_minus "b kleiner c ==> (a - c - b) = (a - b - c)"
2.24
2.25 + (*commute with invariant (a.b).c -association*)
2.26 + tausche_mal "[| b is_atom; a kleiner b |] ==> \
2.27 + \(b * a) = (a * b)"
2.28 + tausche_vor_mal "[| b is_atom; a kleiner b |] ==> \
2.29 + \(-b * a) = (-a * b)"
2.30 + tausche_mal_mal "[| c is_atom; b kleiner c |] ==> \
2.31 + \(x * c * b) = (x * b * c)"
2.32 +(*WN080104^^^ _x_ umbenannt, vvv neu:
2.33 + tausche_mal_mal "[| c is_atom; b kleiner c |] ==> \
2.34 + \(b * a * c) = (a * b * c)"
2.35 +*)
2.36 +
2.37 subtrahiere_x_plus_minus "[| l is_const; m is_const |] ==> \
2.38 - \(k + m * n) - l * n = k + (m - l) * n"
2.39 + \(x + m * v) - l * v = x + (m - l) * v"
2.40 subtrahiere_x_minus_plus "[| l is_const; m is_const |] ==> \
2.41 - \(k - m * n) + l * n = k + (-m + l) * n"
2.42 + \(x - m * v) + l * v = x + (-m + l) * v"
2.43 subtrahiere_x_minus_minus "[| l is_const; m is_const |] ==> \
2.44 - \(k - m * n) - l * n = k + (-m - l) * n"
2.45 + \(x - m * v) - l * v = x + (-m - l) * v"
2.46 + addiere_vor_minus "[| l is_const; m is_const |] ==> \
2.47 + \- (l * v) + m * v = (-l + m) * v"
2.48 + addiere_eins_vor_minus "[| m is_const |] ==> \
2.49 + \- v + m * v = (-1 + m) * v"
2.50 + subtrahiere_vor_minus "[| l is_const; m is_const |] ==> \
2.51 + \- (l * v) - m * v = (-l - m) * v"
2.52 + subtrahiere_eins_vor_minus"[| m is_const |] ==> \
2.53 + \- v - m * v = (-1 - m) * v"
2.54
2.55 vorzeichen_minus_weg1 "l kleiner 0 ==> a + l * b = a - -1*l * b"
2.56 vorzeichen_minus_weg2 "l kleiner 0 ==> a - l * b = a + -1*l * b"
2.57 @@ -57,5 +81,10 @@
2.58 klammer_minus_plus "a - (b + c) = (a - b) - c"
2.59 klammer_minus_minus "a - (b - c) = (a - b) + c"
2.60
2.61 + klammer_mult_minus "a * (b - c) = a * b - a * c"
2.62 + klammer_minus_mult "(b - c) * a = b * a - c * a"
2.63 +
2.64 +
2.65 +
2.66 end
2.67
3.1 --- a/src/sml/ROOT.ML Fri Jan 04 16:08:52 2008 +0100
3.2 +++ b/src/sml/ROOT.ML Fri Jan 04 19:00:50 2008 +0100
3.3 @@ -12,7 +12,7 @@
3.4
3.5 (*.please change HERE and in RCODE-root accordingly,
3.6 if you store a new heap ...*)
3.7 -val version_isac = "WN071206-log-demo";
3.8 +val version_isac = "WN071206-applyTacticTW";
3.9
3.10 print_depth 1;(*reduces verbosity of stdout*)
3.11
4.1 --- a/src/smltest/IsacKnowledge/polyminus.sml Fri Jan 04 16:08:52 2008 +0100
4.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml Fri Jan 04 19:00:50 2008 +0100
4.3 @@ -21,6 +21,7 @@
4.4 "----------- pbl polynom probe -----------------------------------";
4.5 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
4.6 "----------- try fun applyTactics --------------------------------";
4.7 +"----------- pbl binom polynom vereinfachen p.39 -----------------";
4.8 "-----------------------------------------------------------------";
4.9 "-----------------------------------------------------------------";
4.10 "-----------------------------------------------------------------";
4.11 @@ -99,6 +100,10 @@
4.12 Some ("a kleiner b = True", _) => ()
4.13 | _ => raise error "polyminus.sml: a kleiner b = True";
4.14
4.15 +case eval_kleiner 0 0 (str2term "(10*g) kleiner f") 0 of
4.16 + Some ("10 * g kleiner f = False", _) => ()
4.17 + | _ => raise error "polyminus.sml: 10 * g kleiner f = False";
4.18 +
4.19 "----- compare tausche_plus with real_num_collect";
4.20 val od = dummy_ord;
4.21
4.22 @@ -285,10 +290,20 @@
4.23 val ((pt,p),_) = get_calc 1; show_pt pt;
4.24 "----- 2 ^^^";
4.25 trace_rewrite := true;
4.26 +val erls = erls_ordne_alphabetisch;
4.27 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
4.28 val Some (t',_) =
4.29 - rewrite_ Isac.thy e_rew_ord erls_ordne_alphabetisch false tausche_minus t;
4.30 + rewrite_ Isac.thy e_rew_ord erls false tausche_minus t;
4.31 term2str t'; "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
4.32 +
4.33 +val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
4.34 +val None =
4.35 + rewrite_ Isac.thy e_rew_ord erls false tausche_minus_plus t;
4.36 +
4.37 +val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
4.38 +val Some (t',_) =
4.39 + rewrite_set_ Isac.thy false ordne_alphabetisch t;
4.40 +term2str t'; "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
4.41 trace_rewrite := false;
4.42
4.43
4.44 @@ -318,16 +333,101 @@
4.45 (([], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f))]
4.46 ~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
4.47
4.48 -(*
4.49 -use"../smltest/IsacKnowledge/polyminus.sml";
4.50 -use"polyminus.sml";
4.51 - *)
4.52 -
4.53 states:=[];
4.54 -CalcTree [(["term ((- 4 + 6) * f)",
4.55 +CalcTree [(["term (- (8 * g) + 10 * g + h)",
4.56 "normalform N"],
4.57 ("PolyMinus.thy",["polynom","vereinfachen"],
4.58 ["simplification","for_polynomials","with_minus"]))];
4.59 moveActiveRoot 1;
4.60 autoCalculate 1 CompleteCalc;
4.61 val ((pt,p),_) = get_calc 1; show_pt pt;
4.62 +if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "2 * g + h"
4.63 +then () else raise error "polyminus.sml: addiere_vor_minus";
4.64 +
4.65 +
4.66 +states:=[];
4.67 +CalcTree [(["term (- (8 * g) + 10 * g + f)",
4.68 + "normalform N"],
4.69 + ("PolyMinus.thy",["polynom","vereinfachen"],
4.70 + ["simplification","for_polynomials","with_minus"]))];
4.71 +moveActiveRoot 1;
4.72 +autoCalculate 1 CompleteCalc;
4.73 +val ((pt,p),_) = get_calc 1; show_pt pt;
4.74 +if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "f + 2 * g"
4.75 +then () else raise error "polyminus.sml: tausche_vor_plus";
4.76 +
4.77 +
4.78 +"----------- pbl binom polynom vereinfachen p.39 -----------------";
4.79 +"----------- pbl binom polynom vereinfachen p.39 -----------------";
4.80 +"----------- pbl binom polynom vereinfachen p.39 -----------------";
4.81 +val rls = klammern_ausmultiplizieren;
4.82 +val t = str2term "(3 * a + 2) * (4 * a - 1)";
4.83 +val Some (t,_) = rewrite_set_ thy false rls t; term2str t;
4.84 +"3 * a * (4 * a) - 3 * a * 1 + (2 * (4 * a) - 2 * 1)";
4.85 +val rls = discard_parentheses;
4.86 +val Some (t,_) = rewrite_set_ thy false rls t; term2str t;
4.87 +"3 * a * 4 * a - 3 * a * 1 + (2 * 4 * a - 2 * 1)";
4.88 +val rls = ordne_monome;
4.89 +val Some (t,_) = rewrite_set_ thy false rls t; term2str t;
4.90 +"3 * 4 * a * a - 1 * 3 * a + (2 * 4 * a - 1 * 2)";
4.91 +(*
4.92 +val t = str2term "3 * a * 4 * a";
4.93 +val rls = ordne_monome;
4.94 +val Some (t,_) = rewrite_set_ thy false rls t; term2str t;
4.95 +*)
4.96 +val rls = klammern_aufloesen;
4.97 +val Some (t,_) = rewrite_set_ thy false rls t; term2str t;
4.98 +"3 * 4 * a * a - 1 * 3 * a + 2 * 4 * a - 1 * 2";
4.99 +val rls = ordne_alphabetisch;
4.100 +(*TODO: make is_monom more general, a*a=a^2, ...*)
4.101 +val Some (t,_) = rewrite_set_ thy false rls t; term2str t;
4.102 +"3 * 4 * a * a - 1 * 2 - 1 * 3 * a + 2 * 4 * a";
4.103 +(*GOON.WN080104
4.104 +val rls = fasse_zusammen;
4.105 +val Some (t,_) = rewrite_set_ thy false rls t; term2str t;
4.106 +val rls = verschoenere;
4.107 +val Some (t,_) = rewrite_set_ thy false rls t; term2str t;
4.108 +*)
4.109 +
4.110 +
4.111 +trace_rewrite := true;
4.112 +trace_rewrite := false;
4.113 +
4.114 +
4.115 +states:=[];
4.116 +CalcTree [(["term ((3*a + 2) * (4*a - 1))",
4.117 + "normalform N"],
4.118 + ("PolyMinus.thy",["mal","klammer","polynom","vereinfachen"],
4.119 + ["simplification","for_polynomials","with_parentheses_mult"]))];
4.120 +moveActiveRoot 1;
4.121 +autoCalculate 1 CompleteCalc;
4.122 +val ((pt,p),_) = get_calc 1; show_pt pt;
4.123 +
4.124 +(*
4.125 +if p = ([], Res) andalso
4.126 + term2str (get_obj g_res pt (fst p)) = "1 + 14 * u"
4.127 +then () else raise error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
4.128 +*)
4.129 +
4.130 +
4.131 +
4.132 +
4.133 +
4.134 +
4.135 +
4.136 +
4.137 +
4.138 +
4.139 +
4.140 +
4.141 +
4.142 +
4.143 +
4.144 +
4.145 +
4.146 +
4.147 +
4.148 +(*
4.149 +use"../smltest/IsacKnowledge/polyminus.sml";
4.150 +use"polyminus.sml";
4.151 + *)