(* Title:  ProgLang/program.sml

   Author: Walther Neuper 190922

   (c) due to copyright terms

*)

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

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

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

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

"-------- fun eval_is_atom ---------------------------------------------------------------------";

"-------- fun eval_is_even ---------------------------------------------------------------------";

"-------- fun eval_const -----------------------------------------------------------------------";

"-------- fun eval_cancel ----------------------------------------------------------------------";

"-------- fun eval_equ -------------------------------------------------------------------------";

"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";

"-------- occurs_in ----------------------------------------------------------------------------";

"-------- fun eval_occurs_in -------------------------------------------------------------------";

"-------- fun eval_argument_of -----------------------------------------------------------------";

"-------- fun eval_sameFunId -------------------------------------------------------------------";

"-------- fun eval_filter_sameFunId ------------------------------------------------------------";

"-------- fun eval_boollist2sum ----------------------------------------------------------------";

"-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";

"-------- fun matchsub -------------------------------------------------------------------------";

"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";

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

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

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

"-------- fun eval_is_atom ---------------------------------------------------------------------";

"-------- fun eval_is_atom ---------------------------------------------------------------------";

"-------- fun eval_is_atom ---------------------------------------------------------------------";

if is_atom   @{term  0} then () else error "is_atom 0 CHANGED";

val eval_t = @{term "0 is_atom"};

case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of

  SOME ("#is_atom_0_", _) => ()

| _ => error "eval_is_atom 0 CHANGED";

if is_atom   @{term  1} then () else error "is_atom 1 CHANGED";

val eval_t = @{term "1 is_atom"};

case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of

  SOME ("#is_atom_1_", _) => ()

| _ => error "eval_is_atom 1 CHANGED";

if is_atom   @{term  123} then () else error "is_atom 123 CHANGED";

val eval_t = @{term "123 is_atom"};

case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of

  SOME ("#is_atom_123_", _) => ()

| _ => error "eval_is_atom 123 CHANGED";

if is_atom   @{term  abc} then () else error "is_atom abc CHANGED";

val eval_t = @{term "abc is_atom"};

case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of

  SOME ("#is_atom_abc_", _) => ()

| _ => error "eval_is_atom abc CHANGED";

"-------- fun eval_is_even ---------------------------------------------------------------------";

"-------- fun eval_is_even ---------------------------------------------------------------------";

"-------- fun eval_is_even ---------------------------------------------------------------------";

val t = TermC.str2term "2 is_even";

           eval_is_even "aaa" "Prog_Expr.is_even" t "ccc";

"~~~~~ fun eval_is_even , args:"; val ((thmid:string), "Prog_Expr.is_even", (t as (Const _ $ arg)), _) =

  ("aaa", "Prog_Expr.is_even", t, "ccc");

    (*if*) TermC.is_num arg (*then*);

        val i = arg |> HOLogic.dest_number |> snd;

	      (*if*) even i (*then*);

val SOME ("aaa1_", t') =

    SOME (TermC.mk_thmid thmid (string_of_int n) "", 

				  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})));

if UnparseC.term t' = "(2 is_even) = True" then () else error "(2 is_even) = True  CHANGED";

val t = TermC.str2term "3 is_even";

case eval_is_even "aaa" "Prog_Expr.is_even" t "ccc" of

  SOME (str, t') => 

    if str = "aaa_" andalso UnparseC.term t' = "(3 is_even) = False" then ()

    else error "eval_is_even (3 is_even) CHANGED 1"

| NONE => error "eval_is_even (3 is_even) CHANGED 2";

val t = TermC.str2term "a ::real";

val NONE =

           eval_is_even "aaa" "Prog_Expr.is_even" t "ccc";

case eval_is_even "aaa" "Prog_Expr.is_even" t "ccc" of

  SOME _ => error "eval_is_even (a is_even) CHANGED"

| NONE => ();

"-------- fun eval_const -----------------------------------------------------------------------";

"-------- fun eval_const -----------------------------------------------------------------------";

"-------- fun eval_const -----------------------------------------------------------------------";

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

case rewrite_set_ @{theory Test} false tval_rls t of

  SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()

| _ => error "2 is_const CHANGED";

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

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

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

else error "(2 * x is_const) = False CHANGED";

val t = TermC.str2term "- 2 is_const";

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

if UnparseC.term t' = "(- 2 is_const) = True" then ()

else error "(- 2 is_const) = False CHANGED";

val t = TermC.str2term "- 1 is_const";

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

if UnparseC.term t' = "(- 1 is_const) = True" then ()

else error "(- 1 is_const) = False CHANGED";

val t = TermC.str2term "0 is_const";

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

if UnparseC.term t' = "(0 is_const) = True" then ()

else error "(0 is_const) = False CHANGED";

val t = TermC.str2term "AA is_const";

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

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

else error "(0 is_const) = False CHANGED";

"-------- fun eval_cancel ----------------------------------------------------------------------";

"-------- fun eval_cancel ----------------------------------------------------------------------";

"-------- fun eval_cancel ----------------------------------------------------------------------";

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

val NONE = eval_cancel "cancel_"  "Rings.divide_class.divide" t ""

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

case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of

  SOME ("cancel_6_4", t') =>

    if UnparseC.term t'  = "6 / 4 = 3 / 2" then ()

    else error "eval_cancel  - 6 / 4 = - 3 / 2  CHANGED 1"

| _ => error "eval_cancel  - 6 / 4 = - 3 / 2  CHANGED 2";

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

case eval_cancel "cancel_"  "Rings.divide_class.divide" t "" of

  SOME ("cancel_~6_4", t') =>

    if UnparseC.term t'  = "- 6 / 4 = - 3 / 2" then ()

    else error "eval_cancel  - 6 / 4 = - 3 / 2  CHANGED 1"

| _ => error "eval_cancel  - 6 / 4 = - 3 / 2  CHANGED 2";

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

case eval_cancel "cancel_"  "Rings.divide_class.divide" t "" of

  SOME ("cancel_6_~4", t') =>

    if UnparseC.term t' = "6 / - 4 = - 3 / 2" then ()

    else error "eval_cancel  6 / - 4 = - 3 / 2  CHANGED 1"

| _ => error "eval_cancel  6 / - 4 = - 3 / 2  CHANGED 2";

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

case eval_cancel "cancel_"  "Rings.divide_class.divide" t "" of

  SOME ("cancel_~6_~4", t') =>

    if UnparseC.term t' = "- 6 / - 4 = 3 / 2" then ()

    else error "eval_cancel  - 6 / - 4 = 3 / 2  CHANGED 1"

| _ => error "eval_cancel  - 6 / - 4 = 3 / 2  CHANGED 2";

val t = @{term  "- (6 / 4) :: real"};

val NONE = eval_cancel "adhoc_thm_cancel"  "Rings.divide_class.divide" t "";

"-------- fun eval_equ -------------------------------------------------------------------------";

"-------- fun eval_equ -------------------------------------------------------------------------";

"-------- fun eval_equ -------------------------------------------------------------------------";

eval_equ: string -> string -> term -> 'a -> (string * term) option;

case eval_equ "#less_" "Orderings.ord_class.less" @{term "1 < (2::real)"} "" of

SOME

    ("#less_1_2",

     Const (\<^const_name>\<open>Trueprop\<close>, _) $

       (Const (\<^const_name>\<open>HOL.eq\<close>, _) $

         (Const (\<^const_name>\<open>ord_class.less\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) $

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

         Const (\<^const_name>\<open>True\<close>, _))) => ()

| _ => error "eval_equ   1 < 2   CHANGED";

case eval_equ "#less_" "Orderings.ord_class.less" @{term "1 < (1::real)"} "" of

SOME

    ("#less_1_1",

     Const (\<^const_name>\<open>Trueprop\<close>, _) $

       (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>ord_class.less\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _)) $

         Const (\<^const_name>\<open>False\<close>, _))) => ()

| _ => error "eval_equ   1 < 1   CHANGED";

"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";

"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";

"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";

val thy = @{theory}

val t = TermC.str2term "x = 0";

val NONE(*= indetermined*) = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t thy;

val t = TermC.str2term "(x + 1) = (x + 1)";

val (Const _(*op0,t0*) $ t1 $ t2 ) = t

val SOME ("equal_(x + 1)_(x + 1)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t thy;

if UnparseC.term t' = "(x + 1 = x + 1) = True" then () else error "(x + 1) = (x + 1) CHANGED";

val t as Const _ $ v $ c = TermC.str2term "1 = 0";

val false = variable_constant_pair (v, c);

val SOME ("equal_(1)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t thy;

if UnparseC.term t' = "(1 = 0) = False" then () else error "1 = 0 CHANGED";

val t = TermC.str2term "0 = 0";

val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t thy;

if UnparseC.term t' = "(0 = 0) = True" then () else error "0 = 0 CHANGED";

"-------- occurs_in ----------------------------------------------------------------------------";

"-------- occurs_in ----------------------------------------------------------------------------";

"-------- occurs_in ----------------------------------------------------------------------------";

val t = @{term "x::real"};

if occurs_in t t then "OK" else error "occurs_in x x -> f ..changed";

val t = TermC.str2term "x occurs_in x";

val SOME (str, t') = eval_occurs_in 0 "Prog_Expr.occurs_in" t 0;

if UnparseC.term t' = "x occurs_in x = True" then ()

else error "x occurs_in x = True ..changed";

"------- some_occur_in";

if some_occur_in [@{term "c::real"}, @{term "c_2::real"}] @{term "a + b + c::real"} then ()

else error "";

val t = @{term "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2"};

val SOME (str, t') = eval_some_occur_in 0 "Prog_Expr.some_occur_in" t 0;

if UnparseC.term t' =

   "some_of [c, c_2, c_3,\n         c_4] occur_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 =\nTrue" then ()

else error "atools.sml: some_occur_in true";

val t = @{term "some_of [c_3, c_4] occur_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2"};

val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some_occur_in" t 0;

if UnparseC.term t' =

  "some_of [c_3, c_4] occur_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False" then ()

else error "atools.sml: some_occur_in false";

"-------- fun eval_occurs_in -------------------------------------------------------------------";

"-------- fun eval_occurs_in -------------------------------------------------------------------";

"-------- fun eval_occurs_in -------------------------------------------------------------------";

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

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

if occurs_in v t then error "factor_right_deg (1) x ..changed" else ();

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

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

if occurs_in v t then error "factor_right_deg (1) AA ..changed" else ();

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";

if occurs_in v t then error "factor_right_deg (a*b+c) x ..changed" else ();

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";

if occurs_in v t then error "factor_right_deg (a*b+c) AA ..changed" else ();

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c";

if occurs_in v t then () else error "factor_right_deg (a*x+c) x ..changed";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c";

if occurs_in v t then () else error "factor_right_deg (a*AA+c) AA ..changed";

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";

if occurs_in v t then () else error "factor_right_deg (a*b+c)*x \<up> 7) x ..changed";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";

if occurs_in v t then () else error "factor_right_deg (a*b+c)*AA \<up> 7) AA ..changed";

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";

if occurs_in v t then () else error "factor_right_deg (x \<up> 7) x ..changed";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";

if occurs_in v t then () else error "factor_right_deg (AA \<up> 7) AA ..changed";

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";

if occurs_in v t then () else error "factor_right_deg ((a*b+c)*x) x ..changed";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";

if occurs_in v t then () else error "factor_right_deg ((a*b+c)*AA) AA ..changed";

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";

if occurs_in v t then () else error "factor_right_deg ((a*b+x)*x) x ..changed";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";

if occurs_in v t then () else error "factor_right_deg ((a*b+AA)*AA) AA ..changed";

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

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

if occurs_in v t then () else error "factor_right_deg (x) x ..changed";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

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

if occurs_in v t then () else error "factor_right_deg (AA) AA ..changed";

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

val v = (Thm.term_of o the o (TermC.parse thy)) "x";

val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";

if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*x) x ..changed";

val v = (Thm.term_of o the o (TermC.parse thy)) "AA";

val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";

if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*AA) AA ..changed";

"---------fun eval_argument_of -----------------------------------------------------------------";

"---------fun eval_argument_of -----------------------------------------------------------------";

"---------fun eval_argument_of -----------------------------------------------------------------";

val t = TermC.str2term "argument_in (M_b x)";

val SOME (str, t') = eval_argument_in "0" "Prog_Expr.argument_in" t 0;

if UnparseC.term t' = "(argument_in M_b x) = x" then ()

else error "atools.sml:(argument_in M_b x) = x  ???";

"---------fun eval_sameFunId -------------------------------------------------------------------";

"---------fun eval_sameFunId -------------------------------------------------------------------";

"---------fun eval_sameFunId -------------------------------------------------------------------";

val t = @{term "M_b L"}; TermC.atomty t;

val t as f1 $ _ = @{term "M_b L"};

val t as Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _ = @{term "M_b x = c + L*x"};

f1 = f2 (*true*);

val (p as Const (\<^const_name>\<open>sameFunId\<close>, _) $ 

			(f1 $ _) $ 

			(Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _)) = 

    @{term "sameFunId (M_b L) (M_b x = c + L*x)"};

f1 = f2 (*true*);

eval_sameFunId "" "Prog_Expr.sameFunId" 

		 (@{term "sameFunId (M_b L) (M_b x = c + L*x)"})""(*true*);

eval_sameFunId "" "Prog_Expr.sameFunId" 

		 (@{term  "sameFunId (M_b L) ( y' x = c + L*x)"})""(*false*);

eval_sameFunId "" "Prog_Expr.sameFunId" 

		 (@{term  "sameFunId (M_b L) (  y x = c + L*x)"})""(*false*);

eval_sameFunId "" "Prog_Expr.sameFunId" 

		 (@{term  "sameFunId (  y L) (M_b x = c + L*x)"})""(*false*);

eval_sameFunId "" "Prog_Expr.sameFunId" 

		 (@{term  "sameFunId (  y L) (  y x = c + L*x)"})""(*true*);

"---------fun eval_filter_sameFunId ------------------------------------------------------------";

"---------fun eval_filter_sameFunId ------------------------------------------------------------";

"---------fun eval_filter_sameFunId ------------------------------------------------------------";

val flhs as (fid $ _) = @{term "y' L"};

val fs = @{term "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]"};

val (p as Const (\<^const_name>\<open>filter_sameFunId\<close>,_) $ (fid $ _) $ fs) = 

    @{term "filter_sameFunId (y' L) [M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]"};

val SOME (str, es) = eval_filter_sameFunId "" "Prog_Expr.filter_sameFunId" p "";

if UnparseC.term es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n                        y x = c + L * x]) =\n[y' x = c + L * x]" then ()

else error "atools.slm diff.behav. in filter_sameFunId";

"---------fun eval_boollist2sum ----------------------------------------------------------------";

"---------fun eval_boollist2sum ----------------------------------------------------------------";

"---------fun eval_boollist2sum ----------------------------------------------------------------";

fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l

  | lhs t = error("lhs called with (" ^ UnparseC.term t ^ ")");

"----------- \<up> redefined due to overwritten identifier -----------";

val u_ = @{term "[]"};

val u_ = @{term "[b1 = k - 2*q]"};

val u_ = @{term "[b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"};

val ut_ = isalist2list u_;

val sum_ = map lhs ut_;

val t = list2sum sum_;

UnparseC.term t;

val t = @{term "boollist2sum [b1 = k - 2*(q::real), b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"};

case t of

Const (\<^const_name>\<open>boollist2sum\<close>, _) $

     (Const (\<^const_name>\<open>Cons\<close>, _) $

       (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b1", _) $ _ ) $

       (Const (\<^const_name>\<open>Cons\<close>, _) $

         (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b2", _) $ _ ) $

         (Const (\<^const_name>\<open>Cons\<close>, _) $

           (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b3", _) $ _ ) $

           (Const (\<^const_name>\<open>Cons\<close>, _) $

             (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b4", _) $ _ ) $

             Const (\<^const_name>\<open>Nil\<close>, _))))) => ()

| _ => error "boollist2sum CHANGED";

val SOME (str, pred) = eval_boollist2sum "" "Prog_Expr.boollist2sum" t "";

if UnparseC.term pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then () 

else error "atools.sml diff.behav. in eval_boollist2sum";

Rewrite.trace_on := false; (*true false*)

val srls_ = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty 

		      [Eval ("Prog_Expr.boollist2sum", eval_boollist2sum "")];

val t = @{term "boollist2sum [b1 = k - 2*(q::real), b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"};

case rewrite_set_ @{theory} false srls_ t of SOME _ => ()

| _ => error "atools.sml diff.rewrite boollist2sum";

Rewrite.trace_on := false; (*true false*)

"-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";

"-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";

"-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";

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

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

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

;

"~~~~~ fun get_pair, args:"; val (thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =

  (thy, op_, ef, t);

op_ = op0 = true;val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));

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

           ef op_ t thy;

"~~~~~ fun eval_binop , args:"; val ((thmid : string), (op_: string), 

      (t as (Const (op0, _) $ t1 $ t2)), _) =

  ("#mult_", op_, t, thy);                                                (* binary . n1.n2 *)

    (*if*) TermC.is_num t1 andalso TermC.is_num t2 (*then*);

        val res = Eval.calcul op0 (t1, t2);

        val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));

val SOME (thmid, tm) = SOME ("#: " ^ UnparseC.term prop, prop)

;

if thmid = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()

else error "eval_binop changed"

;

val SOME (thmid, tm) = eval_binop "#mult_"  op_ t thy;

if thmid = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()

else error "eval_binop changed 2"

"-------- fun matchsub -------------------------------------------------------------------------";

"-------- fun matchsub -------------------------------------------------------------------------";

"-------- fun matchsub -------------------------------------------------------------------------";

if matchsub thy (TermC.str2term "(a + (b + c))") (TermC.str2term "?x + (?y + ?z)")

then () else error "tools.sml matchsub a + (b + c)";

if matchsub thy (TermC.str2term "(a + (b + c)) + d") (TermC.str2term "?x + (?y + ?z)")

then () else error "tools.sml matchsub (a + (b + c)) + d";

"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";

"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";

"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";

"see: --------- search for Or_to_List ---";

case or2list @{term True} of Const (\<^const_name>\<open>UniversalList\<close>, _) => ()

  | _ => error "TermC.UniversalList changed 1";

case or2list @{term False} of Const (\<^const_name>\<open>Nil\<close>, _) => ()

  | _ => error "TermC.UniversalList changed 2";

val t =  (TermC.str2term "x=3");

if UnparseC.term (or2list t) = "[x = 3]" then ()

else error "or2list changed";

val t =  (TermC.str2term "x=3 | x=-3 | x=0");

if UnparseC.term (or2list t) = "[x = 3, x = - 3, x = 0]" then ()

else error "HOL.eq ? HOL.disj ? changed";