wneuper/isac: src/sml/systest/calculate.sml@90390fecbe74

     1 (* use"tests/calculate.sml";

     2    use"calculate.sml";

     3    *)

     4 (*contents

     5 " ================= calculate.sml: calculate_ ======================== ";

     6 " ================= calculate.sml: aus script ======================== ";

     7 " ================= calculate.sml: from test-root-equ.sml ================== ";

     8 " ================= calculate.sml: 2.8.02 check test-root-equ ======== ";

     9 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";

    10 " ================= calculate.sml: calculate_ 2002 =================== ";

    11 " ================= eval_binop Float  =================== ";

    12 *)

    14 (*  [("Var",("Tools.Var",fn)),("Length",("Tools.Length",fn)),

    15      ("Nth",("Tools.Nth",fn)),

    16    ("power_",("Atools.pow",fn)),("plus",("op +",fn)),("times",("op *",fn)),

    17    ("is_const",("Atools.is'_const",fn)),

    18    ("le",("op <",fn)),("leq",("op <=",fn)),

    19    ("ident",("Atools.ident",fn))]                                                      *)

    21 " ================= calculate.sml: calculate_ ======================== ";

    22 " ================= calculate.sml: calculate_ ======================== ";

    23 " ================= calculate.sml: calculate_ ======================== ";

    26 val thy = Test.thy;

    27 val t = (term_of o the o (parse thy)) "1+2";

    28 val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;

    30 val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";

    31 val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;

    32 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

    33 Sign.string_of_term (sign_of thy) t;

    34 (*val it = "(#3 * #4 // #3) ^^^ #2" : string*)

    35 val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;

    36 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

    37 Sign.string_of_term (sign_of thy) t;

    38 (*val it = "(#12 // #3) ^^^ #2" : string*)

    39 val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;

    40 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

    41 Sign.string_of_term (sign_of thy) t;

    42 (*it = "#4 ^^^ #2" : string*)

    43 val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;

    44 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

    45 Sign.string_of_term (sign_of thy) t;

    46 (*val it = "#16" : string*)

    47 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"

    48 else ();

    50 " ================= calculate.sml: aus script ======================== ";

    51 " ================= calculate.sml: aus script ======================== ";

    52 " ================= calculate.sml: aus script ======================== ";

    54 store_pbt

    55  (prep_pbt Test.thy

    56  (["test"],

    57   [],

    58   e_rls, None, []));

    59 store_pbt

    60  (prep_pbt Test.thy

    61  (["calculate","test"],

    62   [("#Given" ,["realTestGiven t_"]),

    63    ("#Find"  ,["realTestFind s_"])

    64    ],

    65   e_rls, None, [("Test.thy","test_calculate")]));

    67 methods:= overwritel (!methods,

    68 [

    69  prep_met

    70  (("Test.thy","test_calculate"):metID,

    71   [("#Given" ,["realTestGiven t_"]),

    72    ("#Find"  ,["realTestFind s_"])

    73    ],

    74   {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls,

    75    calc=[("plus"    ,("op +"        ,eval_binop "#add_")),

    76 	 ("times"   ,("op *"        ,eval_binop "#mult_")),

    77 	 ("divide_" ,("HOL.divide"  ,eval_cancel "#divide_")),

    78 	 ("power_"  ,("Atools.pow"  ,eval_binop "#power_"))],

    79    asm_rls=[],asm_thm=[]},

    80   "Script STest_simplify (t_::real) =          \

    81   \(Repeat                                        \

    82   \ ((Try (Repeat (Calculate plus))) @@   \

    83   \  (Try (Repeat (Calculate times))) @@  \

    84   \  (Try (Repeat (Calculate divide_))) @@ \

    85   \  (Try (Repeat (Calculate power_))))) t_"

    86    )

    87 ]);

    89 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];

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

    91   ("Test.thy",["calculate","test"],("Test.thy","test_calculate"));

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

    93 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

    94 val (p,_,f,nxt,_,pt) = me (mI,m) p c  EmptyPtree;

    95 (*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*)

    96 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    97 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * mstep*)

    98 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    99 (*nxt = ("Specify_Domain",Specify_Domain "Test.thy") : string * mstep*)

   100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   101 (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)

   102 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   103 (*nxt = ("Specify_Method",Specify_Method ("Test.thy","test_calculate"))*)

   104 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   105 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_calculate"))*)

   106 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   107 (*nxt = ("Calculate",Calculate "plus")*)

   108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   109 (*nxt = ("Calculate",Calculate "times")*)

   110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   111 (*nxt = ("Calculate",Calculate "divide_")*)

   112 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   113 (*nxt = ("Calculate",Calculate "power_")*)

   114 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   115 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)

   116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   117 (*nxt = ("End_Proof'",End_Proof')*)

   118 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()

   119 else raise error "calculate.sml: script test_calculate changed behaviour";

   124 " ================= calculate.sml: from test-root-equ.sml ================== ";

   125 " ================= calculate.sml: from test-root-equ.sml ================== ";

   126 " ================= calculate.sml: from test-root-equ.sml ================== ";

   127 val thy' = "Test.thy";

   128 val ct = "1 + 2";

   129 val (ct,thm') = the (calculate thy' (the(assoc(calclist,"plus"))) ct);

   130 (*val ct = "#3" : string

   131 val thm' = ("#add_#1_#2","\"#1 + #2 = #3\"") : thm'*)

   133 "----- me -----";

   134 val (dI',pI',mI') = ("Test.thy",e_pblID,

   135 		     ("Test.thy","sqrt-equ-test"));

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

   137 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));

   138 val (p,_,_,_,_,pt) = me (mI,m) p c  EmptyPtree;

   139 val nxt = ("Specify_Domain",Specify_Domain "Test.thy");

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

   141 val (pt,_) = cappend_atomic pt [1] e_istate "1 + 2"

   142     (Calculate "test") ct Complete;

   143 val p = ([1],Frm):pos';

   144 val nxt = ("Calculate",Calculate "plus");

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

   146 Compiler.Control.Print.printDepth:=9; (*4 default*)

   147 (* Nd (PblObj...

   148       [Nd (PrfObj

   149       {branch=NoBranch,cell=[],form="#1 + #2",loc=(([],None),([],None)),

   150       mstep=Calculate "plus",ostate=Complete,result="#3"},[])]) : squ*)

   151 Compiler.Control.Print.printDepth:=4; (*4 default*)

   153 val (pt,_) = cappend_atomic pt [1] e_istate "6/4"

   154     (Calculate "test") ct Complete;

   155 val p = ([1],Frm):pos';

   156 val nxt = ("Calculate",Calculate "divide_");

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

   158 (*{branch=NoBranch,cell=[],form="#6 // #4",loc=(([],None),([],None)),

   159   mstep=Calculate "divide_",ostate=Complete,result="#3 // #2"},[])]) *)

   161 (*5.7.00: interne ops in calclist*)

   164 " ================= calculate.sml: 2.8.02 check test-root-equ ======== ";

   165 " ================= calculate.sml: 2.8.02 check test-root-equ ======== ";

   166 " ================= calculate.sml: 2.8.02 check test-root-equ ======== ";

   167 (*(1): 2nd Test_simplify didn't work:

   168 val ct =

   169   "sqrt (x ^^^ 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"

   170 > val rls = ("Test_simplify");

   171 > val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);

   172 val ct = "sqrt (x ^^^ 2 + -3 * x) =

   173 (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";

   174 ie. cancel does not work properly

   175 *)

   176  val thy = "Test.thy";

   177  val op_ = "divide_";

   178  val ct = "sqrt (x ^^^ 2 + -3 * x) =\

   179  \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";

   180  val Some (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;

   181  writeln ct;

   182 (*

   183            sqrt (x ^^^ 2 + -3 * x) =\

   184  \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))

   185 ............... does not work *)

   187 (*--------------(2): does divide work in Test_simplify ?: ------*)

   188  val thy = Test.thy;

   189  val t = (term_of o the o (parse thy)) "6 / 2";

   190  val rls = Test_simplify;

   191  val (t,_) = the (rewrite_set_ thy false rls t);

   192 (*val t = Free ("3","RealDef.real") : term*)

   194  val thy = "Test.thy";

   195  val t = "6 / 2";

   196  val rls = "Test_simplify";

   197  val (t,_) = the (rewrite_set thy false rls t);

   198 (*val t = "3" : string

   199       ....... works, thus: which rule in SqRoot_simplify works differently ?*)

   202 (*--------------(3): is_const works ?: -------------------------------------*)

   203  val t = (term_of o the o (parse Test.thy)) "2 is_const";

   204  atomty Test.thy t;

   205  rewrite_set_ Test.thy false tval_rls t;

   206 (*val it = Some (Const ("True","bool"),[]) ... works*)

   209 (*--------------(4): check bottom up: ---------------------------*)

   210 (*-------------- eval_cancel works: *)

   211  trace_rewrite:=true;

   212  val thy = Test.thy;

   213  val t = (term_of o the o (parse thy)) "(-4) / 2";

   214  val Some (_,t) = eval_cancel "xxx" 111 t thy;

   215  term2str t;

   216 "-4 / 2 = (-2)";

   217 (*-------------- but ... *)

   218  val ct = "x + (-4) / 2";

   219  val (ct,_) = the (rewrite_set thy' false rls ct);

   220 "(-2) + x";

   221 (*-------------- while ... *)

   222  val ct = "(-4) / 2";

   223  val (ct,_) = the (rewrite_set thy'  false rls ct);

   224 "(-2)";

   226 (*--------------(5): reproduce (1) with simpler term: ------------*)

   227  val thy = "Test.thy";

   228  val t = "(3+5)/2";

   229  val (t,_) = the (rewrite_set thy false rls t);

   230 (*val t = "4" ... works*)

   232  val t = "(3+1+2*x)/2";

   233  val (t,_) = the (rewrite_set thy false rls t);

   234 (*val t = "2 + x" ... works*)

   236  val t = "(3+(1+2*x))/2";

   237  val (t,_) = the (rewrite_set thy false rls t);

   238 (*val t = "2 + x" ... works: give up----------------------------------------*)

   242 (*--- trace_rewrite before correction of ... --------------------

   243  val ct = "(-3 + 2 * x + -1) / 2";

   244  val (ct,_) = the (rewrite_set thy'  false rls ct);

   245 :

   246 ### trying thm 'root_ge0_2'

   247 ### rewrite_set_: x + (-1 + -3) / 2

   248 ### trying thm 'radd_real_const_eq'

   249 ### trying thm 'radd_real_const'

   250 ### rewrite_set_: x + (-4) / 2

   251 ### trying thm 'rcollect_right'

   252 :

   253 "x + (-4) / 2"

   254 -------------------------------------while before Isabelle20002:

   255  val ct = "(#-3 + #2 * x + #-1) // #2";

   256  val (ct,_) = the (rewrite_set thy'  false rls ct);

   257 :

   258 ### trying thm 'root_ge0_2'

   259 ### rewrite_set_: x + (#-1 + #-3) // #2

   260 ### trying thm 'radd_real_const_eq'

   261 ### trying thm 'radd_real_const'

   262 ### rewrite_set_: x + #-4 // #2

   263 ### rewrite_set_: x + #-2

   264 ### trying thm 'rcollect_right'

   265 :

   266 "#-2 + x"

   267 -----------------------------------------------------------------*)

   270  toggle trace_rewrite;

   271 (*===================*)

   272  trace_rewrite:=true;

   273  val thy' = "Test.thy";

   274  val rls = "Test_simplify";

   275  val ct = "x + (-1 + -3) / 2";

   276  val (ct,_) = the (rewrite_set thy'  false rls ct);

   277 "x + (-4) / 2";

   278 (*

   279 ### trying calc. 'cancel'

   280 @@@ get_pair: binop, t = x + (-4) / 2

   281 @@@ get_pair: t else

   282 @@@ get_pair: t else -> None

   283 @@@ get_pair: binop, t = (-4) / 2

   284 @@@ get_pair: then 1

   285 @@@ get_pair: t -> None

   286 @@@ get_pair: t1 -> None

   287 @@@ get_calculation: None

   288 ### trying calc. 'pow'

   289 *)

   291  trace_rewrite:=true;

   292  val thy' = "Test.thy";

   293  val rls = "Test_simplify";

   294  val ct = "x + (-4) / 2";

   295  val (ct,_) = the (rewrite_set thy'  false rls ct);

   296 "(-2) + x";

   297 (*

   298 ### trying calc. 'cancel'

   299 @@@ get_pair: binop, t = x + -4 / 2

   300 @@@ get_pair: t else

   301 @@@ get_pair: t else -> None

   302 @@@ get_pair: binop, t = -4 / 2

   303 @@@ get_pair: then 1

   304 @@@ get_calculation: Some #cancel_-4_2

   305 ### calc. to: x + (-2)

   306 ### trying calc. 'cancel'

   307 *)

   308  trace_rewrite:=false;

   310 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";

   311 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";

   312 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";

   313 " ----------------- rewriting works ? -----------------------";

   314  val thy = Isac.thy;

   315  val prop = (#prop o rep_thm) real_divide_1;

   316  atomty thy prop;

   317 (*** -------------

   318 *** Const ( Trueprop, bool => prop)

   319 *** . Const ( op =, [real, real] => bool)

   320 *** . . Const ( HOL.divide, [real, real] => real)

   321 *** . . . Var ((x, 0), real)

   322 *** . . . Const ( 1, real)

   323 *** . . Var ((x, 0), real) *)

   324  val prop' = (#prop o rep_thm o num_str) real_divide_1;

   325  atomty thy prop';

   326 (*** -------------

   327 *** Const ( Trueprop, bool => prop)

   328 *** . Const ( op =, [real, real] => bool)

   329 *** . . Const ( HOL.divide, [real, real] => real)

   330 *** . . . Var ((x, 0), real)

   331 *** . . . Free ( 1, real)   (*app_num_tr'*)

   332 *** . . Var ((x, 0), real)*)

   333  val t = (term_of o the o (parseold thy)) "aaa/1";

   334  atomty thy t;

   335 (*** -------------

   336 *** Const ( HOL.divide, ['a, 'a] => 'a)

   337 *** . Free ( aaa, 'a)

   338 *** . Free ( 1, 'a) *)

   339  val t = (term_of o the o (parse thy)) "aaa/1";

   340  atomty thy t;

   341 (*** -------------

   342 *** Const ( HOL.divide, [real, real] => real)

   343 *** . Free ( aaa, real)

   344 *** . Free ( 1, real)  *)

   345  val thm = num_str real_divide_1;

   346  val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   347 (*val t = Free ("aaa","RealDef.real") : term*)

   350  val prop = (#prop o rep_thm) realpow_eq_one;

   351  atomty thy prop;

   352 (*** -------------

   353 *** Const ( Trueprop, bool => prop)

   354 *** . Const ( op =, [real, real] => bool)

   355 *** . . Const ( Nat.power, [real, nat] => real)

   356 *** . . . Const ( 1, real)

   357 *** . . . Var ((n, 0), nat)

   358 *** . . Const ( 1, real) *)

   359  val prop' = (#prop o rep_thm o num_str) realpow_eq_one;

   360  atomty thy prop';

   361 (*** -------------

   362 *** Const ( Trueprop, bool => prop)

   363 *** . Const ( op =, [real, real] => bool)

   364 *** . . Const ( Nat.power, [real, nat] => real)

   365 *** . . . Free ( 1, real)

   366 *** . . . Var ((n, 0), nat)

   367 *** . . Free ( 1, real)*)

   368  val t = (term_of o the o (parseold thy)) "1 ^ aaa";

   369  atomty thy t;

   370 (*** -------------

   371 *** Const ( Nat.power, ['a, nat] => 'a)

   372 *** . Free ( 1, 'a)

   373 *** . Free ( aaa, nat) *)

   374  val t = (term_of o the o (parse thy)) "1 ^ aaa";

   375  atomty thy t;

   376 (*** -------------

   377 *** Const ( Nat.power, [real, nat] => real)

   378 *** . Free ( 1, real)

   379 *** . Free ( aaa, nat) .......................... nat !!! *)

   380  val thm = num_str realpow_eq_one;

   381  val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   382 (*val t = Free ("1","RealDef.real") : term*)

   384 " ================= calculate.sml: calculate_ 2002 =================== ";

   385 " ================= calculate.sml: calculate_ 2002 =================== ";

   386 " ================= calculate.sml: calculate_ 2002 =================== ";

   388 val thy = Test.thy;

   389 val t = (term_of o the o (parse thy)) "12 / 3";

   390 val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;

   391 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   392 "12 / 3 = 4";

   393 val thy = Test.thy;

   394 val t = (term_of o the o (parse thy)) "4 ^^^ 2";

   395 val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_"))) t;

   396 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   397 "4 ^ 2 = 16";

   399  val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";

   400  val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;

   401 "1 + 2 = 3";

   402  val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   403  Sign.string_of_term (sign_of thy) t;

   404 "(3 * 4 / 3) ^^^ 2";

   405  val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t;

   406 "3 * 4 = 12";

   407  val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   408  Sign.string_of_term (sign_of thy) t;

   409 "(12 / 3) ^^^ 2";

   410  val Some (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t;

   411 "12 / 3 = 4";

   412  val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   413  Sign.string_of_term (sign_of thy) t;

   414 "4 ^^^ 2";

   415  val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;

   416 "4 ^^^ 2 = 16";

   417  val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   418  Sign.string_of_term (sign_of thy) t;

   419 "16";

   420  if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"

   421  else ();

   423 (*13.9.02 *** calc: operator = pow not defined*)

   424   val t = (term_of o the o (parse thy)) "3^^^2";

   425   val Some (thmID,thm) =

   426       get_calculation_ thy (the(assoc(calclist,"power_"))) t;

   427 (*** calc: operator = pow not defined*)

   429   val (op_, eval_fn) = the (assoc(calclist,"power_"));

   430   (*

   431 val op_ = "Atools.pow" : string

   432 val eval_fn = fn : string -> term -> theory -> (string * term) option*)

   434   val Some (thmid,t') = get_pair thy op_ eval_fn t;

   435 (*** calc: operator = pow not defined*)

   437   val Some (id,t') = eval_fn op_ t thy;

   438 (*** calc: operator = pow not defined*)

   440   val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t);

   441   val Some (id,t') = eval_binop thmid op_ t thy;

   442 (*** calc: operator = pow not defined*)

   446 " ================= eval_binop Float  =================== ";

   447 val t = str2term "Float ((1,2),(0,0))";

   448 atomty thy t;

   449 val Const ("Float.Float",_) $

   450 	  (Const ("Pair",_) $

   451 		 (Const ("Pair",_) $ Free (i1,_) $ Free (i2,_)) $ _) = t;

   453 val t = str2term "Float ((1,2),(0,0)) * Float ((3,4),(0,0))";

   454 atomty thy t;

   455 (*GOON.10.4.03*)

author	agriesma
	Thu, 17 Apr 2003 18:01:03 +0200
branch	griesmayer
changeset 338	90390fecbe74
child 708	7d3338563b8c
permissions	-rw-r--r--