1.1 --- a/src/sml/IsacKnowledge/Poly.ML Thu Dec 27 17:44:23 2007 +0100
1.2 +++ b/src/sml/IsacKnowledge/Poly.ML Fri Dec 28 12:10:09 2007 +0100
1.3 @@ -1448,6 +1448,7 @@
1.4 ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))
1.5 ]);
1.6
1.7 +
1.8 (** problems **)
1.9
1.10 store_pbt
1.11 @@ -1462,6 +1463,7 @@
1.12 Some "Simplify t_",
1.13 [["simplification","for_polynomials"]]));
1.14
1.15 +
1.16 (** methods **)
1.17
1.18 store_met
2.1 --- a/src/sml/IsacKnowledge/PolyMinus.ML Thu Dec 27 17:44:23 2007 +0100
2.2 +++ b/src/sml/IsacKnowledge/PolyMinus.ML Fri Dec 28 12:10:09 2007 +0100
2.3 @@ -151,13 +151,54 @@
2.4 Calc ("op *", eval_binop "#mult_")
2.5 ], scr = EmptyScr}:rls;
2.6
2.7 +val multipliziere_aus =
2.8 + Rls{id = "multipliziere_aus", preconds = [],
2.9 + rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
2.10 + rules = [Rls_ ordne_alphabetisch,
2.11 + Rls_ fasse_zusammen,
2.12 + Rls_ verschoenere
2.13 + ], scr = EmptyScr}:rls;
2.14 +
2.15 ruleset' :=
2.16 overwritelthy thy (!ruleset',
2.17 [("ordne_alphabetisch", prep_rls ordne_alphabetisch),
2.18 ("fasse_zusammen", prep_rls fasse_zusammen),
2.19 - ("verschoenere", prep_rls verschoenere)
2.20 + ("verschoenere", prep_rls verschoenere),
2.21 + ("multipliziere_aus", prep_rls multipliziere_aus)
2.22 ]);
2.23
2.24 (** problems **)
2.25
2.26 +store_pbt
2.27 + (prep_pbt Poly.thy "pbl_vereinf_poly" [] e_pblID
2.28 + (["polynom","vereinfachen"],
2.29 + [("#Given" ,["term t_"]),
2.30 + ("#Where" ,["t_ is_polyexp"]),
2.31 + ("#Find" ,["normalform n_"])
2.32 + ],
2.33 + append_rls "e_rls" e_rls [(*for preds in where_*)
2.34 + Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
2.35 + Some "Vereinfache t_",
2.36 + [["simplification","for_polynomials","with_minus"]]));
2.37 +
2.38 +
2.39 +
2.40 (** methods **)
2.41 +
2.42 +store_met
2.43 + (prep_met Poly.thy "met_simp_poly_minus" [] e_metID
2.44 + (["simplification","for_polynomials","with_minus"],
2.45 + [("#Given" ,["term t_"]),
2.46 + ("#Where" ,["t_ is_polyexp"]),
2.47 + ("#Find" ,["normalform n_"])
2.48 + ],
2.49 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
2.50 + prls = append_rls "simplification_for_polynomials_prls" e_rls
2.51 + [(*for preds in where_*)
2.52 + Calc("Poly.is'_polyexp",eval_is_polyexp"")],
2.53 + crls = e_rls, nrls = multipliziere_aus},
2.54 +"Script SimplifyScript (t_::real) = \
2.55 +\ (((Try (Rewrite_Set ordne_alphabetisch False)) @@\
2.56 +\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
2.57 +\ (Try (Rewrite_Set verschoenere False))) t_)"
2.58 + ));
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/sml/IsacKnowledge/Simplify.ML Fri Dec 28 12:10:09 2007 +0100
3.3 @@ -0,0 +1,76 @@
3.4 +(* simplification of terms
3.5 + author: Walther Neuper 050912
3.6 + (c) due to copyright terms
3.7 +
3.8 +use"IsacKnowledge/Simplify.ML";
3.9 +use"Simplify.ML";
3.10 +*)
3.11 +
3.12 +
3.13 +(** interface isabelle -- isac **)
3.14 +
3.15 +theory' := overwritel (!theory', [("Simplify.thy",Simplify.thy)]);
3.16 +
3.17 +(** problems **)
3.18 +
3.19 +store_pbt
3.20 + (prep_pbt Simplify.thy "pbl_simp" [] e_pblID
3.21 + (["simplification"],
3.22 + [("#Given" ,["term t_"]),
3.23 + ("#Find" ,["normalform n_"])
3.24 + ],
3.25 + append_rls "e_rls" e_rls [(*for preds in where_*)],
3.26 + Some "Simplify t_",
3.27 + []));
3.28 +
3.29 +store_pbt
3.30 + (prep_pbt Simplify.thy "pbl_vereinfache" [] e_pblID
3.31 + (["vereinfachen"],
3.32 + [("#Given" ,["term t_"]),
3.33 + ("#Find" ,["normalform n_"])
3.34 + ],
3.35 + append_rls "e_rls" e_rls [(*for preds in where_*)],
3.36 + Some "Vereinfache t_",
3.37 + []));
3.38 +
3.39 +(** methods **)
3.40 +
3.41 +store_met
3.42 + (prep_met Simplify.thy "met_simp" [] e_metID
3.43 + (["simplification"],
3.44 + [("#Given" ,["term t_"]),
3.45 + ("#Find" ,["normalform n_"])
3.46 + ],
3.47 + {rew_ord'="tless_true",
3.48 + rls'= e_rls,
3.49 + calc = [],
3.50 + srls = e_rls,
3.51 + prls=e_rls,
3.52 + crls = e_rls, nrls = e_rls},
3.53 + "empty_script"
3.54 + ));
3.55 +
3.56 +(** CAS-command **)
3.57 +
3.58 +(*.function for handling the cas-input "Simplify (2*a + 3*a)":
3.59 + make a model which is already in ptree-internal format.*)
3.60 +(* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
3.61 + val (h,argl) = strip_comb ((term_of o the o (parse thy))
3.62 + "Simplify (2*a + 3*a)");
3.63 + *)
3.64 +fun argl2dtss t =
3.65 + [((term_of o the o (parse thy)) "term", t),
3.66 + ((term_of o the o (parse thy)) "normalform",
3.67 + [(term_of o the o (parse thy)) "N"])
3.68 + ]
3.69 + | argl2dtss _ = raise error "Simplify.ML: wrong argument for argl2dtss";
3.70 +
3.71 +castab :=
3.72 +overwritel (!castab,
3.73 + [((term_of o the o (parse thy)) "Simplify",
3.74 + (("Isac.thy", ["simplification"], ["no_met"]),
3.75 + argl2dtss)),
3.76 + ((term_of o the o (parse thy)) "Vereinfache",
3.77 + (("Isac.thy", ["vereinfachen"], ["no_met"]),
3.78 + argl2dtss))
3.79 + ]);
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/sml/IsacKnowledge/Simplify.thy Fri Dec 28 12:10:09 2007 +0100
4.3 @@ -0,0 +1,29 @@
4.4 +(* simplification of terms
4.5 + author: Walther Neuper 050912
4.6 + (c) due to copyright terms
4.7 +
4.8 +remove_thy"Simplify";
4.9 +use_thy"~/proto2/isac/src/sml/IsacKnowledge/Simplify";
4.10 +
4.11 +use_thy_only"~/proto2/isac/src/sml/IsacKnowledge/Simplify";
4.12 +use_thy"~/proto2/isac/src/sml/IsacKnowledge/Isac";
4.13 +*)
4.14 +
4.15 +Simplify = Atools +
4.16 +
4.17 +consts
4.18 +
4.19 + (*descriptions in the related problem*)
4.20 + term :: real => una
4.21 + normalform :: real => una
4.22 +
4.23 + (*the CAS-command*)
4.24 + Simplify :: "real => real" (*"Simplify (1+2a+3+4a)*)
4.25 + Vereinfache :: "real => real" (*"Vereinfache (1+2a+3+4a)*)
4.26 +
4.27 + (*Script-name*)
4.28 + SimplifyScript :: "[real, real] => real"
4.29 + ("((Script SimplifyScript (_ =))// (_))" 9)
4.30 +
4.31 +
4.32 +end
4.33 \ No newline at end of file
5.1 --- a/src/smltest/IsacKnowledge/polyminus.sml Thu Dec 27 17:44:23 2007 +0100
5.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml Fri Dec 28 12:10:09 2007 +0100
5.3 @@ -13,8 +13,10 @@
5.4 "-----------------------------------------------------------------";
5.5 "----------- watch order_add_mult -------------------------------";
5.6 "----------- build predicate for +- ordering ---------------------";
5.7 -"----------- build fasse_zuswammen -------------------------------";
5.8 +"----------- build fasse_zusammen --------------------------------";
5.9 "----------- build verschoenere ----------------------------------";
5.10 +"----------- met simplification for_polynomials with_minus -------";
5.11 +"----------- pbl polynom vereinfachen ----------------------------";
5.12 "-----------------------------------------------------------------";
5.13 "-----------------------------------------------------------------";
5.14 "-----------------------------------------------------------------";
5.15 @@ -149,9 +151,9 @@
5.16 then () else raise error "polyminus.sml: ordne_alphabetisch finished";
5.17
5.18
5.19 -"----------- build fasse_zuswammen -------------------------------";
5.20 -"----------- build fasse_zuswammen -------------------------------";
5.21 -"----------- build fasse_zuswammen -------------------------------";
5.22 +"----------- build fasse_zusammen --------------------------------";
5.23 +"----------- build fasse_zusammen --------------------------------";
5.24 +"----------- build fasse_zusammen --------------------------------";
5.25 val t = str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
5.26 val Some (t,_) = rewrite_set_ thy false fasse_zusammen t;
5.27 if term2str t = "3 + -2 * e + 2 * f + 2 * g" then ()
5.28 @@ -167,6 +169,49 @@
5.29
5.30 trace_rewrite:=true;
5.31 trace_rewrite:=false;
5.32 +
5.33 +"----------- met simplification for_polynomials with_minus -------";
5.34 +"----------- met simplification for_polynomials with_minus -------";
5.35 +"----------- met simplification for_polynomials with_minus -------";
5.36 +val str =
5.37 +"Script SimplifyScript (t_::real) = \
5.38 +\ (((Try (Rewrite_Set ordne_alphabetisch False)) @@ \
5.39 +\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
5.40 +\ (Try (Rewrite_Set verschoenere False))) t_)"
5.41 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.42 +atomty sc;
5.43 +
5.44 +
5.45 +"----------- pbl polynom vereinfachen ----------------------------";
5.46 +"----------- pbl polynom vereinfachen ----------------------------";
5.47 +"----------- pbl polynom vereinfachen ----------------------------";
5.48 +states:=[];
5.49 +CalcTree [(["term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
5.50 + "normalform N"],
5.51 + ("PolyMinus.thy",["polynom","vereinfachen"],
5.52 + ["simplification","for_polynomials","with_minus"]))];
5.53 +moveActiveRoot 1;
5.54 +autoCalculate 1 CompleteCalc;
5.55 +val ((pt,p),_) = get_calc 1;
5.56 +if p = ([], Res) andalso
5.57 + term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"
5.58 +then () else raise error "biegelinie.sml: 1st biegelin.7.27 changed";
5.59 +show_pt pt;
5.60 +
5.61 +
5.62 +
5.63 +
5.64 +
5.65 +
5.66 +
5.67 +
5.68 +
5.69 +
5.70 +
5.71 +
5.72 +
5.73 +
5.74 +
5.75 (*
5.76 use"../smltest/IsacKnowledge/polyminus.sml";
5.77 use"polyminus.sml";