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

     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 3b -- 2 contiued";

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

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

    56 term2str t;

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

    59 "===== test 4";

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

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

    62 term2str t;

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

    65 "===== test 5";

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

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

    68 term2str t;

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

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

    71 else ();

    73 "----------- calculate from script ----------------------";

    74 "----------- calculate from script ----------------------";

    75 "----------- calculate from script ----------------------";

    76 store_pbt

    77  (prep_pbt (theory "Test") "pbl_ttest" [] e_pblID

    78  (["test"],

    79   [],

    80   e_rls, NONE, []));

    81 store_pbt

    82  (prep_pbt (theory "Test") "pbl_ttest_calc" [] e_pblID

    83  (["calculate","test"],

    84   [("#Given" ,["realTestGiven t_t"]),

    85    ("#Find"  ,["realTestFind s_s"])

    86    ],

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

    89 store_met

    90  (prep_met (theory "Test") "met_testcal" [] e_metID

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

    92   [("#Given" ,["realTestGiven t_t"]),

    93    ("#Find"  ,["realTestFind s_s"])

    94    ],

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

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

    97 	 ("TIMES"   ,("Groups.times_class.times"        ,eval_binop "#mult_")),

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

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

   100    crls=tval_rls, nrls=e_rls(*,

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

   102   "Script STest_simplify (t_t::real) =          \

   103   \(Repeat                                        \

   104   \ ((Try (Repeat (Calculate PLUS))) @@   \

   105   \  (Try (Repeat (Calculate TIMES))) @@  \

   106   \  (Try (Repeat (Calculate DIVIDE))) @@ \

   107   \  (Try (Repeat (Calculate POWER))))) t_t"

   108    ));

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

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

   112   ("Test",["calculate","test"],["Test","test_calculate"]);

   115 (*===== inhibit exn ?===========================================================

   116 GOON after rewriting works

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

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

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

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

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

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

   124 (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)

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

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

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

   128 (*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)

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

   130 (*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   153 val ct =

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

   155 > val rls = ("Test_simplify");

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

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

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

   159 ie. cancel does not work properly

   160 *)

   161  val thy = "Test";

   162  val op_ = "DIVIDE";

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

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

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

   166  writeln ct;

   167 (*

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

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

   170 ............... does not work *)

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

   173  val thy = Test.thy;

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

   175  val rls = Test_simplify;

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

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

   179  val thy = "Test";

   180  val t = "6 / 2";

   181  val rls = "Test_simplify";

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

   183 (*val t = "3" : string

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

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

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

   189  atomty t;

   190  rewrite_set_ Test.thy false tval_rls t;

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

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

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

   195  term2str t';

   198 "----------- check calculate bottom up ------------------";

   199 "----------- check calculate bottom up ------------------";

   200 "----------- check calculate bottom up ------------------";

   201 (*-------------- eval_cancel works: *)

   202  trace_rewrite:=true;

   203  val thy = Test.thy;

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

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

   206  term2str t;

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

   208 (*-------------- but ... *)

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

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

   211 "(-2) + x";

   212 (*-------------- while ... *)

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

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

   215 "-2";

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

   218  val thy = "Test";

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

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

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

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

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

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

   227  trace_rewrite:=true; (*3.6.03*)

   228  val thy = "Test";

   229  val rls = "Test_simplify";

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

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

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

   233  trace_rewrite:=false;

   235  trace_rewrite:=true; (*3.6.03*)

   236  val thy = Test.thy;

   237  val rls = Test_simplify;

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

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

   240  term2str t';

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

   242  trace_rewrite:=false;

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

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

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

   250 :

   251 ### trying thm 'root_ge0_2'

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

   253 ### trying thm 'radd_real_const_eq'

   254 ### trying thm 'radd_real_const'

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

   256 ### trying thm 'rcollect_right'

   257 :

   258 "x + (-4) / 2"

   259 -------------------------------------while before Isabelle20002:

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

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

   262 :

   263 ### trying thm 'root_ge0_2'

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

   265 ### trying thm 'radd_real_const_eq'

   266 ### trying thm 'radd_real_const'

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

   268 ### rewrite_set_: x + #-2

   269 ### trying thm 'rcollect_right'

   270 :

   271 "#-2 + x"

   272 -----------------------------------------------------------------*)

   275  toggle trace_rewrite;

   276 (*===================*)

   277  trace_rewrite:=true;

   278  val thy' = "Test";

   279  val rls = "Test_simplify";

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

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

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

   283 (*

   284 ### trying calc. 'cancel'

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

   286 @@@ get_pair: t else

   287 @@@ get_pair: t else -> NONE

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

   289 @@@ get_pair: then 1

   290 @@@ get_pair: t -> NONE

   291 @@@ get_pair: t1 -> NONE

   292 @@@ get_calculation: NONE

   293 ### trying calc. 'pow'

   294 *)

   296  trace_rewrite:=true;

   297  val thy' = "Test";

   298  val rls = "Test_simplify";

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

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

   301 "(-2) + x";

   302 (*

   303 ### trying calc. 'cancel'

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

   305 @@@ get_pair: t else

   306 @@@ get_pair: t else -> NONE

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

   308 @@@ get_pair: then 1

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

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

   311 ### trying calc. 'cancel'

   312 *)

   313  trace_rewrite:=false;

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

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

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

   318 " ----------------- rewriting works ? -----------------------";

   319  val thy = Isac.thy;

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

   321  atomty prop;

   322 (*** -------------

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

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

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

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

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

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

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

   330  atomty prop';

   331 (*** -------------

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

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

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

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

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

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

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

   339  atomty t;

   340 (*** -------------

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

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

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

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

   345  atomty t;

   346 (*** -------------

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

   348 *** . Free ( aaa, real)

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

   350  val thm = num_str real_divide_1;

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

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

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

   356  atomty prop;

   357 (*** -------------

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

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

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

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

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

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

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

   365  atomty prop';

   366 (*** -------------

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

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

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

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

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

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

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

   374  atomty t;

   375 (*** -------------

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

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

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

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

   380  atomty t;

   381 (*** -------------

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

   383 *** . Free ( 1, real)

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

   385  val thm = num_str realpow_eq_one;

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

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

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

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

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

   393 val thy = Test.thy;

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

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

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

   397 "12 / 3 = 4";

   398 val thy = Test.thy;

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

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

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

   402 "4 ^ 2 = 16";

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

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

   406 "1 + 2 = 3";

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

   408  term2str t;

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

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

   411 "3 * 4 = 12";

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

   413  term2str t;

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

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

   416 "12 / 3 = 4";

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

   418  term2str t;

   419 "4 ^^^ 2";

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

   421 "4 ^^^ 2 = 16";

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

   423  term2str t;

   424 "16";

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

   426  else ();

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

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

   430   val SOME (thmID,thm) =

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

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

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

   435   (*

   436 val op_ = "Atools.pow" : string

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

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

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

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

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

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

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

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

   450 "----------- get_pair with 3 args --------------------------------";

   451 "----------- get_pair with 3 args --------------------------------";

   452 "----------- get_pair with 3 args --------------------------------";

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

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

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

   456      str2term

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

   458       );

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

   460 if str =

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

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

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

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

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

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

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

   470 term2str t';

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

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

   474 term2str t';

   475 "False";

   476 ===== inhibit exn ?===========================================================*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 28 Sep 2010 13:30:29 +0200
branch	isac-update-Isa09-2
changeset 38035	cd7854f2636d
parent 38034	928cebc9c4aa
child 38037	a51a70334191
permissions	-rw-r--r--