1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Sun Aug 08 15:21:33 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Mon Aug 09 11:19:25 2021 +0200
1.3 @@ -323,6 +323,7 @@
1.4 fun scan vs (t as Const (s, _) $ arg) =
1.5 if is_num t then vs else scan (s :: vs) arg
1.6 | scan vs (Const (s as "Partial_Fractions.AA", _)) = s :: vs (*how get rid of spec.case?*)
1.7 + | scan vs (Const (s as "Partial_Fractions.BB", _)) = s :: vs (*how get rid of spec.case?*)
1.8 | scan vs (Const _) = vs
1.9 | scan vs (Free (s, _)) = if is_num' s then vs else s :: vs
1.10 | scan vs (Var ((s, i), _)) = (s ^ "_" ^ string_of_int i) :: vs
2.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Sun Aug 08 15:21:33 2021 +0200
2.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Mon Aug 09 11:19:25 2021 +0200
2.3 @@ -1,4 +1,4 @@
2.4 -(* Title: tests for rationals
2.5 +(* Title: "Knowledge/rational-2.sml"
2.6 Author: Walther Neuper
2.7 Use is subject to license terms.
2.8 *)
2.9 @@ -434,7 +434,7 @@
2.10 (* Rewrite.trace_on:
2.11 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + - 1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
2.12 (* |||||||||||||||||||||||||||| *)
2.13 -val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| *)
2.14 +val t = TermC.str2term (* ||||||||||||||||||||||||| *)
2.15 "AA / 4 + (BB / 2 + - 1 * BB / 2)";
2.16 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
2.17 val SOME ((n1, d1), (n2, d2)) = (*case*) check_frac_sum t (*of*);
2.18 @@ -444,11 +444,9 @@
2.19
2.20 val vs = TermC.vars_of t;
2.21 val (SOME [(1, [1, 0])], SOME [(4, [0, 0])], NONE, SOME [(1, [0, 0])]) =
2.22 - (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
2.23 -
2.24 + (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
2.25 "~~~~~ fun poly_of_term , args:"; val (vs, t) = (vs, n1);
2.26 -val SOME [(1, [xxx, 0])] = SOME [monom_of_term vs (1, replicate (length vs) 0) t];
2.27 -(*+*)if xxx = 1 then () else error "monom_of_term changed"
2.28 +val SOME [(1, [1, 0])] = SOME [monom_of_term vs (1, replicate (length vs) 0) t];
2.29
2.30 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (id, _))) =
2.31 (vs, (1, replicate (length vs) 0), t);
2.32 @@ -721,23 +719,21 @@
2.33 val (t, _, revsets, _) = ini t;
2.34
2.35 if length (hd revsets) = 11 then () else error "length of revset changed";
2.36 -(*//----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)
2.37 -if (revsets |> nth 1 |> nth 1 |> id_of_thm) =
2.38 +if (revsets |> nth 1 |> nth 1 |> Rule.id) =
2.39 (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.cut_id)
2.40 then () else error "first element of revset changed";
2.41 if
2.42 -(revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\",?r1 \<up> 2 = ?r1 * ?r1)" andalso
2.43 -(revsets |> nth 1 |> nth 2 |> Rule.to_string) = "Thm (\"#: 9 = 3 \<up> 2\",9 = 3 \<up> 2)" andalso
2.44 -(revsets |> nth 1 |> nth 3 |> Rule.to_string) = "Thm (\"#: 6 * x = 2 * (3 * x)\",6 * x = 2 * (3 * x))"
2.45 +(revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\", ?r1 \<up> 2 = ?r1 * ?r1)" andalso
2.46 +(revsets |> nth 1 |> nth 2 |> Rule.to_string) = "Thm (\"#: 9 = 3 \<up> 2\", 9 = 3 \<up> 2)" andalso
2.47 +(revsets |> nth 1 |> nth 3 |> Rule.to_string) = "Thm (\"#: 6 * x = 2 * (3 * x)\", 6 * x = 2 * (3 * x))"
2.48 andalso
2.49 -(revsets |> nth 1 |> nth 4 |> Rule.to_string) = "Thm (\"#: -3 * x = - 1 * (3 * x)\",-3 * x = - 1 * (3 * x))"
2.50 +(revsets |> nth 1 |> nth 4 |> Rule.to_string) = "Thm (\"#: - 3 * x = - 1 * (3 * x)\", - 3 * x = - 1 * (3 * x))"
2.51 andalso
2.52 -(revsets |> nth 1 |> nth 5 |> Rule.to_string) = "Thm (\"#: 9 = 3 * 3\",9 = 3 * 3)" andalso
2.53 +(revsets |> nth 1 |> nth 5 |> Rule.to_string) = "Thm (\"#: 9 = 3 * 3\", 9 = 3 * 3)" andalso
2.54 (revsets |> nth 1 |> nth 6 |> Rule.to_string) = "Rls_ (\"sym_order_mult_rls_\")" andalso
2.55 (revsets |> nth 1 |> nth 7 |> Rule.to_string) =
2.56 - "Thm (\"sym_mult.assoc\",?a * (?b * ?c) = ?a * ?b * ?c)"
2.57 + "Thm (\"sym_mult.assoc\", ?a * (?b * ?c) = ?a * ?b * ?c)"
2.58 then () else error "first 7 elements in revset changed"
2.59 - \\----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)*)
2.60
2.61 (** find the rule 'r' to apply to term 't' **)
2.62 (*/------- WN1309: since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_
2.63 @@ -865,8 +861,7 @@
2.64 "HOL.True";
2.65
2.66 val t = TermC.str2term "(6*x) \<up> 2";
2.67 -val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false
2.68 - (ThmC.numerals_to_Free @{thm realpow_def_atom}) t;
2.69 +val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false @{thm realpow_def_atom} t;
2.70 if UnparseC.term t' = "6 * x * (6 * x) \<up> (2 + - 1)" then ()
2.71 else error "rational.sml powers_erls (6*x) \<up> 2";
2.72
2.73 @@ -1419,7 +1414,7 @@
2.74 if UnparseC.term t = "- 3 * b \<up> 3 / (- 2 * a + 2 * b)"
2.75 then () else error "rational.sml: diff.behav. in norm_Rational_mg 48";
2.76
2.77 -(*//----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)
2.78 +
2.79 "-------- me Schalk I No.186 -------------------------------------------------";
2.80 "-------- me Schalk I No.186 -------------------------------------------------";
2.81 "-------- me Schalk I No.186 -------------------------------------------------";
2.82 @@ -1441,11 +1436,10 @@
2.83 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
2.84 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
2.85 case (f2str f, nxt) of
2.86 - ("14", ("End_Proof'", _)) => ()
2.87 + ("14", End_Proof') => ()
2.88 | _ => error "rational.sml diff.behav. in me Schalk I No.186";
2.89 - \\----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)*)
2.90
2.91 -(*//----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)
2.92 +
2.93 "-------- interSteps ..Simp_Rat_Double_No- 1.xml ------------------------------";
2.94 "-------- interSteps ..Simp_Rat_Double_No- 1.xml ------------------------------";
2.95 "-------- interSteps ..Simp_Rat_Double_No- 1.xml ------------------------------";
2.96 @@ -1488,15 +1482,14 @@
2.97 val (t, asm) = get_obj g_result pt [1, 2];
2.98 if UnparseC.term t = "(2 + - 1 * x) / (2 * a) / (2 * a / (x + - 1 * 2))" andalso UnparseC.terms asm = "[]"
2.99 then () else error "3rd interSteps ..Simp_Rat_Double_No- 1 changed on [1, 2]";
2.100 - \\----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)*)
2.101
2.102
2.103 -(*//----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)
2.104 +
2.105 "-------- interSteps ..Simp_Rat_Cancel_No- 1.xml ------------------------------";
2.106 "-------- interSteps ..Simp_Rat_Cancel_No- 1.xml ------------------------------";
2.107 "-------- interSteps ..Simp_Rat_Cancel_No- 1.xml ------------------------------";
2.108 reset_states ();
2.109 -CalcTree [(["Term ((a^2 + - 1*b^2) / (a^2 + - 2*a*b + b^2))", "normalform N"],
2.110 +CalcTree [(["Term ((a \<up> 2 + - 1*b \<up> 2) / (a \<up> 2 + - 2*a*b + b \<up> 2))", "normalform N"],
2.111 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
2.112 Iterator 1;
2.113 moveActiveRoot 1;
2.114 @@ -1566,7 +1559,6 @@
2.115 val (_, tac, _) = ME_Misc.pt_extract (pt, p);
2.116 case tac of SOME (Rewrite ("sym_distrib_left", _)) => ()
2.117 | _ => error "rational.sml: getTactic, sym_real_plus_binom_times1";
2.118 - \\----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)*)
2.119
2.120
2.121 "-------- investigate rulesets for cancel_p ----------------------------------";
3.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Sun Aug 08 15:21:33 2021 +0200
3.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Mon Aug 09 11:19:25 2021 +0200
3.3 @@ -166,7 +166,7 @@
3.4
3.5 val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2";
3.6 case rewrite_set_ thy false rls t of
3.7 - SOME (t', _) => (*WAS "x + 2" WITH OLD numerals TOODOO?*)
3.8 + SOME (t', _) =>
3.9 if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
3.10 | _ => error "rewrite_set_ (3+1+2*x)/2 changed 2";
3.11
3.12 @@ -204,7 +204,6 @@
3.13 Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
3.14 val t = (Thm.term_of o the o (TermC.parse thy)) "x + (- 1 + -3) / 2";
3.15 val SOME (res, []) = rewrite_set_ thy false rls t;
3.16 - (*WAS "x + - 2" WITH OLD numerals TOODOO?*)
3.17 if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_ x + (- 1 + -3) / 2 changed";
3.18 "x + (-4) / 2";
3.19 (*
3.20 @@ -468,12 +467,16 @@
3.21 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =
3.22 ((ThyC.get_theory "Isac_Knowledge"),
3.23 ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> theory -> (string * term) option), t);
3.24 +
3.25 val SOME (thmid, t) =
3.26 (*case*) get_pair thy op_ eval_fn ct (*of*);
3.27 +(*+*)val "sqrt 4 = 2" = UnparseC.term t;
3.28 +
3.29 (** )
3.30 + Skip_Proof.make_thm thy t;
3.31 +
3.32 exception TYPE raised (line 169 of "consts.ML"): Illegal type
3.33 for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)
3.34 - Skip_Proof.make_thm thy t
3.35 ( **)
3.36
3.37 "----------- fun power -------------------------------------------------------------------------";
4.1 --- a/test/Tools/isac/Test_Some.thy Sun Aug 08 15:21:33 2021 +0200
4.2 +++ b/test/Tools/isac/Test_Some.thy Mon Aug 09 11:19:25 2021 +0200
4.3 @@ -111,9 +111,498 @@
4.4 \<close> ML \<open>
4.5 \<close>
4.6
4.7 -section \<open>===================================================================================\<close>
4.8 +section \<open>========== check integrate.sml ====================================================\<close>
4.9 ML \<open>
4.10 \<close> ML \<open>
4.11 +(* Title: test/Tools/isac/Knowledge/integrate.sml
4.12 + Author: Walther Neuper 050826
4.13 + (c) due to copyright terms
4.14 +*)
4.15 +"--------------------------------------------------------";
4.16 +"table of contents --------------------------------------";
4.17 +"--------------------------------------------------------";
4.18 +"----------- parsing ------------------------------------";
4.19 +"----------- integrate by rewriting ---------------------";
4.20 +"----------- test add_new_c, TermC.is_f_x ---------------------";
4.21 +"----------- simplify by ruleset reducing make_ratpoly_in";
4.22 +"----------- integrate by ruleset -----------------------";
4.23 +"----------- rewrite 3rd integration in 7.27 ------------";
4.24 +"----------- check probem type --------------------------";
4.25 +"----------- me method [diff,integration] ---------------";
4.26 +"----------- autoCalculate [diff,integration] -----------";
4.27 +"----------- me method [diff,integration,named] ---------";
4.28 +"----------- me met [diff,integration,named] Biegelinie.Q";
4.29 +"----------- method analog to rls 'integration' ---------";
4.30 +"--------------------------------------------------------";
4.31 +"--------------------------------------------------------";
4.32 +"--------------------------------------------------------";
4.33 +
4.34 +(*these val/fun provide for exact parsing in Integrate.thy, not Isac.thy;
4.35 +they are used several times below; TODO remove duplicates*)
4.36 +val thy = @{theory "Integrate"};
4.37 +val ctxt = ThyC.to_ctxt thy;
4.38 +
4.39 +fun str2t str = parseNEW ctxt str |> the;
4.40 +fun term2s t = UnparseC.term_in_ctxt ctxt t;
4.41 +
4.42 +val conditions_in_integration_rules =
4.43 + Rule_Set.Repeat {id="conditions_in_integration_rules",
4.44 + preconds = [],
4.45 + rew_ord = ("termlessI",termlessI),
4.46 + erls = Rule_Set.Empty,
4.47 + srls = Rule_Set.Empty, calc = [], errpatts = [],
4.48 + rules = [(*for rewriting conditions in Thm's*)
4.49 + Eval ("Prog_Expr.occurs_in",
4.50 + eval_occurs_in "#occurs_in_"),
4.51 + Thm ("not_true", @{thm not_true}),
4.52 + Thm ("not_false", @{thm not_false})],
4.53 + scr = Empty_Prog};
4.54 +val subs = [(str2t "bdv::real", str2t "x::real")];
4.55 +fun rewrit thm str =
4.56 + fst (the (rewrite_inst_ thy tless_true
4.57 + conditions_in_integration_rules
4.58 + true subs thm str));
4.59 +
4.60 +
4.61 +"----------- parsing ------------------------------------";
4.62 +"----------- parsing ------------------------------------";
4.63 +"----------- parsing ------------------------------------";
4.64 +val t = TermC.str2term "Integral x D x";
4.65 +val t = TermC.str2term "Integral x \<up> 2 D x";
4.66 +case t of
4.67 + Const (\<^const_name>\<open>Integral\<close>, _) $
4.68 + (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ _) $ Free ("x", _) => ()
4.69 + | _ => error "integrate.sml: parsing: Integral x \<up> 2 D x";
4.70 +
4.71 +val t = TermC.str2term "ff x is_f_x";
4.72 +case t of Const (\<^const_name>\<open>is_f_x\<close>, _) $ _ => ()
4.73 + | _ => error "integrate.sml: parsing: ff x is_f_x";
4.74 +
4.75 +
4.76 +"----------- integrate by rewriting ---------------------";
4.77 +"----------- integrate by rewriting ---------------------";
4.78 +"----------- integrate by rewriting ---------------------";
4.79 +val str = rewrit @{thm "integral_const"} (TermC.str2term "Integral 1 D x");
4.80 +if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";
4.81 +
4.82 +val str = rewrit @{thm "integral_const"} (TermC.str2term "Integral M'/EJ D x");
4.83 +if term2s str = "M' / EJ * x" then ()
4.84 +else error "Integral M'/EJ D x BY integral_const";
4.85 +
4.86 +val str = rewrit @{thm "integral_var"} (TermC.str2term "Integral x D x");
4.87 +if term2s str = "x \<up> 2 / 2" then ()
4.88 +else error "Integral x D x BY integral_var";
4.89 +
4.90 +val str = rewrit @{thm "integral_add"} (TermC.str2term "Integral x + 1 D x");
4.91 +if term2s str = "Integral x D x + Integral 1 D x" then ()
4.92 +else error "Integral x + 1 D x BY integral_add";
4.93 +
4.94 +val str = rewrit @{thm "integral_mult"} (TermC.str2term "Integral M'/EJ * x \<up> 3 D x");
4.95 +if term2s str = "M' / EJ * Integral x \<up> 3 D x" then ()
4.96 +else error "Integral M'/EJ * x \<up> 3 D x BY integral_mult";
4.97 +
4.98 +val str = rewrit @{thm "integral_pow"} (TermC.str2term "Integral x \<up> 3 D x");
4.99 +if term2s str = "x \<up> (3 + 1) / (3 + 1)" then ()
4.100 +else error "integrate.sml Integral x \<up> 3 D x";
4.101 +
4.102 +
4.103 +"----------- test add_new_c, TermC.is_f_x ---------------------";
4.104 +"----------- test add_new_c, TermC.is_f_x ---------------------";
4.105 +"----------- test add_new_c, TermC.is_f_x ---------------------";
4.106 +val term = TermC.str2term "x \<up> 2 * c + c_2";
4.107 +val cc = new_c term;
4.108 +if UnparseC.term cc = "c_3" then () else error "integrate.sml: new_c ???";
4.109 +
4.110 +val SOME (id,t') = eval_add_new_c "" "Integrate.add_new_c" term thy;
4.111 +if UnparseC.term t' = "x \<up> 2 * c + c_2 = x \<up> 2 * c + c_2 + c_3" then ()
4.112 +else error "intergrate.sml: diff. eval_add_new_c";
4.113 +
4.114 +val cc = ("Integrate.add_new_c", eval_add_new_c "add_new_c_");
4.115 +val SOME (thmstr, thm) = adhoc_thm1_ thy cc term;
4.116 +
4.117 +val SOME (t',_) = rewrite_set_ thy true add_new_c term;
4.118 +if UnparseC.term t' = "x \<up> 2 * c + c_2 + c_3" then ()
4.119 +else error "intergrate.sml: diff. rewrite_set add_new_c 1";
4.120 +
4.121 +val term = TermC.str2term "ff x = x \<up> 2*c + c_2";
4.122 +val SOME (t',_) = rewrite_set_ thy true add_new_c term;
4.123 +if UnparseC.term t' = "ff x = x \<up> 2 * c + c_2 + c_3" then ()
4.124 +else error "intergrate.sml: diff. rewrite_set add_new_c 2";
4.125 +
4.126 +
4.127 +(*WN080222 replace call_new_c with add_new_c----------------------
4.128 +val term = str2t "new_c (c * x \<up> 2 + c_2)";
4.129 +val SOME (_,t') = eval_new_c 0 0 term 0;
4.130 +if term2s t' = "new_c c * x \<up> 2 + c_2 = c_3" then ()
4.131 +else error "integrate.sml: eval_new_c ???";
4.132 +
4.133 +val t = str2t "matches (?u + new_c ?v) (x \<up> 2 / 2)";
4.134 +val SOME (_,t') = eval_matches "" "Prog_Expr.matches" t thy; term2s t';
4.135 +if term2s t' = "matches (?u + new_c ?v) (x \<up> 2 / 2) = False" then ()
4.136 +else error "integrate.sml: matches new_c = False";
4.137 +
4.138 +val t = str2t "matches (?u + new_c ?v) (x \<up> 2 / 2 + new_c x \<up> 2 / 2)";
4.139 +val SOME (_,t') = eval_matches "" "Prog_Expr.matches" t thy; term2s t';
4.140 +if term2s t'="matches (?u + new_c ?v) (x \<up> 2 / 2 + new_c x \<up> 2 / 2) = True"
4.141 +then () else error "integrate.sml: matches new_c = True";
4.142 +
4.143 +val t = str2t "ff x TermC.is_f_x";
4.144 +val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
4.145 +if term2s t' = "(ff x TermC.is_f_x) = True" then ()
4.146 +else error "integrate.sml: eval_is_f_x --> true";
4.147 +
4.148 +val t = str2t "q_0/2 * L * x TermC.is_f_x";
4.149 +val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
4.150 +if term2s t' = "(q_0 / 2 * L * x TermC.is_f_x) = False" then ()
4.151 +else error "integrate.sml: eval_is_f_x --> false";
4.152 +
4.153 +val conditions_in_integration =
4.154 +Rule_Set.Repeat {id="conditions_in_integration",
4.155 + preconds = [],
4.156 + rew_ord = ("termlessI",termlessI),
4.157 + erls = Rule_Set.Empty,
4.158 + srls = Rule_Set.Empty, calc = [], errpatts = [],
4.159 + rules = [Eval ("Prog_Expr.matches",eval_matches ""),
4.160 + Eval ("Integrate.is_f_x",
4.161 + eval_is_f_x "is_f_x_"),
4.162 + Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
4.163 + Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
4.164 + ],
4.165 + scr = Empty_Prog};
4.166 +fun rewrit thm t =
4.167 + fst (the (rewrite_inst_ thy tless_true
4.168 + conditions_in_integration true subs thm t));
4.169 +val t = rewrit call_for_new_c (str2t "x \<up> 2 / 2"); term2s t;
4.170 +val t = (rewrit call_for_new_c t)
4.171 + handle OPTION => str2t "no_rewrite";
4.172 +
4.173 +val t = rewrit call_for_new_c
4.174 + (str2t "ff x = q_0/2 *L*x"); term2s t;
4.175 +val t = (rewrit call_for_new_c
4.176 + (str2t "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))
4.177 + handle OPTION => (*NOT: + new_c ..=..!!*)str2t "no_rewrite";
4.178 +--------------------------------------------------------------------*)
4.179 +
4.180 +
4.181 +"----------- simplify by ruleset reducing make_ratpoly_in";
4.182 +"----------- simplify by ruleset reducing make_ratpoly_in";
4.183 +"----------- simplify by ruleset reducing make_ratpoly_in";
4.184 +\<close> ML \<open>
4.185 +val subst = [(TermC.str2term "bdv ::real", TermC.str2term "x ::real")]
4.186 +\<close> ML \<open>
4.187 +val thy = @{theory "Isac_Knowledge"};
4.188 +"===== test 1";
4.189 +val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
4.190 +
4.191 +"----- stepwise from the rulesets in simplify_Integral and below-----";
4.192 +val rls = norm_Rational_noadd_fractions;
4.193 +case rewrite_set_inst_ thy true subs rls t of
4.194 + SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
4.195 + | NONE => ();
4.196 +
4.197 +"===== test 2";
4.198 +\<close> ML \<open>
4.199 +val rls = order_add_mult_in;
4.200 +\<close> text \<open> (*GOON*)
4.201 +(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\*)
4.202 + assume flawed test setup hidden by "handle _ => ..."
4.203 + ERROR ord_make_polynomial_in called with subst = []
4.204 +\<close> text \<open>
4.205 +val SOME (t, []) = rewrite_set_ thy true rls t;
4.206 +
4.207 +UnparseC.term t
4.208 +
4.209 +if UnparseC.term t = "1 / EI * (L * (q_0 * x) / 2 + - 1 * (q_0 * x \<up> 2) / 2)" then()
4.210 +else error "integrate.sml simplify by ruleset order_add_mult_in #2";
4.211 +(*\\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----//*)
4.212 +
4.213 +"===== test 3";
4.214 +\<close> ML \<open>
4.215 +val rls = discard_parentheses;
4.216 +(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\
4.217 + assume flawed test setup hidden by "handle _ => ..."
4.218 + ERROR ord_make_polynomial_in called with subst = []
4.219 +val SOME (t,[]) = rewrite_set_ thy true rls t;
4.220 +if UnparseC.term t = "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" then ()
4.221 +else error "integrate.sml simplify by ruleset discard_parenth.. #3";
4.222 + \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO//*)
4.223 +
4.224 +"===== test 4";
4.225 +val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
4.226 +val rls =
4.227 + (Rule_Set.append_rules "separate_bdv" collect_bdv
4.228 + [Thm ("separate_bdv", @{thm separate_bdv}),
4.229 + (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
4.230 + Thm ("separate_bdv_n", @{thm separate_bdv_n}),
4.231 + (*"?a * ?bdv \<up> ?n / ?b = ?a / ?b * ?bdv \<up> ?n"*)
4.232 + Thm ("separate_1_bdv", @{thm separate_1_bdv}),
4.233 + (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
4.234 + Thm ("separate_1_bdv_n", @{thm separate_1_bdv_n})
4.235 + (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
4.236 + ]);
4.237 +(*show_types := true; --- do we need type-constraint in thms? *)
4.238 +@{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
4.239 +@{thm separate_bdv_n}; (*::real ..because of \<up> , rewrites*)
4.240 +@{thm separate_1_bdv}; (*::?'a*)
4.241 +val xxx = @{thm separate_1_bdv}; (*::?'a*)
4.242 +@{thm separate_1_bdv_n}; (*::real ..because of \<up> *)
4.243 +(*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
4.244 +
4.245 +val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;
4.246 +if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2)" then ()
4.247 +else error "integrate.sml simplify by ruleset separate_bdv.. #4";
4.248 +
4.249 +"===== test 5";
4.250 +val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
4.251 +val rls = simplify_Integral;
4.252 +val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
4.253 +(* given was: "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" *)
4.254 +if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2)" then ()
4.255 +else error "integrate.sml, simplify_Integral #99";
4.256 +
4.257 +"........... 2nd integral ........................................";
4.258 +"........... 2nd integral ........................................";
4.259 +"........... 2nd integral ........................................";
4.260 +val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
4.261 +
4.262 +val thy = @{theory Biegelinie};
4.263 +val t = TermC.str2term
4.264 + "Integral 1 / EI * (L * q_0 / 2 * (x \<up> 2 / 2) + - 1 * q_0 / 2 * (x \<up> 3 / 3)) D x";
4.265 +
4.266 +val rls = simplify_Integral;
4.267 +val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
4.268 +if UnparseC.term t = "Integral 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3) D x"
4.269 +then () else raise error "integrate.sml, simplify_Integral #198";
4.270 +
4.271 +val rls = integration_rules;
4.272 +val SOME (t, []) = rewrite_set_ thy true rls t;
4.273 +if UnparseC.term t = "1 / EI * (L * q_0 / 4 * (x \<up> 3 / 3) + - 1 * q_0 / 6 * (x \<up> 4 / 4))"
4.274 +then () else error "integrate.sml, simplify_Integral #199";
4.275 +
4.276 +
4.277 +"----------- integrate by ruleset -----------------------";
4.278 +"----------- integrate by ruleset -----------------------";
4.279 +"----------- integrate by ruleset -----------------------";
4.280 +val thy = @{theory "Integrate"};
4.281 +val rls = integration_rules;
4.282 +val subs = [(@{term "bdv::real"}, @{term "x::real"})];
4.283 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
4.284 +
4.285 +val t = (Thm.term_of o the o (TermC.parse thy)) "Integral x D x";
4.286 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.287 +if UnparseC.term res = "x \<up> 2 / 2" then () else error "Integral x D x changed";
4.288 +
4.289 +val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \<up> 2 + c_2 D x";
4.290 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.291 +if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x" then () else error "Integral c * x \<up> 2 + c_2 D x";
4.292 +
4.293 +val rls = add_new_c;
4.294 +val t = (Thm.term_of o the o (TermC.parse thy)) "c * (x \<up> 3 / 3) + c_2 * x";
4.295 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.296 +if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x + c_3" then ()
4.297 +else error "integrate.sml: diff.behav. in add_new_c simpl.";
4.298 +
4.299 +val t = (Thm.term_of o the o (TermC.parse thy)) "F x = x \<up> 3 / 3 + x";
4.300 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.301 +if UnparseC.term res = "F x = x \<up> 3 / 3 + x + c"(*not "F x + c =..."*) then ()
4.302 +else error "integrate.sml: diff.behav. in add_new_c equation";
4.303 +
4.304 +val rls = simplify_Integral;
4.305 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
4.306 +val t = (Thm.term_of o the o (TermC.parse thy)) "ff x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
4.307 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.308 +if UnparseC.term res = "ff x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2"
4.309 +then () else error "integrate.sml: diff.behav. in simplify_I #1";
4.310 +
4.311 +val rls = integration;
4.312 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
4.313 +val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \<up> 2 + c_2 D x";
4.314 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.315 +if UnparseC.term res = "c_3 + c_2 * x + c / 3 * x \<up> 3"
4.316 +then () else error "integrate.sml: diff.behav. in integration #1";
4.317 +
4.318 +val t = (Thm.term_of o the o (TermC.parse thy)) "Integral 3*x \<up> 2 + 2*x + 1 D x";
4.319 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.320 +if UnparseC.term res = "c + x + x \<up> 2 + x \<up> 3" then ()
4.321 +else error "integrate.sml: diff.behav. in integration #2";
4.322 +
4.323 +val t = (Thm.term_of o the o (TermC.parse thy))
4.324 + "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x";
4.325 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.326 +"Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x";
4.327 +if UnparseC.term res = "c + 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)"
4.328 +then () else error "integrate.sml: diff.behav. in integration #3";
4.329 +
4.330 +val t = (Thm.term_of o the o (TermC.parse thy)) ("Integral " ^ UnparseC.term res ^ " D x");
4.331 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.332 +if UnparseC.term res = "c_2 + c * x +\n1 / EI * (L * q_0 / 12 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)"
4.333 +then () else error "integrate.sml: diff.behav. in integration #4";
4.334 +
4.335 +"----------- rewrite 3rd integration in 7.27 ------------";
4.336 +"----------- rewrite 3rd integration in 7.27 ------------";
4.337 +"----------- rewrite 3rd integration in 7.27 ------------";
4.338 +val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
4.339 +val t = TermC.str2term "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \<up> 2) / 2) D x";
4.340 +val SOME(t, _)= rewrite_set_inst_ thy true subs simplify_Integral t;
4.341 +if UnparseC.term t =
4.342 + "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x"
4.343 +then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral";
4.344 +
4.345 +val SOME(t, _) = rewrite_set_inst_ thy true subs integration t;
4.346 +if UnparseC.term t =
4.347 + "c + 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)"
4.348 +then () else error "integrate.sml 3rd integration in 7.27, integration";
4.349 +
4.350 +
4.351 +"----------- check probem type --------------------------";
4.352 +"----------- check probem type --------------------------";
4.353 +"----------- check probem type --------------------------";
4.354 +val thy = @{theory Integrate};
4.355 +val model = {Given =["functionTerm f_f", "integrateBy v_v"],
4.356 + Where =[],
4.357 + Find =["antiDerivative F_F"],
4.358 + With =[],
4.359 + Relate=[]}:string ppc;
4.360 +val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model;
4.361 +val t1 = (Thm.term_of o hd) chkmodel;
4.362 +val t2 = (Thm.term_of o hd o tl) chkmodel;
4.363 +val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
4.364 +case t3 of Const (\<^const_name>\<open>antiDerivative\<close>, _) $ _ => ()
4.365 + | _ => error "integrate.sml: Integrate.antiDerivative ???";
4.366 +
4.367 +val model = {Given =["functionTerm f_f", "integrateBy v_v"],
4.368 + Where =[],
4.369 + Find =["antiDerivativeName F_F"],
4.370 + With =[],
4.371 + Relate=[]}:string ppc;
4.372 +val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model;
4.373 +val t1 = (Thm.term_of o hd) chkmodel;
4.374 +val t2 = (Thm.term_of o hd o tl) chkmodel;
4.375 +val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
4.376 +case t3 of Const (\<^const_name>\<open>antiDerivativeName\<close>, _) $ _ => ()
4.377 + | _ => error "integrate.sml: Integrate.antiDerivativeName";
4.378 +
4.379 +"----- compare 'Find's from problem, script, formalization -------";
4.380 +val {ppc,...} = Problem.from_store ["named", "integrate", "function"];
4.381 +val ("#Find", (Const (\<^const_name>\<open>antiDerivativeName\<close>, _),
4.382 + F1_ as Free ("F_F", F1_type))) = last_elem ppc;
4.383 +val {scr = Prog sc,... } = MethodC.from_store ["diff", "integration", "named"];
4.384 +val [_,_, F2_] = formal_args sc;
4.385 +if F1_ = F2_ then () else error "integrate.sml: unequal find's";
4.386 +
4.387 +val ((dsc as Const (\<^const_name>\<open>antiDerivativeName\<close>, _))
4.388 + $ Free ("ff", F3_type)) = TermC.str2term "antiDerivativeName ff";
4.389 +if Input_Descript.is_a dsc then () else error "integrate.sml: no description";
4.390 +if F1_type = F3_type then ()
4.391 +else error "integrate.sml: unequal types in find's";
4.392 +
4.393 +Test_Tool.show_ptyps();
4.394 +val pbl = Problem.from_store ["integrate", "function"];
4.395 +case #cas pbl of SOME (Const (\<^const_name>\<open>Integrate\<close>, _) $ _) => ()
4.396 + | _ => error "integrate.sml: Integrate.Integrate ???";
4.397 +
4.398 +
4.399 +"----------- me method [diff,integration] ---------------";
4.400 +"----------- me method [diff,integration] ---------------";
4.401 +"----------- me method [diff,integration] ---------------";
4.402 +(*exp_CalcInt_No- 1.xml*)
4.403 +val p = e_pos'; val c = [];
4.404 +"----- step 0: returns nxt = Model_Problem ---";
4.405 +val (p,_,f,nxt,_,pt) =
4.406 + CalcTreeTEST
4.407 + [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
4.408 + ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
4.409 +"----- step 1: returns nxt = Add_Given \"functionTerm (x \<up> 2 + 1)\" ---";
4.410 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
4.411 +"----- step 2: returns nxt = Add_Given \"integrateBy x\" ---";
4.412 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.413 +"----- step 3: returns nxt = Add_Find \"Integrate.antiDerivative FF\" ---";
4.414 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.415 +"----- step 4: returns nxt = Specify_Theory \"Integrate\" ---";
4.416 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.417 +"----- step 5: returns nxt = Specify_Problem [\"integrate\", \"function\"] ---";
4.418 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.419 +"----- step 6: returns nxt = Specify_Method [\"diff\", \"integration\"] ---";
4.420 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.421 +"----- step 7: returns nxt = Apply_Method [\"diff\", \"integration\"] ---";
4.422 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.423 +case nxt of (Apply_Method ["diff", "integration"]) => ()
4.424 + | _ => error "integrate.sml -- me method [diff,integration] -- spec";
4.425 +"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
4.426 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.427 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.428 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.429 +if f2str f = "c + x + 1 / 3 * x \<up> 3" then ()
4.430 +else error "integrate.sml -- me method [diff,integration] -- end";
4.431 +
4.432 +
4.433 +"----------- autoCalculate [diff,integration] -----------";
4.434 +"----------- autoCalculate [diff,integration] -----------";
4.435 +"----------- autoCalculate [diff,integration] -----------";
4.436 +reset_states ();
4.437 +CalcTree
4.438 + [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
4.439 + ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
4.440 +Iterator 1;
4.441 +moveActiveRoot 1;
4.442 +autoCalculate 1 CompleteCalc;
4.443 +val ((pt,p),_) = get_calc 1; @{make_string} p; Test_Tool.show_pt pt;
4.444 +val (Form t,_,_) = ME_Misc.pt_extract (pt, p);
4.445 +if UnparseC.term t = "c + x + 1 / 3 * x \<up> 3" then ()
4.446 +else error "integrate.sml -- interSteps [diff,integration] -- result";
4.447 +
4.448 +
4.449 +"----------- me method [diff,integration,named] ---------";
4.450 +"----------- me method [diff,integration,named] ---------";
4.451 +"----------- me method [diff,integration,named] ---------";
4.452 +(*exp_CalcInt_No- 2.xml*)
4.453 +val fmz = ["functionTerm (x \<up> 2 + (1::real))",
4.454 + "integrateBy x", "antiDerivativeName F"];
4.455 +val (dI',pI',mI') =
4.456 + ("Integrate",["named", "integrate", "function"],
4.457 + ["diff", "integration", "named"]);
4.458 +val p = e_pos'; val c = [];
4.459 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.460 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.461 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.462 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
4.463 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.464 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.465 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.466 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
4.467 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.468 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.469 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.470 +if f2str f = "F x = c + x + 1 / 3 * x \<up> 3" then()
4.471 +else error "integrate.sml: method [diff,integration,named]";
4.472 +
4.473 +
4.474 +"----------- me met [diff,integration,named] Biegelinie.Q";
4.475 +"----------- me met [diff,integration,named] Biegelinie.Q";
4.476 +"----------- me met [diff,integration,named] Biegelinie.Q";
4.477 +(*exp_CalcInt_No-3.xml*)
4.478 +val fmz = ["functionTerm (- q_0)",
4.479 + "integrateBy x", "antiDerivativeName Q"];
4.480 +val (dI',pI',mI') =
4.481 + ("Biegelinie",["named", "integrate", "function"],
4.482 + ["diff", "integration", "named"]);
4.483 +val p = e_pos'; val c = [];
4.484 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.485 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.486 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.487 +(*Error Tac Q not in ...*)
4.488 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
4.489 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.490 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.491 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.492 +val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
4.493 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.494 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.495 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.496 +if f2str f = "Q x = c + - 1 * q_0 * x" then()
4.497 +else error "integrate.sml: method [diff,integration,named] .Q";
4.498 +
4.499 +
4.500 \<close> ML \<open>
4.501 \<close> ML \<open>
4.502 \<close>