wneuper/isa: test/Tools/isac/ProgLang/termC.sml@e0e3d41ef86c

     1 (* Title: tests on ProgLang/termC.sml

     2    Author: Walther Neuper 051006,

     3    (c) due to copyright terms

     4 *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    32 "--------------------------------------------------------";

    33 "--------------------------------------------------------";

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

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

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

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

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

    40 @{term "0::nat"};

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

    42 @{term "1::nat"};

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

    44 @{term "5::nat"};

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

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

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

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

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

    50 @{term "0::int"};

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

    52 @{term "1::int"};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    71 @{term "0::real"};

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

    73 @{term "1::real"};

    74 (**)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    92 @{term "0::nat"};

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

    94 @{term "1::nat"};

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

    96 @{term "5::nat"};

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

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

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

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

   101 @{term "0::int"};

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

   103 @{term "1::int"};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   119 @{term "0::real"};

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

   121 @{term "1::real"};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   137 @{term "0::nat"};

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

   139 @{term "1::nat"};

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

   141 @{term "5::nat"};

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

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

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

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

   146 @{term "0::int"};

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

   148 @{term "1::int"};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   164 @{term "0::real"};

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

   166 @{term "1::real"};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   187    then ()

   188    else error "termC.sml d1_isolate_add2";

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

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

   191  val t' = inst_bdv subst t;

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

   193    then ()

   194    else error "termC.sml inst_bdv 1";

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

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

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

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

   199 (*default_print_depth 5;*)

   201 val subst =

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

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

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

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

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

   207 val t' = inst_bdv subst t;

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

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

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

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

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

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

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

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

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

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

   221  if all_Free_subst andalso

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

   223    then ()

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

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

   227  if not all_Free_subst andalso

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

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

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

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

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

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

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

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

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

   238 (*default_print_depth 3; 999*) insts;

   239  (*val insts =

   240    ({},

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

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

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

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

   246 (* val t = str2term "x";

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

   248  handle MATCH => ???; *)

   250  val thy = @{theory "Complex_Main"};

   251  val PARSE = Syntax.read_term_global thy;

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

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

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

   256  Vartab.dest tenv;

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

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

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

   261  (*examples see

   262    test/../Knowledge/polyeq.sml:

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

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

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

   266   val thy = @{theory "Complex_Main"};

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

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

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

   271 (***

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

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

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

   275 ***)

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

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

   278  if matches thy tm pa then ()

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

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

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

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

   283   else ();

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

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

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

   288 (***

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

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

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

   292 ***)

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

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

   295  if matches thy tm pa then ()

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

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

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

   299  if matches thy tm pa then ()

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

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

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

   303   else ();*)

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

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

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

   308 (***

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

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

   311 *** . Free (0, real)

   312 ***)

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

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

   315  if matches thy tm pa then ()

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

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

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

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

   320    else ();

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

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

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

   325  val tm = str2term "M_b 0";

   326  if matches thy tm pa then ()

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

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

   329  val tm = str2term "M_b x";

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

   331    else ();

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

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

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

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

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

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

   343 (* added after Isabelle2015->17

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

   345 > atomty (Thm.term_of ct);

   346 *** -------------

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

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

   349 ***     Free ( #5, 'a)

   350 ***   Free ( #3, nat)

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

   352 > atomty (Thm.term_of ct);

   353 *** -------------

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

   355 ***   Free ( R, real)

   356 ***   Free ( R, real)

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

   359 *** -------------

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

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

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

   363  val thy = @{theory "Complex_Main"};

   364  val str = "x + z";

   365  parse thy str;

   366 "---------------";

   367  val str = "x + 2*z";

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

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

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

   371  Thm.global_cterm_of thy t;

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

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

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

   376  parse_patt thy "?p is_addUnordered";

   377  parse_patt thy "?p :: real";

   379  val str = "x + z";

   380  parse thy str;

   381 "---------------";

   382  val str = "x + 2*z";

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

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

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

   386  Thm.global_cterm_of thy t;

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

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

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

   391  parse_patt thy "?p is_addUnordered";

   392  parse_patt thy "?p :: real";

   394 (* Christian Urban, 101001

   395 theory Test

   396 imports Main Complex

   397 begin

   399 let

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

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

   402   |> ML_Syntax.print_term |> ML_Syntax.atomic

   403 in

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

   405 end

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

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

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

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

   412   Envir.subst_term inst precond

   413   |> Syntax.string_of_term @{context}

   414   |> writeln

   415 end *)

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

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

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

   420 val thy = @{theory Partial_Fractions};

   421 val ctxt = Proof_Context.init_global @{theory}

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

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

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

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

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

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

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

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

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

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

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

   438  if uminus_to_string t2 = t1

   439    then ()

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

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

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

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

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

   446  val str = "?a";

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

   448                     |-> Proof_Context.read_term_pattern

   449                     |> numbers_to_string;

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

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

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

   453    then ()

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

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

   457  val str = "?a :: real";

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

   459                     |-> Proof_Context.read_term_pattern

   460                     |> numbers_to_string;

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

   462  val Type (str, tys) = ty;

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

   464    then ()

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

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

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

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

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

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

   472 val ctxt = Proof_Context.init_global thy;

   473 val ctxt = Config.put show_types true ctxt;

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

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

   476                     |-> Proof_Context.read_term_pattern

   477                     |> numbers_to_string;

   478 val t_real = typ_a2real t;

   479 if term_to_string' ctxt t_real =

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

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

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

   483 else error "matchsub";

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

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

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

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

   489  val str_markup = (Syntax.string_of_term

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

   491  val str = term_to_string'' "Isac" t;

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

   494  writeln str_markup;

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

   496  writeln str;

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

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

   500  writeln (@{make_string} str_markup);

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

   502  writeln (@{make_string} str);

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

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

   506  tracing str_markup;

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

   508  tracing str;

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

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

   512  tracing (@{make_string} str_markup);

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

   514  tracing (@{make_string} str);

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

   516 (*

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

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

   519  tracing str_markup;

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

   521  tracing str;

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

   523 *)

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

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

   527  val str_markup = (Syntax.string_of_term

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

   529  val str = term_to_string'' "Isac" t;

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

   532  writeln str_markup;

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

   534  writeln str;

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

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

   538  writeln (@{make_string} str_markup);

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

   540  writeln (@{make_string} str);

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

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

   544  tracing str_markup;

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

   546  tracing str;

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

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

   550  tracing (@{make_string} str_markup);

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

   552  tracing (@{make_string} str);

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

   554 (*

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

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

   557  tracing str_markup;

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

   559  tracing str;

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

   561 *)

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

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

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

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

   567 else error "is_bdv_subst canged 1";

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

   570 else error "is_bdv_subst canged 2";

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

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

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

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

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

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

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

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

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

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

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

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

   586 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\"))))"

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

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

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

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

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

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

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

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

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

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

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

   601 case int_of_str_opt "123" of

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

   603 case int_of_str_opt "(-123)" of

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

   605 case int_of_str_opt "#123" of

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

   607 case int_of_str_opt "-123" of

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

   610 val t = str2term "1";

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

   613 val t = str2term "-1";

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

   616 val t = str2term "a123";

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

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

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

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

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

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

   625 val t = str2term "M_b x";

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

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

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

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

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

   632 val T = type_of t;

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

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

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

   637 val il = isalist2list t;

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

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

   641 val il = isalist2list t;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   659 val SOME t' = strip_imp_prems' t;

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

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

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

   664 val concl = Logic.strip_imp_concl prop;

   665 val SOME prems = strip_imp_prems' prop;

   666 val prop' = ins_concl prems concl;

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

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

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

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

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

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

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

   676 val t = str2term "aaa + bbb";

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

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

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

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

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

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

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

   685 val hT = type_of (head_of t);

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

   687 then () else error "dest_binop_typ";

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

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

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

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

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

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

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

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

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

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

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

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

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

   704 (* cp from Biegelinie.thy*)

   705 val scr = str2term

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

   707    " (let fu_n = Take fu_n;                             " ^

   708    "      bd_v = argument_in (lhs fu_n);                " ^

   709    "      va_l = argument_in (lhs su_b);                " ^

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

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

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

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

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

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

   716                Const ("HOL.Let", _) $

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

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

   719                  Abs _)) = scr;

   721 val scr' = inst_abs scr;

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

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

   724              Abs ("fu_n", _,

   725                Const ("HOL.Let", _) $

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

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

   728                  Abs _)) = scr';

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

   730   ("Script Function2Equality fu_n su_b =\n " ^

   731    "let fu_na = Take fu_n; " ^

   732      "bd_va = argument_in lhs fu_n;\n     " ^

   733      "va_la = argument_in lhs su_b; " ^

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

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

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

   737  then () else error "inst_abs changed";

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

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

   741 ;

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

author	Walther Neuper <wneuper@ist.tugraz.at>
	Sat, 01 Jun 2019 11:09:19 +0200
changeset 59549	e0e3d41ef86c
parent 59546	1ada701c4811
child 59550	2e7631381921
permissions	-rw-r--r--