Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/ProgLang/calculate.sml
author Walther Neuper <neuper@ist.tugraz.at>
Thu, 23 Sep 2010 14:49:23 +0200
branchisac-update-Isa09-2
changeset 38014 3e11e3c2dc42
parent 37969 81922154e742
child 38022 e6d356fc4d38
permissions -rw-r--r--
updated "op +", "op -", "op *". "HOL.divide" in src & test

find . -type f -exec sed -i s/"\"op +\""/"\"Groups.plus_class.plus\""/g {} \;
find . -type f -exec sed -i s/"\"op -\""/"\"Groups.minus_class.minus\""/g {} \;
find . -type f -exec sed -i s/"\"op *\""/"\"Groups.times_class.times\""/g {} \;
find . -type f -exec sed -i s/"\"HOL.divide\""/"\"Rings.inverse_class.divide\""/g {} \; 
     1 (* test calculation of values for function constants

     2    (c) Walther Neuper 2000

     3 

     4 use"../smltest/Scripts/calculate.sml";

     5 use"calculate.sml";

     6 *)

     7 

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

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

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

    11 "--------------(4): check bottom up: ---------------------------";

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

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

    14 "----------- get_pair with 3 args --------------------------------";

    15 " ================= eval_binop Float  =================== ";

    16 "------------------ 3.6.03 (2 * x is_const) ---------------------------";

    17 

    18 (*  [("Vars",("Tools.Vars",fn)),("Length",("Tools.Length",fn)),

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

    20    ("power_",("Atools.pow",fn)),("plus",("Groups.plus_class.plus",fn)),("times",("op *",fn)),

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

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

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

    24 

    25 val thy' = "Isac.thy";

    26 

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

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

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

    30 

    31 

    32 val thy = Test.thy;

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

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

    35 

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

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

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

    39 Syntax.string_of_term (thy2ctxt thy) t;

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

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

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

    43 Syntax.string_of_term (thy2ctxt thy) t;

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

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

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

    47 Syntax.string_of_term (thy2ctxt thy) t;

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

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

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

    51 Syntax.string_of_term (thy2ctxt thy) t;

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

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

    54 else ();

    55 

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

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

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

    59 

    60 store_pbt

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

    62  (["test"],

    63   [],

    64   e_rls, NONE, []));

    65 store_pbt

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

    67  (["calculate","test"],

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

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

    70    ],

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

    72 

    73 store_met

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

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

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

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

    78    ],

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

    80    calc=[("plus"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),

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

    82 	 ("divide_" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_")),

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

    84    crls=tval_rls, nrls=e_rls(*,

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

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

    87   \(Repeat                                        \

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

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

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

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

    92    ));

    93 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   113 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   128 

   129 

   130 

   131 

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

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

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

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

   136 val ct =

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

   138 > val rls = ("Test_simplify");

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

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

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

   142 ie. cancel does not work properly

   143 *)

   144  val thy = "Test.thy";

   145  val op_ = "divide_";

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

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

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

   149  writeln ct;

   150 (*

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

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

   153 ............... does not work *)

   154 

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

   156  val thy = Test.thy;

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

   158  val rls = Test_simplify;

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

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

   161 

   162  val thy = "Test.thy";

   163  val t = "6 / 2";

   164  val rls = "Test_simplify";

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

   166 (*val t = "3" : string

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

   168 

   169 

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

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

   172  atomty t;

   173  rewrite_set_ Test.thy false tval_rls t;

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

   175 

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

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

   178  term2str t';

   179  

   180 

   181 

   182 

   183 "--------------(4): check bottom up: ---------------------------";

   184 (*-------------- eval_cancel works: *)

   185  trace_rewrite:=true;

   186  val thy = Test.thy;

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

   188  val SOME (_,t) = eval_cancel "xxx" "Rings.inverse_class.divide" t thy;

   189  term2str t;

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

   191 (*-------------- but ... *)

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

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

   194 "(-2) + x";

   195 (*-------------- while ... *)

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

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

   198 "-2";

   199 

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

   201  val thy = "Test.thy";

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

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

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

   205 

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

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

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

   209 

   210  trace_rewrite:=true; (*3.6.03*)

   211  val thy = "Test.thy";

   212  val rls = "Test_simplify";

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

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

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

   216  trace_rewrite:=false; 

   217 

   218  trace_rewrite:=true; (*3.6.03*)

   219  val thy = Test.thy;

   220  val rls = Test_simplify;

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

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

   223  term2str t';

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

   225  trace_rewrite:=false; 

   226 

   227 

   228 

   229 

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

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

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

   233 :

   234 ### trying thm 'root_ge0_2'

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

   236 ### trying thm 'radd_real_const_eq'

   237 ### trying thm 'radd_real_const'

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

   239 ### trying thm 'rcollect_right'

   240 :

   241 "x + (-4) / 2"

   242 -------------------------------------while before Isabelle20002:

   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 ### rewrite_set_: x + #-2

   252 ### trying thm 'rcollect_right'

   253 :

   254 "#-2 + x"

   255 -----------------------------------------------------------------*)

   256 

   257 

   258  toggle trace_rewrite;

   259 (*===================*)

   260  trace_rewrite:=true;

   261  val thy' = "Test.thy";

   262  val rls = "Test_simplify";		

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

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

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

   266 (*

   267 ### trying calc. 'cancel'

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

   269 @@@ get_pair: t else

   270 @@@ get_pair: t else -> NONE

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

   272 @@@ get_pair: then 1

   273 @@@ get_pair: t -> NONE

   274 @@@ get_pair: t1 -> NONE

   275 @@@ get_calculation: NONE

   276 ### trying calc. 'pow'

   277 *)

   278 

   279  trace_rewrite:=true;

   280  val thy' = "Test.thy";

   281  val rls = "Test_simplify";		

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

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

   284 "(-2) + x";

   285 (*

   286 ### trying calc. 'cancel'

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

   288 @@@ get_pair: t else

   289 @@@ get_pair: t else -> NONE

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

   291 @@@ get_pair: then 1

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

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

   294 ### trying calc. 'cancel'

   295 *)

   296  trace_rewrite:=false;

   297 

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

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

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

   301 " ----------------- rewriting works ? -----------------------";

   302  val thy = Isac.thy;

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

   304  atomty prop;

   305 (*** -------------

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

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

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

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

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

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

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

   313  atomty prop';

   314 (*** -------------

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

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

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

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

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

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

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

   322  atomty t;

   323 (*** -------------

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

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

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

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

   328  atomty t;

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

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

   331 *** . Free ( aaa, real)

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

   333  val thm = num_str @{thm divide_1};

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

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

   336 

   337 

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

   339  atomty prop;

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

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

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

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

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

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

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

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

   348  atomty prop';

   349 (*** -------------

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

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

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

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

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

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

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

   357  atomty t;

   358 (*** -------------

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

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

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

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

   363  atomty t;

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

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

   366 *** . Free ( 1, real)

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

   368  val thm = num_str @{thm realpow_eq_one;

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

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

   371 

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

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

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

   375 

   376 val thy = Test.thy;

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

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

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

   380 "12 / 3 = 4";

   381 val thy = Test.thy;

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

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

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

   385 "4 ^ 2 = 16";

   386 

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

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

   389 "1 + 2 = 3";

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

   391  Syntax.string_of_term (thy2ctxt thy) t;

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

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

   394 "3 * 4 = 12";

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

   396  Syntax.string_of_term (thy2ctxt thy) t;

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

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

   399 "12 / 3 = 4";

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

   401  Syntax.string_of_term (thy2ctxt thy) t;

   402 "4 ^^^ 2";

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

   404 "4 ^^^ 2 = 16";

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

   406  Syntax.string_of_term (thy2ctxt thy) t;

   407 "16";

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

   409  else ();

   410 

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

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

   413   val SOME (thmID,thm) = 

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

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

   416 

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

   418   (*

   419 val op_ = "Atools.pow" : string

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

   421 

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

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

   424 

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

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

   427 

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

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

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

   431 

   432  

   433 "----------- get_pair with 3 args --------------------------------";

   434 "----------- get_pair with 3 args --------------------------------";

   435 "----------- get_pair with 3 args --------------------------------";

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

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

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

   439      str2term

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

   441       );

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

   443 if str = 

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

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

   446 

   447 

   448 

   449 " ================= eval_binop Float  =================== ";

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

   451 atomty t;

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

   453 	  (Const ("Pair",_) $ 

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

   455     

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

   457 atomty t;

   458 (*WN.10.4.03 eval_binop Float *)

   459 

   460 

   461 "------------------ 3.6.03 (2 * x is_const) ---------------------------";

   462 "------------------ 3.6.03 (2 * x is_const) ---------------------------";

   463 "------------------ 3.6.03 (2 * x is_const) ---------------------------";

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

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

   466 term2str t';

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

   468 

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

   470 term2str t';

   471 "False";
wneuper/isa