1.1 --- a/src/Tools/isac/Knowledge/Diff.thy Tue Jul 27 11:21:14 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Jul 27 12:32:43 2021 +0200
1.3 @@ -150,28 +150,24 @@
1.4 Rule_Def.Repeat {id="diff_sym_conv",
1.5 preconds = [],
1.6 rew_ord = ("termlessI",termlessI),
1.7 - erls = Rule_Set.append_rules "erls_diff_sym_conv" Rule_Set.empty
1.8 - [\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.9 -
1.10 - Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"),
1.11 - Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),
1.12 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.13 - Rule.Thm ("not_false", @{thm not_false}),
1.14 - Rule.Thm ("not_true", @{thm not_true})],
1.15 + erls =
1.16 + Rule_Set.append_rules "erls_diff_sym_conv" Rule_Set.empty
1.17 + [\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.18 + \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
1.19 + \<^rule_eval>\<open>is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
1.20 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.21 + \<^rule_thm>\<open>not_false\<close>,
1.22 + \<^rule_thm>\<open>not_true\<close>],
1.23 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.24 - rules = [\<^rule_thm>\<open>frac_sym_conv\<close>,
1.25 - \<^rule_thm>\<open>sqrt_sym_conv\<close>,
1.26 - \<^rule_thm>\<open>root_sym_conv\<close>,
1.27 - \<^rule_thm_sym>\<open>real_mult_minus1\<close>,
1.28 - (*- ?z = "-1 * ?z"*)
1.29 - \<^rule_thm>\<open>rat_mult\<close>,
1.30 - (*a / b * (c / d) = a * c / (b * d)*)
1.31 - \<^rule_thm>\<open>times_divide_eq_right\<close>,
1.32 - (*?x * (?y / ?z) = ?x * ?y / ?z*)
1.33 - \<^rule_thm>\<open>times_divide_eq_left\<close>,
1.34 - (*?y / ?z * ?x = ?y * ?x / ?z*)
1.35 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_")
1.36 - ],
1.37 + rules = [
1.38 + \<^rule_thm>\<open>frac_sym_conv\<close>,
1.39 + \<^rule_thm>\<open>sqrt_sym_conv\<close>,
1.40 + \<^rule_thm>\<open>root_sym_conv\<close>,
1.41 + \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*),
1.42 + \<^rule_thm>\<open>rat_mult\<close> (*a / b * (c / d) = a * c / (b * d)*),
1.43 + \<^rule_thm>\<open>times_divide_eq_right\<close> (*?x * (?y / ?z) = ?x * ?y / ?z*),
1.44 + \<^rule_thm>\<open>times_divide_eq_left\<close> (*?y / ?z * ?x = ?y * ?x / ?z*),
1.45 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_")],
1.46 scr = Rule.Empty_Prog};
1.47
1.48 (*..*)
2.1 --- a/src/Tools/isac/Knowledge/Poly.thy Tue Jul 27 11:21:14 2021 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Jul 27 12:32:43 2021 +0200
2.3 @@ -750,12 +750,10 @@
2.4 val discard_minus =
2.5 Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
2.6 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
2.7 - rules =
2.8 - [\<^rule_thm>\<open>real_diff_minus\<close>,
2.9 - (*"a - b = a + -1 * b"*)
2.10 - Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym}))
2.11 - (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)],
2.12 - scr = Rule.Empty_Prog};
2.13 + rules = [
2.14 + \<^rule_thm>\<open>real_diff_minus\<close> (*"a - b = a + -1 * b"*),
2.15 + \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)],
2.16 + scr = Rule.Empty_Prog};
2.17
2.18 val expand_poly_ =
2.19 Rule_Def.Repeat{id = "expand_poly_", preconds = [],
2.20 @@ -978,12 +976,9 @@
2.21 \<^rule_thm>\<open>real_plus_minus_binom2_p\<close>,
2.22 (*"(a - b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
2.23
2.24 - \<^rule_thm>\<open>minus_minus\<close>,
2.25 - (*"- (- ?z) = ?z"*)
2.26 - \<^rule_thm>\<open>real_diff_minus\<close>,
2.27 - (*"a - b = a + -1 * b"*)
2.28 - Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym}))
2.29 - (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)
2.30 + \<^rule_thm>\<open>minus_minus\<close> (*"- (- ?z) = ?z"*),
2.31 + \<^rule_thm>\<open>real_diff_minus\<close> (*"a - b = a + -1 * b"*),
2.32 + \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)
2.33
2.34 (*\<^rule_thm>\<open>real_minus_add_distrib\<close>,*)
2.35 (*"- (?x + ?y) = - ?x + - ?y"*)
3.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Tue Jul 27 11:21:14 2021 +0200
3.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Tue Jul 27 12:32:43 2021 +0200
3.3 @@ -15,15 +15,11 @@
3.4
3.5 (*.calculate numeral groundterms.*)
3.6 val calculate_RootRat =
3.7 - Rule_Set.append_rules "calculate_RootRat" calculate_Rational
3.8 - [\<^rule_thm>\<open>distrib_left\<close>,
3.9 - (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
3.10 - \<^rule_thm>\<open>mult_1_left\<close>,
3.11 - (* 1 * z = z *)
3.12 - Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym})),
3.13 - (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)
3.14 - Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_")
3.15 - ];
3.16 + Rule_Set.append_rules "calculate_RootRat" calculate_Rational [
3.17 + \<^rule_thm>\<open>distrib_left\<close> (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *),
3.18 + \<^rule_thm>\<open>mult_1_left\<close> (* 1 * z = z *),
3.19 + \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*),
3.20 + \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_")];
3.21
3.22 val prep_rls' = Auto_Prog.prep_rls @{theory};
3.23 \<close>
4.1 --- a/test/Tools/isac/Knowledge/diff.sml Tue Jul 27 11:21:14 2021 +0200
4.2 +++ b/test/Tools/isac/Knowledge/diff.sml Tue Jul 27 12:32:43 2021 +0200
4.3 @@ -276,17 +276,18 @@
4.4
4.5 val t = TermC.str2term "2 / sqrt x \<up> 3";
4.6 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
4.7 -if UnparseC.term t = "2 * x \<up> (-3 / 2)" then () else error"diff.sml x \<up> - 1/2";
4.8 -val rls = diff_sym_conv;
4.9 +if UnparseC.term t = "2 * x \<up> (- 3 / 2)" then () else error "diff.sml x \<up> - 1/2";
4.10 +
4.11 +val rls = diff_sym_conv;
4.12
4.13 val t = TermC.str2term "2 * x \<up> - 2";
4.14 -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
4.15 +val SOME (t, _) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
4.16 if UnparseC.term t = "2 / x \<up> 2" then () else error "diff.sml sym 1/x";
4.17
4.18
4.19 val t = TermC.str2term "x \<up> (3 / 2)";
4.20 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
4.21 -if UnparseC.term t = "sqrt (x \<up> 3)" then () else error"diff.sml sym x \<up> 1/x";
4.22 +if UnparseC.term t = "sqrt (x \<up> 3)" then ((*..wrong rewrite*)) else error"diff.sml sym x \<up> 1/x";
4.23
4.24 val t = TermC.str2term "2 * x \<up> (-3 / 2)";
4.25 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
4.26 @@ -308,7 +309,7 @@
4.27 autoCalculate 1 CompleteCalc;
4.28 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
4.29 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) =
4.30 - "1 + 2 * x + - 1 / x \<up> 2 + -4 / x \<up> 3" then ()
4.31 + "1 + 2 * x + - 1 / x \<up> 2 + - 4 / x \<up> 3" then ()
4.32 else error "diff.sml: differentiate_on_R 2/x \<up> 2 changed";
4.33
4.34 "---------------------------------------------------------";
4.35 @@ -345,7 +346,7 @@
4.36 LItool.trace_on := true;
4.37 *)
4.38 autoCalculate 1 CompleteCalc;
4.39 -(* Rewrite.trace_on := false; Rewrite.trace_on := false; (*true false*)
4.40 +(* Rewrite.trace_on := false; (*true false*)
4.41 LItool.trace_on := false;
4.42 *)
4.43 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
5.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue Jul 27 11:21:14 2021 +0200
5.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Jul 27 12:32:43 2021 +0200
5.3 @@ -301,7 +301,7 @@
5.4 ML_file "Knowledge/calculus.sml"
5.5 ML_file "Knowledge/trig.sml"
5.6 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
5.7 -(*ML_file "Knowledge/diff.sml" incomplete repair 2 * x \<up> - 2" --> 2 / x \<up> 2 | in Test_Some.thy*)
5.8 + ML_file "Knowledge/diff.sml"
5.9 (*ML_file "Knowledge/integrate.sml" rls simplify_Integral broken | in Test_Some.thy*)
5.10 (*ML_file "Knowledge/eqsystem.sml" simplify_System_parenthesized \<longrightarrow> - 0 + c_4 | in Test_Some.thy*)
5.11 ML_file "Knowledge/test.sml"
6.1 --- a/test/Tools/isac/Test_Some.thy Tue Jul 27 11:21:14 2021 +0200
6.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 27 12:32:43 2021 +0200
6.3 @@ -1159,435 +1159,6 @@
6.4 \<close> text \<open> (*-------^^^^^ polyeq-1.sml------------vvv diff.sml-------TOODOO----------------*)
6.5 \<close>
6.6
6.7 -section \<open>======== check Knowledge/diff.sml =================================================\<close>
6.8 -ML \<open>
6.9 -\<close> ML \<open>
6.10 -(* Title: test/Tools/isac/Knowledge/diff.sml
6.11 - Author: Walther Neuper
6.12 - Use is subject to license terms.
6.13 -*)
6.14 -"-----------------------------------------------------------------------------------------------";
6.15 -"-----------------------------------------------------------------------------------------------";
6.16 -"table of contents -----------------------------------------------------------------------------";
6.17 -"-----------------------------------------------------------------------------------------------";
6.18 -"----------- problemtype --------------------------------";
6.19 -"----------- for correction of diff_const ---------------";
6.20 -"----------- for correction of diff_quot ----------------";
6.21 -"----------- differentiate by rewrite -------------------";
6.22 -"----------- differentiate: me (*+ tacs input*) ---------";
6.23 -"----------- 1.5.02 me from script ----------------------";
6.24 -"----------- primed id ----------------------------------";
6.25 -"----------- diff_conv, sym_diff_conv -------------------";
6.26 -"----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
6.27 -"----------- autoCalculate diff after_simplification ----";
6.28 -"----------- autoCalculate differentiate_equality -------";
6.29 -"----------- tests for examples -------------------------";
6.30 -"------------inform for x \<up> 2+x+1 -------------------------";
6.31 -"--------------------------------------------------------";
6.32 -"--------------------------------------------------------";
6.33 -"--------------------------------------------------------";
6.34 -
6.35 -
6.36 -val thy = @{theory "Diff"};
6.37 -
6.38 -"----------- problemtype --------------------------------";
6.39 -"----------- problemtype --------------------------------";
6.40 -"----------- problemtype --------------------------------";
6.41 -val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"],
6.42 - Where =[],
6.43 - Find =["derivative f_f'"],
6.44 - With =[],
6.45 - Relate=[]}:string ppc;
6.46 -val chkpbt = ((map (the o (TermC.parse thy))) o P_Model.to_list) pbt;
6.47 -
6.48 -val org = ["functionTerm (d_d x (x \<up> 2 + 3 * x + 4))",
6.49 - "differentiateFor x", "derivative f_f'"];
6.50 -val chkorg = map (the o (TermC.parse thy)) org;
6.51 -
6.52 -Problem.from_store ["derivative_of", "function"];
6.53 -MethodC.from_store ["diff", "differentiate_on_R"];
6.54 -
6.55 -"----------- for correction of diff_const ---------------";
6.56 -"----------- for correction of diff_const ---------------";
6.57 -"----------- for correction of diff_const ---------------";
6.58 -(*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*)
6.59 -val t = (Thm.term_of o the o (TermC.parse thy)) "Not (x =!= a)";
6.60 -case rewrite_set_ thy false erls_diff t of
6.61 - SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
6.62 -| _ => error "rewrite_set_ Not (x =!= a) changed";
6.63 -
6.64 -val t =(Thm.term_of o the o (TermC.parse thy)) "2 is_const";
6.65 -case rewrite_set_ thy false erls_diff t of
6.66 - SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
6.67 -| _ => error "rewrite_set_ 2 is_const changed";
6.68 -
6.69 -val thm = @{thm diff_const};
6.70 -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x x";
6.71 -val subst = [(@{term "bdv::real"}, @{term "x::real"})];
6.72 -val NONE = (rewrite_inst_ thy tless_true erls_diff false subst thm ct);
6.73 -
6.74 -"----------- for correction of diff_quot ----------------";
6.75 -"----------- for correction of diff_quot ----------------";
6.76 -"----------- for correction of diff_quot ----------------";
6.77 -val thy = @{theory "Diff"};
6.78 -val ct = (Thm.term_of o the o (TermC.parse thy)) "Not (x = 0)";
6.79 -rewrite_set_ thy false erls_diff ct;
6.80 -
6.81 -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x ((x+1) / (x - 1))";
6.82 -val thm = @{thm diff_quot};
6.83 -val SOME (ctt,_) =
6.84 - (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
6.85 -
6.86 -"----------- differentiate by rewrite -------------------";
6.87 -"----------- differentiate by rewrite -------------------";
6.88 -"----------- differentiate by rewrite -------------------";
6.89 -val thy = @{theory "Diff"};
6.90 -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x (x \<up> 2 + 3 * x + 4)";
6.91 -"--- 1 ---";
6.92 -val thm = @{thm "diff_sum"};
6.93 -val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
6.94 -"--- 2 ---";
6.95 -val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
6.96 -"--- 3 ---";
6.97 -val thm = @{thm "diff_prod_const"};
6.98 -val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
6.99 -"--- 4 ---";
6.100 -val thm = @{thm "diff_pow"};
6.101 -val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
6.102 -"--- 5 ---";
6.103 -val thm = @{thm "diff_const"};
6.104 -val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
6.105 -"--- 6 ---";
6.106 -val thm = @{thm "diff_var"};
6.107 -val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
6.108 -if UnparseC.term ct = "2 * x \<up> (2 - 1) + 3 * 1 + 0" then ()
6.109 -else error "diff.sml diff.behav. in rewrite 1";
6.110 -"--- 7 ---";
6.111 -"--- 7 ---";
6.112 -val rls = Test_simplify;
6.113 -val ct = (Thm.term_of o the o (TermC.parse thy)) "2 * x \<up> (2 - 1) + 3 * 1 + 0";
6.114 -val (ct, _) = the (rewrite_set_ thy true rls ct);
6.115 -if UnparseC.term ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed";
6.116 -
6.117 -"----------- differentiate: me (*+ tacs input*) ---------";
6.118 -"----------- differentiate: me (*+ tacs input*) ---------";
6.119 -"----------- differentiate: me (*+ tacs input*) ---------";
6.120 -val fmz = ["functionTerm (x \<up> 2 + 3 * x + 4)",
6.121 - "differentiateFor x", "derivative f_f'"];
6.122 -val (dI',pI',mI') =
6.123 - ("Diff",["derivative_of", "function"],
6.124 - ["diff", "diff_simpl"]);
6.125 -val p = e_pos'; val c = [];
6.126 -"--- s1 ---";
6.127 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.128 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.129 -"--- s2 ---";
6.130 -(*val nxt = ("Add_Given",
6.131 -Add_Given "functionTerm (d_d x (x \<up> #2 + #3 * x + #4))");*)
6.132 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.133 -"--- s3 ---";
6.134 -(*val nxt = ("Add_Given",Add_Given "differentiateFor x");*)
6.135 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.136 -"--- s4 ---";
6.137 -(*val nxt = ("Add_Find",Add_Find "derivative f_f'");*)
6.138 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.139 -"--- s5 ---";
6.140 -(*val nxt = ("Specify_Theory",Specify_Theory dI');*)
6.141 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.142 -"--- s6 ---";
6.143 -(*val nxt = ("Specify_Problem",Specify_Problem pI');*)
6.144 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.145 -"--- s7 ---";
6.146 -(*val nxt = ("Specify_Method",Specify_Method mI');*)
6.147 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.148 -"--- s8 ---";
6.149 -(*val nxt = ("Apply_Method",Apply_Method mI');*)
6.150 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.151 -"--- 1 ---";
6.152 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum", "")));*)
6.153 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.154 -"--- 2 ---";
6.155 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum", "")));*)
6.156 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.157 -(*val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.158 -val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
6.159 -"--- 3 ---";
6.160 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_prod_const",...;*)
6.161 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.162 -(*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
6.163 -"--- 4 ---";
6.164 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_pow", "")));*)
6.165 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.166 -(*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
6.167 -"--- 5 ---";
6.168 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_prod_const",...;*)
6.169 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.170 -(*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
6.171 -"--- 6 ---";
6.172 -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_var", "")));*)
6.173 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.174 -if f2str f = "2 * x \<up> (2 - 1) + 3 * 1 + 0" then ()
6.175 -else error "diff.sml: diff.behav. in d_d x \<up> 2 + 3 * x + 4";
6.176 -"--- 7 ---";
6.177 -(*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial");*)
6.178 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.179 -"--- 8 ---";
6.180 -(*val nxt = ("Check_Postcond",Check_Postcond ("Diff", "differentiate_on_R"));*)
6.181 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.182 -"--- 9 ---";
6.183 -(*val nxt = ("End_Proof'",End_Proof');*)
6.184 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.185 -if f2str f = "3 + 2 * x"
6.186 - then case nxt of End_Proof' => ()
6.187 - | _ => error "diff.sml: new.behav. in me (*+ tacs input*) 1"
6.188 -else error "diff.sml: new.behav. in me (*+ tacs input*) 2";
6.189 -(*if f = EmptyMout then () else error "new behaviour in + tacs input"*)
6.190 -
6.191 -"----------- 1.5.02 me from script ----------------------";
6.192 -"----------- 1.5.02 me from script ----------------------";
6.193 -"----------- 1.5.02 me from script ----------------------";
6.194 -(*exp_Diff_No- 1.xml*)
6.195 -val fmz = ["functionTerm (x \<up> 2 + 3 * x + 4)",
6.196 - "differentiateFor x", "derivative f_f'"];
6.197 -val (dI',pI',mI') =
6.198 - ("Diff",["derivative_of", "function"],
6.199 - ["diff", "diff_simpl"]);
6.200 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.201 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.202 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.203 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.204 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.205 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.206 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.207 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.208 -(*nxt = ("Apply_Method",Apply_Method ("Diff", "differentiate_on_R*)
6.209 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.210 -
6.211 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.212 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.213 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.214 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.215 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.216 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.217 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.218 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.219 -case nxt of End_Proof' => ()
6.220 -| _ => error "new behaviour in tests/differentiate, 1.5.02 me from script";
6.221 -
6.222 -"----------- primed id ----------------------------------";
6.223 -"----------- primed id ----------------------------------";
6.224 -"----------- primed id ----------------------------------";
6.225 -val f_ = TermC.str2term "f_f::bool";
6.226 -val f = TermC.str2term "A = s * (a - s)";
6.227 -val v_ = TermC.str2term "v_v";
6.228 -val v = TermC.str2term "s";
6.229 -val screxp0 = TermC.str2term "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))";
6.230 -TermC.atomty screxp0;
6.231 -
6.232 -val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0;
6.233 -UnparseC.term screxp1;
6.234 -TermC.atomty screxp1;
6.235 -
6.236 -val SOME (f'_,_) = rewrite_set_ (@{theory "Isac_Knowledge"}) false srls_diff screxp1;
6.237 -if UnparseC.term f'_= "Take (A' = d_d s (s * (a - s)))" then ()
6.238 -else error "diff.sml: diff.behav. in 'primed'";
6.239 -TermC.atomty f'_;
6.240 -
6.241 -val str = "Program DiffEqScr (f_f::bool) (v_v::real) = \
6.242 -\ (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) \
6.243 -\ in (((Try (Repeat (Rewrite frac_conv))) #> \
6.244 - \ (Try (Repeat (Rewrite root_conv))) #> \
6.245 - \ (Try (Repeat (Rewrite realpow_pow))) #> \
6.246 - \ (Repeat \
6.247 - \ ((Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sum )) Or \
6.248 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod_const )) Or \
6.249 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod )) Or \
6.250 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_quot )) Or \
6.251 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin )) Or \
6.252 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin_chain )) Or \
6.253 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos )) Or \
6.254 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos_chain )) Or \
6.255 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow )) Or \
6.256 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow_chain )) Or \
6.257 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln )) Or \
6.258 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln_chain )) Or \
6.259 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp )) Or \
6.260 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp_chain )) Or \
6.261 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt )) Or \
6.262 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt_chain )) Or \
6.263 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_const )) Or \
6.264 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_var )) Or \
6.265 - \ (Repeat (Rewrite_Set make_polynomial)))) #> \
6.266 - \ (Try (Repeat (Rewrite sym_frac_conv))) #> \
6.267 - \ (Try (Repeat (Rewrite sym_root_conv))))) f_f')"
6.268 -;
6.269 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
6.270 -
6.271 -
6.272 -\<close> text \<open> (*TOODOO broken with merge after "eliminate ThmC.numerals_to_Free" *)
6.273 -"----------- diff_conv, sym_diff_conv -------------------";
6.274 -"----------- diff_conv, sym_diff_conv -------------------";
6.275 -"----------- diff_conv, sym_diff_conv -------------------";
6.276 -val subs = [(TermC.str2term "bdv", TermC.str2term "x")];
6.277 -val rls = diff_conv;
6.278 -
6.279 -val t = TermC.str2term "2/x \<up> 2";
6.280 -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
6.281 -if UnparseC.term t = "2 * x \<up> - 2" then () else error "diff.sml 1/x";
6.282 -
6.283 -val t = TermC.str2term "sqrt (x \<up> 3)";
6.284 -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
6.285 -if UnparseC.term t = "x \<up> (3 / 2)" then () else error "diff.sml x \<up> 1/2";
6.286 -
6.287 -val t = TermC.str2term "2 / sqrt x \<up> 3";
6.288 -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
6.289 -if UnparseC.term t = "2 * x \<up> (- 3 / 2)" then () else error "diff.sml x \<up> - 1/2";
6.290 -val rls = diff_sym_conv;
6.291 -
6.292 -val t = TermC.str2term "2 * x \<up> - 2";
6.293 -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
6.294 -if UnparseC.term t = "2 / x \<up> 2" then () else error "diff.sml sym 1/x";
6.295 -
6.296 -val t = TermC.str2term "x \<up> (3 / 2)";
6.297 -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
6.298 -if UnparseC.term t = "sqrt (x \<up> 3)" then ((*..wrong rewrite*)) else error"diff.sml sym x \<up> 1/x";
6.299 -
6.300 -val t = TermC.str2term "2 * x \<up> (-3 / 2)";
6.301 -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
6.302 -if UnparseC.term t ="2 / sqrt (x \<up> 3)"then()else error"diff.sml sym x \<up> - 1/x";
6.303 -
6.304 -
6.305 -\<close> text \<open> (*loops autoCalculate (x \<up> 2 + x+ 1/x + 2/x \<up> 2)"*)
6.306 -"----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
6.307 -"----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
6.308 -"----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
6.309 -reset_states ();
6.310 -CalcTree
6.311 -[(["functionTerm (x \<up> 2 + x+ 1/x + 2/x \<up> 2)",
6.312 - (*"functionTerm ((x \<up> 3) \<up> 5)",*)
6.313 - "differentiateFor x", "derivative f_f'"],
6.314 - ("Isac_Knowledge", ["derivative_of", "function"],
6.315 - ["diff", "differentiate_on_R"]))];
6.316 -Iterator 1;
6.317 -moveActiveRoot 1;
6.318 -autoCalculate 1 CompleteCalc;
6.319 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.320 -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) =
6.321 - "1 + 2 * x + - 1 / x \<up> 2 + -4 / x \<up> 3" then ()
6.322 -else error "diff.sml: differentiate_on_R 2/x \<up> 2 changed";
6.323 -
6.324 -\<close> text \<open> (*loops after repair of error "diff.sml sym 1/x": 2 * x \<up> - 2" --> 2 / x \<up> 2*)
6.325 -"---------------------------------------------------------";
6.326 -reset_states ();
6.327 -CalcTree
6.328 -[(["functionTerm (x \<up> 3 * x \<up> 5)",
6.329 - "differentiateFor x", "derivative f_f'"],
6.330 - ("Isac_Knowledge", ["derivative_of", "function"],
6.331 - ["diff", "differentiate_on_R"]))];
6.332 -Iterator 1;
6.333 -moveActiveRoot 1;
6.334 -autoCalculate 1 CompleteCalc;
6.335 -(* Rewrite.trace_on := false; (*true false*)
6.336 - LItool.trace_on := false;
6.337 - *)
6.338 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.339 -
6.340 -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) =
6.341 - "8 * x \<up> 7" then ()
6.342 -else error "diff.sml: differentiate_on_R (x \<up> 3 * x \<up> 5) changed";
6.343 -
6.344 -\<close> text \<open> (*loops after repair of error "diff.sml sym 1/x": 2 * x \<up> - 2" --> 2 / x \<up> 2*)
6.345 -"----------- autoCalculate diff after_simplification ----";
6.346 -"----------- autoCalculate diff after_simplification ----";
6.347 -"----------- autoCalculate diff after_simplification ----";
6.348 -reset_states ();
6.349 -CalcTree
6.350 -[(["functionTerm (x \<up> 3 * x \<up> 5)",
6.351 - "differentiateFor x", "derivative f_f'"],
6.352 - ("Isac_Knowledge", ["derivative_of", "function"],
6.353 - ["diff", "after_simplification"]))];
6.354 -Iterator 1;
6.355 -moveActiveRoot 1;
6.356 -(* Rewrite.trace_on := true; (*true false*)
6.357 - LItool.trace_on := true;
6.358 - *)
6.359 -autoCalculate 1 CompleteCalc;
6.360 -(* Rewrite.trace_on := false; (*true false*)
6.361 - LItool.trace_on := false;
6.362 - *)
6.363 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.364 -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "8 * x \<up> 7"
6.365 -then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
6.366 -
6.367 -\<close> text \<open> (*loops after repair of error "diff.sml sym 1/x": 2 * x \<up> - 2" --> 2 / x \<up> 2*)
6.368 -"--------------------------------------------------------";
6.369 -reset_states ();
6.370 -CalcTree
6.371 -[(["functionTerm ((x \<up> 3) \<up> 5)",
6.372 - "differentiateFor x", "derivative f_f'"],
6.373 - ("Isac_Knowledge", ["derivative_of", "function"],
6.374 - ["diff", "after_simplification"]))];
6.375 -Iterator 1;
6.376 -moveActiveRoot 1;
6.377 -autoCalculate 1 CompleteCalc;
6.378 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.379 -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "15 * x \<up> 14"
6.380 -then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
6.381 -
6.382 -\<close> text \<open> (*loops autoCalculate (A = s * (a - (s::real))*)
6.383 -"----------- autoCalculate differentiate_equality -------";
6.384 -"----------- autoCalculate differentiate_equality -------";
6.385 -"----------- autoCalculate differentiate_equality -------";
6.386 -reset_states ();
6.387 -CalcTree
6.388 -[(["functionEq (A = s * (a - (s::real)))", "differentiateFor s", "derivativeEq f_f'"],
6.389 - ("Isac_Knowledge", ["named", "derivative_of", "function"],
6.390 - ["diff", "differentiate_equality"]))];
6.391 -Iterator 1;
6.392 -moveActiveRoot 1;
6.393 -autoCalculate 1 CompleteCalc;
6.394 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.395 -
6.396 -\<close> ML \<open>
6.397 -"----------- tests for examples -------------------------";
6.398 -"----------- tests for examples -------------------------";
6.399 -"----------- tests for examples -------------------------";
6.400 -"----- TermC.parse errors";
6.401 -(*TermC.str2term "F = sqrt( y \<up> 2 - O) * (z + O \<up> 2)";
6.402 -TermC.str2term "O";
6.403 -TermC.str2term "OO"; ---errors*)
6.404 -TermC.str2term "OOO";
6.405 -
6.406 -"----- thm 'diff_prod_const'";
6.407 -val subs = [(TermC.str2term "bdv", TermC.str2term "l")];
6.408 -val f = TermC.str2term "G' = d_d l (l * sqrt (7 * s \<up> 2 - l \<up> 2))";
6.409 -
6.410 -\<close> text \<open> (*loops after repair of error "diff.sml sym 1/x": 2 * x \<up> - 2" --> 2 / x \<up> 2*)
6.411 -"------------inform for x \<up> 2+x+1 -------------------------";
6.412 -"------------inform for x \<up> 2+x+1 -------------------------";
6.413 -"------------inform for x \<up> 2+x+1 -------------------------";
6.414 -reset_states ();
6.415 -CalcTree
6.416 -[(["functionTerm (x \<up> 2 + x + 1)",
6.417 - "differentiateFor x", "derivative f_f'"],
6.418 - ("Isac_Knowledge", ["derivative_of", "function"],
6.419 - ["diff", "differentiate_on_R"]))];
6.420 -Iterator 1;
6.421 -moveActiveRoot 1;
6.422 -autoCalculate 1 CompleteCalcHead;
6.423 -autoCalculate 1 (Steps 1);
6.424 -autoCalculate 1 (Steps 1);
6.425 -autoCalculate 1 (Steps 1);
6.426 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.427 -appendFormula 1 "2*x + d_d x x + d_d x 1" (*|> Future.join*);
6.428 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
6.429 -if existpt' ([3], Res) pt then ()
6.430 -else error "diff.sml: inform d_d x (x \<up> 2 + x + 1) doesnt work";
6.431 -
6.432 -\<close> ML \<open>
6.433 -\<close> text \<open> (*-------^^^^^ diff.sml------------vvv integrate.sml-----------TOODOO------------*)
6.434 -\<close>
6.435 -
6.436 section \<open>======== check Knowledge/integrate.sml ============================================\<close>
6.437 ML \<open>
6.438 \<close> ML \<open>
6.439 @@ -1765,11 +1336,11 @@
6.440 --------------------------------------------------------------------*)
6.441
6.442
6.443 -\<close> ML \<open>
6.444 +\<close> text \<open>(* broken with repair /sym_/real_mult_minus1+sym *)
6.445 "----------- simplify by ruleset reducing make_ratpoly_in";
6.446 "----------- simplify by ruleset reducing make_ratpoly_in";
6.447 "----------- simplify by ruleset reducing make_ratpoly_in";
6.448 -val thy = @{theory "Isac_Knowledge"};
6.449 +val thy = @ {theory "Isac_Knowledge"};
6.450 "===== test 1";
6.451 val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
6.452