1.1 --- a/TODO.md Mon Aug 09 11:19:25 2021 +0200
1.2 +++ b/TODO.md Mon Aug 09 14:20:20 2021 +0200
1.3 @@ -63,10 +63,10 @@
1.4 - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun');
1.5 - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
1.6
1.7 -* WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation, DONE partially;
1.8 - + TOODOO are exclusive for this changeset; most follow from TOODOO.1
1.9 - + TOODOO.1: exception TYPE raised by Skip_Proof.make_thm
1.10 - + ? how to do algebraic operations on numerals ? Presburger ? simplifier ?
1.11 +* WN: eliminate ThmC.numerals_to_Free, done except 1 error:
1.12 + + exception TYPE raised by Skip_Proof.make_thm, several inherited errors in tests marked TOODOO.1
1.13 + + ? how do algebraic operations on numerals ? Presburger ? simplifier ? hack see
1.14 + https://hg.risc.uni-linz.ac.at/wneuper/isa/file/a14022b99b92/src/Tools/isac/ProgLang/evaluate.sml#l210
1.15
1.16 * WN: DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art), partially;
1.17 Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too)
2.1 --- a/test/Tools/isac/Knowledge/integrate.sml Mon Aug 09 11:19:25 2021 +0200
2.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Mon Aug 09 14:20:20 2021 +0200
2.3 @@ -172,6 +172,7 @@
2.4 "----------- simplify by ruleset reducing make_ratpoly_in";
2.5 "----------- simplify by ruleset reducing make_ratpoly_in";
2.6 val thy = @{theory "Isac_Knowledge"};
2.7 +val subst = [(TermC.str2term "bdv ::real", TermC.str2term "x ::real")]; (*DOESN'T HELP*)
2.8 "===== test 1";
2.9 val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
2.10
2.11 @@ -183,23 +184,15 @@
2.12
2.13 "===== test 2";
2.14 val rls = order_add_mult_in;
2.15 -(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\
2.16 - assume flawed test setup hidden by "handle _ => ..."
2.17 - ERROR ord_make_polynomial_in called with subst = []
2.18 -val SOME (t,[]) = rewrite_set_ thy true rls t;
2.19 +val SOME (t, []) = rewrite_set_inst_ thy true subst rls t;
2.20 if UnparseC.term t = "1 / EI * (L * (q_0 * x) / 2 + - 1 * (q_0 * x \<up> 2) / 2)" then()
2.21 else error "integrate.sml simplify by ruleset order_add_mult_in #2";
2.22 - \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----//*)
2.23
2.24 "===== test 3";
2.25 val rls = discard_parentheses;
2.26 -(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\
2.27 - assume flawed test setup hidden by "handle _ => ..."
2.28 - ERROR ord_make_polynomial_in called with subst = []
2.29 -val SOME (t,[]) = rewrite_set_ thy true rls t;
2.30 +val SOME (t, []) = rewrite_set_ thy true rls t;
2.31 if UnparseC.term t = "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" then ()
2.32 else error "integrate.sml simplify by ruleset discard_parenth.. #3";
2.33 - \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO//*)
2.34
2.35 "===== test 4";
2.36 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
3.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Mon Aug 09 11:19:25 2021 +0200
3.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Mon Aug 09 14:20:20 2021 +0200
3.3 @@ -22,6 +22,7 @@
3.4 "----------- calculate (2 * x is_const) -----------------";
3.5 "----------- fun get_pair: examples ------------------------------------------------------------";
3.6 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
3.7 +"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
3.8 "----------- fun power -------------------------------------------------------------------------";
3.9 "----------- fun divisors ----------------------------------------------------------------------";
3.10 "----------- fun doubles, fun squfact ----------------------------------------------------------";
3.11 @@ -459,8 +460,8 @@
3.12 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
3.13 val t = TermC.str2term "sqrt 4";
3.14
3.15 -(* TOODOO.1: exception TYPE raised by Skip_Proof.make_thm * )
3.16 - exception TYPE raised (line 169 of "consts.ML"): Illegal type
3.17 +(* error-from-Skip_Proof.make_thm: inherited errors are marked TOODOO.1 in test/*
3.18 + exception TYPE raised (line 169 of "consts.ML"): Illegal type
3.19 for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)
3.20 Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t
3.21 ( **)
4.1 --- a/test/Tools/isac/Test_Some.thy Mon Aug 09 11:19:25 2021 +0200
4.2 +++ b/test/Tools/isac/Test_Some.thy Mon Aug 09 14:20:20 2021 +0200
4.3 @@ -111,498 +111,9 @@
4.4 \<close> ML \<open>
4.5 \<close>
4.6
4.7 -section \<open>========== check integrate.sml ====================================================\<close>
4.8 +section \<open>===================================================================================\<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>