wneuper/isa: test/Tools/isac/BaseDefinitions/termC.sml@f92963a33fe3

     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 TermC.matches --------------------------------";

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

    15 "----------- fun TermC.vars_of ---------------------------------------------------------------";

    16 "----------- fun TermC.vars --------------------------------------------------------------------";

    17 "----------- *** Problem.prep_input: syntax error in '#Where' of [v";

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

    19 "----------- build fun TermC.is_bdv_subst ------------------------------------------------------------";

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

    21 "----------- fun TermC.scala_of_term -----------------------------------------------------------------";

    22 "----------- fun TermC.contains_Var ------------------------------------------------------------------";

    23 "----------- fun int_opt_of_string, fun is_num -------------------------------------------------";

    24 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";

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

    26 "----------- fun TermC.strip_imp_prems' --------------------------------------------------------------";

    27 "----------- fun TermC.ins_concl ---------------------------------------------------------------------";

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

    29 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";

    30 "----------- fun TermC.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 (\<^const_name>\<open>zero_class.zero\<close>, "Nat.nat")*)

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

    43 (*Const (\<^const_name>\<open>one_class.one\<close>, "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 (\<^const_name>\<open>zero_class.zero\<close>, "Int.int")*)

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

    53 (*Const (\<^const_name>\<open>one_class.one\<close>, "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 (\<^const_name>\<open>uminus\<close>, "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 (\<^const_name>\<open>zero_class.zero\<close>, "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 (\<^const_name>\<open>uminus\<close>, "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 (\<^const_name>\<open>zero_class.zero\<close>, "nat")*)

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

    95 (*Const (\<^const_name>\<open>one_class.one\<close>, "nat")*)

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

    97 (*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> nat") $

    98      (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

    99        (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

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

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

   102 (*Const (\<^const_name>\<open>zero_class.zero\<close>, "int")*)

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

   104 (*Const (\<^const_name>\<open>one_class.one\<close>, "int")*)

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

   106 (*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> int") $

   107      (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

   108        (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

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

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

   111      (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

   112        (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

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

   114 (*Const (\<^const_name>\<open>uminus\<close>, "int \<Rightarrow> int") $

   115      (Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> int") $

   116        (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

   117          (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const ("...", "num"))))*)

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

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

   120 (*Const (\<^const_name>\<open>zero_class.zero\<close>, "real")*)

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

   122 (*Const (\<^const_name>\<open>one_class.one\<close>, "real")*)

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

   124 (*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> real") $

   125      (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

   126        (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

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

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

   129      (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

   130        (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

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

   132 (*Const (\<^const_name>\<open>uminus\<close>, "real \<Rightarrow> real") $

   133      (Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> real") $

   134        (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

   135          (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const ("...", "num"))))*)

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

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

   138 (*Const (\<^const_name>\<open>zero_class.zero\<close>, "nat")*)

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

   140 (*Const (\<^const_name>\<open>one_class.one\<close>, "nat")*)

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

   142 (*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> nat") $

   143      (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

   144        (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

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

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

   147 (*Const (\<^const_name>\<open>zero_class.zero\<close>, "int")*)

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

   149 (*Const (\<^const_name>\<open>one_class.one\<close>, "int")*)

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

   151 (*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> int") $

   152      (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

   153        (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

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

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

   156      (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

   157        (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

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

   159 (*Const (\<^const_name>\<open>uminus\<close>, "int \<Rightarrow> int") $

   160      (Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> int") $

   161        (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

   162          (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const ("...", "num"))))*)

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

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

   165 (*Const (\<^const_name>\<open>zero_class.zero\<close>, "real")*)

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

   167 (*Const (\<^const_name>\<open>one_class.one\<close>, "real")*)

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

   169 (*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> real") $

   170      (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

   171        (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

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

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

   174      (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

   175        (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

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

   177 (*Const (\<^const_name>\<open>uminus\<close>, "real \<Rightarrow> real") $

   178      (Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> real") $

   179        (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

   180          (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const ("...", "num"))))*)

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

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

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

   185  if (UnparseC.term o Thm.prop_of) @{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 = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];

   190  val t = (Eval.norm o Thm.prop_of)  @{thm d1_isolate_add2};

   191  val t' = TermC.inst_bdv subst t;

   192  if UnparseC.term 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 (UnparseC.term o Thm.prop_of) @{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) * ?a)"

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

   199 (*default_print_depth 5;*)

   201 val subst =

   202   [(TermC.parse_test @{context} "bdv_1", TermC.parse_test @{context} "c"),

   203  	   (TermC.parse_test @{context} "bdv_2", TermC.parse_test @{context} "c_2"),

   204  	   (TermC.parse_test @{context} "bdv_3", TermC.parse_test @{context} "c_3"),

   205  	   (TermC.parse_test @{context} "bdv_4", TermC.parse_test @{context} "c_4")];

   206 val t = (Eval.norm o Thm.prop_of)  @{thm separate_bdvs_add};

   207 val t' = TermC.inst_bdv subst t;

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

   210   "(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?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 = TermC.parse_test @{context} "(tl vs_vs) from vs_vs occur_exactly_in (NTH 1 (es_es::bool list))";

   217  val env = [(TermC.parse_test @{context} "vs_vs::real list", TermC.parse_test @{context} "[c, c_2]"),

   218  	   (TermC.parse_test @{context} "es_es::bool list", TermC.parse_test @{context} "[c_2 = 0, c + c_2 = 1]")];

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

   221  if all_Free_subst andalso

   222     UnparseC.term 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') = TermC.subst_atomic_all (tl env) t;

   227  if not all_Free_subst andalso

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

   229  else error "TermC.subst_atomic_all should be 'false'";

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

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

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

   234  val t = TermC.parse_test @{context} "3 * x\<up>2 = (1::real)";

   235  val pat = (TermC.free2var o TermC.parse_test @{context}) "a * b\<up>2 = (c::real)";

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

   237  val insts = Pattern.match @{theory "Isac_Knowledge"} (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 = TermC.parse_test @{context} "x";

   247  (Pattern.match @{theory "Isac_Knowledge"} (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 TermC.matches --------------------------------";

   259 "----------- fun TermC.matches --------------------------------";

   260 "----------- fun TermC.matches --------------------------------";

   261  (*examples see

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

   263    Where=[Correct "matches (?a = 0) (-8 - 2 * x + x \<up> 2 = 0)"*)

   264  (*test/../Specify/refine.sml:

   265    |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x \<up> #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=..."; TermC.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 TermC.matches thy tm pa then ()

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

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

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

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

   283   else ();

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

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

   287  tracing "paLo2=..."; TermC.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 = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)";     (*<<<<<<<-------------*)

   295  if TermC.matches thy tm pa then ()

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

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

   298  val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)";     (*<<<<<<<-------------*)

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

   300    else ();

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

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

   303   else ();*)

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

   306  val pa = TermC.free2var (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)

   307  tracing "paF2=..."; TermC.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 = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)";     (*<<<<<<<-------------*)

   315  if TermC.matches thy tm pa then ()

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

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

   318  val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)";     (*<<<<<<<-------------*)

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

   320    else ();

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

   323  val pa = TermC.free2var (TermC.parse_test @{context} "M_b 0");

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

   325  val tm = TermC.parse_test @{context} "M_b 0";

   326  if TermC.matches thy tm pa then ()

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

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

   329  val tm = TermC.parse_test @{context} "M_b x";

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

   331    else ();

   333 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------";

   334 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------";

   335 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------";

   336 (* added after Isabelle2015->17

   337 > val (SOME ct) = TermC.parse thy "(-#5)\<up>#3";

   338 > TermC.atomty (Thm.term_of ct);

   339 *** -------------

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

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

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

   343 ***   Free ( #3, nat)

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

   345 > TermC.atomty (Thm.term_of ct);

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

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

   348 ***   Free ( R, real)

   349 ***   Free ( R, real)

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

   352 *** -------------

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

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

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

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

   357  val ctxt = (ThyC.id_to_ctxt "Isac_Knowledge")

   358  val str = "x + z";

   359  TermC.parseNEW' ctxt str;

   361 "---------------";

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

   363  val t =  Syntax.read_term_global thy str;

   364  val t = TermC.typ_a2real (Syntax.read_term_global thy str);

   365  Thm.global_cterm_of thy t;

   366  case TermC.parseNEW ctxt str of

   367    SOME t' => t'

   368  | NONE => error "termC.sml parsing 'x + 2*z' failed";

   370 "===== fun TermC.parse_patt caused error in fun T_a2real ===";

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

   372  TermC.parse_patt thy "?p is_addUnordered";

   373  TermC.parse_patt thy "?p :: real";

   375 "===== fun TermC.parse_patt caused error in fun T_a2real ===";

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

   377  TermC.parse_patt thy "?p is_addUnordered";

   378  TermC.parse_patt thy "?p :: real";

   380 (* Christian Urban, 101001

   381 theory Test

   382 imports Main Complex

   383 begin

   385 let

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

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

   388   |> ML_Syntax.print_term |> ML_Syntax.atomic

   389 in

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

   391 end

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

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

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

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

   398   Envir.subst_term inst precond

   399   |> Syntax.string_of_term @{context}

   400   |> writeln

   401 end *)

   403 "----------- fun TermC.vars_of ---------------------------------------------------------------";

   404 "----------- fun TermC.vars_of ---------------------------------------------------------------";

   405 "----------- fun TermC.vars_of ---------------------------------------------------------------";

   406 val thy = @{theory Partial_Fractions};

   407 val ctxt = Proof_Context.init_global @{theory}

   409 val SOME t = TermC.parseNEW ctxt "x \<up> 2 + -1 * x * y";

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

   411 | _ => error "TermC.vars_of (x \<up> 2 + -1 * x * y) ..changed";

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

   415 case TermC.vars_of t of [Const (\<^const_name>\<open>AA\<close>, _), Const (\<^const_name>\<open>HOL.eq\<close>, _)] => ()

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

   419 "----------- *** Problem.prep_input: syntax error in '#Where' of [v";

   420 "----------- *** Problem.prep_input: syntax error in '#Where' of [v";

   421 "----------- *** Problem.prep_input: syntax error in '#Where' of [v";

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

   423  val str = "?a";

   424  val t = (thy, str) |>> Proof_Context.init_global

   425                     |-> Proof_Context.read_term_pattern;

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

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

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

   429    then ()

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

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

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

   434  val t = (thy, str) |>> Proof_Context.init_global

   435                     |-> Proof_Context.read_term_pattern;

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

   437  val Type (str, tys) = ty;

   438  if str = \<^type_name>\<open>real\<close> andalso tys = [] andalso ty = HOLogic.realT

   439    then ()

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

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

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

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

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

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

   447 val ctxt = Proof_Context.init_global thy;

   448 val ctxt = Config.put show_types true ctxt;

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

   450 val t = (thy, str) |>> Proof_Context.init_global

   451                     |-> Proof_Context.read_term_pattern;

   452 val t_real = TermC.typ_a2real t;

   453 if UnparseC.term_in_ctxt ctxt t_real =

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

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

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

   457 else error "matchsub";

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

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

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

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

   463  val str_markup = (Syntax.string_of_term

   464        (Proof_Context.init_global (ThyC.get_theory "Isac_Knowledge"))) t;

   465  val str = UnparseC.term_by_thyID "Isac_Knowledge" t;

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

   468  writeln str_markup;

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

   470  writeln str;

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

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

   474  writeln (@{make_string} str_markup);

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

   476  writeln (@{make_string} str);

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

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

   480  tracing str_markup;

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

   482  tracing str;

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

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

   486  tracing (@{make_string} str_markup);

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

   488  tracing (@{make_string} str);

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

   490 (*

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

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

   493  tracing str_markup;

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

   495  tracing str;

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

   497 *)

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

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

   501  val str_markup = (Syntax.string_of_term

   502        (Proof_Context.init_global (ThyC.get_theory "Isac_Knowledge"))) t;

   503  val str = UnparseC.term_by_thyID "Isac_Knowledge" t;

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

   506  writeln str_markup;

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

   508  writeln str;

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

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

   512  writeln (@{make_string} str_markup);

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

   514  writeln (@{make_string} str);

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

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

   518  tracing str_markup;

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

   520  tracing str;

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

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

   524  tracing (@{make_string} str_markup);

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

   526  tracing (@{make_string} str);

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

   528 (*

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

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

   531  tracing str_markup;

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

   533  tracing str;

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

   535 *)

   537 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";

   538 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";

   539 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";

   540 if TermC.is_bdv_subst (TermC.parse_test @{context} "[(''bdv'', v_v)]") then ()

   541 else error "TermC.is_bdv_subst canged 1";

   543 if TermC.is_bdv_subst (TermC.parse_test @{context} "[(''bdv_1'', v_s1),(''bdv_2'', v_s2)]") then ()

   544 else error "TermC.is_bdv_subst canged 2";

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

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

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

   549 if TermC.str_of_int 1 = "1" then () else error "str_of_int 1";

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

   552 "----------- fun TermC.scala_of_term -----------------------------------------------------------------";

   553 "----------- fun TermC.scala_of_term -----------------------------------------------------------------";

   554 "----------- fun TermC.scala_of_term -----------------------------------------------------------------";

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

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

   557 then () else error "TermC.scala_of_term  aaa::real";

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

   560 if TermC.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\"))))"

   561 then () else error "TermC.scala_of_term  aaa + bbb";

   563 "----------- fun TermC.contains_Var ------------------------------------------------------------------";

   564 "----------- fun TermC.contains_Var ------------------------------------------------------------------";

   565 "----------- fun TermC.contains_Var ------------------------------------------------------------------";

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

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

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

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

   572 "----------- fun int_opt_of_string, fun is_num -------------------------------------------------";

   573 "----------- fun int_opt_of_string, fun is_num -------------------------------------------------";

   574 "----------- fun int_opt_of_string, fun is_num -------------------------------------------------";

   575 case ThmC_Def.int_opt_of_string "123" of

   576   SOME 123 => () | _ => raise error "ThmC_Def.int_opt_of_string  123  changed";

   577 case ThmC_Def.int_opt_of_string "(-123)" of

   578   SOME ~123 => () | _ => raise error "ThmC_Def.int_opt_of_string  (-123)  changed";

   579 case ThmC_Def.int_opt_of_string "#123" of

   580   NONE => () | _ => raise error "ThmC_Def.int_opt_of_string  #123  changed";

   581 case ThmC_Def.int_opt_of_string "-123" of

   582   SOME ~123 => () | _ => raise error "ThmC_Def.int_opt_of_string  -123  changed";

   584 val t = TermC.parse_test @{context} "1";

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

   587 val t = TermC.parse_test @{context} "-1";

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

   590 val t = TermC.parse_test @{context} "a123";

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

   593 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";

   594 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";

   595 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";

   596 val t = TermC.parse_test @{context} "q_0/2 * L * x";

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

   599 val t = TermC.parse_test @{context} "M_b x";

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

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

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

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

   605 val t = TermC.parse_test @{context} "R=(R::real)";

   606 val T = type_of t;

   607 val ss = TermC.list2isalist T [t,t,t];

   608 if UnparseC.term ss = "[R = R, R = R, R = R]" then () else error "list2isalist 1";

   610 val t = TermC.parse_test @{context} "[a=b,c=d,e=f]";

   611 val il = TermC.isalist2list t;

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

   614 val t = TermC.parse_test @{context} "[a=b,c=d,e=f]";

   615 val il = TermC.isalist2list t;

   616 if UnparseC.terms il = "[\"a = b\", \"c = d\", \"e = f\"]" then () else error "isalist2list 3";

   618 val t = TermC.parse_test @{context} "ss___s::bool list";

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

   621 "----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------";

   622 "----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------";

   623 "----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------";

   624 val prop = Thm.prop_of @{thm real_mult_div_cancel2};

   625 UnparseC.term prop = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";

   626 val t as Const (\<^const_name>\<open>Pure.imp\<close>, _) $

   627       (Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>Not\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Var (("k", 0), _) $ Const (\<^const_name>\<open>Groups.zero\<close>, _)))) $

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

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

   630           (Const (\<^const_name>\<open>divide\<close>, _) $ (Const (\<^const_name>\<open>times\<close>, _) $ Var (("m", 0), _) $ Var (("k", 0), _)) $

   631             (Const (\<^const_name>\<open>times\<close>, _) $ Var (("n", 0), _) $ Var (("k", 0), _))) $

   632           (Const (\<^const_name>\<open>divide\<close>, _) $ Var (("m", 0), _) $ Var (("n", 0), _)))) = prop;

   633 val SOME t' = TermC.strip_imp_prems' t;

   634 if  UnparseC.term t' = "(\<Longrightarrow>) (?k \<noteq> 0)" then () else error "TermC.strip_imp_prems' changed";

   636 val thm = @{thm frac_sym_conv};

   637 val prop = Thm.prop_of thm;

   638 val concl = Logic.strip_imp_concl prop;

   639 val SOME prems = TermC.strip_imp_prems' prop;

   640 val prop' = TermC.ins_concl prems concl;

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

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

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

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

   646 val T =  type_of (TermC.parseNEW' ctxt "12::real");

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

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

   650 val t = TermC.parse_test @{context} "aaa + bbb";

   651 val op_ as Const (\<^const_name>\<open>plus\<close>, Top) $ Free ("aaa", T1) $ Free ("bbb", T2) = t;

   652 val t' = TermC.mk_num_op_num T1 T2 (\<^const_name>\<open>plus\<close>, Top) 2 3;

   653 if UnparseC.term t' = "2 + 3" then () else error "mk_num_op_num";

   655 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";

   656 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";

   657 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";

   658 val t = TermC.parseNEW' ctxt "(3::real) ^ 4";

   659 val hT = type_of (head_of t);

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

   661 then () else error "TermC.dest_binop_typ";

   663 "----------- fun TermC.is_list -----------------------------------------------------------------------";

   664 "----------- fun TermC.is_list -----------------------------------------------------------------------";

   665 "----------- fun TermC.is_list -----------------------------------------------------------------------";

   666 val (SOME ct) = TermC.parseNEW ctxt "lll::real list";

   667 val t = TermC.parse_test @{context} "lll::real list";

   668 val ty = Term.type_of ct;

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

   671 val t = TermC.parse_test @{context} "[a, b, c]";

   672 val ty = Term.type_of ct;

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

   675 "----------- fun mk_frac, proper term with uminus ----------------------------------------------";

   676 "----------- fun mk_frac, proper term with uminus ----------------------------------------------";

   677 "----------- fun mk_frac, proper term with uminus ----------------------------------------------";

   678      TermC.mk_frac: typ -> int * (int * int) -> term;

   679      TermC.mk_frac HOLogic.realT (~1, (6, 8));

   680 "~~~~~ fun mk_frac , args:"; val (T, (sg, (i1, i2))) = (HOLogic.realT, (~1, (6, 8)));

   681 val xxx = (*return value*) Const (\<^const_name>\<open>divide\<close>, T --> T) $

   682       mk_negative T (HOLogic.mk_number T i1) $ HOLogic.mk_number T i2;

   684 val (T_div, T_uminus) =

   685 case xxx of

   686   Const (\<^const_name>\<open>divide\<close>, T_div) $                                  (* divide *)

   687     (Const (\<^const_name>\<open>uminus\<close>, T_uminus) $                           (* uminus *)

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

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

   690     => (T_div, T_uminus)

   691 | _ => error "mk_frac 6 / - 8 \<longrightarrow> - 3 / 4 CHANGED";

   693 case T_div of

   694   Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>real\<close>, []), Type (\<^type_name>\<open>real\<close>, [])]) => ()

   695 | _ => error "T_div CHANGED in fun mk_frac";

   696 case T_uminus of

   697   Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>real\<close>, []), Type (\<^type_name>\<open>real\<close>, [])]) => ()

   698 | _ => error "T_uminus CHANGED in fun mk_frac";

   700 (* IMproper term for "6 / - 8 = - 3 / (4::real)"

   702   (Const (\<^const_name>\<open>uminus\<close>, _) $                                    (* uminus *)

   703     (Const (\<^const_name>\<open>divide\<close>, _) $                                   (* divide *)

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

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

   706 *)

author	wneuper <Walther.Neuper@jku.at>
	Sun, 09 Oct 2022 07:44:22 +0200
changeset 60565	f92963a33fe3
parent 60477	4ac966aaa785
child 60581	f66543d75c0c
permissions	-rw-r--r--