1.1 --- a/test/Tools/isac/Knowledge/integrate.sml Tue Jul 27 12:32:43 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Sun Aug 01 14:39:03 2021 +0200
1.3 @@ -38,8 +38,8 @@
1.4 rules = [(*for rewriting conditions in Thm's*)
1.5 Eval ("Prog_Expr.occurs_in",
1.6 eval_occurs_in "#occurs_in_"),
1.7 - Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
1.8 - Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})],
1.9 + Thm ("not_true", @{thm not_true}),
1.10 + Thm ("not_false", @{thm not_false})],
1.11 scr = Empty_Prog};
1.12 val subs = [(str2t "bdv::real", str2t "x::real")];
1.13 fun rewrit thm str =
1.14 @@ -51,14 +51,14 @@
1.15 "----------- parsing ------------------------------------";
1.16 "----------- parsing ------------------------------------";
1.17 "----------- parsing ------------------------------------";
1.18 -val t = str2t "Integral x D x";
1.19 -val t = str2t "Integral x \<up> 2 D x";
1.20 +val t = TermC.str2term "Integral x D x";
1.21 +val t = TermC.str2term "Integral x \<up> 2 D x";
1.22 case t of
1.23 Const (\<^const_name>\<open>Integral\<close>, _) $
1.24 - (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ Free _) $ Free ("x", _) => ()
1.25 + (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ _) $ Free ("x", _) => ()
1.26 | _ => error "integrate.sml: parsing: Integral x \<up> 2 D x";
1.27
1.28 -val t = str2t "ff x is_f_x";
1.29 +val t = TermC.str2term "ff x is_f_x";
1.30 case t of Const (\<^const_name>\<open>is_f_x\<close>, _) $ _ => ()
1.31 | _ => error "integrate.sml: parsing: ff x is_f_x";
1.32
1.33 @@ -66,26 +66,26 @@
1.34 "----------- integrate by rewriting ---------------------";
1.35 "----------- integrate by rewriting ---------------------";
1.36 "----------- integrate by rewriting ---------------------";
1.37 -val str = rewrit @{thm "integral_const"} (str2t "Integral 1 D x");
1.38 +val str = rewrit @{thm "integral_const"} (TermC.str2term "Integral 1 D x");
1.39 if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";
1.40
1.41 -val str = rewrit @{thm "integral_const"} (str2t "Integral M'/EJ D x");
1.42 +val str = rewrit @{thm "integral_const"} (TermC.str2term "Integral M'/EJ D x");
1.43 if term2s str = "M' / EJ * x" then ()
1.44 else error "Integral M'/EJ D x BY integral_const";
1.45
1.46 -val str = rewrit @{thm "integral_var"} (str2t "Integral x D x");
1.47 +val str = rewrit @{thm "integral_var"} (TermC.str2term "Integral x D x");
1.48 if term2s str = "x \<up> 2 / 2" then ()
1.49 else error "Integral x D x BY integral_var";
1.50
1.51 -val str = rewrit @{thm "integral_add"} (str2t "Integral x + 1 D x");
1.52 +val str = rewrit @{thm "integral_add"} (TermC.str2term "Integral x + 1 D x");
1.53 if term2s str = "Integral x D x + Integral 1 D x" then ()
1.54 else error "Integral x + 1 D x BY integral_add";
1.55
1.56 -val str = rewrit @{thm "integral_mult"} (str2t "Integral M'/EJ * x \<up> 3 D x");
1.57 +val str = rewrit @{thm "integral_mult"} (TermC.str2term "Integral M'/EJ * x \<up> 3 D x");
1.58 if term2s str = "M' / EJ * Integral x \<up> 3 D x" then ()
1.59 else error "Integral M'/EJ * x \<up> 3 D x BY integral_mult";
1.60
1.61 -val str = rewrit @{thm "integral_pow"} (str2t "Integral x \<up> 3 D x");
1.62 +val str = rewrit @{thm "integral_pow"} (TermC.str2term "Integral x \<up> 3 D x");
1.63 if term2s str = "x \<up> (3 + 1) / (3 + 1)" then ()
1.64 else error "integrate.sml Integral x \<up> 3 D x";
1.65
1.66 @@ -93,7 +93,7 @@
1.67 "----------- test add_new_c, TermC.is_f_x ---------------------";
1.68 "----------- test add_new_c, TermC.is_f_x ---------------------";
1.69 "----------- test add_new_c, TermC.is_f_x ---------------------";
1.70 -val term = str2t "x \<up> 2 * c + c_2";
1.71 +val term = TermC.str2term "x \<up> 2 * c + c_2";
1.72 val cc = new_c term;
1.73 if UnparseC.term cc = "c_3" then () else error "integrate.sml: new_c ???";
1.74
1.75 @@ -108,7 +108,7 @@
1.76 if UnparseC.term t' = "x \<up> 2 * c + c_2 + c_3" then ()
1.77 else error "intergrate.sml: diff. rewrite_set add_new_c 1";
1.78
1.79 -val term = str2t "ff x = x \<up> 2*c + c_2";
1.80 +val term = TermC.str2term "ff x = x \<up> 2*c + c_2";
1.81 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
1.82 if UnparseC.term t' = "ff x = x \<up> 2 * c + c_2 + c_3" then ()
1.83 else error "intergrate.sml: diff. rewrite_set add_new_c 2";
1.84 @@ -183,7 +183,7 @@
1.85
1.86 "===== test 2";
1.87 val rls = order_add_mult_in;
1.88 -(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
1.89 +(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\
1.90 assume flawed test setup hidden by "handle _ => ..."
1.91 ERROR ord_make_polynomial_in called with subst = []
1.92 val SOME (t,[]) = rewrite_set_ thy true rls t;
1.93 @@ -193,32 +193,32 @@
1.94
1.95 "===== test 3";
1.96 val rls = discard_parentheses;
1.97 -(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
1.98 +(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\
1.99 assume flawed test setup hidden by "handle _ => ..."
1.100 ERROR ord_make_polynomial_in called with subst = []
1.101 val SOME (t,[]) = rewrite_set_ thy true rls t;
1.102 if UnparseC.term t = "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" then ()
1.103 else error "integrate.sml simplify by ruleset discard_parenth.. #3";
1.104 - \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----//*)
1.105 + \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO//*)
1.106
1.107 "===== test 4";
1.108 -val subs = [(str2t "bdv::real", str2t "x::real")];
1.109 +val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
1.110 val rls =
1.111 (Rule_Set.append_rules "separate_bdv" collect_bdv
1.112 - [Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
1.113 + [Thm ("separate_bdv", @{thm separate_bdv}),
1.114 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.115 - Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
1.116 + Thm ("separate_bdv_n", @{thm separate_bdv_n}),
1.117 (*"?a * ?bdv \<up> ?n / ?b = ?a / ?b * ?bdv \<up> ?n"*)
1.118 - Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
1.119 + Thm ("separate_1_bdv", @{thm separate_1_bdv}),
1.120 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.121 - Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})
1.122 + Thm ("separate_1_bdv_n", @{thm separate_1_bdv_n})
1.123 (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
1.124 ]);
1.125 (*show_types := true; --- do we need type-constraint in thms? *)
1.126 @{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
1.127 @{thm separate_bdv_n}; (*::real ..because of \<up> , rewrites*)
1.128 @{thm separate_1_bdv}; (*::?'a*)
1.129 -val xxx = ThmC.numerals_to_Free @{thm separate_1_bdv}; (*::?'a*)
1.130 +val xxx = @{thm separate_1_bdv}; (*::?'a*)
1.131 @{thm separate_1_bdv_n}; (*::real ..because of \<up> *)
1.132 (*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
1.133
1.134 @@ -227,7 +227,7 @@
1.135 else error "integrate.sml simplify by ruleset separate_bdv.. #4";
1.136
1.137 "===== test 5";
1.138 -val t = str2t "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
1.139 +val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
1.140 val rls = simplify_Integral;
1.141 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
1.142 (* given was: "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" *)
1.143 @@ -237,19 +237,20 @@
1.144 "........... 2nd integral ........................................";
1.145 "........... 2nd integral ........................................";
1.146 "........... 2nd integral ........................................";
1.147 -val t = str2t
1.148 -"Integral 1 / EI * (L * q_0 / 2 * (x \<up> 2 / 2) + - 1 * q_0 / 2 * (x \<up> 3 / 3)) D x";
1.149 +val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
1.150 +
1.151 +val thy = @{theory Biegelinie};
1.152 +val t = TermC.str2term
1.153 + "Integral 1 / EI * (L * q_0 / 2 * (x \<up> 2 / 2) + - 1 * q_0 / 2 * (x \<up> 3 / 3)) D x";
1.154 +
1.155 val rls = simplify_Integral;
1.156 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
1.157 -if UnparseC.term t =
1.158 - "Integral 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3) D x"
1.159 +if UnparseC.term t = "Integral 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3) D x"
1.160 then () else raise error "integrate.sml, simplify_Integral #198";
1.161
1.162 val rls = integration_rules;
1.163 -val SOME (t,[]) = rewrite_set_ thy true rls t;
1.164 -UnparseC.term t;
1.165 -if UnparseC.term t =
1.166 - "1 / EI * (L * q_0 / 4 * (x \<up> 3 / 3) + - 1 * q_0 / 6 * (x \<up> 4 / 4))"
1.167 +val SOME (t, []) = rewrite_set_ thy true rls t;
1.168 +if UnparseC.term t = "1 / EI * (L * q_0 / 4 * (x \<up> 3 / 3) + - 1 * q_0 / 6 * (x \<up> 4 / 4))"
1.169 then () else error "integrate.sml, simplify_Integral #199";
1.170
1.171
1.172 @@ -315,14 +316,13 @@
1.173 "----------- rewrite 3rd integration in 7.27 ------------";
1.174 "----------- rewrite 3rd integration in 7.27 ------------";
1.175 val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
1.176 -val t = str2t "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \<up> 2) / 2) D x";
1.177 -val SOME(t,_)= rewrite_set_inst_ thy true subs simplify_Integral t;
1.178 +val t = TermC.str2term "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \<up> 2) / 2) D x";
1.179 +val SOME(t, _)= rewrite_set_inst_ thy true subs simplify_Integral t;
1.180 if UnparseC.term t =
1.181 "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x"
1.182 then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral";
1.183
1.184 -val SOME(t,_)= rewrite_set_inst_ thy true subs integration t;
1.185 -UnparseC.term t;
1.186 +val SOME(t, _) = rewrite_set_inst_ thy true subs integration t;
1.187 if UnparseC.term t =
1.188 "c + 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)"
1.189 then () else error "integrate.sml 3rd integration in 7.27, integration";
1.190 @@ -331,6 +331,7 @@
1.191 "----------- check probem type --------------------------";
1.192 "----------- check probem type --------------------------";
1.193 "----------- check probem type --------------------------";
1.194 +val thy = @{theory Integrate};
1.195 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
1.196 Where =[],
1.197 Find =["antiDerivative F_F"],
1.198 @@ -364,14 +365,14 @@
1.199 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
1.200
1.201 val ((dsc as Const (\<^const_name>\<open>antiDerivativeName\<close>, _))
1.202 - $ Free ("ff", F3_type)) = str2t "antiDerivativeName ff";
1.203 + $ Free ("ff", F3_type)) = TermC.str2term "antiDerivativeName ff";
1.204 if Input_Descript.is_a dsc then () else error "integrate.sml: no description";
1.205 if F1_type = F3_type then ()
1.206 else error "integrate.sml: unequal types in find's";
1.207
1.208 Test_Tool.show_ptyps();
1.209 val pbl = Problem.from_store ["integrate", "function"];
1.210 -case #cas pbl of SOME (Const (\<^const_name>\<open>Integrate\<close>,_) $ _) => ()
1.211 +case #cas pbl of SOME (Const (\<^const_name>\<open>Integrate\<close>, _) $ _) => ()
1.212 | _ => error "integrate.sml: Integrate.Integrate ???";
1.213
1.214
1.215 @@ -472,8 +473,7 @@
1.216 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.217 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.218 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.219 -
1.220 -if f2str f = "Q x = c + - 1 * q_0 * x" then()
1.221 +if f2str f = "Q x = c + - q_0 * x" then()
1.222 else error "integrate.sml: method [diff,integration,named] .Q";
1.223
1.224