# HG changeset patch # User wneuper # Date 1627381963 -7200 # Node ID 59106f9e08ccc8c53aa9f1aa5b32f70813eb9398 # Parent 0ee698b0a703ed1b23ef8227a3f4079b4364179c //test/../diff.sml works again diff -r 0ee698b0a703 -r 59106f9e08cc src/Tools/isac/Knowledge/Diff.thy --- a/src/Tools/isac/Knowledge/Diff.thy Tue Jul 27 11:21:14 2021 +0200 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Jul 27 12:32:43 2021 +0200 @@ -150,28 +150,24 @@ Rule_Def.Repeat {id="diff_sym_conv", preconds = [], rew_ord = ("termlessI",termlessI), - erls = Rule_Set.append_rules "erls_diff_sym_conv" Rule_Set.empty - [\<^rule_eval>\less\ (Prog_Expr.eval_equ "#less_"), - - Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"), - Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"), - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), - Rule.Thm ("not_false", @{thm not_false}), - Rule.Thm ("not_true", @{thm not_true})], + erls = + Rule_Set.append_rules "erls_diff_sym_conv" Rule_Set.empty + [\<^rule_eval>\less\ (Prog_Expr.eval_equ "#less_"), + \<^rule_eval>\matches\ (Prog_Expr.eval_matches "#matches_"), + \<^rule_eval>\is_atom\ (Prog_Expr.eval_is_atom "#is_atom_"), + \<^rule_eval>\less\ (Prog_Expr.eval_equ "#less_"), + \<^rule_thm>\not_false\, + \<^rule_thm>\not_true\], srls = Rule_Set.Empty, calc = [], errpatts = [], - rules = [\<^rule_thm>\frac_sym_conv\, - \<^rule_thm>\sqrt_sym_conv\, - \<^rule_thm>\root_sym_conv\, - \<^rule_thm_sym>\real_mult_minus1\, - (*- ?z = "-1 * ?z"*) - \<^rule_thm>\rat_mult\, - (*a / b * (c / d) = a * c / (b * d)*) - \<^rule_thm>\times_divide_eq_right\, - (*?x * (?y / ?z) = ?x * ?y / ?z*) - \<^rule_thm>\times_divide_eq_left\, - (*?y / ?z * ?x = ?y * ?x / ?z*) - \<^rule_eval>\times\ (**)(eval_binop "#mult_") - ], + rules = [ + \<^rule_thm>\frac_sym_conv\, + \<^rule_thm>\sqrt_sym_conv\, + \<^rule_thm>\root_sym_conv\, + \<^rule_thm>\real_mult_minus1_sym\ (*"\(z is_const) ==> - (z::real) = -1 * z"*), + \<^rule_thm>\rat_mult\ (*a / b * (c / d) = a * c / (b * d)*), + \<^rule_thm>\times_divide_eq_right\ (*?x * (?y / ?z) = ?x * ?y / ?z*), + \<^rule_thm>\times_divide_eq_left\ (*?y / ?z * ?x = ?y * ?x / ?z*), + \<^rule_eval>\times\ (**)(eval_binop "#mult_")], scr = Rule.Empty_Prog}; (*..*) diff -r 0ee698b0a703 -r 59106f9e08cc src/Tools/isac/Knowledge/Poly.thy --- a/src/Tools/isac/Knowledge/Poly.thy Tue Jul 27 11:21:14 2021 +0200 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Jul 27 12:32:43 2021 +0200 @@ -750,12 +750,10 @@ val discard_minus = Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], - rules = - [\<^rule_thm>\real_diff_minus\, - (*"a - b = a + -1 * b"*) - Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym})) - (*"\(z is_const) ==> - (z::real) = -1 * z"*)], - scr = Rule.Empty_Prog}; + rules = [ + \<^rule_thm>\real_diff_minus\ (*"a - b = a + -1 * b"*), + \<^rule_thm>\real_mult_minus1_sym\ (*"\(z is_const) ==> - (z::real) = -1 * z"*)], + scr = Rule.Empty_Prog}; val expand_poly_ = Rule_Def.Repeat{id = "expand_poly_", preconds = [], @@ -978,12 +976,9 @@ \<^rule_thm>\real_plus_minus_binom2_p\, (*"(a - b)*(a + b) = a \ 2 + -1*b \ 2"*) - \<^rule_thm>\minus_minus\, - (*"- (- ?z) = ?z"*) - \<^rule_thm>\real_diff_minus\, - (*"a - b = a + -1 * b"*) - Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym})) - (*"\(z is_const) ==> - (z::real) = -1 * z"*) + \<^rule_thm>\minus_minus\ (*"- (- ?z) = ?z"*), + \<^rule_thm>\real_diff_minus\ (*"a - b = a + -1 * b"*), + \<^rule_thm>\real_mult_minus1_sym\ (*"\(z is_const) ==> - (z::real) = -1 * z"*) (*\<^rule_thm>\real_minus_add_distrib\,*) (*"- (?x + ?y) = - ?x + - ?y"*) diff -r 0ee698b0a703 -r 59106f9e08cc src/Tools/isac/Knowledge/RootRat.thy --- a/src/Tools/isac/Knowledge/RootRat.thy Tue Jul 27 11:21:14 2021 +0200 +++ b/src/Tools/isac/Knowledge/RootRat.thy Tue Jul 27 12:32:43 2021 +0200 @@ -15,15 +15,11 @@ (*.calculate numeral groundterms.*) val calculate_RootRat = - Rule_Set.append_rules "calculate_RootRat" calculate_Rational - [\<^rule_thm>\distrib_left\, - (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *) - \<^rule_thm>\mult_1_left\, - (* 1 * z = z *) - Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym})), - (*"\(z is_const) ==> - (z::real) = -1 * z"*) - Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_") - ]; + Rule_Set.append_rules "calculate_RootRat" calculate_Rational [ + \<^rule_thm>\distrib_left\ (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *), + \<^rule_thm>\mult_1_left\ (* 1 * z = z *), + \<^rule_thm>\real_mult_minus1_sym\ (*"\(z is_const) ==> - (z::real) = -1 * z"*), + \<^rule_eval>\sqrt\ (eval_sqrt "#sqrt_")]; val prep_rls' = Auto_Prog.prep_rls @{theory}; \ diff -r 0ee698b0a703 -r 59106f9e08cc test/Tools/isac/Knowledge/diff.sml --- a/test/Tools/isac/Knowledge/diff.sml Tue Jul 27 11:21:14 2021 +0200 +++ b/test/Tools/isac/Knowledge/diff.sml Tue Jul 27 12:32:43 2021 +0200 @@ -276,17 +276,18 @@ val t = TermC.str2term "2 / sqrt x \ 3"; val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t; -if UnparseC.term t = "2 * x \ (-3 / 2)" then () else error"diff.sml x \ - 1/2"; -val rls = diff_sym_conv; +if UnparseC.term t = "2 * x \ (- 3 / 2)" then () else error "diff.sml x \ - 1/2"; + +val rls = diff_sym_conv; val t = TermC.str2term "2 * x \ - 2"; -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t; +val SOME (t, _) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t; if UnparseC.term t = "2 / x \ 2" then () else error "diff.sml sym 1/x"; val t = TermC.str2term "x \ (3 / 2)"; val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t; -if UnparseC.term t = "sqrt (x \ 3)" then () else error"diff.sml sym x \ 1/x"; +if UnparseC.term t = "sqrt (x \ 3)" then ((*..wrong rewrite*)) else error"diff.sml sym x \ 1/x"; val t = TermC.str2term "2 * x \ (-3 / 2)"; val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t; @@ -308,7 +309,7 @@ autoCalculate 1 CompleteCalc; val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = - "1 + 2 * x + - 1 / x \ 2 + -4 / x \ 3" then () + "1 + 2 * x + - 1 / x \ 2 + - 4 / x \ 3" then () else error "diff.sml: differentiate_on_R 2/x \ 2 changed"; "---------------------------------------------------------"; @@ -345,7 +346,7 @@ LItool.trace_on := true; *) autoCalculate 1 CompleteCalc; -(* Rewrite.trace_on := false; Rewrite.trace_on := false; (*true false*) +(* Rewrite.trace_on := false; (*true false*) LItool.trace_on := false; *) val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; diff -r 0ee698b0a703 -r 59106f9e08cc test/Tools/isac/Test_Isac_Short.thy --- a/test/Tools/isac/Test_Isac_Short.thy Tue Jul 27 11:21:14 2021 +0200 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Jul 27 12:32:43 2021 +0200 @@ -301,7 +301,7 @@ ML_file "Knowledge/calculus.sml" ML_file "Knowledge/trig.sml" (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*) -(*ML_file "Knowledge/diff.sml" incomplete repair 2 * x \ - 2" --> 2 / x \ 2 | in Test_Some.thy*) + ML_file "Knowledge/diff.sml" (*ML_file "Knowledge/integrate.sml" rls simplify_Integral broken | in Test_Some.thy*) (*ML_file "Knowledge/eqsystem.sml" simplify_System_parenthesized \ - 0 + c_4 | in Test_Some.thy*) ML_file "Knowledge/test.sml" diff -r 0ee698b0a703 -r 59106f9e08cc test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Tue Jul 27 11:21:14 2021 +0200 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 27 12:32:43 2021 +0200 @@ -1159,435 +1159,6 @@ \ text \ (*-------^^^^^ polyeq-1.sml------------vvv diff.sml-------TOODOO----------------*) \ -section \======== check Knowledge/diff.sml =================================================\ -ML \ -\ ML \ -(* Title: test/Tools/isac/Knowledge/diff.sml - Author: Walther Neuper - Use is subject to license terms. -*) -"-----------------------------------------------------------------------------------------------"; -"-----------------------------------------------------------------------------------------------"; -"table of contents -----------------------------------------------------------------------------"; -"-----------------------------------------------------------------------------------------------"; -"----------- problemtype --------------------------------"; -"----------- for correction of diff_const ---------------"; -"----------- for correction of diff_quot ----------------"; -"----------- differentiate by rewrite -------------------"; -"----------- differentiate: me (*+ tacs input*) ---------"; -"----------- 1.5.02 me from script ----------------------"; -"----------- primed id ----------------------------------"; -"----------- diff_conv, sym_diff_conv -------------------"; -"----------- autoCalculate differentiate_on_R 2/x \ 2 -----"; -"----------- autoCalculate diff after_simplification ----"; -"----------- autoCalculate differentiate_equality -------"; -"----------- tests for examples -------------------------"; -"------------inform for x \ 2+x+1 -------------------------"; -"--------------------------------------------------------"; -"--------------------------------------------------------"; -"--------------------------------------------------------"; - - -val thy = @{theory "Diff"}; - -"----------- problemtype --------------------------------"; -"----------- problemtype --------------------------------"; -"----------- problemtype --------------------------------"; -val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"], - Where =[], - Find =["derivative f_f'"], - With =[], - Relate=[]}:string ppc; -val chkpbt = ((map (the o (TermC.parse thy))) o P_Model.to_list) pbt; - -val org = ["functionTerm (d_d x (x \ 2 + 3 * x + 4))", - "differentiateFor x", "derivative f_f'"]; -val chkorg = map (the o (TermC.parse thy)) org; - -Problem.from_store ["derivative_of", "function"]; -MethodC.from_store ["diff", "differentiate_on_R"]; - -"----------- for correction of diff_const ---------------"; -"----------- for correction of diff_const ---------------"; -"----------- for correction of diff_const ---------------"; -(*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*) -val t = (Thm.term_of o the o (TermC.parse thy)) "Not (x =!= a)"; -case rewrite_set_ thy false erls_diff t of - SOME (Const (\<^const_name>\True\, _), []) => () -| _ => error "rewrite_set_ Not (x =!= a) changed"; - -val t =(Thm.term_of o the o (TermC.parse thy)) "2 is_const"; -case rewrite_set_ thy false erls_diff t of - SOME (Const (\<^const_name>\True\, _), []) => () -| _ => error "rewrite_set_ 2 is_const changed"; - -val thm = @{thm diff_const}; -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x x"; -val subst = [(@{term "bdv::real"}, @{term "x::real"})]; -val NONE = (rewrite_inst_ thy tless_true erls_diff false subst thm ct); - -"----------- for correction of diff_quot ----------------"; -"----------- for correction of diff_quot ----------------"; -"----------- for correction of diff_quot ----------------"; -val thy = @{theory "Diff"}; -val ct = (Thm.term_of o the o (TermC.parse thy)) "Not (x = 0)"; -rewrite_set_ thy false erls_diff ct; - -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x ((x+1) / (x - 1))"; -val thm = @{thm diff_quot}; -val SOME (ctt,_) = - (rewrite_inst_ thy tless_true erls_diff true subst thm ct); - -"----------- differentiate by rewrite -------------------"; -"----------- differentiate by rewrite -------------------"; -"----------- differentiate by rewrite -------------------"; -val thy = @{theory "Diff"}; -val ct = (Thm.term_of o the o (TermC.parse thy)) "d_d x (x \ 2 + 3 * x + 4)"; -"--- 1 ---"; -val thm = @{thm "diff_sum"}; -val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct); -"--- 2 ---"; -val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct); -"--- 3 ---"; -val thm = @{thm "diff_prod_const"}; -val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct); -"--- 4 ---"; -val thm = @{thm "diff_pow"}; -val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct); -"--- 5 ---"; -val thm = @{thm "diff_const"}; -val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct); -"--- 6 ---"; -val thm = @{thm "diff_var"}; -val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct); -if UnparseC.term ct = "2 * x \ (2 - 1) + 3 * 1 + 0" then () -else error "diff.sml diff.behav. in rewrite 1"; -"--- 7 ---"; -"--- 7 ---"; -val rls = Test_simplify; -val ct = (Thm.term_of o the o (TermC.parse thy)) "2 * x \ (2 - 1) + 3 * 1 + 0"; -val (ct, _) = the (rewrite_set_ thy true rls ct); -if UnparseC.term ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed"; - -"----------- differentiate: me (*+ tacs input*) ---------"; -"----------- differentiate: me (*+ tacs input*) ---------"; -"----------- differentiate: me (*+ tacs input*) ---------"; -val fmz = ["functionTerm (x \ 2 + 3 * x + 4)", - "differentiateFor x", "derivative f_f'"]; -val (dI',pI',mI') = - ("Diff",["derivative_of", "function"], - ["diff", "diff_simpl"]); -val p = e_pos'; val c = []; -"--- s1 ---"; -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"--- s2 ---"; -(*val nxt = ("Add_Given", -Add_Given "functionTerm (d_d x (x \ #2 + #3 * x + #4))");*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"--- s3 ---"; -(*val nxt = ("Add_Given",Add_Given "differentiateFor x");*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"--- s4 ---"; -(*val nxt = ("Add_Find",Add_Find "derivative f_f'");*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"--- s5 ---"; -(*val nxt = ("Specify_Theory",Specify_Theory dI');*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"--- s6 ---"; -(*val nxt = ("Specify_Problem",Specify_Problem pI');*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"--- s7 ---"; -(*val nxt = ("Specify_Method",Specify_Method mI');*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"--- s8 ---"; -(*val nxt = ("Apply_Method",Apply_Method mI');*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"--- 1 ---"; -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum", "")));*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"--- 2 ---"; -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum", "")));*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt;*) -"--- 3 ---"; -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_prod_const",...;*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*val (p,_,f,nxt,_,pt) = me nxt p c pt;*) -"--- 4 ---"; -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_pow", "")));*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*val (p,_,f,nxt,_,pt) = me nxt p c pt;*) -"--- 5 ---"; -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_prod_const",...;*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*val (p,_,f,nxt,_,pt) = me nxt p c pt;*) -"--- 6 ---"; -(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_var", "")));*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -if f2str f = "2 * x \ (2 - 1) + 3 * 1 + 0" then () -else error "diff.sml: diff.behav. in d_d x \ 2 + 3 * x + 4"; -"--- 7 ---"; -(*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial");*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"--- 8 ---"; -(*val nxt = ("Check_Postcond",Check_Postcond ("Diff", "differentiate_on_R"));*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"--- 9 ---"; -(*val nxt = ("End_Proof'",End_Proof');*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; -if f2str f = "3 + 2 * x" - then case nxt of End_Proof' => () - | _ => error "diff.sml: new.behav. in me (*+ tacs input*) 1" -else error "diff.sml: new.behav. in me (*+ tacs input*) 2"; -(*if f = EmptyMout then () else error "new behaviour in + tacs input"*) - -"----------- 1.5.02 me from script ----------------------"; -"----------- 1.5.02 me from script ----------------------"; -"----------- 1.5.02 me from script ----------------------"; -(*exp_Diff_No- 1.xml*) -val fmz = ["functionTerm (x \ 2 + 3 * x + 4)", - "differentiateFor x", "derivative f_f'"]; -val (dI',pI',mI') = - ("Diff",["derivative_of", "function"], - ["diff", "diff_simpl"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*nxt = ("Apply_Method",Apply_Method ("Diff", "differentiate_on_R*) -val (p,_,f,nxt,_,pt) = me nxt p c pt; - -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -case nxt of End_Proof' => () -| _ => error "new behaviour in tests/differentiate, 1.5.02 me from script"; - -"----------- primed id ----------------------------------"; -"----------- primed id ----------------------------------"; -"----------- primed id ----------------------------------"; -val f_ = TermC.str2term "f_f::bool"; -val f = TermC.str2term "A = s * (a - s)"; -val v_ = TermC.str2term "v_v"; -val v = TermC.str2term "s"; -val screxp0 = TermC.str2term "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))"; -TermC.atomty screxp0; - -val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0; -UnparseC.term screxp1; -TermC.atomty screxp1; - -val SOME (f'_,_) = rewrite_set_ (@{theory "Isac_Knowledge"}) false srls_diff screxp1; -if UnparseC.term f'_= "Take (A' = d_d s (s * (a - s)))" then () -else error "diff.sml: diff.behav. in 'primed'"; -TermC.atomty f'_; - -val str = "Program DiffEqScr (f_f::bool) (v_v::real) = \ -\ (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) \ -\ in (((Try (Repeat (Rewrite frac_conv))) #> \ - \ (Try (Repeat (Rewrite root_conv))) #> \ - \ (Try (Repeat (Rewrite realpow_pow))) #> \ - \ (Repeat \ - \ ((Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sum )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod_const )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_quot )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin_chain )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos_chain )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow_chain )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln_chain )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp_chain )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt_chain )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_const )) Or \ - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_var )) Or \ - \ (Repeat (Rewrite_Set make_polynomial)))) #> \ - \ (Try (Repeat (Rewrite sym_frac_conv))) #> \ - \ (Try (Repeat (Rewrite sym_root_conv))))) f_f')" -; -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str; - - -\ text \ (*TOODOO broken with merge after "eliminate ThmC.numerals_to_Free" *) -"----------- diff_conv, sym_diff_conv -------------------"; -"----------- diff_conv, sym_diff_conv -------------------"; -"----------- diff_conv, sym_diff_conv -------------------"; -val subs = [(TermC.str2term "bdv", TermC.str2term "x")]; -val rls = diff_conv; - -val t = TermC.str2term "2/x \ 2"; -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t; -if UnparseC.term t = "2 * x \ - 2" then () else error "diff.sml 1/x"; - -val t = TermC.str2term "sqrt (x \ 3)"; -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t; -if UnparseC.term t = "x \ (3 / 2)" then () else error "diff.sml x \ 1/2"; - -val t = TermC.str2term "2 / sqrt x \ 3"; -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t; -if UnparseC.term t = "2 * x \ (- 3 / 2)" then () else error "diff.sml x \ - 1/2"; -val rls = diff_sym_conv; - -val t = TermC.str2term "2 * x \ - 2"; -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t; -if UnparseC.term t = "2 / x \ 2" then () else error "diff.sml sym 1/x"; - -val t = TermC.str2term "x \ (3 / 2)"; -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t; -if UnparseC.term t = "sqrt (x \ 3)" then ((*..wrong rewrite*)) else error"diff.sml sym x \ 1/x"; - -val t = TermC.str2term "2 * x \ (-3 / 2)"; -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t; -if UnparseC.term t ="2 / sqrt (x \ 3)"then()else error"diff.sml sym x \ - 1/x"; - - -\ text \ (*loops autoCalculate (x \ 2 + x+ 1/x + 2/x \ 2)"*) -"----------- autoCalculate differentiate_on_R 2/x \ 2 -----"; -"----------- autoCalculate differentiate_on_R 2/x \ 2 -----"; -"----------- autoCalculate differentiate_on_R 2/x \ 2 -----"; -reset_states (); -CalcTree -[(["functionTerm (x \ 2 + x+ 1/x + 2/x \ 2)", - (*"functionTerm ((x \ 3) \ 5)",*) - "differentiateFor x", "derivative f_f'"], - ("Isac_Knowledge", ["derivative_of", "function"], - ["diff", "differentiate_on_R"]))]; -Iterator 1; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = - "1 + 2 * x + - 1 / x \ 2 + -4 / x \ 3" then () -else error "diff.sml: differentiate_on_R 2/x \ 2 changed"; - -\ text \ (*loops after repair of error "diff.sml sym 1/x": 2 * x \ - 2" --> 2 / x \ 2*) -"---------------------------------------------------------"; -reset_states (); -CalcTree -[(["functionTerm (x \ 3 * x \ 5)", - "differentiateFor x", "derivative f_f'"], - ("Isac_Knowledge", ["derivative_of", "function"], - ["diff", "differentiate_on_R"]))]; -Iterator 1; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -(* Rewrite.trace_on := false; (*true false*) - LItool.trace_on := false; - *) -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; - -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = - "8 * x \ 7" then () -else error "diff.sml: differentiate_on_R (x \ 3 * x \ 5) changed"; - -\ text \ (*loops after repair of error "diff.sml sym 1/x": 2 * x \ - 2" --> 2 / x \ 2*) -"----------- autoCalculate diff after_simplification ----"; -"----------- autoCalculate diff after_simplification ----"; -"----------- autoCalculate diff after_simplification ----"; -reset_states (); -CalcTree -[(["functionTerm (x \ 3 * x \ 5)", - "differentiateFor x", "derivative f_f'"], - ("Isac_Knowledge", ["derivative_of", "function"], - ["diff", "after_simplification"]))]; -Iterator 1; -moveActiveRoot 1; -(* Rewrite.trace_on := true; (*true false*) - LItool.trace_on := true; - *) -autoCalculate 1 CompleteCalc; -(* Rewrite.trace_on := false; (*true false*) - LItool.trace_on := false; - *) -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "8 * x \ 7" -then () else error "biegelinie.sml: 1st biegelin.7.27 changed"; - -\ text \ (*loops after repair of error "diff.sml sym 1/x": 2 * x \ - 2" --> 2 / x \ 2*) -"--------------------------------------------------------"; -reset_states (); -CalcTree -[(["functionTerm ((x \ 3) \ 5)", - "differentiateFor x", "derivative f_f'"], - ("Isac_Knowledge", ["derivative_of", "function"], - ["diff", "after_simplification"]))]; -Iterator 1; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "15 * x \ 14" -then () else error "biegelinie.sml: 1st biegelin.7.27 changed"; - -\ text \ (*loops autoCalculate (A = s * (a - (s::real))*) -"----------- autoCalculate differentiate_equality -------"; -"----------- autoCalculate differentiate_equality -------"; -"----------- autoCalculate differentiate_equality -------"; -reset_states (); -CalcTree -[(["functionEq (A = s * (a - (s::real)))", "differentiateFor s", "derivativeEq f_f'"], - ("Isac_Knowledge", ["named", "derivative_of", "function"], - ["diff", "differentiate_equality"]))]; -Iterator 1; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; - -\ ML \ -"----------- tests for examples -------------------------"; -"----------- tests for examples -------------------------"; -"----------- tests for examples -------------------------"; -"----- TermC.parse errors"; -(*TermC.str2term "F = sqrt( y \ 2 - O) * (z + O \ 2)"; -TermC.str2term "O"; -TermC.str2term "OO"; ---errors*) -TermC.str2term "OOO"; - -"----- thm 'diff_prod_const'"; -val subs = [(TermC.str2term "bdv", TermC.str2term "l")]; -val f = TermC.str2term "G' = d_d l (l * sqrt (7 * s \ 2 - l \ 2))"; - -\ text \ (*loops after repair of error "diff.sml sym 1/x": 2 * x \ - 2" --> 2 / x \ 2*) -"------------inform for x \ 2+x+1 -------------------------"; -"------------inform for x \ 2+x+1 -------------------------"; -"------------inform for x \ 2+x+1 -------------------------"; -reset_states (); -CalcTree -[(["functionTerm (x \ 2 + x + 1)", - "differentiateFor x", "derivative f_f'"], - ("Isac_Knowledge", ["derivative_of", "function"], - ["diff", "differentiate_on_R"]))]; -Iterator 1; -moveActiveRoot 1; -autoCalculate 1 CompleteCalcHead; -autoCalculate 1 (Steps 1); -autoCalculate 1 (Steps 1); -autoCalculate 1 (Steps 1); -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -appendFormula 1 "2*x + d_d x x + d_d x 1" (*|> Future.join*); -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; -if existpt' ([3], Res) pt then () -else error "diff.sml: inform d_d x (x \ 2 + x + 1) doesnt work"; - -\ ML \ -\ text \ (*-------^^^^^ diff.sml------------vvv integrate.sml-----------TOODOO------------*) -\ - section \======== check Knowledge/integrate.sml ============================================\ ML \ \ ML \ @@ -1765,11 +1336,11 @@ --------------------------------------------------------------------*) -\ ML \ +\ text \(* broken with repair /sym_/real_mult_minus1+sym *) "----------- simplify by ruleset reducing make_ratpoly_in"; "----------- simplify by ruleset reducing make_ratpoly_in"; "----------- simplify by ruleset reducing make_ratpoly_in"; -val thy = @{theory "Isac_Knowledge"}; +val thy = @ {theory "Isac_Knowledge"}; "===== test 1"; val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \ 2 / 2)";