wneuper/isa: test/Tools/isac/ProgLang/calculate.sml@491b133d154a

     1 (* Title:  test calculation of values for function constants

     2    Author: Walther Neuper 2000

     3    (c) copyright due to lincense terms.

     5 12345678901234567890123456789012345678901234567890123456789012345678901234567890

     6         10        20        30        40        50        60        70        80

     7 *)

     9 "--------------------------------------------------------";

    10 "table of contents --------------------------------------";

    11 "--------------------------------------------------------";

    12 "----------- check return value of get_calculation_  ----";

    13 "----------- fun calculate_ -----------------------------";

    14 "----------- fun calculate_ -----------------------------";

    15 "----------- calculate from script ----------------------";

    16 "----------- calculate check test-root-equ --------------";

    17 "----------- check calculate bottom up ------------------";

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

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

    20 "----------- get_pair with 3 args -----------------------";

    21 "----------- calculate (2 * x is_const) -----------------";

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

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

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

    27 "----------- check return value of get_calculation_  ----";

    28 "----------- check return value of get_calculation_  ----";

    29 "----------- check return value of get_calculation_  ----";

    30 val thy = theory "Poly";

    31 val cal = snd (assoc1 (! calclist', "is_polyexp"));

    32 val t = @{term "(x / x) is_polyexp"};

    33 val SOME (thmID, thm) = get_calculation_ thy cal t;

    34 (HOLogic.dest_Trueprop (prop_of thm); writeln "all thms wrapped by Trueprop")

    35 handle TERM _ =>

    36        error "calculate.sml: get_calculation_ must return Trueprop";

    38 "----------- fun calculate_ -----------------------------";

    39 "----------- fun calculate_ -----------------------------";

    40 "----------- fun calculate_ -----------------------------";

    41 val thy = theory "Test";

    42 "===== test 1";

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

    44 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;

    45 term2str (prop_of thm) = "1 + 2 = 3";

    47 "===== test 2";

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

    49 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;

    50 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;

    51 term2str t = "(3 * 4 / 3) ^^^ 2";

    53 "===== test 3: step into code";

    55 val ttt = str2term "2*3";

    57 get_calculation_ thy (the(assoc(calclist, "TIMES"))) ttt;

    58 (*===== inhibit exn ?===========================================================

    60 "===== test 3b -- 2 contiued";

    61 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t;

    62 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;

    63 term2str t;

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

    66 "===== test 4";

    67 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;

    68 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;

    69 term2str t;

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

    72 "===== test 5";

    73 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER")))t;

    74 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;

    75 term2str t;

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

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

    78 else ();

    82 "----------- calculate from script ----------------------";

    83 "----------- calculate from script ----------------------";

    84 "----------- calculate from script ----------------------";

    85 store_pbt

    86  (prep_pbt Test.thy "pbl_ttest" [] e_pblID

    87  (["test"],

    88   [],

    89   e_rls, NONE, []));

    90 store_pbt

    91  (prep_pbt Test.thy "pbl_ttest_calc" [] e_pblID

    92  (["calculate","test"],

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

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

    95    ],

    96   e_rls, NONE, [["Test","test_calculate"]]));

    98 store_met

    99  (prep_met Test.thy "met_testcal" [] e_metID

   100  (["Test","test_calculate"]:metID,

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

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

   103    ],

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

   105    calc=[("PLUS"    ,("op +"        ,eval_binop "#add_")),

   106 	 ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

   107 	 ("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_")),

   108 	 ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],

   109    crls=tval_rls, nrls=e_rls(*,

   110    asm_rls=[],asm_thm=[]*)},

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

   112   \(Repeat                                        \

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

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

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

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

   117    ));

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

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

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

   122 (*val p = e_pos'; val c = [];

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

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

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

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

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

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

   129 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)

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

   131 (*nxt = ("Specify_Theory",Specify_Theory "Test.thy") : string * tac*)

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

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

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

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

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

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

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

   140 (*nxt = ("Calculate",Calculate "PLUS")*)

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

   142 (*nxt = ("Calculate",Calculate "TIMES")*)

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

   144 (*nxt = ("Calculate",Calculate "DIVIDE")*)

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

   146 (*nxt = ("Calculate",Calculate "POWER")*)

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

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

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

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

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

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

   156 "----------- calculate check test-root-equ --------------";

   157 "----------- calculate check test-root-equ --------------";

   158 "----------- calculate check test-root-equ --------------";

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

   160 val ct =

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

   162 > val rls = ("Test_simplify");

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

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

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

   166 ie. cancel does not work properly

   167 *)

   168  val thy = "Test.thy";

   169  val op_ = "DIVIDE";

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

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

   172  val SOME (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;

   173  writeln ct;

   174 (*

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

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

   177 ............... does not work *)

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

   180  val thy = Test.thy;

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

   182  val rls = Test_simplify;

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

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

   186  val thy = "Test.thy";

   187  val t = "6 / 2";

   188  val rls = "Test_simplify";

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

   190 (*val t = "3" : string

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

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

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

   196  atomty t;

   197  rewrite_set_ Test.thy false tval_rls t;

   198 (*val it = SOME (Const ("True","bool"),[]) ... works*)

   200  val t = str2term "2 * x is_const";

   201  val SOME (str,t') = eval_const "" "" t Isac.thy;

   202  term2str t';

   205 "----------- check calculate bottom up ------------------";

   206 "----------- check calculate bottom up ------------------";

   207 "----------- check calculate bottom up ------------------";

   208 (*-------------- eval_cancel works: *)

   209  trace_rewrite:=true;

   210  val thy = Test.thy;

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

   212  val SOME (_,t) = eval_cancel "xxx" "HOL.divide" t thy;

   213  term2str t;

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

   215 (*-------------- but ... *)

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

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

   218 "(-2) + x";

   219 (*-------------- while ... *)

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

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

   222 "-2";

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

   225  val thy = "Test.thy";

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

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

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

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

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

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

   234  trace_rewrite:=true; (*3.6.03*)

   235  val thy = "Test.thy";

   236  val rls = "Test_simplify";

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

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

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

   240  trace_rewrite:=false;

   242  trace_rewrite:=true; (*3.6.03*)

   243  val thy = Test.thy;

   244  val rls = Test_simplify;

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

   246  val SOME (t',asm) = rewrite_set_ thy false rls t;

   247  term2str t';

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

   249  trace_rewrite:=false;

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

   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 ### trying thm 'rcollect_right'

   264 :

   265 "x + (-4) / 2"

   266 -------------------------------------while before Isabelle20002:

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

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

   269 :

   270 ### trying thm 'root_ge0_2'

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

   272 ### trying thm 'radd_real_const_eq'

   273 ### trying thm 'radd_real_const'

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

   275 ### rewrite_set_: x + #-2

   276 ### trying thm 'rcollect_right'

   277 :

   278 "#-2 + x"

   279 -----------------------------------------------------------------*)

   282  toggle trace_rewrite;

   283 (*===================*)

   284  trace_rewrite:=true;

   285  val thy' = "Test.thy";

   286  val rls = "Test_simplify";

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

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

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

   290 (*

   291 ### trying calc. 'cancel'

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

   293 @@@ get_pair: t else

   294 @@@ get_pair: t else -> NONE

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

   296 @@@ get_pair: then 1

   297 @@@ get_pair: t -> NONE

   298 @@@ get_pair: t1 -> NONE

   299 @@@ get_calculation: NONE

   300 ### trying calc. 'pow'

   301 *)

   303  trace_rewrite:=true;

   304  val thy' = "Test.thy";

   305  val rls = "Test_simplify";

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

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

   308 "(-2) + x";

   309 (*

   310 ### trying calc. 'cancel'

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

   312 @@@ get_pair: t else

   313 @@@ get_pair: t else -> NONE

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

   315 @@@ get_pair: then 1

   316 @@@ get_calculation: SOME #cancel_-4_2

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

   318 ### trying calc. 'cancel'

   319 *)

   320  trace_rewrite:=false;

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

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

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

   325 " ----------------- rewriting works ? -----------------------";

   326  val thy = Isac.thy;

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

   328  atomty prop;

   329 (*** -------------

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

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

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

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

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

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

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

   337  atomty prop';

   338 (*** -------------

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

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

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

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

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

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

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

   346  atomty t;

   347 (*** -------------

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

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

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

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

   352  atomty t;

   353 (*** -------------

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

   355 *** . Free ( aaa, real)

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

   357  val thm = num_str real_divide_1;

   358  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;

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

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

   363  atomty prop;

   364 (*** -------------

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

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

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

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

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

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

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

   372  atomty prop';

   373 (*** -------------

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

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

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

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

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

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

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

   381  atomty t;

   382 (*** -------------

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

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

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

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

   387  atomty t;

   388 (*** -------------

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

   390 *** . Free ( 1, real)

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

   392  val thm = num_str realpow_eq_one;

   393  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;

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

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

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

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

   400 val thy = Test.thy;

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

   402 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;

   403 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   404 "12 / 3 = 4";

   405 val thy = Test.thy;

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

   407 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER"))) t;

   408 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   409 "4 ^ 2 = 16";

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

   412  val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;

   413 "1 + 2 = 3";

   414  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   415  term2str t;

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

   417  val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES")))t;

   418 "3 * 4 = 12";

   419  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   420  term2str t;

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

   422  val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;

   423 "12 / 3 = 4";

   424  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   425  term2str t;

   426 "4 ^^^ 2";

   427  val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER")))t;

   428 "4 ^^^ 2 = 16";

   429  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;

   430  term2str t;

   431 "16";

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

   433  else ();

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

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

   437   val SOME (thmID,thm) =

   438       get_calculation_ thy (the(assoc(calclist,"POWER"))) t;

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

   441   val (op_, eval_fn) = the (assoc(calclist,"POWER"));

   442   (*

   443 val op_ = "Atools.pow" : string

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

   446   val SOME (thmid,t') = get_pair thy op_ eval_fn t;

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

   449   val SOME (id,t') = eval_fn op_ t thy;

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

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

   453   val SOME (id,t') = eval_binop thmid op_ t thy;

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

   457 "----------- get_pair with 3 args --------------------------------";

   458 "----------- get_pair with 3 args --------------------------------";

   459 "----------- get_pair with 3 args --------------------------------";

   460 val (thy, op_, ef, arg) =

   461     (thy, "EqSystem.occur'_exactly'_in",

   462      snd (the (assoc(!calclist',"occur_exactly_in"))),

   463      str2term

   464       "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"

   465       );

   466 val SOME (str, simpl) = get_pair thy op_ ef arg;

   467 if str =

   468 "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"

   469 then () else error "calculate.sml get_pair with 3 args:occur_exactly_in";

   472 "----------- calculate (2 * x is_const) -----------------";

   473 "----------- calculate (2 * x is_const) -----------------";

   474 "----------- calculate (2 * x is_const) -----------------";

   475 val t = str2term "2 * x is_const";

   476 val SOME (str, t') = eval_const "" "" t Test.thy;

   477 term2str t';

   478 "(2 * x is_const) = False";

   480 val SOME (t',_) = rewrite_set_ Test.thy false tval_rls t;

   481 term2str t';

   482 "False";

   483 ===== inhibit exn ?===========================================================*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 28 Sep 2010 10:01:18 +0200
branch	isac-update-Isa09-2
changeset 38033	491b133d154a
parent 38032	121765ba0a34
child 38034	928cebc9c4aa
permissions	-rw-r--r--