(* Title:  "ProgLang/evaluate.sml"

           test calculation of values for function constants

   Author: Walther Neuper 2000

   (c) copyright due to lincense terms.

*)

"--------------------------------------------------------";

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

"--------------------------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

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

"----------- calculate (2 * x is_num) -------------------";

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

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

"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";

"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";

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

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

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

"--------------------------------------------------------";

"--------------------------------------------------------";

"--------------------------------------------------------";

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

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

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

val thy = @{theory "Poly"};

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

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

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

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

handle TERM _ => 

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

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

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

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

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

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

val thy = @{theory};

val ctxt = Proof_Context.init_global @{theory}

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

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

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

val pow =    (\<^const_name>\<open>realpow\<close>, eval_binop "#power_") : string * Eval_Def.eval_fn;

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

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

val SOME (t', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;

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

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

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

val SOME (t'', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;

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

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

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

val SOME (t''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;

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

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

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

val SOME (t'''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;

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

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

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

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

val thy = @{theory "Test"};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

val ct =

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

> val rls = ("Test_simplify");

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

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

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

ie. cancel does not work properly

*)

 val thy = @{theory "Test"};

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

 val ct = @{term

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

case calculate_ ctxt op_ ct of

  SOME _ => ()

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

(*

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

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

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

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

 val thy = @{theory Test};

 val ctxt = (ThyC.id_to_ctxt "Test")

 val t = TermC.parseNEW' ctxt "6 / 2";

 val rls = Test_simplify;

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

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

(*--------------(3): is_num works ?: -------------------------------------*)

 val t = TermC.parseNEW' ctxt "2 is_num";

 TermC.atomty t;

 rewrite_set_ ctxt false tval_rls t;

(*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)

 val t = TermC.str2term "2 * x is_num";

 val NONE = eval_is_num "" "" t (@{theory "Isac_Knowledge"});

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

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

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

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

 val thy = @{theory Test};

 val rls = Test_simplify;

 val t = TermC.parseNEW' ctxt "(-4) / 2";

val SOME (_, t) = eval_cancel "xxx" \<^const_name>\<open>divide\<close> t thy;

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

 val t = TermC.parseNEW' ctxt "(3+5)/(2::real)";

case rewrite_set_ ctxt false rls t of

  SOME (t', []) =>

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

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

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

 val t = TermC.parseNEW' ctxt "(3+1+2*x)/(2::real)";

case rewrite_set_ ctxt false rls t of

  SOME (t', _) =>

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

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

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

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

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

:

### trying thm 'root_ge0_2'

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

### trying thm 'radd_real_const_eq'

### trying thm 'radd_real_const'

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

### trying thm 'rcollect_right'

:

"x + (-4) / 2"

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

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

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

:

### trying thm 'root_ge0_2'

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

### trying thm 'radd_real_const_eq'

### trying thm 'radd_real_const'

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

### rewrite_set_: x + #- 2

### trying thm 'rcollect_right'

:

"#- 2 + x"

-----------------------------------------------------------------*)

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

 val t = TermC.parseNEW' ctxt "x + (- 1 + -3) / (2::real)";

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

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

"x + (-4) / 2";						

(*

### trying calc. 'cancel'

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

@@@ get_pair: t else

@@@ get_pair: t else -> NONE

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

@@@ get_pair: then 1

@@@ get_pair: t -> NONE

@@@ get_pair: t1 -> NONE

@@@ adhoc_thm': NONE

### trying calc. 'pow'

*)

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

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

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

val thy = @{theory Test};

 val t = TermC.parseNEW' ctxt "12 / 3";

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

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

"12 / 3 = 4";

val thy = @{theory Test};

 val t = TermC.parseNEW' ctxt "4 \<up> 2";

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

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

"4 ^ 2 = 16";

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

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

"1 + 2 = 3";

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

 UnparseC.term t;

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

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

"3 * 4 = 12";

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

 UnparseC.term t;

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

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

"12 / 3 = 4";

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

 UnparseC.term t;

"4 \<up> 2";

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

"4 \<up> 2 = 16";

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

 UnparseC.term t;

"16";

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

 else ();

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

  val t = TermC.parseNEW' ctxt  "3 \<up> 2";

  val SOME (thmID,thm) = 

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

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

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

  (*

val op_ = \<^const_name>\<open>realpow\<close> : string

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

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

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

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

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

case (op_, t) of

  (\<^const_name>\<open>realpow\<close>,

    Const (\<^const_name>\<open>realpow\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $

      (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

"~~~~~ fun calcul , args:"; val (thy, lhs) = (@{theory}, t);

    val simp_ctxt =

      Proof_Context.init_global thy

      |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});

    val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs);

if ThmC.string_of_thm eq = "2 + 3 \<equiv> 5" then () else error "calcul 1";

    val rhs = Thm.term_of (Thm.rhs_of eq);

    val _ = \<^assert> (is_num rhs);

(*return value*) rhs;

if TermC.to_string rhs = "5" then () else error "calcul 2";

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

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

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

val (thy, op_, ef, arg) =

    (thy, "EqSystem.occur_exactly_in", 

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

     TermC.str2term

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

      );

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

if str = 

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

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

"----------- calculate (2 * x is_num) -------------------";

"----------- calculate (2 * x is_num) -------------------";

"----------- calculate (2 * x is_num) -------------------";

val t = TermC.str2term "(2::real) * x is_num";

val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t @{theory Test};

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

else error "is_num 2 * x is_num CHANGED";

val SOME (t',_) = rewrite_set_ ctxt false tval_rls t;

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

else error "rewrite_set_ 2 * x is_num CHANGED";

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

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

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

val thy = @{theory};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

val t = @{term "9 is_num"};

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

if str = "#is_num_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_num) = True"

then () else error "adhoc_thm  9 is_num  changed";

case assoc_calc thy \<^const_name>\<open>less\<close> of

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

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

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

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

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

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

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

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

case adhoc_thm thy (isa_str, eval_fn) t of

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

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

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

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

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

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

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

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

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

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

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

case assoc_calc thy "Prog_Expr.ident" of

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

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

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

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

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

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

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

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

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"

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

"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";

"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";

"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";

val eval_ = ("Rings.divide_class.divide", eval_cancel "#divide_e" : eval_fn);

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

(* 

  ML\<open>Eval.adhoc_thm\<close> is called while searching terms for adjacent numerals 

  given a certain ML_type\<open>eval_fn\<close> and a certain  ML\<open>term\<close> ..

  THE ERROR WAS:

    rew_once:

    Eval.get_pair for \<^const_name>\<open>divide\<close> \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2")

    but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE

  STEP-INTO BEVORE REMOVING THE ERROR:

val SOME ("#divide_e~1_2", adhoc_thm) =

      Eval.adhoc_thm @{theory} eval_ t;

"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);

val SOME

    ("#divide_e~1_2", t'') =

  (*case*) get_pair ctxt op_ eval_fn t (*of*);

(*

  get_pair finds two adjacent numerals and does NOT distinguish between different kinds of 

  \<^ML_type>\<open>eval_fn\<close>. In case of \<^ML>\<open>eval_cancel\<close> the return value WAS the same as the input..

*)

(*+*)ThmC.string_of_thm adhoc_thm = "- 1 / 2 = - 1 / 2"

*)

val NONE = adhoc_thm @{theory} eval_ t;

"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);

val NONE =

  (*case*) get_pair ctxt op_ eval_fn t (*of*);

"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";

"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";

"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";

val t = TermC.str2term "sqrt 4";

Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t;

"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =

  ((ThyC.get_theory "Isac_Knowledge"),

    ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> Proof.context -> (string * term) option), t);

val SOME (thmid, t) =

  (*case*) get_pair ctxt op_ eval_fn ct (*of*);

(*+*)val "sqrt 4 = 2" = UnparseC.term t;

(** )

      Skip_Proof.make_thm thy t;

  exception TYPE raised (line 169 of "consts.ML"): Illegal type

   for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)

( **)

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

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

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

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

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

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

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

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

| NONE => ();

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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