1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/smltest/IsacKnowledge/integrate.sml	Sun Aug 14 13:42:54 2005 +0200
     1.3 @@ -0,0 +1,103 @@
     1.4 +(* tests on integration over the reals
     1.5 +   author: Walther Neuper
     1.6 +   050814, 08:51
     1.7 +   (c) due to copyright terms
     1.8 +
     1.9 +use"~/proto2/isac/src/smltest/IsacKnowledge/integrate.sml";
    1.10 +*)
    1.11 +
    1.12 +"-----------------------------------------------------------------";
    1.13 +"table of contents -----------------------------------------------";
    1.14 +"-----------------------------------------------------------------";
    1.15 +"----------- parsing ---------------------------------------------";
    1.16 +"----------- set up rewriting ------------------------------------";
    1.17 +"----------- integrate by rewriting ------------------------------";
    1.18 +"----------- set up ruleset --------------------------------------";
    1.19 +"----------- integrate by ruleset --------------------------------";
    1.20 +"-----------------------------------------------------------------";
    1.21 +"-----------------------------------------------------------------";
    1.22 +"-----------------------------------------------------------------";
    1.23 +
    1.24 +"----------- parsing ---------------------------------------------";
    1.25 +"----------- parsing ---------------------------------------------";
    1.26 +"----------- parsing ---------------------------------------------";
    1.27 +fun str2t thy str = (term_of o the o (parse thy )) str;
    1.28 +fun term2s thy t = Sign.string_of_term (sign_of thy) t;
    1.29 +    
    1.30 +val t = str2t Integrate.thy "Integral x D x";
    1.31 +val t = str2t Integrate.thy "Integral x^^^2 D x";
    1.32 +atomty thy t;
    1.33 +
    1.34 +"----------- set up rewriting ------------------------------------";
    1.35 +"----------- set up rewriting ------------------------------------";
    1.36 +"----------- set up rewriting ------------------------------------";
    1.37 +val conditions_in_integration_rules = 
    1.38 +    prep_rls (Rls {id="conditions_in_integration_rules", preconds = [], 
    1.39 +		   rew_ord = ("termlessI",termlessI), 
    1.40 +		   erls = Erls, 
    1.41 +		   srls = Erls, calc = [],
    1.42 +		   rules = [Calc ("Atools.occurs'_in", 
    1.43 +				  eval_occurs_in "#occurs_in_"),
    1.44 +			    Thm ("not_true",num_str not_true),
    1.45 +			    Thm ("not_false",not_false)
    1.46 +			    ],
    1.47 +		   scr = EmptyScr});
    1.48 +ruleset' := overwritel (!ruleset', [("conditions_in_integration_rules", 
    1.49 +				     conditions_in_integration_rules)]);
    1.50 +    
    1.51 +"----------- integrate by rewriting ------------------------------";
    1.52 +"----------- integrate by rewriting ------------------------------";
    1.53 +"----------- integrate by rewriting ------------------------------";
    1.54 +fun rewrit subs thm str = 
    1.55 +    fst (the (rewrite_inst "Integrate.thy" "tless_true" 
    1.56 +			   "conditions_in_integration_rules" 
    1.57 +			   true subs thm str));
    1.58 +val thm = ("integral_const","");
    1.59 +val str = rewrit [("bdv","x::real")] thm "Integral 1 D x";
    1.60 +val str = rewrit [("bdv","x::real")] thm "Integral M'/EJ D x";
    1.61 +val str = (rewrit [("bdv","x::real")] thm "Integral x D x") 
    1.62 +    handle OPTION => "no rewrite -- OK";
    1.63 +
    1.64 +val thm = ("integral_var","");
    1.65 +val str = rewrit [("bdv","x::real")] thm "Integral x D x";
    1.66 +val str = (rewrit [("bdv","x::real")] thm "Integral a D x")
    1.67 +    handle OPTION => "no rewrite -- OK";
    1.68 +
    1.69 +val thm = ("integral_add","");
    1.70 +val str = rewrit [("bdv","x::real")] thm "Integral x + 1 D x";
    1.71 +
    1.72 +val thm = ("integral_mult","");
    1.73 +val str = rewrit [("bdv","x::real")] thm "Integral M'/EJ * x^^^3 D x";
    1.74 +val str = (rewrit [("bdv","x::real")] thm "Integral x * x D x")
    1.75 +    handle OPTION => "no rewrite -- OK";
    1.76 +
    1.77 +val thm = ("integral_pow","");
    1.78 +val str = rewrit [("bdv","x::real")] thm "Integral x^^^3 D x";
    1.79 +
    1.80 +"----------- set up ruleset --------------------------------------";
    1.81 +"----------- set up ruleset --------------------------------------";
    1.82 +"----------- set up ruleset --------------------------------------";
    1.83 +val integration_rules = 
    1.84 +    prep_rls (Rls {id="integration_rules", preconds = [], 
    1.85 +		   rew_ord = ("termlessI",termlessI), 
    1.86 +		   erls = conditions_in_integration_rules, 
    1.87 +		   srls = Erls, calc = [],
    1.88 +		   rules = [
    1.89 +			    Thm ("integral_const",num_str integral_const),
    1.90 +			    Thm ("integral_var",num_str integral_var),
    1.91 +			    Thm ("integral_add",num_str integral_add),
    1.92 +			    Thm ("integral_mult",num_str integral_mult),
    1.93 +			    Thm ("integral_pow",num_str integral_pow),
    1.94 +			    Rls_ make_polynomial
    1.95 +			    ],
    1.96 +		   scr = EmptyScr});
    1.97 +ruleset' := overwritel (!ruleset', [("integration_rules", integration_rules)]);
    1.98 +
    1.99 +"----------- integrate by ruleset --------------------------------";
   1.100 +"----------- integrate by ruleset --------------------------------";
   1.101 +"----------- integrate by ruleset --------------------------------";
   1.102 +fun rewrite_se subs rls str = 
   1.103 +    fst (the (rewrite_set_inst "Integrate.thy" true subs rls str));
   1.104 +val subs = [("bdv","x::real")];
   1.105 +val rls = "integration_rules";
   1.106 +val str = rewrite_se subs rls "Integral 1 D x";