wneuper/isa: src/Pure/isac/smltest/ME/me.sml@875b6efa7ced

     1 (* tests on me.sml

     2    author: Walther Neuper

     3    060225,

     4    (c) due to copyright terms

     6 use"../smltest/ME/me.sml";

     7 use"me.sml";

     8 *)

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

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

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

    13 "=====new ptree 1: crippled by cut_level_'_ ======================";

    14 "-------------- get_interval from ctree with move_dn:modspec.sml -";

    15 "=====new ptree 2 without changes ================================";

    16 "-------------- getFormulaeFromTo --------------------------------";

    17 "autoCalculate";

    18 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

    19 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";

    20 "--------- maximum-example: complete_metitms ---------------------";

    21 "--------- maximum-example: complete_mod -------------------------";

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

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

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

    28 "=====new ptree 1: crippled by cut_level_'_ ======================";

    29 "=====new ptree 1: crippled by cut_level_'_ ======================";

    30 "=====new ptree 1: crippled by cut_level_'_ ======================";

    31 states:=[];

    32 CalcTree

    33 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",

    34 	   "solveFor x","solutions L"],

    35   ("RatEq.thy",["univariate","equation"],["no_met"]))];

    36 Iterator 1; moveActiveRoot 1;

    37 autoCalculate 1 CompleteCalc;

    39 getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)

    40 getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)

    41 getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*)

    42 getTactic 1 ([4,1],Res);(*Rewrite all_left*)

    43 getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*)

    44 getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*)

    46 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);

    47 moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);

    48 moveActiveFormula 1 ([3],Res)(*3.1.*);

    49 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);

    50 moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*);

    52 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);

    53 interSteps 1 ([1],Res)(*..is activeFormula !?!*);

    55 getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*)

    56 getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*)

    57 getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*)

    58 getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)

    60 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);

    61 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);

    62 val ((pt,_),_) = get_calc 1;

    63 writeln(pr_ptree pr_short pt);

    64 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:

    65  ###########################################################################*)

    66 val (pt, _) = cut_level_'_ [] [] pt ([4,1],Frm);                         (*#*)

    67 (*##########################################################################*)

    68 writeln(pr_ptree pr_short pt);

    69 (*##########################################################################

    70   attention: the ctree in states is still the old (perfect) !!!

    71 ############################################################################*)

    75 "-------------- get_interval from ctree with move_dn:modspec.sml -";

    76 "-------------- get_interval from ctree with move_dn:modspec.sml -";

    77 "-------------- get_interval from ctree with move_dn:modspec.sml -";

    78 writeln(pr_ptree pr_short pt);

    79 writeln(posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));

    81 case map fst (get_interval ([],Frm) ([],Res) 99999 pt) of

    82     [([], Frm),

    83      ([1], Frm),

    84      ([1, 1], Frm),

    85      ([1, 1], Res),

    86      ([1, 2], Res),

    87      ([1, 3], Res),

    88      ([1, 4], Res),

    89      ([1], Res),

    90      ([2], Res),

    91      ([3], Res),

    92      ([4], Pbl),

    93      ([4, 1], Frm),

    94      ([4, 1, 1], Frm),

    95      ([4, 1, 1], Res),

    96      ([4, 1], Res),

    97      ([4, 2], Res),

    98      ([4, 3], Pbl),

    99      ([4, 3, 1], Frm),

   100      ([4, 3, 1], Res),

   101      ([4, 3, 2], Res),

   102      ([4, 3, 3], Res),

   103      ([4, 3, 4], Res),

   104      ([4, 3, 5], Res),

   105      ([4, 3], Res),

   106      ([4], Res),

   107      ([5], Res),

   108      ([], Res)] => ()

   109   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";

   110 case map fst (get_interval ([],Frm) ([],Res) 1 pt) of

   111     [([], Frm),

   112      ([1], Frm),

   113      ([1], Res),

   114      ([2], Res),

   115      ([3], Res),

   116      ([4], Pbl),

   117      ([4], Res),

   118      ([5], Res),

   119      ([], Res)] => ()

   120   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";

   121 case map fst (get_interval ([],Frm) ([],Res) 0 pt) of

   122     [([], Frm),

   123      ([], Res)] => ()

   124   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f";

   126 case map fst (get_interval ([1,3],Res) ([4,1,1],Frm) 99999 pt) of

   127     [([1, 3], Res),

   128      ([1, 4], Res),

   129      ([1], Res),

   130      ([2], Res),

   131      ([3], Res),

   132      ([4], Pbl),

   133      ([4, 1], Frm),

   134      ([4, 1, 1], Frm)] => ()

   135   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1a";

   137 (*this pos' is not generated bu move_dn:......vvv: goes to end of calc*)

   138 case map fst (get_interval ([2],Res) ([4,3,2],Frm) 99999 pt) of

   139     [([2], Res),

   140      ([3], Res),

   141      ([4], Pbl),

   142      ([4, 1], Frm),

   143      ([4, 1, 1], Frm),

   144      ([4, 1, 1], Res),

   145      ([4, 1], Res),

   146      ([4, 2], Res),

   147      ([4, 3], Pbl),

   148      ([4, 3, 1], Frm),

   149      ([4, 3, 1], Res),

   150      ([4, 3, 2], Res),

   151      ([4, 3, 3], Res),(*this is beyond 'to'*)

   152      ([4, 3, 4], Res),(*this is beyond 'to'*)

   153      ([4, 3, 5], Res),(*this is beyond 'to'*)

   154      ([4, 3], Res),   (*this is beyond 'to'*)

   155      ([4], Res),      (*this is beyond 'to'*)

   156      ([5], Res),      (*this is beyond 'to'*)

   157      ([], Res)] => () (*this is beyond 'to'*)

   158   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1b";

   159 case map fst (get_interval ([1,4],Res) ([4,3,1],Frm) 99999 pt) of

   160     [([1, 4], Res),

   161      ([1], Res),

   162      ([2], Res),

   163      ([3], Res),

   164      ([4], Pbl),

   165      ([4, 1], Frm),

   166      ([4, 1, 1], Frm),

   167      ([4, 1, 1], Res),

   168      ([4, 1], Res),

   169      ([4, 2], Res),

   170      ([4, 3], Pbl),

   171      ([4, 3, 1], Frm)] => ()

   172   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1c";

   173 case map fst (get_interval ([4,2],Res) ([5],Res) 99999 pt) of

   174     [([4, 2], Res),

   175      ([4, 3], Pbl),

   176      ([4, 3, 1], Frm),

   177      ([4, 3, 1], Res),

   178      ([4, 3, 2], Res),

   179      ([4, 3, 3], Res),

   180      ([4, 3, 4], Res),

   181      ([4, 3, 5], Res),

   182      ([4, 3], Res),

   183      ([4], Res),

   184      ([5], Res)]=>()

   185   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1d";

   186 case map fst (get_interval ([],Frm) ([4,3,2],Res) 99999 pt) of

   187     [([], Frm),

   188      ([1], Frm),

   189      ([1, 1], Frm),

   190      ([1, 1], Res),

   191      ([1, 2], Res),

   192      ([1, 3], Res),

   193      ([1, 4], Res),

   194      ([1], Res),

   195      ([2], Res),

   196      ([3], Res),

   197      ([4], Pbl),

   198      ([4, 1], Frm),

   199      ([4, 1, 1], Frm),

   200      ([4, 1, 1], Res),

   201      ([4, 1], Res),

   202      ([4, 2], Res),

   203      ([4, 3], Pbl),

   204      ([4, 3, 1], Frm),

   205      ([4, 3, 1], Res),

   206      ([4, 3, 2], Res)] => ()

   207   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1e";

   208 case map fst (get_interval ([4,3],Frm) ([4,3],Res) 99999 pt) of

   209     [([4, 3], Frm),

   210      ([4, 3, 1], Frm),

   211      ([4, 3, 1], Res),

   212      ([4, 3, 2], Res),

   213      ([4, 3, 3], Res),

   214      ([4, 3, 4], Res),

   215      ([4, 3, 5], Res),

   216      ([4, 3], Res)] => ()

   217   | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1g";

   222 "=====new ptree 2 without changes ================================";

   223 "=====new ptree 2 without changes ================================";

   224 "=====new ptree 2 without changes ================================";

   225 states:=[];

   226 CalcTree

   227 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",

   228 	   "solveFor x","solutions L"],

   229   ("RatEq.thy",["univariate","equation"],["no_met"]))];

   230 Iterator 1; moveActiveRoot 1;

   231 autoCalculate 1 CompleteCalc;

   232 val ((pt,_),_) = get_calc 1;

   233 writeln(pr_ptree pr_short pt);

   236 "-------------- getFormulaeFromTo --------------------------------";

   237 "-------------- getFormulaeFromTo --------------------------------";

   238 "-------------- getFormulaeFromTo --------------------------------";

   239 getFormulaeFromTo 1 ([4, 2], Res) ([4, 4], Pbl) 000;

   240 (*

   241 "@@@@@begin@@@@@" //...................................................

   242 + " 1" //..............................................................

   243 + "<GETELEMENTSFROMTO>" //...................................................

   244 + "  <CALCID> 1 </CALCID>" //..........................................

   245 + "  <POSFORMHEADS>" //................................................

   246 + "    <POSFORM>" //...................................................

   247 + "      <GENERATED>" //...............................................

   248 + "        <INTLIST>" //...............................................

   249 + "          <INT> 4 </INT>" //........................................

   250 + "          <INT> 3 </INT>" //........................................

   251 + "        </INTLIST>" //..............................................

   252 + "        <POS> Res </POS>" //........................................

   253 + "      </GENERATED>" //..............................................

   254 + "      <FORMULA>" //.................................................

   255 + "        <MATHML>" //................................................

   256 + "          <ISA> -6 * x + 5 * x ^^^ 2 = 0 </ISA>" //.................

   257 + "        </MATHML>" //...............................................

   258 + "      </FORMULA>" //................................................

   259 + "    </POSFORM>" //..................................................

   260 + "    <POSHEAD>" //...................................................

   261 + "      <GENERATED>" //...............................................

   262 + "        <INTLIST>" //...............................................

   263 + "          <INT> 4 </INT>" //........................................

   264 + "          <INT> 4 </INT>" //........................................

   265 + "        </INTLIST>" //..............................................

   266 + "        <POS> Pbl </POS>" //........................................

   267 + "      </GENERATED>" //..............................................

   268 + "      <CALCHEAD status = "correct">" //.............................

   269 + "       <HEAD>" //...................................................

   270 + "         <MATHML>" //...............................................

   271 + "           <ISA> solve (-6 * x + 5 * x ^^^ 2 = 0, x) </ISA>" //.....

   272 + "         </MATHML>" //..............................................

   273 + "       </HEAD>" //..................................................

   274 + "        <MODEL>" //.................................................

   275 + "          <GIVEN>" //...............................................

   276 + "            <ITEM status="correct">" //.............................

   277 + "              <MATHML>" //..........................................

   278 + "                <ISA> equality (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //

   279 + "              </MATHML>" //.........................................

   280 + "            </ITEM>" //.............................................

   281 + "            <ITEM status="correct">" //.............................

   282 + "              <MATHML>" //..........................................

   283 + "                <ISA> solveFor x </ISA>" //.........................

   284 + "              </MATHML>" //.........................................

   285 + "            </ITEM>" //.............................................

   286 + "          </GIVEN>" //..............................................

   287 + "          <WHERE>" //...............................................

   288 + "            <ITEM status="correct">" //.............................

   289 + "              <MATHML>" //..........................................

   290 + "                <ISA> matches (?a * ?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"

   291 + "matches (?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //......

   292 + "matches (?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"

   293 + "matches (?a * ?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |"

   294 + "matches (?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //............

   295 + "matches (?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //..

   296 + "              </MATHML>" //.........................................

   297 + "            </ITEM>" //.............................................

   298 + "          </WHERE>" //..............................................

   299 + "          <FIND>" //................................................

   300 + "            <ITEM status="correct">" //.............................

   301 + "              <MATHML>" //..........................................

   302 + "                <ISA> solutions x_i </ISA>" //......................

   303 + "              </MATHML>" //.........................................

   304 + "            </ITEM>" //.............................................

   305 + "          </FIND>" //...............................................

   306 + "          <RELATE>  </RELATE>" //...................................

   307 + "        </MODEL>" //................................................

   308 + "        <BELONGSTO> Pbl </BELONGSTO>" //............................

   309 + "        <SPECIFICATION>" //.........................................

   310 + "          <THEORYID> PolyEq.thy </THEORYID>" //.....................

   311 + "          <PROBLEMID>" //...........................................

   312 + "            <STRINGLIST>" //........................................

   313 + "              <STRING> bdv_only </STRING>" //.......................

   314 + "              <STRING> degree_2 </STRING>" //.......................

   315 + "              <STRING> polynomial </STRING>" //.....................

   316 + "              <STRING> univariate </STRING>" //.....................

   317 + "              <STRING> equation </STRING>" //.......................

   318 + "            </STRINGLIST>" //.......................................

   319 + "          </PROBLEMID>" //..........................................

   320 + "          <METHODID>" //............................................

   321 + "            <STRINGLIST>" //........................................

   322 + "              <STRING> PolyEq </STRING>" //.........................

   323 + "              <STRING> solve_d2_polyeq_bdvonly_equation </STRING>"

   324 + "            </STRINGLIST>" //.......................................

   325 + "          </METHODID>" //...........................................

   326 + "        </SPECIFICATION>" //........................................

   327 + "      </CALCHEAD>" //...............................................

   328 + "    </POSHEAD>" //..................................................

   329 + "  <POSFORMHEADS>" //................................................

   330 + "</GETELEMENTSFROMTO>" //..................................................

   331 + "@@@@@end@@@@@"

   332 *)

   335 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

   336 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

   337 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

   338  val c = [];

   339  val (p,_,f,nxt,_,pt) = CalcTreeTEST

   340      [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],

   341        ("Test.thy",

   342 	["linear","univariate","equation","test"],

   343 	["Test","solve_linear"]))];

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

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

   346  (*xt = Add_Given "solveFor x"*)

   347  writeln (itms2str thy (get_obj g_pbl pt (fst p)));

   348 (*[

   349 (0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])),

   350 (0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])),

   351 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*)

   352  val (pt,p) = complete_mod (pt, p);

   353  if itms2str thy (get_obj g_pbl pt (fst p)) = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" then ()

   354  else raise error "completetest.sml: new behav. in complete_mod 1";

   355  writeln (itms2str thy (get_obj g_pbl pt (fst p)));

   356 (*[

   357 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),

   358 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),

   359 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)

   360  val mits = get_obj g_met pt (fst p);

   361  if itms2str thy mits = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]"

   362  then () else raise error "completetest.sml: new behav. in complete_mod 2";

   363  writeln (itms2str thy mits);

   364 (*[

   365 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),

   366 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),

   367 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)

   371 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";

   372 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";

   373 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";

   374  states:=[];

   375  CalcTree      (*start of calculation, return No.1*)

   376      [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],

   377        ("Test.thy",

   378 	["linear","univariate","equation","test"],

   379 	["Test","solve_linear"]))];

   380  Iterator 1; moveActiveRoot 1;

   382 (*

   383  autoCalculate 1 CompleteCalcHead;

   384  autoCalculate 1 (Step 1);

   385  refFormula 1 (get_pos 1 1);

   387 ... works

   389  autoCalculate 1 CompleteCalcHead;

   390  fetchProposedTactic 1; (*-> Apply_Method*);

   391  setNextTactic 1 (Apply_Method ["Test","solve_linear"]);

   392  autoCalculate 1 (Step 1);

   393  refFormula 1 (get_pos 1 1);

   395 ... works *)

   397  autoCalculate 1 (Step 1);

   398  refFormula 1 (get_pos 1 1);

   400  autoCalculate 1 CompleteModel;

   401  refFormula 1 (get_pos 1 1);

   403  autoCalculate 1 CompleteCalcHead;

   404 (* *** complete_mod: only impl.for Pbl, called with ([], Met) FIXXXXXXXXXXME*)

   408 "--------- maximum-example: complete_metitms ---------------------";

   409 "--------- maximum-example: complete_metitms ---------------------";

   410 "--------- maximum-example: complete_metitms ---------------------";

   411  val (p,_,f,nxt,_,pt) =

   412      CalcTreeTEST

   413      [(["fixedValues [r=Arbfix]","maximum A",

   414 	"valuesFor [a,b]",

   415 	"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

   416 	"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

   417 	"relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",

   419 	"boundVariable a","boundVariable b","boundVariable alpha",

   420 	"interval {x::real. 0 <= x & x <= 2*r}",

   421 	"interval {x::real. 0 <= x & x <= 2*r}",

   422 	"interval {x::real. 0 <= x & x <= pi}",

   423 	"errorBound (eps=(0::real))"],

   424        ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])

   425        )];

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

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

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

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

   430  val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;

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

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

   433  (*nxt = Specify_Theory "DiffApp.thy"*)

   434  val (oris, _, _) = get_obj g_origin pt (fst p);

   435  writeln (oris2str oris);

   436 (*[

   437 (1, ["1","2","3"], #Given,fixedValues, ["[r = Arbfix]"]),

   438 (2, ["1","2","3"], #Find,maximum, ["A"]),

   439 (3, ["1","2","3"], #Find,valuesFor, ["[a]","[b]"]),

   440 (4, ["1","2"], #Relate,relations, ["[A = a * b]","[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"]),

   441 (5, ["3"], #Relate,relations, ["[A = a * b]","[a / 2 = r * sin alpha]","[b / 2 = r * cos alpha]"]),

   442 (6, ["1"], #undef,boundVariable, ["a"]),

   443 (7, ["2"], #undef,boundVariable, ["b"]),

   444 (8, ["3"], #undef,boundVariable, ["alpha"]),

   445 (9, ["1","2"], #undef,interval, ["{x. 0 <= x & x <= 2 * r}"]),

   446 (10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),

   447 (11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*)

   448  val pits = get_obj g_pbl pt (fst p);

   449  writeln (itms2str thy pits);

   450 (*[

   451 (1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),

   452 (2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),

   453 (3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),

   454 (4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^

   455 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)

   456  val mits = get_obj g_met pt (fst p);

   457  val mits = complete_metitms oris pits []

   458 			((#ppc o get_met) ["DiffApp","max_by_calculus"]);

   459  writeln (itms2str thy mits);

   460 (*[

   461 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

   462 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),

   463 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),

   464 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^

   465 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),

   466 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),

   467 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.

   468 0 <= x & x <= 2 * r}])),

   469 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)

   470  if itms2str thy mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then ()

   471  else raise error "completetest.sml: new behav. in complete_metitms 1";

   474 "--------- maximum-example: complete_mod -------------------------";

   475 "--------- maximum-example: complete_mod -------------------------";

   476 "--------- maximum-example: complete_mod -------------------------";

   477  val (p,_,f,nxt,_,pt) =

   478      CalcTreeTEST

   479      [(["fixedValues [r=Arbfix]","maximum A",

   480 	"valuesFor [a,b]",

   481 	"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

   482 	"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

   483 	"relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",

   485 	"boundVariable a","boundVariable b","boundVariable alpha",

   486 	"interval {x::real. 0 <= x & x <= 2*r}",

   487 	"interval {x::real. 0 <= x & x <= 2*r}",

   488 	"interval {x::real. 0 <= x & x <= pi}",

   489 	"errorBound (eps=(0::real))"],

   490        ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])

   491        )];

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

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

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

   495  (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)

   496  val pits = get_obj g_pbl pt (fst p);

   497  writeln (itms2str thy pits);

   498 (*[

   499 (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),

   500 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),

   501 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

   502 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)

   503  val (pt,p) = complete_mod (pt,p);

   504  val pits = get_obj g_pbl pt (fst p);

   505  if itms2str thy pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]"

   506  then () else raise error "completetest.sml: new behav. in complete_mod 3";

   507  writeln (itms2str thy pits);

   508 (*[

   509 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

   510 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),

   511 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),

   512 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^

   513 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)

   514  val mits = get_obj g_met pt (fst p);

   515  if itms2str thy mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]"

   516  then () else raise error "completetest.sml: new behav. in complete_mod 3";

   517  writeln (itms2str thy mits);

   518 (*[

   519 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

   520 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),

   521 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),

   522 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^

   523 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),

   524 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),

   525 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.

   526 0 <= x & x <= 2 * r}])),

   527 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Wed, 21 Jul 2010 13:53:39 +0200
branch	isac-from-Isabelle2009-2
changeset 37871	875b6efa7ced
permissions	-rw-r--r--