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/evaluate.sml
author wneuper <walther.neuper@jku.at>
Sat, 03 Jul 2021 16:21:07 +0200
changeset 60318 e6e7a9b9ced7
parent 60317 638d02a9a96a
child 60324 5c7128feb370
permissions -rw-r--r--
//test/../rewrite.sml,poly.sml WORK 
     1 (* Title:  "ProgLang/evaluate.sml"

     2    Author: Walther Neuper 2000

     3    (c) copyright due to lincense terms.

     4 *)

     5 

     6 "--------------------------------------------------------";

     7 "table of contents --------------------------------------";

     8 "--------------------------------------------------------";

     9 "-calculate.thy: provides 'setup' -----------------------";

    10 "----------- fun norm -----------------------------------";

    11 "----------- check return value of adhoc_thm  ----";

    12 "----------- fun calculate_ --------------------------------------------------------------------";

    13 "----------- calculate from Prog --------------------------------- -----------------------------";

    14 "----------- calculate from script --requires 'setup'----";

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

    16 "----------- check calculate bottom up -----------------";

    17 "----------- Prog_Expr.pow Power.power_class.power ---------";

    18 " ================= evaluate.sml: calculate_ 2002 ======";

    19 "----------- fun cancel_int --------------------------------------------------------------------";

    20 "----------- RE-BUILD fun calcul ---------------------------------------------------------------";

    21 "----------- get_pair with 3 args -----------------------";

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

    23 "----------- fun get_pair: examples ------------------------------------------------------------";

    24 "----------- fun adhoc_thm: examples -----------------------------------------------------------";

    25 "----------- fun power -------------------------------------------------------------------------";

    26 "----------- fun divisors ----------------------------------------------------------------------";

    27 "----------- fun doubles, fun squfact ----------------------------------------------------------";

    28 "--------------------------------------------------------";

    29 "--------------------------------------------------------";

    30 "--------------------------------------------------------";

    31 

    32 "----------- check return value of adhoc_thm  ----";

    33 "----------- check return value of adhoc_thm  ----";

    34 "----------- check return value of adhoc_thm  ----";

    35 val thy = @{theory "Poly"};

    36 val cal = snd (assoc_calc' thy "is_polyexp");

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

    38 val SOME (thmID, thm) = adhoc_thm thy cal t;

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

    40 handle TERM _ => 

    41        error "evaluate.sml: adhoc_thm must return Trueprop";

    42 

    43 "----------- fun calculate_ --------------------------------------------------------------------";

    44 "----------- fun calculate_ --------------------------------------------------------------------";

    45 "----------- fun calculate_ --------------------------------------------------------------------";

    46 (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)

    47 val t = TermC.str2term "((1+2)*4/3) \<up> 2";

    48 val thy = @{theory};

    49 val times =  ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;

    50 val plus =   ("Groups.plus_class.plus", eval_binop "#add_") : string * Eval_Def.eval_fn;

    51 val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn;

    52 val pow =    ("Transcendental.powr", eval_binop "#power_") : string * Eval_Def.eval_fn;

    53 

    54 "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);

    55 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;

    56 val SOME (t', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;

    57 if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_  1 + 2 = 3  changed";

    58 

    59 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');

    60 val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t';

    61 val SOME (t'', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;

    62 if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_  3 * 4 = 12  changed";

    63 

    64 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');

    65 val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t;

    66 val SOME (t''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;

    67 if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_  12 / 3 = 4  changed";

    68 

    69 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');

    70 val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;

    71 val SOME (t'''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;

    72 if UnparseC.term t'''' = "16" then () else error "calculate_  12 / 3 = 4  changed";

    73 

    74 "----------- calculate from Prog --------------------------------- -----------------------------";

    75 "----------- calculate from Prog --------------------------------- -----------------------------";

    76 "----------- calculate from Prog --------------------------------- -----------------------------";

    77 val thy = @{theory "Test"};

    78 val fmz = ["realTestGiven (((1+2)*4/3) \<up> 2)", "realTestFind s"];

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

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

    81 

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

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

    84 (*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3)  \<up> #2)")*)

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

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

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

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

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

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

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

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

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

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

    95 

    96 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "PLUS")*)

    97 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "TIMES")*)

    98 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "DIVIDE")*)

    99 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "POWER")*)

   100 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Check_Postcond",Check_Postcond ["calculate", "test"])*)

   101 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("End_Proof'",End_Proof')*)

   102 case f of Test_Out.FormKF "16" => () | _ =>

   103 error "evaluate.sml: script test_calculate changed behaviour";

   104 

   105 

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

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

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

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

   110 val ct =

   111   "sqrt (x \<up> 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"

   112 > val rls = ("Test_simplify");

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

   114 val ct = "sqrt (x \<up> 2 + -3 * x) =

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

   116 ie. cancel does not work properly

   117 *)

   118  val thy = @{theory "Test"};

   119  val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));

   120  val ct = ThmC_Def.num_to_Free @{term

   121    "sqrt (x \<up> 2 + -3 * x) = (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"};

   122 case calculate_ thy op_ ct of

   123   SOME _ => ()

   124 | NONE => error "calculate_ test-root-equ changed";

   125 (*

   126            sqrt (x \<up> 2 + -3 * x) =\

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

   128 ............... does not work *)

   129 

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

   131  val thy = @{theory Test};

   132  val t = (Thm.term_of o the o (TermC.parse thy)) "6 / 2";

   133  val rls = Test_simplify;

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

   135 (*val t = Free ("3", "Real.real") : term*)

   136 

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

   138  val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_const";

   139  TermC.atomty t;

   140  rewrite_set_ @{theory Test} false tval_rls t;

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

   142 

   143  val t = TermC.str2term "2 * x is_const";

   144  val SOME (str,t') = eval_const "" "" t (@{theory "Isac_Knowledge"});

   145  UnparseC.term t';

   146  

   147 

   148 "----------- check calculate bottom up ------------------";

   149 "----------- check calculate bottom up ------------------";

   150 "----------- check calculate bottom up ------------------";

   151 (*-------------- eval_cancel works: *)

   152  Rewrite.trace_on := false;

   153  val thy = @{theory Test};

   154  val rls = Test_simplify;

   155  val t = (Thm.term_of o the o (TermC.parse thy)) "(-4) / 2";

   156 

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

   158 

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

   160  val t = (Thm.term_of o the o (TermC.parse thy)) "(3+5)/2";

   161 case rewrite_set_ thy false rls t of

   162   SOME (t', []) =>

   163     if UnparseC.term t' = "4" then ()

   164     else error "rewrite_set_ (3+5)/2 changed 1"

   165 | _ => error "rewrite_set_ (3+5)/2 changed 2";

   166 

   167  val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2";

   168 case rewrite_set_ thy false rls t of

   169   SOME (t', _) => 

   170     if UnparseC.term t' = "x + 2" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"

   171 | _ => error "rewrite_set_ (3+1+2*x)/2 changed 2";

   172 

   173  Rewrite.trace_on:=false; (*=true3.6.03*)

   174 

   175 (*--- Rewrite.trace_on before correction of ... --------------------

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

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

   178 :

   179 ### trying thm 'root_ge0_2'

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

   181 ### trying thm 'radd_real_const_eq'

   182 ### trying thm 'radd_real_const'

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

   184 ### trying thm 'rcollect_right'

   185 :

   186 "x + (-4) / 2"

   187 -------------------------------------while before Isabelle20002:

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

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

   190 :

   191 ### trying thm 'root_ge0_2'

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

   193 ### trying thm 'radd_real_const_eq'

   194 ### trying thm 'radd_real_const'

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

   196 ### rewrite_set_: x + #-2

   197 ### trying thm 'rcollect_right'

   198 :

   199 "#-2 + x"

   200 -----------------------------------------------------------------*)

   201 

   202 

   203 (*===================*)

   204  Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)

   205  val t = (Thm.term_of o the o (TermC.parse thy))  "x + (-1 + -3) / 2";

   206 val SOME (res, []) = rewrite_set_ thy false rls t;

   207 if UnparseC.term res = "x + - 2" then () else error "rewrite_set_  x + (-1 + -3) / 2  changed";

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

   209 (*

   210 ### trying calc. 'cancel'

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

   212 @@@ get_pair: t else

   213 @@@ get_pair: t else -> NONE

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

   215 @@@ get_pair: then 1

   216 @@@ get_pair: t -> NONE

   217 @@@ get_pair: t1 -> NONE

   218 @@@ adhoc_thm': NONE

   219 ### trying calc. 'pow'

   220 *)

   221 

   222  Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)

   223 

   224 " ================= evaluate.sml: calculate_ 2002 =================== ";

   225 " ================= evaluate.sml: calculate_ 2002 =================== ";

   226 " ================= evaluate.sml: calculate_ 2002 =================== ";

   227 

   228 val thy = @{theory Test};

   229 val t = (Thm.term_of o the o (TermC.parse thy)) "12 / 3";

   230 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;

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

   232 "12 / 3 = 4";

   233 val thy = @{theory Test};

   234 val t = (Thm.term_of o the o (TermC.parse thy)) "4 \<up> 2";

   235 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;

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

   237 "4 ^ 2 = 16";

   238 

   239  val t = (Thm.term_of o the o (TermC.parse thy)) "((1 + 2) * 4 / 3) \<up> 2";

   240  val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;

   241 "1 + 2 = 3";

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

   243  UnparseC.term t;

   244 "(3 * 4 / 3) \<up> 2";

   245  val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;

   246 "3 * 4 = 12";

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

   248  UnparseC.term t;

   249 "(12 / 3) \<up> 2";

   250  val SOME (thmID,thm) =adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;

   251 "12 / 3 = 4";

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

   253  UnparseC.term t;

   254 "4 \<up> 2";

   255  val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;

   256 "4 \<up> 2 = 16";

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

   258  UnparseC.term t;

   259 "16";

   260  if it <> "16" then error "evaluate.sml: new behaviour in calculate_"

   261  else ();

   262 

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

   264   val t = (Thm.term_of o the o (TermC.parse thy)) "3 \<up> 2";

   265   val SOME (thmID,thm) = 

   266       adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;

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

   268 

   269   val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));

   270   (*

   271 val op_ = "Transcendental.powr" : string

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

   273 

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

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

   276 

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

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

   279 

   280 case (op_, t) of

   281   ("Transcendental.powr",

   282     Const ("Transcendental.powr", _) $ (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))) $

   283       (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _)))) => ()

   284 | _ => error "3 \<up> 2 CHANGED";

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

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

   287 

   288 if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop  3 \<up> 2 = 9  CHANGED";

   289 

   290 

   291 "----------- fun cancel_int --------------------------------------------------------------------";

   292 "----------- fun cancel_int --------------------------------------------------------------------";

   293 "----------- fun cancel_int --------------------------------------------------------------------";

   294 if cancel_int (~4, 2) = (~1, (2, 1)) then () else error "cancel_int (~4, 2) CHANGED";

   295 if cancel_int (4, ~8) = (~1, (1, 2)) then () else error "cancel_int (4, ~8) CHANGED";

   296 if cancel_int (6, 4) = (1, (3, 2)) then () else error "cancel_int (6, 4)CHANGED";

   297 

   298 

   299 "----------- RE-BUILD fun calcul ---------------------------------------------------------------";

   300 "----------- RE-BUILD fun calcul ---------------------------------------------------------------";

   301 "----------- RE-BUILD fun calcul ---------------------------------------------------------------";

   302 val (t1, t2) = (@{term 3}, @{term "2::real"});

   303 

   304 "~~~~~ fun calcul , args:"; val (op_, (t1, t2)) = ("Groups.plus_class.plus", (t1, t2));

   305     val (Const ("Num.numeral_class.numeral", _) $ n1) = t1;

   306     val (Const ("Num.numeral_class.numeral", _) $ n2) = t2;

   307     val (T, _) = HOLogic.dest_number t1

   308     val (i1, i2) = (HOLogic.dest_numeral n1, HOLogic.dest_numeral n2)

   309     val result =

   310       case op_ of

   311         "Groups.plus_class.plus" => i1 + i2

   312       | "Groups.minus_class.minus" => i1 - i2

   313       | "Groups.times_class.times" => i1 * i2

   314       | "Transcendental.powr" => power i1 i2

   315       | str => raise ERROR ("calcul not impl.for op_ " ^ str)

   316   (*in*)

   317     val xxx = HOLogic.mk_number T result;

   318   (*end*)

   319 case HOLogic.dest_number xxx of

   320   (_, 5) => ()

   321 | _ => error "calcul + 2 3 CHANGED";

   322 

   323 case HOLogic.dest_number (calcul "Groups.minus_class.minus" (t1, t2)) of

   324   (_, 1) => xxx

   325 | _ => error "calcul - 2 3 CHANGED";

   326 

   327 case HOLogic.dest_number (calcul "Groups.times_class.times" (t1, t2)) of

   328   (_, 6) => xxx

   329 | _ => error "calcul - 2 3 CHANGED";

   330 

   331 (*                       (calcul "Rings.divide_class.divide" (t1, t2)

   332 ERROR: calcul not impl.for op_ Rings.divide_class.divide*)

   333 

   334 case HOLogic.dest_number (calcul "Transcendental.powr" (t1, t2)) of

   335   (_, 9) => xxx

   336 | _ => error "calcul - 2 3 CHANGED";

   337 

   338 

   339 "----------- get_pair with 3 args --------------------------------";

   340 "----------- get_pair with 3 args --------------------------------";

   341 "----------- get_pair with 3 args --------------------------------";

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

   343     (thy, "EqSystem.occur_exactly_in", 

   344      assoc_calc' (@{theory "EqSystem"}) "occur_exactly_in" |> snd |> snd,

   345      TermC.str2term

   346       "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L \<up> 2) / 2"

   347       );

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

   349 if str = 

   350 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2 = True"

   351 then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in";

   352 

   353 

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

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

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

   357 val t = TermC.str2term "2 * x is_const";

   358 val SOME (str, t') = eval_const "" "" t @{theory Test};

   359 if UnparseC.term t' = "(2 * x is_const) = False" then ()

   360 else error "eval_const 2 * x is_const CHANGED";

   361 

   362 val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;

   363 if UnparseC.term t' = "False" then ()

   364 else error "rewrite_set_ 2 * x is_const CHANGED";

   365 

   366 "----------- fun get_pair: examples ------------------------------------------------------------";

   367 "----------- fun get_pair: examples ------------------------------------------------------------";

   368 "----------- fun get_pair: examples ------------------------------------------------------------";

   369 val thy = @{theory};

   370 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");

   371 if isa_str = "Groups.plus_class.plus" then () else error "eval_fn PLUS changed";

   372 

   373 val t = @{term "3 + 4 :: real"};

   374 val SOME (str, term) = get_pair thy isa_str eval_fn t;

   375 (*+*)if str =  "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7"

   376 (*+*)then () else error "get_pair  3 + 4  changed";

   377 

   378 val t = @{term "(a + 3) + 4 :: real"};

   379 val SOME (str, term) = get_pair thy isa_str eval_fn t;

   380 if str =  "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"

   381 then () else error "get_pair  (a + 3) + 4  changed";

   382 

   383 val t = @{term "(a + 3) + 4 :: real"};

   384 val SOME (str, term) = get_pair thy isa_str eval_fn t;

   385 if str =  "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"

   386 then () else error "get_pair  (a + 3) + 4  changed";

   387 

   388 val t = @{term "x = 5 * (3 + (4 + a) :: real)"};

   389 val SOME (str, term) = get_pair thy isa_str eval_fn t;

   390 if str =  "#: 3 + (4 + a) = 7 + a" andalso UnparseC.term term = "3 + (4 + a) = 7 + a"

   391 then ((* !!! gets subterm !!!*)) else error "get_pair  x = 5 * (3 + (4 + a))  (subterm) changed";

   392 

   393 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");

   394 

   395 val t = @{term "-4 / -2 :: real"};

   396 val SOME (str, term) = get_pair thy isa_str eval_fn t;

   397 if str = "#divide_e~4_~2" andalso UnparseC.term term = "- 4 / - 2 = 2"

   398 then () else error "get_pair  -4 / -2   changed";

   399 

   400 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");

   401 

   402 val t = @{term "2 \<up> 3 :: real"};

   403 val SOME (str, term) = get_pair thy isa_str eval_fn t;

   404 if str =  "#: 2 \<up> 3 = 8" andalso UnparseC.term term = "2 \<up> 3 = 8"

   405 then () else error "get_pair  2 \<up> 3   changed";

   406 

   407 "----------- fun adhoc_thm: examples -----------------------------------------------------------";

   408 "----------- fun adhoc_thm: examples -----------------------------------------------------------";

   409 "----------- fun adhoc_thm: examples -----------------------------------------------------------";

   410 (*--------------------------------------------------------------------vvvvvvvvvv*)

   411 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_const");

   412 val t = @{term "9 is_const"};

   413 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;

   414 if str = "#is_const_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_const) = True"

   415 then () else error "adhoc_thm  9 is_const  changed";

   416 

   417 case assoc_calc thy "Orderings.ord_class.less" of

   418   "le" => () | _ => error "Orderings.ord_class.less <-> le changed";

   419 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "le");

   420 if isa_str = "Orderings.ord_class.less" then () else error "adhoc_thm (4 < 4) = False CHANGED";

   421 

   422 val t = @{term "4 < (4 :: real)"};

   423 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;

   424 if str = "#less_4_4" andalso ThmC_Def.string_of_thm thm = "(4 < 4) = False"

   425 then () else error "adhoc_thm  4 < 4  changed";

   426 

   427 val SOME t = parseNEW @{context} "a < 4";

   428 case adhoc_thm thy (isa_str, eval_fn) t of

   429 NONE => () | _ => error "adhoc_thm  a < 4  does NOT result in NONE";

   430 

   431 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");

   432 val SOME t = parseNEW @{context} "1 + (2::real)";

   433 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;

   434 if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3"

   435 then () else error "adhoc_thm  1 + 2  changed";

   436 

   437 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");

   438 val t = @{term "6 / -8 :: real"};

   439 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;

   440 if str = "#divide_e6_~8" andalso ThmC_Def.string_of_thm thm = "6 / - 8 = - 3 / 4"

   441 then () else error "adhoc_thm  6 / -8 = - 3 / 4  changed";

   442 

   443 case assoc_calc thy "Prog_Expr.ident" of

   444   "ident" => () | _ => error "Prog_Expr.ident <-> ident  changed";

   445 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident");

   446 

   447 val t = @{term "3 =!= (3 :: real)"};

   448 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;

   449 if str = "#ident_(3)_(3)" andalso ThmC_Def.string_of_thm thm = "(3 =!= 3) = True"

   450 then () else error "adhoc_thm  (3 =!= 3)  changed";

   451 

   452 val t = @{term "\<not> ((4 :: real) + (4 * x + x \<up> 2) =!= 0)"};

   453 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;

   454 if str = "#ident_(4 + (4 * x + x \<up> 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x \<up> 2) =!= 0) = False"

   455 then () else error "adhoc_thm  (\<not> (4 + (4 * x + x ^ 2) =!= 0))  changed";

   456 

   457 "----------- fun power -------------------------------------------------------------------------";

   458 "----------- fun power -------------------------------------------------------------------------";

   459 "----------- fun power -------------------------------------------------------------------------";

   460 if power 2 3 = 8 then () else error "power 2 3 = 8";

   461 if power ~2 3 = ~8 then () else error "power ~2 3 = ~8";

   462 if power ~3 2 = 9 then () else error "power ~3 2 = 9";

   463 case \<^try>\<open> power 3 ~2 \<close> of

   464   SOME _ => raise error "power 3 ~2: should raise an exn 1"

   465 | NONE => ();

   466 

   467 "----------- fun divisors ----------------------------------------------------------------------";

   468 "----------- fun divisors ----------------------------------------------------------------------";

   469 "----------- fun divisors ----------------------------------------------------------------------";

   470 if divisors 30 = [5, 3, 2] then () else error "divisors 30 = [5, 3, 2]";

   471 if divisors 32 = [2, 2, 2, 2, 2] then () else error "divisors 32 = [2, 2, 2, 2, 2]";

   472 if divisors 60 = [5, 3, 2, 2] then () else error "divisors 60 = [5, 3, 2, 2]";

   473 if divisors 11 = [11] then () else error "divisors 11 = [11]";

   474 

   475 "----------- fun doubles, fun squfact ----------------------------------------------------------";

   476 "----------- fun doubles, fun squfact ----------------------------------------------------------";

   477 "----------- fun doubles, fun squfact ----------------------------------------------------------";

   478 if doubles [2,3,4] = [] then () else error "doubles [2,3,4] changed";

   479 if doubles [2,3,3,5,5,7] = [5, 3] then () else error "doubles [2,3,3,5,5,7] changed";

   480 

   481 if squfact 30 = 1 then () else error "squfact  30  changed";

   482 if squfact 32 = 4 then () else error "squfact  32  changed";

   483 if squfact 60 = 2 then () else error "squfact  60  changed";

   484 if squfact 11 = 1 then () else error "squfact  11  changed";
wneuper/isa