Mercurial Mercurial > wneuper > isac / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/smltest/IsacKnowledge/integrate.sml
author wneuper
Sun, 28 Aug 2005 16:53:19 +0200
branchstart_Take
changeset 349 2f33cdc92be2
parent 348 0094f47effaa
child 365 022b8b845fbe
permissions -rw-r--r--
corrected error in Add_Find "antiDerivativeName M_b" 
     1 (* tests on integration over the reals

     2    author: Walther Neuper

     3    050814, 08:51

     4    (c) due to copyright terms

     5 

     6 use"~/proto2/isac/src/smltest/IsacKnowledge/integrate.sml";

     7 *)

     8 val thy = Integrate.thy;

     9 

    10 "-----------------------------------------------------------------";

    11 "table of contents -----------------------------------------------";

    12 "-----------------------------------------------------------------";

    13 "----------- parsing ---------------------------------------------";

    14 "----------- integrate by rewriting ------------------------------";

    15 "----------- test new_c, is_f_x ----------------------------------";

    16 "----------- integrate by ruleset --------------------------------";

    17 "----------- check probem type -----------------------------------";

    18 "----------- check Scripts ---------------------------------------";

    19 "----------- me method [Diff,integration] ------------------------";

    20 "----------- me method [Diff,integration,named] ------------------";

    21 "-----------------------------------------------------------------";

    22 "-----------------------------------------------------------------";

    23 "-----------------------------------------------------------------";

    24 

    25 "----------- parsing ---------------------------------------------";

    26 "----------- parsing ---------------------------------------------";

    27 "----------- parsing ---------------------------------------------";

    28 fun str2t str = (term_of o the o (parse Integrate.thy)) str;

    29 fun term2s t = Sign.string_of_term (sign_of Integrate.thy) t;

    30     

    31 val t = str2t "Integral x D x";

    32 val t = str2t "Integral x^^^2 D x";

    33 atomty thy t;

    34 

    35 val t = str2t "M_b x is_f_x";

    36 case t of Const ("Integrate.is'_f'_x", _) $ _ => ()

    37 	| _ => raise error "integrate.sml: parsing: M_b x is_f_x";

    38 

    39 "----------- integrate by rewriting ------------------------------";

    40 "----------- integrate by rewriting ------------------------------";

    41 "----------- integrate by rewriting ------------------------------";

    42 val conditions_in_integration_rules =

    43 Rls {id="conditions_in_integration_rules", 

    44      preconds = [], 

    45      rew_ord = ("termlessI",termlessI), 

    46      erls = Erls, 

    47      srls = Erls, calc = [],

    48      rules = [(*for rewriting conditions in Thm's*)

    49 	      Calc ("Atools.occurs'_in", 

    50 		    eval_occurs_in "#occurs_in_"),

    51 	      Thm ("not_true",num_str not_true),

    52 	      Thm ("not_false",not_false)

    53 	      ],

    54      scr = EmptyScr};

    55 val subs = [(str2t "bdv", str2t "x")];

    56 fun rewrit thm str = 

    57     fst (the (rewrite_inst_ Integrate.thy tless_true 

    58 			   conditions_in_integration_rules 

    59 			   true subs thm str));

    60 val str = rewrit integral_const (str2t "Integral 1 D x"); term2s str;

    61 val str = rewrit integral_const (str2t  "Integral M'/EJ D x"); term2s str;

    62 val str = (rewrit integral_const (str2t "Integral x D x")) 

    63     handle OPTION => str2t "no_rewrite";

    64 

    65 val str = rewrit integral_var (str2t "Integral x D x"); term2s str;

    66 val str = (rewrit integral_var (str2t "Integral a D x"))

    67     handle OPTION => str2t "no_rewrite";

    68 

    69 val str = rewrit integral_add (str2t "Integral x + 1 D x"); term2s str;

    70 

    71 val str = rewrit integral_mult (str2t "Integral M'/EJ * x^^^3 D x");term2s str;

    72 val str = (rewrit integral_mult (str2t "Integral x * x D x"))

    73     handle OPTION => str2t "no_rewrite";

    74 

    75 val str = rewrit integral_pow (str2t "Integral x^^^3 D x"); term2s str;

    76 

    77 

    78 "----------- test new_c, is_f_x ----------------------------------";

    79 "----------- test new_c, is_f_x ----------------------------------";

    80 "----------- test new_c, is_f_x ----------------------------------";

    81 val term = str2t "x^^^2*c + c_2";

    82 val cc = new_c term;

    83 if term2s cc = "c_3" then () else raise error "integrate.sml: new_c ???";

    84 

    85 val term = str2t "new_c (c * x^^^2 + c_2)";

    86 val Some (_,t') = eval_new_c 0 0 term 0;

    87 if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()

    88 else raise error "integrate.sml: eval_new_c ???";

    89 

    90 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2)";

    91 val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';

    92 if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()

    93 else raise error "integrate.sml: matches new_c = False";

    94 

    95 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";

    96 val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';

    97 if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"

    98 then () else raise error "integrate.sml: matches new_c = True";

    99 

   100 val t = str2t "M_b x is_f_x";

   101 val Some (_,t') = eval_is_f_x "" "" t thy; term2s t';

   102 if term2s t' = "(M_b x is_f_x) = True" then ()

   103 else raise error "integrate.sml: eval_is_f_x --> true";

   104 

   105 val t = str2t "q_0/2 * L * x is_f_x";

   106 val Some (_,t') = eval_is_f_x "" "" t thy; term2s t';

   107 if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then ()

   108 else raise error "integrate.sml: eval_is_f_x --> false";

   109 

   110 val conditions_in_integration =

   111 Rls {id="conditions_in_integration", 

   112 			       preconds = [], 

   113 			       rew_ord = ("termlessI",termlessI), 

   114 			       erls = Erls, 

   115 			       srls = Erls, calc = [],

   116 			       rules = [Calc ("Tools.matches",eval_matches ""),

   117 					Calc ("Integrate.is'_f'_x", 

   118 					      eval_is_f_x "is_f_x_"),

   119 					Thm ("not_true",num_str not_true),

   120 					Thm ("not_false",num_str not_false)

   121 					],

   122 			       scr = EmptyScr};

   123 fun rewrit thm t = 

   124     fst (the (rewrite_inst_ Integrate.thy tless_true 

   125 			    conditions_in_integration true subs thm t));

   126 val t = rewrit call_for_new_c (str2t "x ^^^ 2 / 2"); term2s t;

   127 val t = (rewrit call_for_new_c t)

   128     handle OPTION =>  str2t "no_rewrite";

   129 

   130 val t = rewrit call_for_new_c 

   131 	       (str2t "M_b x = q_0/2 *L*x"); term2s t;

   132 val t = (rewrit call_for_new_c 

   133 	       (str2t "M_b x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))

   134     handle OPTION => (*NOT:  + new_c ..=..!!*)str2t "no_rewrite";

   135 

   136 

   137 "----------- integrate by ruleset --------------------------------";

   138 "----------- integrate by ruleset --------------------------------";

   139 "----------- integrate by ruleset --------------------------------";

   140 fun rewrit_sinst subs rls str = 

   141     fst (the (rewrite_set_inst "Integrate.thy" true subs rls str));

   142 val subs = [("bdv","x::real")];

   143 val rls = "integration_rules";

   144 val str = rewrit_sinst subs rls "Integral x D x";

   145 val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";

   146 if str = "c * (x ^^^ 3 / 3) + c_2 * x"

   147 then () else raise error "integrate.sml: diff.behav. in integration_rules";

   148 

   149 val rls = "add_new_c";

   150 val str = rewrit_sinst subs rls "c * (x ^^^ 3 / 3) + c_2 * x";

   151 if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then () 

   152 else raise error "integrate.sml: diff.behav. in add_new_c simpl.";

   153 

   154 val str = rewrit_sinst subs rls "F x = x ^^^ 3 / 3 + x";

   155 if str = "F x = x ^^^ 3 / 3 + x + c"(*not "F x + c =..."*) then () 

   156 else raise error "integrate.sml: diff.behav. in add_new_c equation";

   157 

   158 val rls = "integration";

   159 val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";

   160 if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3"

   161 then () else raise error "integrate.sml: diff.behav. in integration";

   162 

   163 

   164 "----------- check probem type -----------------------------------";

   165 "----------- check probem type -----------------------------------";

   166 "----------- check probem type -----------------------------------";

   167 val model = {Given =["functionTerm f_", "integrateBy v_"],

   168 	     Where =[],

   169 	     Find  =["antiDerivative F_"],

   170 	     With  =[],

   171 	     Relate=[]}:string ppc;

   172 val chkmodel = ((map (the o (parse Integrate.thy))) o ppc2list) model;

   173 val t1 = (term_of o hd) chkmodel;

   174 val t2 = (term_of o hd o tl) chkmodel;

   175 val t3 = (term_of o hd o tl o tl) chkmodel;

   176 case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()

   177 	 | _ => raise error "integrate.sml: Integrate.antiDerivative ???";

   178 

   179 val model = {Given =["functionTerm f_", "integrateBy v_"],

   180 	     Where =[],

   181 	     Find  =["antiDerivativeName F_"],

   182 	     With  =[],

   183 	     Relate=[]}:string ppc;

   184 val chkmodel = ((map (the o (parse Integrate.thy))) o ppc2list) model;

   185 val t1 = (term_of o hd) chkmodel;

   186 val t2 = (term_of o hd o tl) chkmodel;

   187 val t3 = (term_of o hd o tl o tl) chkmodel;

   188 case t3 of Const ("Integrate.antiDerivativeName", _) $ _ => ()

   189 	 | _ => raise error "integrate.sml: Integrate.antiDerivativeName";

   190 

   191 "----- compare 'Find's from problem, script, formalization -------";

   192 val {ppc,...} = get_pbt ["named","integrate","function"];

   193 val ("#Find", (Const ("Integrate.antiDerivativeName", _),

   194 	       F1_ as Free ("F_", F1_type))) = last_elem ppc;

   195 val {scr = Script sc,... } = get_met ["Diff","integration","named"];

   196 val [_,_, F2_] = formal_args sc;

   197 if F1_ = F2_ then () else raise error "integrate.sml: unequal find's";

   198 

   199 val ((dsc as Const ("Integrate.antiDerivativeName", _)) 

   200 	 $ Free ("M_b", F3_type)) = str2t "antiDerivativeName M_b";

   201 if is_dsc dsc then () else raise error "integrate.sml: no description";

   202 if F1_type = F3_type then () 

   203 else raise error "integrate.sml: unequal types in find's";

   204 

   205 show_ptyps();

   206 val pbl = get_pbt ["integrate","function"];

   207 case #cas pbl of Some (Const ("Integrate.Integrate",_) $ _) => ()

   208 	 | _ => raise error "integrate.sml: Integrate.Integrate ???";

   209 

   210 

   211 "----------- check Scripts ---------------------------------------";

   212 "----------- check Scripts ---------------------------------------";

   213 "----------- check Scripts ---------------------------------------";

   214 val str = 

   215 "Script IntegrationScript (f_::real) (v_::real) =               \

   216 \  (let t_ = Take (Integral f_ D v_)                                 \

   217 \   in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))";

   218 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   219 atomty thy sc;

   220 

   221 val str = 

   222 "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real=>real) = \

   223 \  (let t_ = Take (F_ v_ = Integral f_ D v_)                         \

   224 \   in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)";

   225 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   226 atomty thy sc;

   227 show_mets();

   228 

   229 

   230 "----------- me method [Diff,integration] ---------------------";

   231 "----------- me method [Diff,integration] ---------------------";

   232 "----------- me method [Diff,integration] ---------------------";

   233 val fmz = ["functionTerm (x^^^2 + 1)", 

   234 	   "integrateBy x","antiDerivative FF"];

   235 val (dI',pI',mI') =

   236   ("Integrate.thy",["integrate","function"],

   237    ["Diff","integration"]);

   238 val p = e_pos'; val c = []; 

   239 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   240 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   241 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   242 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   243 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   244 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   245 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   246 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);

   247 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   248 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   249 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   250 if f=Form' (FormKF (~1, EdUndef, 0, Nundef, "x ^^^ 3 / 3 + x + c")) then ()

   251 else raise error "integrate.sml: method [Diff,integration]";

   252 

   253 

   254 "----------- me method [Diff,integration,named] ------------------";

   255 "----------- me method [Diff,integration,named] ------------------";

   256 "----------- me method [Diff,integration,named] ------------------";

   257 val fmz = ["functionTerm (x^^^2 + 1)", 

   258 	   "integrateBy x","antiDerivativeName F"];

   259 val (dI',pI',mI') =

   260   ("Integrate.thy",["named","integrate","function"],

   261    ["Diff","integration","named"]);

   262 val p = e_pos'; val c = []; 

   263 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   264 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   265 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   266 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);

   267 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   268 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   269 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   270 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);

   271 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   272 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   273 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   274 val Form' (FormKF (~1, EdUndef, 0, Nundef, str)) = f;

   275 if str = "F x = x ^^^ 3 / 3 + x + c" then() 

   276 else raise error "integrate.sml: method [Diff,integration,named]";

   277 

   278 (*

   279 use"~/proto2/isac/src/smltest/IsacKnowledge/integrate.sml";

   280 *)
wneuper/isac