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
Mon, 05 Sep 2005 12:51:55 +0200
branchstart_Take
changeset 375 49f28e3acadb
parent 371 4927811bff98
child 376 eeed17c7f62e
permissions -rw-r--r--
considering normalform for equation system 
     1 (* tests on integration over the reals

     2    author: Walther Neuper

     3    050814, 08:51

     4    (c) due to copyright terms

     5 

     6 use"../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 "----------- me method [Diff,integration,named] Biegelinie.Q -----";

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

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

    24 "-----------------------------------------------------------------";

    25 

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

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

    28 "----------- parsing ---------------------------------------------";

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

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

    31     

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

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

    34 atomty t;

    35 

    36 val t = str2t "M_b x is_f_x";

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

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

    39 

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

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

    42 "----------- integrate by rewriting ------------------------------";

    43 val conditions_in_integration_rules =

    44 Rls {id="conditions_in_integration_rules", 

    45      preconds = [], 

    46      rew_ord = ("termlessI",termlessI), 

    47      erls = Erls, 

    48      srls = Erls, calc = [],

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

    50 	      Calc ("Atools.occurs'_in", 

    51 		    eval_occurs_in "#occurs_in_"),

    52 	      Thm ("not_true",num_str not_true),

    53 	      Thm ("not_false",not_false)

    54 	      ],

    55      scr = EmptyScr};

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

    57 fun rewrit thm str = 

    58     fst (the (rewrite_inst_ Integrate.thy tless_true 

    59 			   conditions_in_integration_rules 

    60 			   true subs thm str));

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

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

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

    64     handle OPTION => str2t "no_rewrite";

    65 

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

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

    68     handle OPTION => str2t "no_rewrite";

    69 

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

    71 

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

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

    74     handle OPTION => str2t "no_rewrite";

    75 

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

    77 

    78 

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

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

    81 "----------- test new_c, is_f_x ----------------------------------";

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

    83 val cc = new_c term;

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

    85 

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

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

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

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

    90 

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

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

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

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

    95 

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

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

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

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

   100 

   101 val t = str2t "M_b x is_f_x";

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

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

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

   105 

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

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

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

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

   110 

   111 val conditions_in_integration =

   112 Rls {id="conditions_in_integration", 

   113 			       preconds = [], 

   114 			       rew_ord = ("termlessI",termlessI), 

   115 			       erls = Erls, 

   116 			       srls = Erls, calc = [],

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

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

   119 					      eval_is_f_x "is_f_x_"),

   120 					Thm ("not_true",num_str not_true),

   121 					Thm ("not_false",num_str not_false)

   122 					],

   123 			       scr = EmptyScr};

   124 fun rewrit thm t = 

   125     fst (the (rewrite_inst_ Integrate.thy tless_true 

   126 			    conditions_in_integration true subs thm t));

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

   128 val t = (rewrit call_for_new_c t)

   129     handle OPTION =>  str2t "no_rewrite";

   130 

   131 val t = rewrit call_for_new_c 

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

   133 val t = (rewrit call_for_new_c 

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

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

   136 

   137 

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

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

   140 "----------- integrate by ruleset --------------------------------";

   141 fun rewrit_sinst subs rls str = 

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

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

   144 val rls = "integration_rules";

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

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

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

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

   149 

   150 val rls = "add_new_c";

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

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

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

   154 

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

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

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

   158 

   159 val rls = "integration";

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

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

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

   163 

   164 

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

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

   167 "----------- check probem type -----------------------------------";

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

   169 	     Where =[],

   170 	     Find  =["antiDerivative F_"],

   171 	     With  =[],

   172 	     Relate=[]}:string ppc;

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

   174 val t1 = (term_of o hd) chkmodel;

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

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

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

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

   179 

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

   181 	     Where =[],

   182 	     Find  =["antiDerivativeName F_"],

   183 	     With  =[],

   184 	     Relate=[]}:string ppc;

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

   186 val t1 = (term_of o hd) chkmodel;

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

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

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

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

   191 

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

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

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

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

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

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

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

   199 

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

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

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

   203 if F1_type = F3_type then () 

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

   205 

   206 show_ptyps();

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

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

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

   210 

   211 

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

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

   214 "----------- check Scripts ---------------------------------------";

   215 val str = 

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

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

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

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

   220 atomty sc;

   221 

   222 val str = 

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

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

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

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

   227 atomty sc;

   228 show_mets();

   229 

   230 

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

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

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

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

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

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

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

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

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

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

   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;

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

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

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

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

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

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

   253 

   254 

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

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

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

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

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

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

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

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

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

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

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

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

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

   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;

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

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

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

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

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

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

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

   278 

   279 

   280 "----------- me method [Diff,integration,named] Biegelinie.Q -----";

   281 "----------- me method [Diff,integration,named] Biegelinie.Q -----";

   282 "----------- me method [Diff,integration,named] Biegelinie.Q -----";

   283 val fmz = ["functionTerm (- q_0)", 

   284 	   "integrateBy x","antiDerivativeName Q"];

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

   286   ("Biegelinie.thy",["named","integrate","function"],

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

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

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

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

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

   292 

   293 

   294 (*Error Tac Q not in ...*)

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

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

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

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

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

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

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

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

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

   304 if str = "Q x = c + -1 * q_0 * x" then() 

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

   306 

   307 (*

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

   309 *)
wneuper/isac