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

     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..--- details----------------";

    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 @{context} 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 = [(ParseC.parse_test @{context} "bdv", ParseC.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 @{context} 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 @{context} 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   [(ParseC.parse_test @{context} "bdv_1", ParseC.parse_test @{context} "c"),

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

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

   205  	   (ParseC.parse_test @{context} "bdv_4", ParseC.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 @{context} 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_orig =

   217   ParseC.parse_test @{context} "(tl vs_vs) from vs_vs occur_exactly_in (NTH 1 (es_es::bool list))";

   218  val env =

   219    [(ParseC.parse_test @{context} "vs_vs::real list", ParseC.parse_test @{context} "[c, c_2]"),

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

   222  val (all_Free_subst, t''') = (*keep for final test*)

   223      TermC.subst_atomic_all env t_orig;

   224 "~~~~~ fun subst_atomic_all , args:"; val (instl, t) = (env, t_orig);

   225 (*//------------------ step into subst_atomic_all ------------------------------------------\\*)

   226 (*redefine local fun*)

   227      fun subst (Abs (a, T, body)) =

   228           let

   229             val (all, body') = subst body

   230           in (all, Abs(a, T, body')) end

   231         | subst (f $ tt) =

   232 	        let

   233 	          val (all1, f') = subst f

   234 	          val (all2, tt') = subst tt

   235 	        in (all1 andalso all2, f' $ tt') end

   236         | subst (t as Free _) =

   237 	        if TermC.is_num t then (true, t) (*numerals cannot be subst*)

   238 	        else (case assoc (instl, t) of

   239 					  SOME t' => (true, t')

   240 				  | NONE => (false, t))

   241         | subst t = (true, if_none (assoc (instl, t)) t)

   243           (*pattern in fun.def.*)

   244 	        val (f $ tt) = t

   245 	          val (all1, f') = subst f

   246 (*+*)val "occur_exactly_in (tl [c, c_2]) [c, c_2]" = UnparseC.term @{context} f'

   248           (*pattern in fun.def.*)

   249 	        val (f $ tt) = f

   250 	          val (all1, f') = subst f

   251 (*+*)val "occur_exactly_in (tl [c, c_2])" = UnparseC.term @{context} f'

   253           (*pattern in fun.def.*)

   254 (*1.f*)   val (f $ tt) = f

   255 	          val (all1, f') = subst f

   256 (*+*)val (*Const ("EqSystem.*)"occur_exactly_in" = UnparseC.term @{context} f'

   258           (*pattern in fun.def.*)

   259 	        val t = f

   260 val return_occur_exactly_in as (true, Const ("EqSystem.occur_exactly_in", _)) =

   261             (true, if_none (assoc (instl, t)) t)

   263           (*pattern in fun.def.*)

   264 (*1.tt*)  val (f $ tt) = tt

   265 (*+*)val Free ("vs_vs", _) = tt

   267           (*pattern in fun.def.*)

   268 (*2*)     val (t as Free _) = tt

   269 val				  SOME t' =

   270             (*case*) assoc (instl, t) (*of*);

   271 val return_Free_ = (true, t')

   272 (*+*)val "[c, c_2]" = UnparseC.term @{context} t'

   273 (*\\------------------ step into subst_atomic_all ------------------------------------------//*)

   274 (* final test ... ----------------------------------------------------------------------------*)

   275  val (all_Free_subst, t') = (all_Free_subst, t'''); (*kept for final test*)

   276  if all_Free_subst andalso      (*-----vvvvvv--------vvvvvv--------------------------vvvvvvv, vvvvvvvvvvv*)

   277     UnparseC.term @{context} t' = "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1 [c_2 = 0, c + c_2 = 1]"

   278    then ()

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

   281  val (all_Free_subst, t') = TermC.subst_atomic_all (tl env) t_orig;

   282  if not all_Free_subst andalso  (*----vvvvv------vvvvv-------------------------ok..*)

   283     UnparseC.term @{context} t' = "tl vs_vs from vs_vs occur_exactly_in NTH 1 [c_2 = 0, c + c_2 = 1]" then ()

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

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

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

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

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

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

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

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

   293 (*default_print_depth 3; 999*) insts;

   294  (*val insts =

   295    ({},

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

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

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

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

   301 (* val t = ParseC.parse_test @{context} "x";

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

   303  handle MATCH => ???; *)

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

   306  val PARSE = Syntax.read_term_global thy;

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

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

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

   311  Vartab.dest tenv;

   313 "----------- fun TermC.matches --------------------------------";

   314 "----------- fun TermC.matches --------------------------------";

   315 "----------- fun TermC.matches --------------------------------";

   316  (*examples see

   317    test/../Knowledge/polyeq.sml:

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

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

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

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

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

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

   325  tracing "paIsa=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paIsa";

   326 (**

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

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

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

   330 **)

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

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

   333  if TermC.matches thy tm pa then ()

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

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

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

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

   338   else ();

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

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

   342  tracing "paLo2=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paLo2";

   343 (**

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

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

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

   347 **)

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

   349  val tm = ParseC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)";     (*<<<<<<<-------------*)

   350  if TermC.matches thy tm pa then ()

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

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

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

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

   355    else ();

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

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

   358   else ();*)

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

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

   362  tracing "paF2=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paF2";

   363 (**

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

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

   366 *** . Free (0, real)

   367 **)

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

   369  val tm = ParseC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)";     (*<<<<<<<-------------*)

   370  if TermC.matches thy tm pa then ()

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

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

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

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

   375    else ();

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

   378  val pa = TermC.mk_Var (ParseC.parse_test @{context} "M_b 0");

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

   380  val tm = ParseC.parse_test @{context} "M_b 0";

   381  if TermC.matches thy tm pa then ()

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

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

   384  val tm = ParseC.parse_test @{context} "M_b x";

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

   386    else ();

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

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

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

   391 (* added after Isabelle2015->17

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

   393 > TermC.atom_trace_detail @{context} (Thm.term_of ct);

   394 *** -------------

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

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

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

   398 ***   Free ( #3, nat)

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

   400 > TermC.atom_trace_detail @{context} (Thm.term_of ct);

   401 *** -------------

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

   403 ***   Free ( R, real)

   404 ***   Free ( R, real)

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

   407 *** -------------

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

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

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

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

   412  val ctxt = @{context}

   413  val str = "x + z";

   414  ParseC.term_opt ctxt str;

   416 "---------------";

   417  val ctxt = @{context}

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

   419  val t =  Syntax.read_term_global thy str;

   420  val t = ParseC.adapt_term_to_type ctxt (Syntax.read_term_global thy str);

   421  Thm.global_cterm_of thy t;

   422  case ParseC.term_opt ctxt str of

   423    SOME t' => t'

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

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

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

   428  ParseC.patt_opt thy "?p is_addUnordered";

   429  ParseC.patt_opt thy "?p :: real";

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

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

   433  ParseC.patt_opt thy "?p is_addUnordered";

   434  ParseC.patt_opt thy "?p :: real";

   436 (* Christian Urban, 101001

   437 theory Test

   438 imports Main Complex

   439 begin

   441 let

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

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

   444   |> ML_Syntax.print_term |> ML_Syntax.atomic

   445 in

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

   447 end

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

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

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

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

   454   Envir.subst_term inst precond

   455   |> Syntax.string_of_term @{context}

   456   |> writeln

   457 end *)

   459 "----------- fun TermC.vars_of ---------------------------------------------------------------";

   460 "----------- fun TermC.vars_of ---------------------------------------------------------------";

   461 "----------- fun TermC.vars_of ---------------------------------------------------------------";

   462 val thy = @{theory Partial_Fractions};

   463 val ctxt = Proof_Context.init_global @{theory}

   465 val SOME t = ParseC.term_opt ctxt "x \<up> 2 + -1 * x * y";

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

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

   469 val SOME t = ParseC.term_opt ctxt "3 = 3 * AA / 4";

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

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

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

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

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

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

   479  val str = "?a";

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

   481                     |-> Proof_Context.read_term_pattern;

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

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

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

   485    then ()

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

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

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

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

   491                     |-> Proof_Context.read_term_pattern;

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

   493  val Type (str, tys) = ty;

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

   495    then ()

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

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

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

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

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

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

   503 val ctxt = Proof_Context.init_global thy;

   504 val ctxt = Config.put show_types true ctxt;

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

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

   507                     |-> Proof_Context.read_term_pattern;

   508 val t_real = ParseC.adapt_term_to_type ctxt t;

   509 if UnparseC.term ctxt t_real =

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

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

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

   513 else error "matchsub";

   514 val ctxt = Config.put show_types false ctxt;

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

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

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

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

   521  val str_markup = (Syntax.string_of_term ctxt) t;

   522  val str = UnparseC.term @{context} t;

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

   525  writeln str_markup;

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

   527  writeln str;

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

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

   531  writeln (@{make_string} str_markup);

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

   533  writeln (@{make_string} str);

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

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

   537  tracing str_markup;

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

   539  tracing str;

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

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

   543  tracing (@{make_string} str_markup);

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

   545  tracing (@{make_string} str);

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

   547 (*

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

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

   550  tracing str_markup;

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

   552  tracing str;

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

   554 *)

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

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

   558  val str_markup = (Syntax.string_of_term ctxt) t;

   559  val str = UnparseC.term @{context} t;

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

   562  writeln str_markup;

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

   564  writeln str;

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

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

   568  writeln (@{make_string} str_markup);

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

   570  writeln (@{make_string} str);

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

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

   574  tracing str_markup;

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

   576  tracing str;

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

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

   580  tracing (@{make_string} str_markup);

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

   582  tracing (@{make_string} str);

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

   584 (*

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

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

   587  tracing str_markup;

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

   589  tracing str;

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

   591 *)

   593 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";

   594 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";

   595 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";

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

   597 else error "TermC.is_bdv_subst canged 1";

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

   600 else error "TermC.is_bdv_subst canged 2";

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

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

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

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

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

   608 "----------- fun TermC.scala_of_term -----------------------------------------------------------------";

   609 "----------- fun TermC.scala_of_term -----------------------------------------------------------------";

   610 "----------- fun TermC.scala_of_term -----------------------------------------------------------------";

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

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

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

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

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

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

   619 "----------- fun TermC.contains_Var ------------------------------------------------------------------";

   620 "----------- fun TermC.contains_Var ------------------------------------------------------------------";

   621 "----------- fun TermC.contains_Var ------------------------------------------------------------------";

   622 val SOME t = ParseC.patt_opt @{theory} "?z = 3";

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

   625 val SOME t = ParseC.patt_opt @{theory} "z = 3";

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

   628 "----------- fun int_opt_of_string, fun is_num -------------------------------------------------";

   629 "----------- fun int_opt_of_string, fun is_num -------------------------------------------------";

   630 "----------- fun int_opt_of_string, fun is_num -------------------------------------------------";

   631 case ThmC_Def.int_opt_of_string "123" of

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

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

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

   635 case ThmC_Def.int_opt_of_string "#123" of

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

   637 case ThmC_Def.int_opt_of_string "-123" of

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

   640 val t = ParseC.parse_test @{context} "1";

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

   643 val t = ParseC.parse_test @{context} "-1";

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

   646 val t = ParseC.parse_test @{context} "a123";

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

   649 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";

   650 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";

   651 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";

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

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

   655 val t = ParseC.parse_test @{context} "M_b x";

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

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

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

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

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

   662 val T = type_of t;

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

   664 if UnparseC.term @{context} ss = "[R = R, R = R, R = R]" then () else error "list2isalist 1";

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

   667 val il = TermC.isalist2list t;

   668 if UnparseC.terms @{context} il = "[a = b, c = d, e = f]" then () else error "isalist2list 2";

   670 val t = ParseC.parse_test @{context} "ss___s::bool list";

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

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

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

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

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

   677 UnparseC.term @{context} prop = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";

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

   679       (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>, _)))) $

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

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

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

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

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

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

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

   688 val thm = @{thm frac_sym_conv};

   689 val prop = Thm.prop_of thm;

   690 val concl = Logic.strip_imp_concl prop;

   691 val SOME prems = TermC.strip_imp_prems' prop;

   692 val prop' = TermC.ins_concl prems concl;

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

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

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

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

   698 val T =  type_of (ParseC.term_opt ctxt "12::real" |> the);

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

   700 if UnparseC.term @{context} t = "2 * ??.SqRoot.sqrt 3" then () else error "mk_factroot";

   702 val t = ParseC.parse_test @{context} "aaa + bbb";

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

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

   705 if UnparseC.term @{context} t' = "2 + 3" then () else error "mk_num_op_num";

   707 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";

   708 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";

   709 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";

   710 val t = ParseC.term_opt ctxt "(3::real) ^ 4" |> the;

   711 val hT = type_of (head_of t);

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

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

   715 "----------- fun TermC.is_list -----------------------------------------------------------------------";

   716 "----------- fun TermC.is_list -----------------------------------------------------------------------";

   717 "----------- fun TermC.is_list -----------------------------------------------------------------------";

   718 val (SOME ct) = ParseC.term_opt ctxt "lll::real list";

   719 val t = ParseC.parse_test @{context} "lll::real list";

   720 val ty = Term.type_of ct;

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

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

   724 val ty = Term.type_of ct;

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

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

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

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

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

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

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

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

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

   736 val (T_div, T_uminus) =

   737 case xxx of

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

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

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

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

   742     => (T_div, T_uminus)

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

   745 case T_div of

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

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

   748 case T_uminus of

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

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

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

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

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

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

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

   758 *)

author	wneuper <Walther.Neuper@jku.at>
	Mon, 01 Jan 2024 11:31:16 +0100
changeset 60789	8fa678b678e8
parent 60766	2e0603ca18a4
permissions	-rw-r--r--