Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/IsacKnowledge/integrate.sml
branchisac-update-Isa09-2
changeset 37926 e6fc98fbcb85
parent 37924 6c53fe2519e5
child 37934 56f10b13005e
equal deleted inserted replaced
37925:d957275620d4 37926:e6fc98fbcb85 
    92 "----------- test add_new_c, is_f_x ------------------------------";
 
    92 "----------- test add_new_c, is_f_x ------------------------------";
 
    93 val term = str2term "x^^^2*c + c_2";
 
    93 val term = str2term "x^^^2*c + c_2";
 
    94 val cc = new_c term;
 
    94 val cc = new_c term;
 
    95 if term2str cc = "c_3" then () else raise error "integrate.sml: new_c ???";
 
    95 if term2str cc = "c_3" then () else raise error "integrate.sml: new_c ???";
 
    96 
    96 
    97 val Some (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
 
    97 val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
 
    98 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()
 
    98 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()
 
    99 else raise error "intergrate.sml: diff. eval_add_new_c";
 
    99 else raise error "intergrate.sml: diff. eval_add_new_c";
 
   100 
   100 
   101 val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");
 
   101 val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");
 
   102 val Some (thmstr, thm) = get_calculation1_ thy cc term;
 
   102 val SOME (thmstr, thm) = get_calculation1_ thy cc term;
 
   103 
   103 
   104 val Some (t',_) = rewrite_set_ thy true add_new_c term;
 
   104 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
 
   105 if term2str t' = "x ^^^ 2 * c + c_2 + c_3" then ()
 
   105 if term2str t' = "x ^^^ 2 * c + c_2 + c_3" then ()
 
   106 else raise error "intergrate.sml: diff. rewrite_set add_new_c 1";
 
   106 else raise error "intergrate.sml: diff. rewrite_set add_new_c 1";
 
   107 
   107 
   108 val term = str2term "ff x = x^^^2*c + c_2";
 
   108 val term = str2term "ff x = x^^^2*c + c_2";
 
   109 val Some (t',_) = rewrite_set_ thy true add_new_c term;
 
   109 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
 
   110 if term2str t' = "ff x = x ^^^ 2 * c + c_2 + c_3" then ()
 
   110 if term2str t' = "ff x = x ^^^ 2 * c + c_2 + c_3" then ()
 
   111 else raise error "intergrate.sml: diff. rewrite_set add_new_c 2";
 
   111 else raise error "intergrate.sml: diff. rewrite_set add_new_c 2";
 
   112 
   112 
   113 
   113 
   114 (*WN080222 replace call_new_c with add_new_c----------------------
 
   114 (*WN080222 replace call_new_c with add_new_c----------------------
 
   115 val term = str2term "new_c (c * x^^^2 + c_2)";
 
   115 val term = str2term "new_c (c * x^^^2 + c_2)";
 
   116 val Some (_,t') = eval_new_c 0 0 term 0;
 
   116 val SOME (_,t') = eval_new_c 0 0 term 0;
 
   117 if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()
 
   117 if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()
 
   118 else raise error "integrate.sml: eval_new_c ???";
 
   118 else raise error "integrate.sml: eval_new_c ???";
 
   119 
   119 
   120 val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2)";
 
   120 val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2)";
 
   121 val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
 
   121 val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
 
   122 if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()
 
   122 if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()
 
   123 else raise error "integrate.sml: matches new_c = False";
 
   123 else raise error "integrate.sml: matches new_c = False";
 
   124 
   124 
   125 val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
 
   125 val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
 
   126 val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
 
   126 val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
 
   127 if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
 
   127 if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
 
   128 then () else raise error "integrate.sml: matches new_c = True";
 
   128 then () else raise error "integrate.sml: matches new_c = True";
 
   129 
   129 
   130 val t = str2term "ff x is_f_x";
 
   130 val t = str2term "ff x is_f_x";
 
   131 val Some (_,t') = eval_is_f_x "" "" t thy; term2s t';
 
   131 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
 
   132 if term2s t' = "(ff x is_f_x) = True" then ()
 
   132 if term2s t' = "(ff x is_f_x) = True" then ()
 
   133 else raise error "integrate.sml: eval_is_f_x --> true";
 
   133 else raise error "integrate.sml: eval_is_f_x --> true";
 
   134 
   134 
   135 val t = str2term "q_0/2 * L * x is_f_x";
 
   135 val t = str2term "q_0/2 * L * x is_f_x";
 
   136 val Some (_,t') = eval_is_f_x "" "" t thy; term2s t';
 
   136 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
 
   137 if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then ()
 
   137 if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then ()
 
   138 else raise error "integrate.sml: eval_is_f_x --> false";
 
   138 else raise error "integrate.sml: eval_is_f_x --> false";
 
   139 
   139 
   140 val conditions_in_integration =
 
   140 val conditions_in_integration =
 
   141 Rls {id="conditions_in_integration", 
   141 Rls {id="conditions_in_integration", 
   173 val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
 
   173 val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
 
   174 
   174 
   175 "----- stepwise from the rulesets in simplify_Integral and below-----";
 
   175 "----- stepwise from the rulesets in simplify_Integral and below-----";
 
   176 (*###*)val rls = norm_Rational_noadd_fractions;
 
   176 (*###*)val rls = norm_Rational_noadd_fractions;
 
   177 case rewrite_set_inst_ thy true subs rls t of
 
   177 case rewrite_set_inst_ thy true subs rls t of
 
   178     Some _ => raise error "integrate.sml simplify by ruleset norm_Rational_.#2"
 
   178     SOME _ => raise error "integrate.sml simplify by ruleset norm_Rational_.#2"
 
   179   | None => ();
 
   179   | NONE => ();
 
   180 (* WN051028 Rational.ML 'rat_mult_div_pow' with erls = e_rls
 
   180 (* WN051028 Rational.ML 'rat_mult_div_pow' with erls = e_rls
 
   181 applies 'rat_mult_poly_r'="?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"
 
   181 applies 'rat_mult_poly_r'="?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"
 
   182 to "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI"
 
   182 to "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI"
 
   183 and keeps "..." is_polyexp" as an assumption.
 
   183 and keeps "..." is_polyexp" as an assumption.
 
   184 AFTER CORRECTION in Integrate.ML as above*)
 
   184 AFTER CORRECTION in Integrate.ML as above*)
 
   185 
   185 
   186 (*###*)val rls = order_add_mult_in;
 
   186 (*###*)val rls = order_add_mult_in;
 
   187 val Some (t,[]) = rewrite_set_ thy true rls t;
 
   187 val SOME (t,[]) = rewrite_set_ thy true rls t;
 
   188 if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)"then()
 
   188 if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)"then()
 
   189 else raise error "integrate.sml simplify by ruleset order_add_mult_in #2";
 
   189 else raise error "integrate.sml simplify by ruleset order_add_mult_in #2";
 
   190 
   190 
   191 (*###*)val rls = discard_parentheses;
 
   191 (*###*)val rls = discard_parentheses;
 
   192 val Some (t,[]) = rewrite_set_ thy true rls t;
 
   192 val SOME (t,[]) = rewrite_set_ thy true rls t;
 
   193 if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
 
   193 if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
 
   194 else raise error "integrate.sml simplify by ruleset discard_parenth.. #3";
 
   194 else raise error "integrate.sml simplify by ruleset discard_parenth.. #3";
 
   195 
   195 
   196 (*###*)val rls = 
   196 (*###*)val rls = 
   197 	   (append_rls "separate_bdv"
 
   197 	   (append_rls "separate_bdv"
 
   201 			Thm ("separate_bdv_n", num_str separate_bdv_n),
 
   201 			Thm ("separate_bdv_n", num_str separate_bdv_n),
 
   202 			Thm ("separate_1_bdv", num_str separate_1_bdv),
 
   202 			Thm ("separate_1_bdv", num_str separate_1_bdv),
 
   203 			(*"?bdv / ?b = (1 / ?b) * ?bdv"*)
 
   203 			(*"?bdv / ?b = (1 / ?b) * ?bdv"*)
 
   204 			Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)
 
   204 			Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)
 
   205 			]);
 
   205 			]);
 
   206 val Some (t,[]) = rewrite_set_inst_ thy true subs rls t;
 
   206 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
 
   207 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
 
   207 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
 
   208 else raise error "integrate.sml simplify by ruleset separate_bdv.. #4";
 
   208 else raise error "integrate.sml simplify by ruleset separate_bdv.. #4";
 
   209 
   209 
   210 
   210 
   211 val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
 
   211 val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
 
   212 val rls = simplify_Integral;
 
   212 val rls = simplify_Integral;
 
   213 val Some (t,[]) = rewrite_set_inst_ thy true subs rls t;
 
   213 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
 
   214 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
 
   214 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
 
   215 else raise error "integrate.sml, simplify_Integral #99";
 
   215 else raise error "integrate.sml, simplify_Integral #99";
 
   216 
   216 
   217 "........... 2nd integral ........................................";
 
   217 "........... 2nd integral ........................................";
 
   218 "........... 2nd integral ........................................";
 
   218 "........... 2nd integral ........................................";
 
   219 "........... 2nd integral ........................................";
 
   219 "........... 2nd integral ........................................";
 
   220 val t = str2term 
   220 val t = str2term 
   221 	    "Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + \
 
   221 	    "Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + \
 
   222 	    \-1 * q_0 / 2 * (x ^^^ 3 / 3)) D x";
 
   222 	    \-1 * q_0 / 2 * (x ^^^ 3 / 3)) D x";
 
   223 val rls = simplify_Integral;
 
   223 val rls = simplify_Integral;
 
   224 val Some (t,[]) = rewrite_set_inst_ thy true subs rls t;
 
   224 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
 
   225 if term2str t = 
   225 if term2str t = 
   226    "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"
 
   226    "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"
 
   227 then () else raise error "integrate.sml, simplify_Integral #198";
 
   227 then () else raise error "integrate.sml, simplify_Integral #198";
 
   228 
   228 
   229 val rls = integration_rules;
 
   229 val rls = integration_rules;
 
   230 val Some (t,[]) = rewrite_set_ thy true rls t;
 
   230 val SOME (t,[]) = rewrite_set_ thy true rls t;
 
   231 if term2str t = 
   231 if term2str t = 
   232    "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"
 
   232    "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"
 
   233 then () else raise error "integrate.sml, simplify_Integral #199";
 
   233 then () else raise error "integrate.sml, simplify_Integral #199";
 
   234 
   234 
   235 
   235 
   299 "----------- rewrite 3rd integration in 7.27 ---------------------";
 
   299 "----------- rewrite 3rd integration in 7.27 ---------------------";
 
   300 val thy = Isac.thy (*because of Undeclared constant "Biegelinie.EI*);
 
   300 val thy = Isac.thy (*because of Undeclared constant "Biegelinie.EI*);
 
   301 val bdv = [(str2term"bdv", str2term"x")];
 
   301 val bdv = [(str2term"bdv", str2term"x")];
 
   302 val t = str2term
 
   302 val t = str2term
 
   303 	    "Integral 1 / EI * ((L * q_0 * x + -1 * q_0 * x ^^^ 2) / 2) D x";
 
   303 	    "Integral 1 / EI * ((L * q_0 * x + -1 * q_0 * x ^^^ 2) / 2) D x";
 
   304 val Some(t,_)= rewrite_set_inst_ thy true bdv simplify_Integral t;
 
   304 val SOME(t,_)= rewrite_set_inst_ thy true bdv simplify_Integral t;
 
   305 if term2str t = 
   305 if term2str t = 
   306    "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x" then ()
 
   306    "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x" then ()
 
   307 else raise error "integrate.sml 3rd integration in 7.27, simplify_Integral";
 
   307 else raise error "integrate.sml 3rd integration in 7.27, simplify_Integral";
 
   308 
   308 
   309 val Some(t,_)= rewrite_set_inst_ thy true bdv integration t;
 
   309 val SOME(t,_)= rewrite_set_inst_ thy true bdv integration t;
 
   310 if term2str t = "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
 
   310 if term2str t = "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
 
   311 then () else raise error "integrate.sml 3rd integration in 7.27, integration";
 
   311 then () else raise error "integrate.sml 3rd integration in 7.27, integration";
 
   312 
   312 
   313 
   313 
   314 "----------- check probem type -----------------------------------";
 
   314 "----------- check probem type -----------------------------------";
 
   352 if F1_type = F3_type then () 
   352 if F1_type = F3_type then () 
   353 else raise error "integrate.sml: unequal types in find's";
 
   353 else raise error "integrate.sml: unequal types in find's";
 
   354 
   354 
   355 show_ptyps();
 
   355 show_ptyps();
 
   356 val pbl = get_pbt ["integrate","function"];
 
   356 val pbl = get_pbt ["integrate","function"];
 
   357 case #cas pbl of Some (Const ("Integrate.Integrate",_) $ _) => ()
 
   357 case #cas pbl of SOME (Const ("Integrate.Integrate",_) $ _) => ()
 
   358 	 | _ => raise error "integrate.sml: Integrate.Integrate ???";
 
   358 	 | _ => raise error "integrate.sml: Integrate.Integrate ???";
 
   359 
   359 
   360 
   360 
   361 "----------- check Scripts ---------------------------------------";
 
   361 "----------- check Scripts ---------------------------------------";
 
   362 "----------- check Scripts ---------------------------------------";
 
   362 "----------- check Scripts ---------------------------------------";
wneuper/isa