(* Title:  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 script --requires 'setup'----";

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

"----------- check calcul,ate bottom up -----------------";

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

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

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

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

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

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

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

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

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

"----------- 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 "calculate.sml: adhoc_thm must return Trueprop";

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

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

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

val thy = @{theory "Test"};

"===== test 1";

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

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

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

"===== test 2";

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

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

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

if term2str t = "(3 * 4 / 3) ^^^ 2" then ()

else error "calculate.sml: ((1+2)*4/3)^^^2 --> (3 * 4 / 3) ^^^ 2";

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

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

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

term2str t;

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

"===== test 4";

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

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

term2str t;

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

"===== test 5";

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

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

(*show_types := false;*)

if term2str t <> "16" then error "calculate.sml: new behaviour in calculate_"

else ();

val fmz = ["realTestGiven (((1+2)*4/3)^^^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) ^^^#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"))*)

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

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

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

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

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

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

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

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

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

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

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

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

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

error "calculate.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 ^^^ 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 ^^^ 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 (assoc (calclist, "DIVIDE"));

 val ct = numbers_to_string @{term

   "sqrt (x ^^^ 2 + -3 * x) = (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"};

case calculate_ thy op_ ct of

  SOME _ => ()

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

(*

           sqrt (x ^^^ 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 t = (Thm.term_of o the o (parse thy)) "6 / 2";

 val rls = Test_simplify;

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

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

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

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

 atomty t;

 rewrite_set_ @{theory Test} false tval_rls t;

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

 val t = str2term "2 * x is_const";

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

 term2str t';

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

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

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

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

 trace_rewrite:=false;

 val thy = @{theory Test};

 val rls = Test_simplify;

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

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

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

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

case rewrite_set_ thy false rls t of

  SOME (Free ("4", _), []) => ()

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

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

case rewrite_set_ thy false rls t of

  SOME (Const ("Groups.plus_class.plus", _) $ Free ("2", _) $ Free ("x", _), []) => ()

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

 trace_rewrite:=false; (*=true3.6.03*)

(*--- 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"

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

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

 trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)

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

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

if term2str 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'

*)

 trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)

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

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

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

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

atomty t;

(*** -------------

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

*** . Free ( 1, 'a)

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

val t = str2term "1 ^^^ aaa";

atomty t;

(**** 

*** Const (Atools.pow, real => real => real)

*** . Free (1, real)

*** . Free (aaa, real)

*** *);

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

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

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

val thy = @{theory Test};

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

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

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

"12 / 3 = 4";

val thy = @{theory Test};

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

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

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

"4 ^ 2 = 16";

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

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

"1 + 2 = 3";

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

 term2str t;

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

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

"3 * 4 = 12";

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

 term2str t;

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

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

"12 / 3 = 4";

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

 term2str t;

"4 ^^^ 2";

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

"4 ^^^ 2 = 16";

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

 term2str t;

"16";

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

 else ();

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

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

  val SOME (thmID,thm) = 

      adhoc_thm thy (the(assoc(calclist,"POWER"))) t;

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

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

  (*

val op_ = "Atools.pow" : string

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

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

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

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

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

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

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

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

"----------- 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' (Thy_Info_get_theory "EqSystem") "occur_exactly_in" |> snd |> snd,

     str2term

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

      );

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

if str = 

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

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

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

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

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

val t = str2term "2 * x is_const";

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

term2str t';

"(2 * x is_const) = False";

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

term2str t';

"HOL.False";

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

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

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

 (*

>  val t = (Thm.term_of o the o (parse thy)) "#3 + #4";

>  val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus"));

>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;

>  term2str t';

>  atomty t';

> 

>  val t = (Thm.term_of o the o (parse thy)) "(a + #3) + #4";

>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;

>  term2str t';

> 

>  val t = (Thm.term_of o the o (parse thy)) "#3 + (#4 + (a::real))";

>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;

>  term2str t';

> 

>  val t = (Thm.term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";

>  atomty t;

>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;

>  term2str t';

>  val it = "#3 + (#4 + a) = #7 + a" : string

>

>

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

>  val eval_fn = the (assoc (!eval_list, "cancel"));

>  val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;

>  term2str t';

> 

>  val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";

>  eval_binop "xxx" "pow" t thy;

>  val eval_fn = (eval_binop "xxx")

>		 : string -> term -> theory -> (string * term) option;

>  val SOME (id,t') = get_pair thy "pow" eval_fn t;

>  term2str t';

>  val eval_fn = the (assoc (!eval_list, "pow"));

>  val (SOME (id,t')) = get_pair thy "pow" eval_fn t;

>  term2str t';

> 

>  val t = (Thm.term_of o the o (parse thy)) "x = #0 + #-1 * #-4";

>  val eval_fn = the (assoc (!eval_list, "Groups.times_class.times"));

>  val (SOME (id,t')) = get_pair thy "Groups.times_class.times" eval_fn t;

>  term2str t';

> 

>  val t = (Thm.term_of o the o (parse thy)) "#0 < #4";

>  val eval_fn = the (assoc (!eval_list, "Orderings.ord_class.less"));

>  val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;

>  term2str t';

>  val t = (Thm.term_of o the o (parse thy)) "#0 < #-4";

>  val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;

>  term2str t';

> 

>  val t = (Thm.term_of o the o (parse thy)) "#3 is_const";

>  val eval_fn = the (assoc (!eval_list, "is'_const"));

>  val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;

>  term2str t';

>  val t = (Thm.term_of o the o (parse thy)) "a is_const";

>  val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;

>  term2str t';

> 

>  val t = (Thm.term_of o the o (parse thy)) "#6//(#8::real)";

>  val eval_fn = the (assoc (!eval_list, "cancel"));

>  val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;

>  term2str t';

> 

>  val t = (Thm.term_of o the o (parse thy)) "sqrt #12";

>  val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt"));

>  val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;

>  term2str t';

>  val it = "sqrt #12 = #2 * sqrt #3 " : string

>

>  val t = (Thm.term_of o the o (parse thy)) "sqrt #9";

>  val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;

>  term2str t';

>

>  val t = (Thm.term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]";

>  val eval_fn = the (assoc (!eval_list, "Tools.Nth"));

>  val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t;

>  term2str t';

*)

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

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

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

(*

> val ct = (the o (parse thy)) "#9 is_const";

> adhoc_thm thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;

val it = SOME ("is_const9_","(is_const 9 ) = True  [(is_const 9 ) = True]")

> val ct = (the o (parse thy)) "sqrt #9";

> adhoc_thm thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct;

val it = SOME ("sqrt_9_","sqrt 9  = 3  [sqrt 9  = 3]") : (string * thm) option

> val ct = (the o (parse thy)) "#4<#4";

> adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;fun is_no str = (hd o Symbol.explode) str = "#";

val it = SOME ("less_5_4","(5 < 4) = False  [(5 < 4) = False]")

> val ct = (the o (parse thy)) "a<#4";

> adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;

val it = NONE : (string * thm) option

> val ct = (the o (parse thy)) "#5<=#4";

> adhoc_thm thy ("Orderings.ord_class.less_eq",the (assoc(!eval_list,"Orderings.ord_class.less_eq"))) ct;

val it = SOME ("less_equal_5_4","(5 <= 4) = False  [(5 <= 4) = False]")

-------------------------------------------------------------------6.8.02:

 val thy = SqRoot.thy;

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

 adhoc_thm thy (the(assoc(!calc_list,"PLUS"))) t;

 val it = SOME ("add_3_4","3 + 4 = 7  [3 + 4 = 7]") : (string * thm) option

-------------------------------------------------------------------6.8.02:

 val t = (Thm.term_of o the o (parse thy)) "-1";

 atomty t;

 val t = (Thm.term_of o the o (parse thy)) "0";

 atomty t;

 val t = (Thm.term_of o the o (parse thy)) "1";

 atomty t;

 val t = (Thm.term_of o the o (parse thy)) "2";

 atomty t;

 val t = (Thm.term_of o the o (parse thy)) "999999999";

 atomty t;

-------------------------------------------------------------------6.8.02:

> val ct = (the o (parse thy)) "a+#3+#4";

> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;

val it = SOME ("add_3_4","a + 3 + 4 = a + 7  [a + 3 + 4 = a + 7]")

> val ct = (the o (parse thy)) "#3+(#4+a)";

> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;

val it = SOME ("add_3_4","3 + (4 + a) = 7 + a  [3 + (4 + a) = 7 + a]")

> val ct = (the o (parse thy)) "a+(#3+#4)+#5";

> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;

val it = SOME ("add_3_4","3 + 4 = 7  [3 + 4 = 7]") : (string * thm) option

> val ct = (the o (parse thy)) "#3*(#4*a)";

> adhoc_thm thy ("Groups.times_class.times",the (assoc(!eval_list,"Groups.times_class.times"))) ct;

val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a  [3 * (4 * a) = 12 * a]")

> val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5";

> adhoc_thm thy ("pow",the (assoc(!eval_list,"pow"))) ct;

val it = SOME ("4_(+2)","4 ^ 2 = 16  [4 ^ 2 = 16]") : (string * thm) option

> val ct = (the o (parse thy)) "#-4//#-2";

> adhoc_thm thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;

val it = SOME ("cancel_(-4)_(-2)","(-4) // (-2) = (+2)  [(-4) // (-2) = (+2)]")

> val ct = (the o (parse thy)) "#6//#-8";

> adhoc_thm thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;

val it = SOME ("cancel_6_(-8)","6 // (-8) = (-3) // 4  [6 // (-8) = (-3) // 4]")

*) 

(*

--------------------------

> val ct = (the o (parse thy)) "3 =!= 3";

> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);

val thm = "(3 =!= 3) = True  [(3 =!= 3) = True]" : thm

> val ct = (the o (parse thy)) "~ (3 =!= 3)";

> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);

val thm = "(3 =!= 3) = True  [(3 =!= 3) = True]" : thm

> val ct = (the o (parse thy)) "3 =!= 4";

> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);

val thm = "(3 =!= 4) = False  [(3 =!= 4) = False]" : thm

> val ct = (the o (parse thy)) "( 4 + (4 * x + x ^ 2) =!= (+0))";

> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);

  "(4 + (4 * x + x ^ 2) =!= (+0)) = False"

> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";

> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);

  "(4 + (4 * x + x ^ 2) =!= (+0)) = False"

> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";

> val rls = eval_rls;

> val (ct,_) = the (rewrite_set_ thy false rls ct);

val ct = "HOL.True" : cterm

--------------------------

*)