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/Knowledge/integrate.sml
changeset 60565 f92963a33fe3
parent 60559 aba19e46dd84
child 60571 19a172de0bb5
equal deleted inserted replaced
60564:90ea835c07b3 60565:f92963a33fe3 
    49 
    49 
    50 
    50 
    51 "----------- parsing ------------------------------------";
 
    51 "----------- parsing ------------------------------------";
 
    52 "----------- parsing ------------------------------------";
 
    52 "----------- parsing ------------------------------------";
 
    53 "----------- parsing ------------------------------------";
 
    53 "----------- parsing ------------------------------------";
 
    54 val t = TermC.str2term "Integral x D x";
 
    54 val t = TermC.parse_test @{context} "Integral x D x";
 
    55 val t = TermC.str2term "Integral x \<up> 2 D x";
 
    55 val t = TermC.parse_test @{context} "Integral x \<up> 2 D x";
 
    56 case t of 
    56 case t of 
    57     Const (\<^const_name>\<open>Integral\<close>, _) $
 
    57     Const (\<^const_name>\<open>Integral\<close>, _) $
 
    58      (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ _) $ Free ("x", _) => ()
 
    58      (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ _) $ Free ("x", _) => ()
 
    59   | _ => error "integrate.sml: parsing: Integral x \<up> 2 D x";
 
    59   | _ => error "integrate.sml: parsing: Integral x \<up> 2 D x";
 
    60 
    60 
    61 val t = TermC.str2term "ff x is_f_x";
 
    61 val t = TermC.parse_test @{context} "ff x is_f_x";
 
    62 case t of Const (\<^const_name>\<open>is_f_x\<close>, _) $ _ => ()
 
    62 case t of Const (\<^const_name>\<open>is_f_x\<close>, _) $ _ => ()
 
    63 	| _ => error "integrate.sml: parsing: ff x is_f_x";
 
    63 	| _ => error "integrate.sml: parsing: ff x is_f_x";
 
    64 
    64 
    65 
    65 
    66 "----------- integrate by rewriting ---------------------";
 
    66 "----------- integrate by rewriting ---------------------";
 
    67 "----------- integrate by rewriting ---------------------";
 
    67 "----------- integrate by rewriting ---------------------";
 
    68 "----------- integrate by rewriting ---------------------";
 
    68 "----------- integrate by rewriting ---------------------";
 
    69 val str = rewrit @{thm "integral_const"} (TermC.str2term "Integral 1 D x");
 
    69 val str = rewrit @{thm "integral_const"} (TermC.parse_test @{context} "Integral 1 D x");
 
    70 if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";
 
    70 if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";
 
    71 
    71 
    72 val str = rewrit @{thm "integral_const"} (TermC.str2term  "Integral M'/EJ D x");
 
    72 val str = rewrit @{thm "integral_const"} (TermC.parse_test @{context}  "Integral M'/EJ D x");
 
    73 if term2s str = "M' / EJ * x" then ()
 
    73 if term2s str = "M' / EJ * x" then ()
 
    74 else error "Integral M'/EJ D x   BY integral_const";
 
    74 else error "Integral M'/EJ D x   BY integral_const";
 
    75 
    75 
    76 val str = rewrit @{thm "integral_var"} (TermC.str2term "Integral x D x");
 
    76 val str = rewrit @{thm "integral_var"} (TermC.parse_test @{context} "Integral x D x");
 
    77 if term2s str = "x \<up> 2 / 2" then ()
 
    77 if term2s str = "x \<up> 2 / 2" then ()
 
    78 else error "Integral x D x   BY integral_var";
 
    78 else error "Integral x D x   BY integral_var";
 
    79 
    79 
    80 val str = rewrit @{thm "integral_add"} (TermC.str2term "Integral x + 1 D x");
 
    80 val str = rewrit @{thm "integral_add"} (TermC.parse_test @{context} "Integral x + 1 D x");
 
    81 if term2s str = "Integral x D x + Integral 1 D x" then ()
 
    81 if term2s str = "Integral x D x + Integral 1 D x" then ()
 
    82 else error "Integral x + 1 D x   BY integral_add";
 
    82 else error "Integral x + 1 D x   BY integral_add";
 
    83 
    83 
    84 val str = rewrit @{thm "integral_mult"} (TermC.str2term "Integral M'/EJ * x \<up> 3 D x");
 
    84 val str = rewrit @{thm "integral_mult"} (TermC.parse_test @{context} "Integral M'/EJ * x \<up> 3 D x");
 
    85 if term2s str = "M' / EJ * Integral x \<up> 3 D x" then ()
 
    85 if term2s str = "M' / EJ * Integral x \<up> 3 D x" then ()
 
    86 else error "Integral M'/EJ * x \<up> 3 D x   BY integral_mult";
 
    86 else error "Integral M'/EJ * x \<up> 3 D x   BY integral_mult";
 
    87 
    87 
    88 val str = rewrit @{thm "integral_pow"} (TermC.str2term "Integral x \<up> 3 D x");
 
    88 val str = rewrit @{thm "integral_pow"} (TermC.parse_test @{context} "Integral x \<up> 3 D x");
 
    89 if term2s str = "x \<up> (3 + 1) / (3 + 1)" then ()
 
    89 if term2s str = "x \<up> (3 + 1) / (3 + 1)" then ()
 
    90 else error "integrate.sml Integral x \<up> 3 D x";
 
    90 else error "integrate.sml Integral x \<up> 3 D x";
 
    91 
    91 
    92 
    92 
    93 "----------- test add_new_c, TermC.is_f_x ---------------------";
 
    93 "----------- test add_new_c, TermC.is_f_x ---------------------";
 
    94 "----------- test add_new_c, TermC.is_f_x ---------------------";
 
    94 "----------- test add_new_c, TermC.is_f_x ---------------------";
 
    95 "----------- test add_new_c, TermC.is_f_x ---------------------";
 
    95 "----------- test add_new_c, TermC.is_f_x ---------------------";
 
    96 val term = TermC.str2term "x \<up> 2 * c + c_2";
 
    96 val term = TermC.parse_test @{context} "x \<up> 2 * c + c_2";
 
    97 val cc = new_c term;
 
    97 val cc = new_c term;
 
    98 if UnparseC.term cc = "c_3" then () else error "integrate.sml: new_c ???";
 
    98 if UnparseC.term cc = "c_3" then () else error "integrate.sml: new_c ???";
 
    99 
    99 
   100 val SOME (id,t') = eval_add_new_c "" "Integrate.add_new_c" term ctxt;
 
   100 val SOME (id,t') = eval_add_new_c "" "Integrate.add_new_c" term ctxt;
 
   101 if UnparseC.term t' = "x \<up> 2 * c + c_2 = x \<up> 2 * c + c_2 + c_3" then ()
 
   101 if UnparseC.term t' = "x \<up> 2 * c + c_2 = x \<up> 2 * c + c_2 + c_3" then ()
 
   106 
   106 
   107 val SOME (t',_) = rewrite_set_ ctxt true add_new_c term;
 
   107 val SOME (t',_) = rewrite_set_ ctxt true add_new_c term;
 
   108 if UnparseC.term t' = "x \<up> 2 * c + c_2 + c_3" then ()
 
   108 if UnparseC.term t' = "x \<up> 2 * c + c_2 + c_3" then ()
 
   109 else error "intergrate.sml: diff. rewrite_set add_new_c 1";
 
   109 else error "intergrate.sml: diff. rewrite_set add_new_c 1";
 
   110 
   110 
   111 val term = TermC.str2term "ff x = x \<up> 2*c + c_2";
 
   111 val term = TermC.parse_test @{context} "ff x = x \<up> 2*c + c_2";
 
   112 val SOME (t',_) = rewrite_set_ ctxt true add_new_c term;
 
   112 val SOME (t',_) = rewrite_set_ ctxt true add_new_c term;
 
   113 if UnparseC.term t' = "ff x = x \<up> 2 * c + c_2 + c_3" then ()
 
   113 if UnparseC.term t' = "ff x = x \<up> 2 * c + c_2 + c_3" then ()
 
   114 else error "intergrate.sml: diff. rewrite_set add_new_c 2";
 
   114 else error "intergrate.sml: diff. rewrite_set add_new_c 2";
 
   115 
   115 
   116 
   116 
   171 "----------- simplify by ruleset reducing make_ratpoly_in";
 
   171 "----------- simplify by ruleset reducing make_ratpoly_in";
 
   172 "----------- simplify by ruleset reducing make_ratpoly_in";
 
   172 "----------- simplify by ruleset reducing make_ratpoly_in";
 
   173 "----------- simplify by ruleset reducing make_ratpoly_in";
 
   173 "----------- simplify by ruleset reducing make_ratpoly_in";
 
   174 val thy = @{theory "Isac_Knowledge"};
 
   174 val thy = @{theory "Isac_Knowledge"};
 
   175 val ctxt = Proof_Context.init_global thy;
 
   175 val ctxt = Proof_Context.init_global thy;
 
   176 val subst = [(TermC.str2term "bdv ::real", TermC.str2term "x ::real")]; (*DOESN'T HELP*)
 
   176 val subst = [(TermC.parse_test @{context} "bdv ::real", TermC.parse_test @{context} "x ::real")]; (*DOESN'T HELP*)
 
   177 "===== test 1";
 
   177 "===== test 1";
 
   178 val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
 
   178 val t = TermC.parse_test @{context} "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
 
   179 
   179 
   180 "----- stepwise from the rulesets in simplify_Integral and below-----";
 
   180 "----- stepwise from the rulesets in simplify_Integral and below-----";
 
   181 val rls = norm_Rational_noadd_fractions;
 
   181 val rls = norm_Rational_noadd_fractions;
 
   182 case rewrite_set_inst_ ctxt true subs rls t of
 
   182 case rewrite_set_inst_ ctxt true subs rls t of
 
   183     SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
 
   183     SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
 
   194 val SOME (t, []) = rewrite_set_ ctxt true rls t;
 
   194 val SOME (t, []) = rewrite_set_ ctxt true rls t;
 
   195 if UnparseC.term t = "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" then ()
 
   195 if UnparseC.term t = "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" then ()
 
   196 else error "integrate.sml simplify by ruleset discard_parenth.. #3";
 
   196 else error "integrate.sml simplify by ruleset discard_parenth.. #3";
 
   197 
   197 
   198 "===== test 4";
 
   198 "===== test 4";
 
   199 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
 
   199 val subs = [(TermC.parse_test @{context} "bdv::real", TermC.parse_test @{context} "x::real")];
 
   200 val rls = 
   200 val rls = 
   201   (Rule_Set.append_rules "separate_bdv" collect_bdv
 
   201   (Rule_Set.append_rules "separate_bdv" collect_bdv
 
   202  	  [Thm ("separate_bdv", @{thm separate_bdv}),
 
   202  	  [Thm ("separate_bdv", @{thm separate_bdv}),
 
   203  		  (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
 
   203  		  (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
 
   204  		 Thm ("separate_bdv_n", @{thm separate_bdv_n}),
 
   204  		 Thm ("separate_bdv_n", @{thm separate_bdv_n}),
 
   219 val SOME (t, []) = rewrite_set_inst_ ctxt true subs rls t;
 
   219 val SOME (t, []) = rewrite_set_inst_ ctxt true subs rls t;
 
   220 if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2)" then ()
 
   220 if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2)" then ()
 
   221 else error "integrate.sml simplify by ruleset separate_bdv.. #4";
 
   221 else error "integrate.sml simplify by ruleset separate_bdv.. #4";
 
   222 
   222 
   223 "===== test 5";
 
   223 "===== test 5";
 
   224 val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
 
   224 val t = TermC.parse_test @{context} "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
 
   225 val rls = simplify_Integral;
 
   225 val rls = simplify_Integral;
 
   226 val SOME (t,[]) = rewrite_set_inst_ ctxt true subs rls t;
 
   226 val SOME (t,[]) = rewrite_set_inst_ ctxt true subs rls t;
 
   227 (* given was:   "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" *)
 
   227 (* given was:   "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" *)
 
   228 if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2)" then ()
 
   228 if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2)" then ()
 
   229 else error "integrate.sml, simplify_Integral #99";
 
   229 else error "integrate.sml, simplify_Integral #99";
 
   230 
   230 
   231 "........... 2nd integral ........................................";
 
   231 "........... 2nd integral ........................................";
 
   232 "........... 2nd integral ........................................";
 
   232 "........... 2nd integral ........................................";
 
   233 "........... 2nd integral ........................................";
 
   233 "........... 2nd integral ........................................";
 
   234 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
 
   234 val subs = [(TermC.parse_test @{context} "bdv::real", TermC.parse_test @{context} "x::real")];
 
   235 
   235 
   236 val thy = @{theory Biegelinie};
 
   236 val thy = @{theory Biegelinie};
 
   237 val t = TermC.str2term 
   237 val t = TermC.parse_test @{context} 
   238   "Integral 1 / EI * (L * q_0 / 2 * (x \<up> 2 / 2) + - 1 * q_0 / 2 * (x \<up> 3 / 3)) D x";
 
   238   "Integral 1 / EI * (L * q_0 / 2 * (x \<up> 2 / 2) + - 1 * q_0 / 2 * (x \<up> 3 / 3)) D x";
 
   239 
   239 
   240 val rls = simplify_Integral;
 
   240 val rls = simplify_Integral;
 
   241 val SOME (t,[]) = rewrite_set_inst_ ctxt true subs rls t;
 
   241 val SOME (t,[]) = rewrite_set_inst_ ctxt true subs rls t;
 
   242 if UnparseC.term t = "Integral 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3) D x"
 
   242 if UnparseC.term t = "Integral 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3) D x"
 
   307 then () else error "integrate.sml: diff.behav. in integration #4";
 
   307 then () else error "integrate.sml: diff.behav. in integration #4";
 
   308 
   308 
   309 "----------- rewrite 3rd integration in 7.27 ------------";
 
   309 "----------- rewrite 3rd integration in 7.27 ------------";
 
   310 "----------- rewrite 3rd integration in 7.27 ------------";
 
   310 "----------- rewrite 3rd integration in 7.27 ------------";
 
   311 "----------- rewrite 3rd integration in 7.27 ------------";
 
   311 "----------- rewrite 3rd integration in 7.27 ------------";
 
   312 val t = TermC.str2term "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \<up> 2) / 2) D x";
 
   312 val t = TermC.parse_test @{context} "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \<up> 2) / 2) D x";
 
   313 val SOME(t, _)= rewrite_set_inst_ ctxt true subs simplify_Integral t;
 
   313 val SOME(t, _)= rewrite_set_inst_ ctxt true subs simplify_Integral t;
 
   314 if UnparseC.term t = 
   314 if UnparseC.term t = 
   315   "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x"
 
   315   "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x"
 
   316 then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral";
 
   316 then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral";
 
   317 
   317 
   356 val {scr = Prog sc,... } = MethodC.from_store ctxt ["diff", "integration", "named"];
 
   356 val {scr = Prog sc,... } = MethodC.from_store ctxt ["diff", "integration", "named"];
 
   357 val [_,_, F2_] = formal_args sc;
 
   357 val [_,_, F2_] = formal_args sc;
 
   358 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
 
   358 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
 
   359 
   359 
   360 val ((dsc as Const (\<^const_name>\<open>antiDerivativeName\<close>, _)) 
   360 val ((dsc as Const (\<^const_name>\<open>antiDerivativeName\<close>, _)) 
   361 	 $ Free ("ff", F3_type)) = TermC.str2term "antiDerivativeName ff";
 
   361 	 $ Free ("ff", F3_type)) = TermC.parse_test @{context} "antiDerivativeName ff";
 
   362 if Input_Descript.is_a dsc then () else error "integrate.sml: no description";
 
   362 if Input_Descript.is_a dsc then () else error "integrate.sml: no description";
 
   363 if F1_type = F3_type then () 
   363 if F1_type = F3_type then () 
   364 else error "integrate.sml: unequal types in find's";
 
   364 else error "integrate.sml: unequal types in find's";
 
   365 
   365 
   366 Test_Tool.show_ptyps();
 
   366 Test_Tool.show_ptyps();
wneuper/isa