(* Title: tests on ProgLang/termC.sml

   Author: Walther Neuper 051006,

   (c) due to copyright terms

*)

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

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

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

"----------- numerals in Isabelle2011/12/13 -------------";

"----------- inst_bdv -----------------------------------";

"----------- subst_atomic_all ---------------------------";

"----------- Pattern.match ------------------------------";

"----------- fun matches --------------------------------";

"----------- fun parse, fun parse_patt, fun T_a2real -------------------------------------------";

"----------- fun vars_of -----------------------------------------------------------------------";

"----------- uminus_to_string ---------------------------";

"----------- *** prep_pbt: syntax error in '#Where' of [v";

"----------- check writeln, tracing for string markup ---";

"----------- build fun is_bdv_subst ------------------------------------------------------------";

"----------- fun str_of_int --------------------------------------------------------------------";

"----------- fun scala_of_term -----------------------------------------------------------------";

"----------- fun contains_Var ------------------------------------------------------------------";

"----------- fun int_of_str_opt, fun is_num ----------------------------------------------------";

"----------- fun is_f_x ------------------------------------------------------------------------";

"----------- fun list2isalist, fun isalist2list ------------------------------------------------";

"----------- fun strip_imp_prems' --------------------------------------------------------------";

"----------- fun ins_concl ---------------------------------------------------------------------";

"----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";

"----------- fun dest_binop_typ ----------------------------------------------------------------";

"----------- fun is_list -----------------------------------------------------------------------";

"----------- fun inst_abs ----------------------------------------------------------------------";

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

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

"----------- numerals in Isabelle2011/12/13 -------------";

"----------- numerals in Isabelle2011/12/13 -------------";

"----------- numerals in Isabelle2011/12/13 -------------";

"***Isabelle2011 ~= Isabelle2012 = Isabelle2013";

"***Isabelle2011**********************************************************************************";

@{term "0::nat"};

(*Const ("Groups.zero_class.zero", "Nat.nat")*)

@{term "1::nat"};

(*Const ("Groups.one_class.one", "Nat.nat")*)

@{term "5::nat"};

(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> Nat.nat") $

     (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

       (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $

         (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)

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

@{term "0::int"};

(*Const ("Groups.zero_class.zero", "Int.int")*)

@{term "1::int"};

(*Const ("Groups.one_class.one", "Int.int")*)

@{term "5::int"};

(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> Int.int") $

     (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

       (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $

         (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)

@{term "-5::int"};

(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> Int.int") $

     (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

       (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

         (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)

@{term "- 5::int"};

(*Const ("Groups.uminus_class.uminus", "Int.int \<Rightarrow> Int.int") $

     (Const ("Int.number_class.number_of", "Int.int \<Rightarrow> Int.int") $

       (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

         (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $

           (Const ("Int.Bit1...", "Int.int \<Rightarrow> Int.int") $ Const (...)))))*)

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

@{term "0::real"};

(*Const ("Groups.zero_class.zero", "Real.real")*)

@{term "1::real"};

(**)

@{term "5::real"};

(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> "Real.real") $

     (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

       (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $

         (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)

@{term "-5::real"};

(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> "Real.real") $

     (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

       (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

         (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)

@{term "- 5::real"};

(*Const ("Groups.uminus_class.uminus", "Real.real \<Rightarrow> "Real.real") $

     (Const ("Int.number_class.number_of", "Int.int \<Rightarrow> "Real.real") $

       (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

         (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $

           (Const ("Int.Bit1...", "Int.int \<Rightarrow> Int.int") $ Const (...)))))*)

"***Isabelle2012**********************************************************************************";

@{term "0::nat"};

(*Const ("Groups.zero_class.zero", "nat")*)

@{term "1::nat"};

(*Const ("Groups.one_class.one", "nat")*)

@{term "5::nat"};

(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> nat") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

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

@{term "0::int"};

(*Const ("Groups.zero_class.zero", "int")*)

@{term "1::int"};

(*Const ("Groups.one_class.one", "int")*)

@{term "5::int"};

(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

@{term "-5::int"};

(*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> int") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

@{term "- 5::int"};

(*Const ("Groups.uminus_class.uminus", "int \<Rightarrow> int") $

     (Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $

       (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

         (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)

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

@{term "0::real"};

(*Const ("Groups.zero_class.zero", "real")*)

@{term "1::real"};

(*Const ("Groups.one_class.one", "real")*)

@{term "5::real"};

(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

@{term "-5::real"};

(*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> real") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

@{term "- 5::real"};

(*Const ("Groups.uminus_class.uminus", "real \<Rightarrow> real") $

     (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $

       (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

         (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)

"***Isabelle2013**********************************************************************************";

@{term "0::nat"};

(*Const ("Groups.zero_class.zero", "nat")*)

@{term "1::nat"};

(*Const ("Groups.one_class.one", "nat")*)

@{term "5::nat"};

(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> nat") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

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

@{term "0::int"};

(*Const ("Groups.zero_class.zero", "int")*)

@{term "1::int"};

(*Const ("Groups.one_class.one", "int")*)

@{term "5::int"};

(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

@{term "-5::int"};

(*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> int") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

@{term "- 5::int"};

(*Const ("Groups.uminus_class.uminus", "int \<Rightarrow> int") $

     (Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $

       (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

         (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)

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

@{term "0::real"};

(*Const ("Groups.zero_class.zero", "real")*)

@{term "1::real"};

(*Const ("Groups.one_class.one", "real")*)

@{term "5::real"};

(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

@{term "-5::real"};

(*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> real") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

@{term "- 5::real"};

(*Const ("Groups.uminus_class.uminus", "real \<Rightarrow> real") $

     (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $

       (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

         (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)

"----------- inst_bdv -----------------------------------";

"----------- inst_bdv -----------------------------------";

"----------- inst_bdv -----------------------------------";

 if (term2str o Thm.prop_of o num_str) @{thm d1_isolate_add2} = 

     "\<not> ?bdv occurs_in ?a \<Longrightarrow>\n(?a + ?bdv = 0) = (?bdv = -1 * ?a)"

   then ()

   else error "termC.sml d1_isolate_add2";

 val subst = [(str2term "bdv", str2term "x")];

 val t = (norm o #prop o Thm.rep_thm) (num_str @{thm d1_isolate_add2});

 val t' = inst_bdv subst t;

 if term2str t' = "\<not> x occurs_in ?a \<Longrightarrow> (?a + x = 0) = (x = -1 * ?a)"

   then ()

   else error "termC.sml inst_bdv 1";

if (term2str o Thm.prop_of o num_str) @{thm separate_bdvs_add} = 

  "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0,\n         "

  ^ "?bdv_4.0] occur_exactly_in ?a \<Longrightarrow>\n(?a + ?b = ?c) = (?b = ?c + -1 * ?a)"

then () else error "termC.sml separate_bdvs_add";

(*default_print_depth 5;*)

val subst = 

  [(str2term "bdv_1", str2term "c"),

 	   (str2term "bdv_2", str2term "c_2"),

 	   (str2term "bdv_3", str2term "c_3"),

 	   (str2term "bdv_4", str2term "c_4")];

val t = (norm o #prop o Thm.rep_thm) (num_str @{thm separate_bdvs_add});

val t' = inst_bdv subst t;

if term2str t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a \<Longrightarrow>\n"

  ^ "(?a + ?b = ?c) = (?b = ?c + -1 * ?a)"

then () else error "termC.sml inst_bdv 2";

"----------- subst_atomic_all ---------------------------";

"----------- subst_atomic_all ---------------------------";

"----------- subst_atomic_all ---------------------------";

 val t = str2term "(tl vs_vs) from vs_vs occur_exactly_in (NTH 1 (es_es::bool list))";

 val env = [(str2term "vs_vs::real list", str2term "[c, c_2]"),

 	   (str2term "es_es::bool list", str2term "[c_2 = 0, c + c_2 = 1]")];

 val (all_Free_subst, t') = subst_atomic_all env t;

 if all_Free_subst andalso 

    term2str t' = "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1 [c_2 = 0, c + c_2 = 1]"

   then ()

   else error "termC.sml subst_atomic_all should be 'true'";

 val (all_Free_subst, t') = subst_atomic_all (tl env) t;

 if not all_Free_subst andalso 

    term2str t' = "tl vs_vs from vs_vs occur_exactly_in NTH 1 [c_2 = 0, c + c_2 = 1]" then ()

 else error "termC.sml subst_atomic_all should be 'false'";

"----------- Pattern.match ------------------------------";

"----------- Pattern.match ------------------------------";

"----------- Pattern.match ------------------------------";

 val t = (Thm.term_of o the o (parse thy)) "3 * x^^^2 = (1::real)";

 val pat = (free2var o Thm.term_of o the o (parse thy)) "a * b^^^2 = (c::real)";

 (*        !^^^^^^^^!... necessary for Pattern.match, see Logic.varify_global below*)

 val insts = Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty);

(*default_print_depth 3; 999*) insts; 

 (*val insts =

   ({}, 

    {(("a", 0), ("Real.real", Free ("3", "Real.real"))), 

     (("b", 0), ("Real.real", Free ("x", "Real.real"))),

     (("c", 0), ("Real.real", Free ("1", "Real.real")))})*)

 "----- throws exn MATCH...";

(* val t = str2term "x";

 (Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty))

 handle MATCH => ???; *)

 val thy = @{theory "Complex_Main"};

 val PARSE = Syntax.read_term_global thy;

 val (pa, tm) = (PARSE "a + b::real", PARSE  "x + 2*z::real");

 val (tye, tme) = (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);

 val (tyenv, tenv) = Pattern.match thy (Logic.varify_global pa, tm) (tye, tme);

 Vartab.dest tenv;

"----------- fun matches --------------------------------";

"----------- fun matches --------------------------------";

"----------- fun matches --------------------------------";

 (*examples see

   test/../Knowledge/polyeq.sml:     

   Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)

 (*test/../Interpret/ptyps.sml:        

   |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)

  val thy = @{theory "Complex_Main"}; 

"----- test 1: OK";

 val pa = Logic.varify_global @{term "a = (0::real)"}; (*<<<<<<<---------------*)

 tracing "paIsa=..."; atomty pa; tracing "...=paIsa";

(*** 

*** Const (op =, real => real => bool)

*** . Var ((a, 0), real)

*** . Const (Groups.zero_class.zero, real)

***)

"----- test 1a true";

 val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"};    (*<<<<<<<---------------*)

 if matches thy tm pa then () 

   else error "termC.sml diff.behav. in matches true 1";

"----- test 1b false";

 val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"};    (*<<<<<<<---------------*)

 if matches thy tm pa then error "termC.sml diff.behav. in matches false 1"

  else ();

"----- test 2: Nok";

 val pa = Logic.varify_global (str2term "a = (0::real)");(*<<<<<<<-------------*)

 tracing "paLo2=..."; atomty pa; tracing "...=paLo2";

(*** 

*** Const (op =, real => real => bool)

*** . Var ((a, 0), real)

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

***)

"----- test 2a true";

 val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)";     (*<<<<<<<-------------*)

 if matches thy tm pa then () 

   else error "termC.sml diff.behav. in matches true 2";

"----- test 2b false";

 val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)";     (*<<<<<<<-------------*)

 if matches thy tm pa then () 

   else error "termC.sml diff.behav. in matches false 2";

(* i.e. !!!!!!!!!!!!!!!!! THIS KIND OF PATTERN IS NOT RELIABLE !!!!!!!!!!!!!!!!!

if matches thy tm pa then error "termC.sml diff.behav. in matches false 2"

  else ();*)

"----- test 3: OK";

 val pa = free2var (str2term "a = (0::real)");(*<<<<<<<-------------*)

 tracing "paF2=..."; atomty pa; tracing "...=paF2";

(*** 

*** Const (op =, real => real => bool)

*** . Var ((a, 0), real)

*** . Free (0, real)

***)

"----- test 3a true";

 val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)";     (*<<<<<<<-------------*)

 if matches thy tm pa then () 

   else error "termC.sml diff.behav. in matches true 3";

"----- test 3b false";

 val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)";     (*<<<<<<<-------------*)

 if matches thy tm pa then error "termC.sml diff.behav. in matches false 3"

   else ();

"----- test 4=3 with specific data";

 val pa = free2var (str2term "M_b 0");

"----- test 4a true";

 val tm = str2term "M_b 0";

 if matches thy tm pa then () 

   else error "termC.sml diff.behav. in matches true 4";

"----- test 4b false";

 val tm = str2term "M_b x";

 if matches thy tm pa then error "termC.sml diff.behav. in matches false 4"

   else ();

"----------- fun matches, repair 'Handler catches all exceptions' ------------------------------";

"----------- fun matches, repair 'Handler catches all exceptions' ------------------------------";

"----------- fun matches, repair 'Handler catches all exceptions' ------------------------------";

"----------- fun parse, fun parse_patt, fun T_a2real -------------------------------------------";

"----------- fun parse, fun parse_patt, fun T_a2real -------------------------------------------";

"----------- fun parse, fun parse_patt, fun T_a2real -------------------------------------------";

(* added after Isabelle2015->17

> val (SOME ct) = parse thy "(-#5)^^^#3"; 

> atomty (Thm.term_of ct);

*** -------------

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

***   Const ( uminus, 'a => 'a)

***     Free ( #5, 'a)

***   Free ( #3, nat)                

> val (SOME ct) = parse thy "R=R"; 

> atomty (Thm.term_of ct);

*** -------------

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

***   Free ( R, real)

***   Free ( R, real)

THIS IS THE OUTPUT FOR VERSION (3) above at typ_a2real !!!!!

*** -------------

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

***   Free ( R, RealDef.real)

***   Free ( R, RealDef.real)                  *)

 val thy = @{theory "Complex_Main"};

 val str = "x + z";

 parse thy str;

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

 val str = "x + 2*z";

 val t = (Syntax.read_term_global thy str);

 val t = numbers_to_string (Syntax.read_term_global thy str);

 val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);

 Thm.global_cterm_of thy t;

 val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";

"===== fun parse_patt caused error in fun T_a2real ===";

 val thy = @{theory "Poly"};

 parse_patt thy "?p is_addUnordered";

 parse_patt thy "?p :: real";

 val str = "x + z";

 parse thy str;

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

 val str = "x + 2*z";

 val t = (Syntax.read_term_global thy str);

 val t = numbers_to_string (Syntax.read_term_global thy str);

 val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);

 Thm.global_cterm_of thy t;

 val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";

"===== fun parse_patt caused error in fun T_a2real ===";

 val thy = @{theory "Poly"};

 parse_patt thy "?p is_addUnordered";

 parse_patt thy "?p :: real";

(* Christian Urban, 101001 

theory Test

imports Main Complex

begin

let

  val parser = Args.context -- Scan.lift Args.name_source

  fun term_pat (ctxt, str) = str |> Proof_Context.read_term_pattern ctxt

  |> ML_Syntax.print_term |> ML_Syntax.atomic

in

  ML_Antiquote.inline "term_pat" (parser >> term_pat)

end

  val t = @{term "a + b * x = (0 ::real)"};

  val pat = @{term_pat "?l = (?r ::real)"};

  val precond = @{term_pat "is_polynomial (?l::real)"};

  val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);

  Envir.subst_term inst precond

  |> Syntax.string_of_term @{context}

  |> writeln

end *)

"----------- fun vars_of -----------------------------------------------------------------------";

"----------- fun vars_of -----------------------------------------------------------------------";

"----------- fun vars_of -----------------------------------------------------------------------";

val thy = @{theory Partial_Fractions};

val ctxt = Proof_Context.init_global @{theory}

val SOME t = TermC.parseNEW ctxt "x ^^^ 2 + -1 * x * y";

case vars_of t of [Free ("x", _), Free ("y", _)] => ()

| _ => error "vars_of (x ^^^ 2 + -1 * x * y) ..changed";

val SOME t = TermC.parseNEW ctxt "3 = 3 * AA / 4";

case vars_of t of [Const ("Partial_Fractions.AA", _), Const ("HOL.eq", _)] => ()

| _ => error "vars_of (3 = 3 * AA / 4) ..changed (! use only for polynomials, not equations!)";

"----------- uminus_to_string ---------------------------";

"----------- uminus_to_string ---------------------------";

"----------- uminus_to_string ---------------------------";

 val t1 = numbers_to_string @{term "-2::real"};

 val t2 = numbers_to_string @{term "- 2::real"};

 if uminus_to_string t2 = t1 

   then ()

   else error "termC.sml diff.behav. in uminus_to_string";

"----------- *** prep_pbt: syntax error in '#Where' of [v";

"----------- *** prep_pbt: syntax error in '#Where' of [v";

"----------- *** prep_pbt: syntax error in '#Where' of [v";

"===== deconstruct datatype typ ===";

 val str = "?a";

 val t = (thy, str) |>> thy2ctxt 

                    |-> Proof_Context.read_term_pattern

                    |> numbers_to_string;

 val Var (("a", 0), ty) = t;

 val TVar ((str, i), srt) = ty;

 if str = "'a" andalso i = 1 andalso srt = [] 

   then ()

   else error "termC.sml type-structure of \"?a\" changed";

"----- real type in pattern ---";

 val str = "?a :: real";

 val t = (thy, str) |>> thy2ctxt 

                    |-> Proof_Context.read_term_pattern

                    |> numbers_to_string;

 val Var (("a", 0), ty) = t;

 val Type (str, tys) = ty;

 if str = "Real.real" andalso tys = [] andalso ty = HOLogic.realT

   then ()

   else error "termC.sml type-structure of \"?a :: real\" changed";

"===== Not (matchsub (?a + (?b + ?c)) t_t |... ===";

val (thy, str) = (thy, "Not (matchsub (?a + (?b + ?c)) t_t | " ^

	                "     matchsub (?a + (?b - ?c)) t_t | " ^

	                "     matchsub (?a - (?b + ?c)) t_t | " ^

	                "     matchsub (?a + (?b - ?c)) t_t )");

val ctxt = Proof_Context.init_global thy;

val ctxt = Config.put show_types true ctxt;

"----- read_term_pattern ---";

val t = (thy, str) |>> thy2ctxt 

                    |-> Proof_Context.read_term_pattern

                    |> numbers_to_string;

val t_real = typ_a2real t;

if term_to_string' ctxt t_real =

  "\<not> (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) \<or>\n        "

  ^ "matchsub (?a + (?b - ?c)) t_t \<or>\n        "

  ^ "matchsub (?a - (?b + ?c)) t_t \<or> matchsub (?a + (?b - ?c)) t_t)" then ()

else error "matchsub";

"----------- check writeln, tracing for string markup ---";

"----------- check writeln, tracing for string markup ---";

"----------- check writeln, tracing for string markup ---";

 val t = @{term "x + 1"};

 val str_markup = (Syntax.string_of_term

       (Proof_Context.init_global (Thy_Info_get_theory "Isac"))) t;

 val str = term_to_string'' "Isac" t;

 writeln "----------------writeln str_markup---";

 writeln str_markup;

 writeln "----------------writeln str---";

 writeln str;

 writeln "----------------SAME output: no markup----";

 writeln "----------------writeln PolyML.makestring str_markup---";

 writeln (@{make_string} str_markup);

 writeln "----------------writeln PolyML.makestring str---";

 writeln (@{make_string} str);

 writeln "----------------DIFFERENT output----";

 tracing "----------------tracing str_markup---";

 tracing str_markup;

 tracing "----------------tracing str---";

 tracing str;

 tracing "----------------SAME output: no markup----";

 tracing "----------------writeln PolyML.makestring str_markup---";

 tracing (@{make_string} str_markup);

 tracing "----------------writeln PolyML.makestring str---";

 tracing (@{make_string} str);

 tracing "----------------DIFFERENT output----";

(*

 redirect_tracing "../../tmp/";

 tracing "----------------writeln str_markup---";

 tracing str_markup;

 tracing "----------------writeln str---";

 tracing str;

 tracing "----------------DIFFERENT output----";

*)

"----------- check writeln, tracing for string markup ---";

 val t = @{term "x + 1"};

 val str_markup = (Syntax.string_of_term

       (Proof_Context.init_global (Thy_Info_get_theory "Isac"))) t;

 val str = term_to_string'' "Isac" t;

 writeln "----------------writeln str_markup---";

 writeln str_markup;

 writeln "----------------writeln str---";

 writeln str;

 writeln "----------------SAME output: no markup----";

 writeln "----------------writeln PolyML.makestring str_markup---";

 writeln (@{make_string} str_markup);

 writeln "----------------writeln PolyML.makestring str---";

 writeln (@{make_string} str);

 writeln "----------------DIFFERENT output----";

 tracing "----------------tracing str_markup---";

 tracing str_markup;

 tracing "----------------tracing str---";

 tracing str;

 tracing "----------------SAME output: no markup----";

 tracing "----------------writeln PolyML.makestring str_markup---";

 tracing (@{make_string} str_markup);

 tracing "----------------writeln PolyML.makestring str---";

 tracing (@{make_string} str);

 tracing "----------------DIFFERENT output----";

(*

 redirect_tracing "../../tmp/";

 tracing "----------------writeln str_markup---";

 tracing str_markup;

 tracing "----------------writeln str---";

 tracing str;

 tracing "----------------DIFFERENT output----";

*)

"----------- fun is_bdv_subst ------------------------------------------------------------------";

"----------- fun is_bdv_subst ------------------------------------------------------------------";

"----------- fun is_bdv_subst ------------------------------------------------------------------";

if is_bdv_subst (str2term "[(''bdv'', v_v)]") then ()

else error "is_bdv_subst canged 1";

if is_bdv_subst (str2term "[(''bdv_1'', v_s1),(''bdv_2'', v_s2)]") then ()

else error "is_bdv_subst canged 2";

"----------- fun str_of_int --------------------------------------------------------------------";

"----------- fun str_of_int --------------------------------------------------------------------";

"----------- fun str_of_int --------------------------------------------------------------------";

if str_of_int 1 = "1" then () else error "str_of_int 1";

if str_of_int ~1 = "-1" then () else error "str_of_int -1";

"----------- fun scala_of_term -----------------------------------------------------------------";

"----------- fun scala_of_term -----------------------------------------------------------------";

"----------- fun scala_of_term -----------------------------------------------------------------";

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

if scala_of_term t = "Free(\"aaa\", Type(\"Real.real\", List()))"

then () else error "scala_of_term  aaa::real";

val t = @{term "aaa + bbb"};

if scala_of_term t = "App(App(Const(\"Groups.plus_class.plus\", Type(\"fun\", List(TFree(\"'a\", List(\"Groups.plus\")),Type(\"fun\", List(TFree(\"'a\", List(\"Groups.plus\")),TFree(\"'a\", List(\"Groups.plus\"))))))), Free(\"aaa\", TFree(\"'a\", List(\"Groups.plus\")))), Free(\"bbb\", TFree(\"'a\", List(\"Groups.plus\"))))"

then () else error "scala_of_term  aaa + bbb";

"----------- fun contains_Var ------------------------------------------------------------------";

"----------- fun contains_Var ------------------------------------------------------------------";

"----------- fun contains_Var ------------------------------------------------------------------";

val t = parse_patt @{theory} "?z = 3";

if contains_Var t = true then () else error "contains_Var  ?z = 3";

val t = parse_patt @{theory} "z = 3";

if contains_Var t = false then () else error "contains_Var  ?z = 3";

"----------- fun int_of_str_opt, fun is_num ----------------------------------------------------";

"----------- fun int_of_str_opt, fun is_num ----------------------------------------------------";

"----------- fun int_of_str_opt, fun is_num ----------------------------------------------------";

case int_of_str_opt "123" of

  SOME 123 => () | _ => raise error "int_of_str_opt  123  changed";

case int_of_str_opt "(-123)" of

  SOME ~123 => () | _ => raise error "int_of_str_opt  (-123)  changed";

case int_of_str_opt "#123" of

  NONE => () | _ => raise error "int_of_str_opt  #123  changed";

case int_of_str_opt "-123" of

  SOME ~123 => () | _ => raise error "int_of_str_opt  -123  changed";

val t = str2term "1";

if is_num t = true then () else error "is_num   1";

val t = str2term "-1";

if is_num t = true then () else error "is_num  -1";

val t = str2term "a123";

if is_num t = false then () else error "is_num   a123";

"----------- fun is_f_x ------------------------------------------------------------------------";

"----------- fun is_f_x ------------------------------------------------------------------------";

"----------- fun is_f_x ------------------------------------------------------------------------";

val t = str2term "q_0/2 * L * x";

if is_f_x t = false then () else error "is_f_x   q_0/2 * L * x";

val t = str2term "M_b x";

if is_f_x t = true then () else error "M_b x";

"----------- fun list2isalist, fun isalist2list ------------------------------------------------";

"----------- fun list2isalist, fun isalist2list ------------------------------------------------";

"----------- fun list2isalist, fun isalist2list ------------------------------------------------";

val t = str2term "R=(R::real)";

val T = type_of t;

val ss = list2isalist T [t,t,t];

if term2str ss = "[R = R, R = R, R = R]" then () else error "list2isalist 1";

val t = str2term "[a=b,c=d,e=f]";

val il = isalist2list t;

if terms2str il = "[\"a = b\",\"c = d\",\"e = f\"]" then () else error "isalist2list 2";

val t = str2term "[a=b,c=d,e=f]";

val il = isalist2list t;

if terms2str il = "[\"a = b\",\"c = d\",\"e = f\"]" then () else error "isalist2list 2";

val t = str2term "ss___s::bool list";

(isalist2list t; error "isalist2list 1") handle TERM ("isalist2list applied to NON-list: ", _) =>();

"----------- fun strip_imp_prems', fun ins_concl -----------------------------------------------";

"----------- fun strip_imp_prems', fun ins_concl -----------------------------------------------";

"----------- fun strip_imp_prems', fun ins_concl -----------------------------------------------";

val prop = (#prop o Thm.rep_thm) @{thm real_mult_div_cancel2};

term2str prop = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";

val t as Const ("Pure.imp", _) $

      (Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $ (Const ("HOL.eq", _) $ Var (("k", 0), _) $ Const ("Groups.zero_class.zero", _)))) $

      (Const ("HOL.Trueprop", _) $

        (Const ("HOL.eq", _) $

          (Const ("Rings.divide_class.divide", _) $ (Const ("Groups.times_class.times", _) $ Var (("m", 0), _) $ Var (("k", 0), _)) $

            (Const ("Groups.times_class.times", _) $ Var (("n", 0), _) $ Var (("k", 0), _))) $

          (Const ("Rings.divide_class.divide", _) $ Var (("m", 0), _) $ Var (("n", 0), _)))) = prop;

val SOME t' = strip_imp_prems' t;

if  term2str t' = "(\<Longrightarrow>) (?k \<noteq> 0)" then () else error "strip_imp_prems' changed";

val thm = TermC.num_str @{thm frac_sym_conv};

val prop = (#prop o Thm.rep_thm) thm;

val concl = Logic.strip_imp_concl prop;

val SOME prems = strip_imp_prems' prop;

val prop' = ins_concl prems concl;

if prop = prop' then () else error "ins_concl o strip_imp_concl";

"----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";

"----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";

"----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";

val T =  (type_of o Thm.term_of o the) (parse thy "12::real");

val t = mk_factroot "SqRoot.sqrt" T 2 3;

if term2str t = "2 * ??.SqRoot.sqrt 3" then () else error "mk_factroot";

val t = str2term "aaa + bbb";

val op_ as Const ("Groups.plus_class.plus", Top) $ Free ("aaa", T1) $ Free ("bbb", T2) = t;

val t' = mk_num_op_num T1 T2 ("Groups.plus_class.plus", Top) 2 3;

if term2str t' = "2 + 3" then () else error "mk_num_op_num";

"----------- fun dest_binop_typ ----------------------------------------------------------------";

"----------- fun dest_binop_typ ----------------------------------------------------------------";

"----------- fun dest_binop_typ ----------------------------------------------------------------";

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

val hT = type_of (head_of t);

if (HOLogic.realT, HOLogic.natT, HOLogic.realT) = dest_binop_typ hT

then () else error "dest_binop_typ";

"----------- fun is_list -----------------------------------------------------------------------";

"----------- fun is_list -----------------------------------------------------------------------";

"----------- fun is_list -----------------------------------------------------------------------";

val (SOME ct) = parse thy "lll::real list";

val t = str2term "lll::real list";

val ty = (Term.type_of o Thm.term_of) ct;

if is_list t = false then () else error "is_list   lll::real list";

val t = str2term "[a, b, c]";

val ty = (Term.type_of o Thm.term_of) ct;

if is_list t = true then () else error "is_list  [a, b, c]";

"----------- fun inst_abs ----------------------------------------------------------------------";

"----------- fun inst_abs ----------------------------------------------------------------------";

"----------- fun inst_abs ----------------------------------------------------------------------";

(* cp from Biegelinie.thy*)

val scr = str2term 

  ("Script Function2Equality (fu_n::bool) (su_b::bool) =" ^

   " (let fu_n = Take fu_n;                             " ^

   "      bd_v = argument_in (lhs fu_n);                " ^

   "      va_l = argument_in (lhs su_b);                " ^

   "      eq_u = (Substitute [bd_v = va_l]) fu_n;       " ^

   "      eq_u = (Substitute [su_b]) eq_u               " ^

   " in (Rewrite_Set ''norm_Rational'' False) eq_u)         ")

val Const ("Equation.Function2Equality", _) $ Free ("fu_n", _) $ Free ("su_b", _) $

           (Const ("HOL.Let", _) $ (Const ("Script.Take", _) $ Free ("fu_n", _)) $

             Abs ("fu_n", _,           (* <-- ID taken from here ------------------------------*)

               Const ("HOL.Let", _) $ 

                 (Const ("Atools.argument'_in", _) $ (Const ("Tools.lhs", _) $ 

                   Bound 0)) $         (* difference --vvv ------------------------------------*)

                 Abs _)) = scr;

val scr' = inst_abs scr;

val Const ("Equation.Function2Equality", _) $ Free ("fu_n", _) $ Free ("su_b", _) $

           (Const ("HOL.Let", _) $ (Const ("Script.Take", _) $ Free ("fu_n", _)) $

             Abs ("fu_n", _,

               Const ("HOL.Let", _) $ 

                 (Const ("Atools.argument'_in", _) $ (Const ("Tools.lhs", _) $ 

                   Free ("fu_n", _))) $ (* difference --^^^ -----------------------------------*)

                 Abs _)) = scr';

if term2str scr' = (* see the ugly IDs ...*)

  ("Script Function2Equality fu_n su_b =\n " ^

   "let fu_na = Take fu_n; " ^

     "bd_va = argument_in lhs fu_n;\n     " ^

     "va_la = argument_in lhs su_b; " ^

     "eq_ua = Substitute [bd_v = va_l] fu_n;\n     " ^

     "eq_ua = Substitute [su_b] eq_u\n " ^

   "in (Rewrite_Set ''norm_Rational'' False) eq_u")

 then () else error "inst_abs changed";

val {scr = Prog original, ...} = get_met ["Equation","fromFunction"];

val Const ("Equation.Function2Equality", _) $ Free ("fu_n", _) $ Free ("su_b", _) $ scr'_body = scr'

;

if scr'_body = LTool.body_of original then () else error "inst_abs changed";