1.1 --- a/src/sml/IsacKnowledge/Diff.ML Fri Sep 12 11:17:20 2008 +0200
1.2 +++ b/src/sml/IsacKnowledge/Diff.ML Mon Sep 22 17:28:37 2008 +0200
1.3 @@ -30,6 +30,7 @@
1.4
1.5 (** rulesets **)
1.6
1.7 +(*.converts a term such that differentiation works optimally.*)
1.8 val diff_conv =
1.9 Rls {id="diff_conv",
1.10 preconds = [],
1.11 @@ -61,6 +62,7 @@
1.12 ],
1.13 scr = EmptyScr};
1.14
1.15 +(*.beautifies a term after differentiation.*)
1.16 val diff_sym_conv =
1.17 Rls {id="diff_sym_conv",
1.18 preconds = [],
1.19 @@ -85,6 +87,7 @@
1.20 ],
1.21 scr = EmptyScr};
1.22
1.23 +(*..*)
1.24 val srls_diff =
1.25 Rls {id="srls_differentiate..",
1.26 preconds = [],
1.27 @@ -97,6 +100,7 @@
1.28 ],
1.29 scr = EmptyScr};
1.30
1.31 +(*..*)
1.32 val erls_diff =
1.33 append_rls "erls_differentiate.." e_rls
1.34 [Thm ("not_true",num_str not_true),
1.35 @@ -108,6 +112,7 @@
1.36 Calc ("Atools.is'_const",eval_const "#is_const_")
1.37 ];
1.38
1.39 +(*.rules for differentiation, _no_ simplification.*)
1.40 val diff_rules =
1.41 Rls {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI),
1.42 erls = erls_diff, srls = Erls, calc = [],
1.43 @@ -185,7 +190,7 @@
1.44 (prep_met Diff.thy "met_diff" [] e_metID
1.45 (["diff"], [],
1.46 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
1.47 - crls = Atools_erls, nrls=norm_Rational}, "empty_script"));
1.48 + crls = Atools_erls, nrls = norm_diff}, "empty_script"));
1.49
1.50 store_met
1.51 (prep_met Diff.thy "met_diff_onR" [] e_metID
1.52 @@ -194,7 +199,7 @@
1.53 ("#Find" ,["derivative f_'_"])
1.54 ],
1.55 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
1.56 - prls=e_rls, crls = Atools_erls, nrls = e_rls},
1.57 + prls=e_rls, crls = Atools_erls, nrls = norm_diff},
1.58 "Script DiffScr (f_::real) (v_::real) = \
1.59 \ (let f'_ = Take (d_d v_ f_) \
1.60 \ in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ \
1.61 @@ -226,7 +231,7 @@
1.62 ("#Find" ,["derivative f_'_"])
1.63 ],
1.64 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
1.65 - prls=e_rls, crls = Atools_erls, nrls = norm_Rational},
1.66 + prls=e_rls, crls = Atools_erls, nrls = norm_diff},
1.67 "Script DiffScr (f_::real) (v_::real) = \
1.68 \ (let f'_ = Take (d_d v_ f_) \
1.69 \ in (( \
1.70 @@ -315,7 +320,7 @@
1.71 ("#Find" ,["derivative f_'_"])
1.72 ],
1.73 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls,
1.74 - crls=Atools_erls, nrls = e_rls},
1.75 + crls=Atools_erls, nrls = norm_Rational},
1.76 "Script DiffScr (f_::real) (v_::real) = \
1.77 \ (let f'_ = Take (d_d v_ f_) \
1.78 \ in ((Try (Rewrite_Set norm_Rational False)) @@ \
2.1 --- a/src/sml/IsacKnowledge/LogExp.thy Fri Sep 12 11:17:20 2008 +0200
2.2 +++ b/src/sml/IsacKnowledge/LogExp.thy Mon Sep 22 17:28:37 2008 +0200
2.3 @@ -22,6 +22,7 @@
2.4 rules
2.5
2.6 equality_pow "0 < a ==> (l = r) = (a^^^l = a^^^r)"
2.7 + (* this is what students ^^^^^^^... are told to do *)
2.8 equality_power "((a log b) = c) = (a^^^(a log b) = a^^^c)"
2.9 exp_invers_log "a^^^(a log b) = b"
2.10 (*---------------------------------------------------*)
3.1 --- a/src/sml/ROOT.ML Fri Sep 12 11:17:20 2008 +0200
3.2 +++ b/src/sml/ROOT.ML Mon Sep 22 17:28:37 2008 +0200
3.3 @@ -1,6 +1,11 @@
3.4 (*.evaluate isac (all the code of the kernel) and isactest
3.5 (c) Walther Neuper 1997
3.6
3.7 + poly /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux/HOL-Real
3.8 + cd"/home/neuper/proto2/isac/src/sml"; use"ROOT.ML";
3.9 +
3.10 +############################# nb-setup 080917 broke the isabelle configuration; thus HOL-Real CANNOT BE RECOMPUTED todo !
3.11 +
3.12 /usr/local/Isabelle2002/bin/isabelle HOL-Real
3.13 cd"/home/neuper/proto2/isac/src/sml"; use"ROOT.ML";
3.14
3.15 @@ -244,7 +249,7 @@
3.16 cd /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux
3.17 rm HOL-Real-Isac
3.18 cp HOL-Real HOL-Real-Isac
3.19 - /usr/local/Isabelle2002/bin/isabelle HOL-Real-Isac
3.20 + poly /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux/HOL-Real-Isac
3.21 cd"/home/neuper/proto2/isac/src/sml"; use"RCODE-root.sml";
3.22 <ctrl><d>
3.23 exit
4.1 --- a/src/smltest/IsacKnowledge/diff.sml Fri Sep 12 11:17:20 2008 +0200
4.2 +++ b/src/smltest/IsacKnowledge/diff.sml Mon Sep 22 17:28:37 2008 +0200
4.3 @@ -22,6 +22,7 @@
4.4 "----------- autoCalculate differentiate_equality ----------------";
4.5 "----------- tests for examples ----------------------------------";
4.6 "----------- CAS input -------------------------------------------";
4.7 +"------------inform for x^2+x+1 ----------------------------------";
4.8 "-----------------------------------------------------------------";
4.9 "-----------------------------------------------------------------";
4.10 "-----------------------------------------------------------------";
4.11 @@ -736,4 +737,25 @@
4.12 (* WN070703 does not work like Integrate due to error in next-pos
4.13 if p = ([], Res) andalso term2str res = "1 + 2 * x" then ()
4.14 else raise error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
4.15 -*)
4.16 \ No newline at end of file
4.17 +*)
4.18 +
4.19 +"------------inform for x^2+x+1 ----------------------------------";
4.20 +"------------inform for x^2+x+1 ----------------------------------";
4.21 +"------------inform for x^2+x+1 ----------------------------------";
4.22 +states:=[];
4.23 +CalcTree
4.24 +[(["functionTerm (x^2 + x + 1)",
4.25 + "differentiateFor x", "derivative f_'_"],
4.26 + ("Isac.thy", ["derivative_of","function"],
4.27 + ["diff","differentiate_on_R"]))];
4.28 +Iterator 1;
4.29 +moveActiveRoot 1;
4.30 +autoCalculate 1 CompleteCalcHead;
4.31 +autoCalculate 1 (Step 1);
4.32 +autoCalculate 1 (Step 1);
4.33 +autoCalculate 1 (Step 1);
4.34 +val ((pt,p),_) = get_calc 1; show_pt pt;
4.35 +appendFormula 1 "2*x + d_d x x + d_d x 1";
4.36 +val ((pt,p),_) = get_calc 1; show_pt pt;
4.37 +if existpt' ([3], Res) pt then ()
4.38 +else raise error "diff.sml: inform d_d x (x^2 + x + 1) doesnt work";