src/HOL/SMT_Examples/SMT_Examples.thy
author haftmann
Sat Jul 05 11:01:53 2014 +0200 (2014-07-05)
changeset 57514 bdc2c6b40bf2
parent 57232 8cecd655eef4
child 57696 fb71c6f100f8
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
     1 (*  Title:      HOL/SMT_Examples/SMT_Examples.thy
     2     Author:     Sascha Boehme, TU Muenchen
     3 *)
     4 
     5 header {* Examples for the SMT binding *}
     6 
     7 theory SMT_Examples
     8 imports Complex_Main
     9 begin
    10 
    11 declare [[smt_certificates = "SMT_Examples.certs"]]
    12 declare [[smt_read_only_certificates = true]]
    13 
    14 declare [[smt2_certificates = "SMT_Examples.certs2"]]
    15 declare [[smt2_read_only_certificates = true]]
    16 
    17 
    18 section {* Propositional and first-order logic *}
    19 
    20 lemma "True" by smt2
    21 lemma "p \<or> \<not>p" by smt2
    22 lemma "(p \<and> True) = p" by smt2
    23 lemma "(p \<or> q) \<and> \<not>p \<Longrightarrow> q" by smt2
    24 lemma "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)" by smt2
    25 lemma "(p1 \<and> p2) \<or> p3 \<longrightarrow> (p1 \<longrightarrow> (p3 \<and> p2) \<or> (p1 \<and> p3)) \<or> p1" by smt2
    26 lemma "P = P = P = P = P = P = P = P = P = P" by smt2
    27 
    28 lemma
    29   assumes "a \<or> b \<or> c \<or> d"
    30       and "e \<or> f \<or> (a \<and> d)"
    31       and "\<not> (a \<or> (c \<and> ~c)) \<or> b"
    32       and "\<not> (b \<and> (x \<or> \<not> x)) \<or> c"
    33       and "\<not> (d \<or> False) \<or> c"
    34       and "\<not> (c \<or> (\<not> p \<and> (p \<or> (q \<and> \<not> q))))"
    35   shows False
    36   using assms by smt2
    37 
    38 axiomatization symm_f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    39   symm_f: "symm_f x y = symm_f y x"
    40 
    41 lemma "a = a \<and> symm_f a b = symm_f b a" by (smt2 symm_f)
    42 
    43 (*
    44 Taken from ~~/src/HOL/ex/SAT_Examples.thy.
    45 Translated from TPTP problem library: PUZ015-2.006.dimacs
    46 *)
    47 lemma
    48   assumes "~x0"
    49   and "~x30"
    50   and "~x29"
    51   and "~x59"
    52   and "x1 \<or> x31 \<or> x0"
    53   and "x2 \<or> x32 \<or> x1"
    54   and "x3 \<or> x33 \<or> x2"
    55   and "x4 \<or> x34 \<or> x3"
    56   and "x35 \<or> x4"
    57   and "x5 \<or> x36 \<or> x30"
    58   and "x6 \<or> x37 \<or> x5 \<or> x31"
    59   and "x7 \<or> x38 \<or> x6 \<or> x32"
    60   and "x8 \<or> x39 \<or> x7 \<or> x33"
    61   and "x9 \<or> x40 \<or> x8 \<or> x34"
    62   and "x41 \<or> x9 \<or> x35"
    63   and "x10 \<or> x42 \<or> x36"
    64   and "x11 \<or> x43 \<or> x10 \<or> x37"
    65   and "x12 \<or> x44 \<or> x11 \<or> x38"
    66   and "x13 \<or> x45 \<or> x12 \<or> x39"
    67   and "x14 \<or> x46 \<or> x13 \<or> x40"
    68   and "x47 \<or> x14 \<or> x41"
    69   and "x15 \<or> x48 \<or> x42"
    70   and "x16 \<or> x49 \<or> x15 \<or> x43"
    71   and "x17 \<or> x50 \<or> x16 \<or> x44"
    72   and "x18 \<or> x51 \<or> x17 \<or> x45"
    73   and "x19 \<or> x52 \<or> x18 \<or> x46"
    74   and "x53 \<or> x19 \<or> x47"
    75   and "x20 \<or> x54 \<or> x48"
    76   and "x21 \<or> x55 \<or> x20 \<or> x49"
    77   and "x22 \<or> x56 \<or> x21 \<or> x50"
    78   and "x23 \<or> x57 \<or> x22 \<or> x51"
    79   and "x24 \<or> x58 \<or> x23 \<or> x52"
    80   and "x59 \<or> x24 \<or> x53"
    81   and "x25 \<or> x54"
    82   and "x26 \<or> x25 \<or> x55"
    83   and "x27 \<or> x26 \<or> x56"
    84   and "x28 \<or> x27 \<or> x57"
    85   and "x29 \<or> x28 \<or> x58"
    86   and "~x1 \<or> ~x31"
    87   and "~x1 \<or> ~x0"
    88   and "~x31 \<or> ~x0"
    89   and "~x2 \<or> ~x32"
    90   and "~x2 \<or> ~x1"
    91   and "~x32 \<or> ~x1"
    92   and "~x3 \<or> ~x33"
    93   and "~x3 \<or> ~x2"
    94   and "~x33 \<or> ~x2"
    95   and "~x4 \<or> ~x34"
    96   and "~x4 \<or> ~x3"
    97   and "~x34 \<or> ~x3"
    98   and "~x35 \<or> ~x4"
    99   and "~x5 \<or> ~x36"
   100   and "~x5 \<or> ~x30"
   101   and "~x36 \<or> ~x30"
   102   and "~x6 \<or> ~x37"
   103   and "~x6 \<or> ~x5"
   104   and "~x6 \<or> ~x31"
   105   and "~x37 \<or> ~x5"
   106   and "~x37 \<or> ~x31"
   107   and "~x5 \<or> ~x31"
   108   and "~x7 \<or> ~x38"
   109   and "~x7 \<or> ~x6"
   110   and "~x7 \<or> ~x32"
   111   and "~x38 \<or> ~x6"
   112   and "~x38 \<or> ~x32"
   113   and "~x6 \<or> ~x32"
   114   and "~x8 \<or> ~x39"
   115   and "~x8 \<or> ~x7"
   116   and "~x8 \<or> ~x33"
   117   and "~x39 \<or> ~x7"
   118   and "~x39 \<or> ~x33"
   119   and "~x7 \<or> ~x33"
   120   and "~x9 \<or> ~x40"
   121   and "~x9 \<or> ~x8"
   122   and "~x9 \<or> ~x34"
   123   and "~x40 \<or> ~x8"
   124   and "~x40 \<or> ~x34"
   125   and "~x8 \<or> ~x34"
   126   and "~x41 \<or> ~x9"
   127   and "~x41 \<or> ~x35"
   128   and "~x9 \<or> ~x35"
   129   and "~x10 \<or> ~x42"
   130   and "~x10 \<or> ~x36"
   131   and "~x42 \<or> ~x36"
   132   and "~x11 \<or> ~x43"
   133   and "~x11 \<or> ~x10"
   134   and "~x11 \<or> ~x37"
   135   and "~x43 \<or> ~x10"
   136   and "~x43 \<or> ~x37"
   137   and "~x10 \<or> ~x37"
   138   and "~x12 \<or> ~x44"
   139   and "~x12 \<or> ~x11"
   140   and "~x12 \<or> ~x38"
   141   and "~x44 \<or> ~x11"
   142   and "~x44 \<or> ~x38"
   143   and "~x11 \<or> ~x38"
   144   and "~x13 \<or> ~x45"
   145   and "~x13 \<or> ~x12"
   146   and "~x13 \<or> ~x39"
   147   and "~x45 \<or> ~x12"
   148   and "~x45 \<or> ~x39"
   149   and "~x12 \<or> ~x39"
   150   and "~x14 \<or> ~x46"
   151   and "~x14 \<or> ~x13"
   152   and "~x14 \<or> ~x40"
   153   and "~x46 \<or> ~x13"
   154   and "~x46 \<or> ~x40"
   155   and "~x13 \<or> ~x40"
   156   and "~x47 \<or> ~x14"
   157   and "~x47 \<or> ~x41"
   158   and "~x14 \<or> ~x41"
   159   and "~x15 \<or> ~x48"
   160   and "~x15 \<or> ~x42"
   161   and "~x48 \<or> ~x42"
   162   and "~x16 \<or> ~x49"
   163   and "~x16 \<or> ~x15"
   164   and "~x16 \<or> ~x43"
   165   and "~x49 \<or> ~x15"
   166   and "~x49 \<or> ~x43"
   167   and "~x15 \<or> ~x43"
   168   and "~x17 \<or> ~x50"
   169   and "~x17 \<or> ~x16"
   170   and "~x17 \<or> ~x44"
   171   and "~x50 \<or> ~x16"
   172   and "~x50 \<or> ~x44"
   173   and "~x16 \<or> ~x44"
   174   and "~x18 \<or> ~x51"
   175   and "~x18 \<or> ~x17"
   176   and "~x18 \<or> ~x45"
   177   and "~x51 \<or> ~x17"
   178   and "~x51 \<or> ~x45"
   179   and "~x17 \<or> ~x45"
   180   and "~x19 \<or> ~x52"
   181   and "~x19 \<or> ~x18"
   182   and "~x19 \<or> ~x46"
   183   and "~x52 \<or> ~x18"
   184   and "~x52 \<or> ~x46"
   185   and "~x18 \<or> ~x46"
   186   and "~x53 \<or> ~x19"
   187   and "~x53 \<or> ~x47"
   188   and "~x19 \<or> ~x47"
   189   and "~x20 \<or> ~x54"
   190   and "~x20 \<or> ~x48"
   191   and "~x54 \<or> ~x48"
   192   and "~x21 \<or> ~x55"
   193   and "~x21 \<or> ~x20"
   194   and "~x21 \<or> ~x49"
   195   and "~x55 \<or> ~x20"
   196   and "~x55 \<or> ~x49"
   197   and "~x20 \<or> ~x49"
   198   and "~x22 \<or> ~x56"
   199   and "~x22 \<or> ~x21"
   200   and "~x22 \<or> ~x50"
   201   and "~x56 \<or> ~x21"
   202   and "~x56 \<or> ~x50"
   203   and "~x21 \<or> ~x50"
   204   and "~x23 \<or> ~x57"
   205   and "~x23 \<or> ~x22"
   206   and "~x23 \<or> ~x51"
   207   and "~x57 \<or> ~x22"
   208   and "~x57 \<or> ~x51"
   209   and "~x22 \<or> ~x51"
   210   and "~x24 \<or> ~x58"
   211   and "~x24 \<or> ~x23"
   212   and "~x24 \<or> ~x52"
   213   and "~x58 \<or> ~x23"
   214   and "~x58 \<or> ~x52"
   215   and "~x23 \<or> ~x52"
   216   and "~x59 \<or> ~x24"
   217   and "~x59 \<or> ~x53"
   218   and "~x24 \<or> ~x53"
   219   and "~x25 \<or> ~x54"
   220   and "~x26 \<or> ~x25"
   221   and "~x26 \<or> ~x55"
   222   and "~x25 \<or> ~x55"
   223   and "~x27 \<or> ~x26"
   224   and "~x27 \<or> ~x56"
   225   and "~x26 \<or> ~x56"
   226   and "~x28 \<or> ~x27"
   227   and "~x28 \<or> ~x57"
   228   and "~x27 \<or> ~x57"
   229   and "~x29 \<or> ~x28"
   230   and "~x29 \<or> ~x58"
   231   and "~x28 \<or> ~x58"
   232   shows False
   233   using assms by smt2
   234 
   235 lemma "\<forall>x::int. P x \<longrightarrow> (\<forall>y::int. P x \<or> P y)"
   236   by smt2
   237 
   238 lemma
   239   assumes "(\<forall>x y. P x y = x)"
   240   shows "(\<exists>y. P x y) = P x c"
   241   using assms by smt2
   242 
   243 lemma
   244   assumes "(\<forall>x y. P x y = x)"
   245   and "(\<forall>x. \<exists>y. P x y) = (\<forall>x. P x c)"
   246   shows "(EX y. P x y) = P x c"
   247   using assms by smt2
   248 
   249 lemma
   250   assumes "if P x then \<not>(\<exists>y. P y) else (\<forall>y. \<not>P y)"
   251   shows "P x \<longrightarrow> P y"
   252   using assms by smt2
   253 
   254 
   255 section {* Arithmetic *}
   256 
   257 subsection {* Linear arithmetic over integers and reals *}
   258 
   259 lemma "(3::int) = 3" by smt2
   260 lemma "(3::real) = 3" by smt2
   261 lemma "(3 :: int) + 1 = 4" by smt2
   262 lemma "x + (y + z) = y + (z + (x::int))" by smt2
   263 lemma "max (3::int) 8 > 5" by smt2
   264 lemma "abs (x :: real) + abs y \<ge> abs (x + y)" by smt2
   265 lemma "P ((2::int) < 3) = P True" by smt2
   266 lemma "x + 3 \<ge> 4 \<or> x < (1::int)" by smt2
   267 
   268 lemma
   269   assumes "x \<ge> (3::int)" and "y = x + 4"
   270   shows "y - x > 0"
   271   using assms by smt2
   272 
   273 lemma "let x = (2 :: int) in x + x \<noteq> 5" by smt2
   274 
   275 lemma
   276   fixes x :: real
   277   assumes "3 * x + 7 * a < 4" and "3 < 2 * x"
   278   shows "a < 0"
   279   using assms by smt2
   280 
   281 lemma "(0 \<le> y + -1 * x \<or> \<not> 0 \<le> x \<or> 0 \<le> (x::int)) = (\<not> False)" by smt2
   282 
   283 lemma "
   284   (n < m \<and> m < n') \<or> (n < m \<and> m = n') \<or> (n < n' \<and> n' < m) \<or>
   285   (n = n' \<and> n' < m) \<or> (n = m \<and> m < n') \<or>
   286   (n' < m \<and> m < n) \<or> (n' < m \<and> m = n) \<or>
   287   (n' < n \<and> n < m) \<or> (n' = n \<and> n < m) \<or> (n' = m \<and> m < n) \<or>
   288   (m < n \<and> n < n') \<or> (m < n \<and> n' = n) \<or> (m < n' \<and> n' < n) \<or>
   289   (m = n \<and> n < n') \<or> (m = n' \<and> n' < n) \<or>
   290   (n' = m \<and> m = (n::int))"
   291   by smt2
   292 
   293 text{*
   294 The following example was taken from HOL/ex/PresburgerEx.thy, where it says:
   295 
   296   This following theorem proves that all solutions to the
   297   recurrence relation $x_{i+2} = |x_{i+1}| - x_i$ are periodic with
   298   period 9.  The example was brought to our attention by John
   299   Harrison. It does does not require Presburger arithmetic but merely
   300   quantifier-free linear arithmetic and holds for the rationals as well.
   301 
   302   Warning: it takes (in 2006) over 4.2 minutes!
   303 
   304 There, it is proved by "arith". SMT is able to prove this within a fraction
   305 of one second. With proof reconstruction, it takes about 13 seconds on a Core2
   306 processor.
   307 *}
   308 
   309 lemma "\<lbrakk> x3 = abs x2 - x1; x4 = abs x3 - x2; x5 = abs x4 - x3;
   310          x6 = abs x5 - x4; x7 = abs x6 - x5; x8 = abs x7 - x6;
   311          x9 = abs x8 - x7; x10 = abs x9 - x8; x11 = abs x10 - x9 \<rbrakk>
   312  \<Longrightarrow> x1 = x10 \<and> x2 = (x11::int)"
   313   by smt2
   314 
   315 
   316 lemma "let P = 2 * x + 1 > x + (x::real) in P \<or> False \<or> P" by smt2
   317 
   318 lemma "x + (let y = x mod 2 in 2 * y + 1) \<ge> x + (1::int)"
   319   using [[z3_new_extensions]] by smt2
   320 
   321 lemma "x + (let y = x mod 2 in y + y) < x + (3::int)"
   322   using [[z3_new_extensions]] by smt2
   323 
   324 lemma
   325   assumes "x \<noteq> (0::real)"
   326   shows "x + x \<noteq> (let P = (abs x > 1) in if P \<or> \<not> P then 4 else 2) * x"
   327   using assms [[z3_new_extensions]] by smt2
   328 
   329 lemma
   330   assumes "(n + m) mod 2 = 0" and "n mod 4 = 3"
   331   shows "n mod 2 = 1 \<and> m mod 2 = (1::int)"
   332   using assms [[z3_new_extensions]] by smt2
   333 
   334 
   335 subsection {* Linear arithmetic with quantifiers *}
   336 
   337 lemma "~ (\<exists>x::int. False)" by smt2
   338 lemma "~ (\<exists>x::real. False)" by smt2
   339 
   340 lemma "\<exists>x::int. 0 < x" by smt2
   341 
   342 lemma "\<exists>x::real. 0 < x"
   343   using [[smt2_oracle=true]] (* no Z3 proof *)
   344   by smt2
   345 
   346 lemma "\<forall>x::int. \<exists>y. y > x" by smt2
   347 
   348 lemma "\<forall>x y::int. (x = 0 \<and> y = 1) \<longrightarrow> x \<noteq> y" by smt2
   349 lemma "\<exists>x::int. \<forall>y. x < y \<longrightarrow> y < 0 \<or> y >= 0" by smt2
   350 lemma "\<forall>x y::int. x < y \<longrightarrow> (2 * x + 1) < (2 * y)" by smt2
   351 lemma "\<forall>x y::int. (2 * x + 1) \<noteq> (2 * y)" by smt2
   352 lemma "\<forall>x y::int. x + y > 2 \<or> x + y = 2 \<or> x + y < 2" by smt2
   353 lemma "\<forall>x::int. if x > 0 then x + 1 > 0 else 1 > x" by smt2
   354 lemma "if (ALL x::int. x < 0 \<or> x > 0) then False else True" by smt2
   355 lemma "(if (ALL x::int. x < 0 \<or> x > 0) then -1 else 3) > (0::int)" by smt2
   356 lemma "~ (\<exists>x y z::int. 4 * x + -6 * y = (1::int))" by smt2
   357 lemma "\<exists>x::int. \<forall>x y. 0 < x \<and> 0 < y \<longrightarrow> (0::int) < x + y" by smt2
   358 lemma "\<exists>u::int. \<forall>(x::int) y::real. 0 < x \<and> 0 < y \<longrightarrow> -1 < x" by smt2
   359 lemma "\<exists>x::int. (\<forall>y. y \<ge> x \<longrightarrow> y > 0) \<longrightarrow> x > 0" by smt2
   360 lemma "\<forall>x::int.
   361   SMT2.trigger (SMT2.Symb_Cons (SMT2.Symb_Cons (SMT2.pat x) SMT2.Symb_Nil) SMT2.Symb_Nil)
   362     (x < a \<longrightarrow> 2 * x < 2 * a)" by smt2
   363 lemma "\<forall>(a::int) b::int. 0 < b \<or> b < 1" by smt2
   364 
   365 
   366 subsection {* Non-linear arithmetic over integers and reals *}
   367 
   368 lemma "a > (0::int) \<Longrightarrow> a*b > 0 \<Longrightarrow> b > 0"
   369   using [[smt2_oracle, z3_new_extensions]]
   370   by smt2
   371 
   372 lemma  "(a::int) * (x + 1 + y) = a * x + a * (y + 1)"
   373   using [[z3_new_extensions]]
   374   by smt2
   375 
   376 lemma "((x::real) * (1 + y) - x * (1 - y)) = (2 * x * y)"
   377   using [[z3_new_extensions]]
   378   by smt2
   379 
   380 lemma
   381   "(U::int) + (1 + p) * (b + e) + p * d =
   382    U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)"
   383   using [[z3_new_extensions]] by smt2
   384 
   385 lemma [z3_rule, z3_new_rule]:
   386   fixes x :: "int"
   387   assumes "x * y \<le> 0" and "\<not> y \<le> 0" and "\<not> x \<le> 0"
   388   shows False
   389   using assms by (metis mult_le_0_iff)
   390 
   391 lemma "x * y \<le> (0 :: int) \<Longrightarrow> x \<le> 0 \<or> y \<le> 0"
   392   using [[z3_with_extensions]] [[z3_new_extensions]]
   393   by smt (* smt2 FIXME: "th-lemma" tactic fails *)
   394 
   395 
   396 subsection {* Linear arithmetic for natural numbers *}
   397 
   398 lemma "2 * (x::nat) ~= 1" by smt2
   399 
   400 lemma "a < 3 \<Longrightarrow> (7::nat) > 2 * a" by smt2
   401 
   402 lemma "let x = (1::nat) + y in x - y > 0 * x" by smt2
   403 
   404 lemma
   405   "let x = (1::nat) + y in
   406    let P = (if x > 0 then True else False) in
   407    False \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> False)"
   408   by smt2
   409 
   410 lemma "int (nat \<bar>x::int\<bar>) = \<bar>x\<bar>" by smt2
   411 
   412 definition prime_nat :: "nat \<Rightarrow> bool" where
   413   "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
   414 lemma "prime_nat (4*m + 1) \<Longrightarrow> m \<ge> (1::nat)" by (smt2 prime_nat_def)
   415 
   416 
   417 section {* Pairs *}
   418 
   419 lemma "fst (x, y) = a \<Longrightarrow> x = a"
   420   using fst_conv by smt2
   421 
   422 lemma "p1 = (x, y) \<and> p2 = (y, x) \<Longrightarrow> fst p1 = snd p2"
   423   using fst_conv snd_conv by smt2
   424 
   425 
   426 section {* Higher-order problems and recursion *}
   427 
   428 lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> (f (i1 := v1, i2 := v2)) i = f i"
   429   using fun_upd_same fun_upd_apply by smt2
   430 
   431 lemma "(f g (x::'a::type) = (g x \<and> True)) \<or> (f g x = True) \<or> (g x = True)"
   432   by smt2
   433 
   434 lemma "id x = x \<and> id True = True"
   435   by (smt2 id_def)
   436 
   437 lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> ((f (i1 := v1)) (i2 := v2)) i = f i"
   438   using fun_upd_same fun_upd_apply by smt2
   439 
   440 lemma
   441   "f (\<exists>x. g x) \<Longrightarrow> True"
   442   "f (\<forall>x. g x) \<Longrightarrow> True"
   443   by smt2+
   444 
   445 lemma True using let_rsp by smt2
   446 lemma "le = op \<le> \<Longrightarrow> le (3::int) 42" by smt2
   447 lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]" by (smt2 list.map)
   448 lemma "(ALL x. P x) \<or> ~ All P" by smt2
   449 
   450 fun dec_10 :: "nat \<Rightarrow> nat" where
   451   "dec_10 n = (if n < 10 then n else dec_10 (n - 10))"
   452 
   453 lemma "dec_10 (4 * dec_10 4) = 6" by (smt2 dec_10.simps)
   454 
   455 axiomatization
   456   eval_dioph :: "int list \<Rightarrow> nat list \<Rightarrow> int"
   457 where
   458   eval_dioph_mod:
   459   "eval_dioph ks xs mod int n = eval_dioph ks (map (\<lambda>x. x mod n) xs) mod int n"
   460 and
   461   eval_dioph_div_mult:
   462   "eval_dioph ks (map (\<lambda>x. x div n) xs) * int n +
   463    eval_dioph ks (map (\<lambda>x. x mod n) xs) = eval_dioph ks xs"
   464 
   465 lemma
   466   "(eval_dioph ks xs = l) =
   467    (eval_dioph ks (map (\<lambda>x. x mod 2) xs) mod 2 = l mod 2 \<and>
   468     eval_dioph ks (map (\<lambda>x. x div 2) xs) =
   469       (l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)"
   470   using [[smt2_oracle=true]] (*FIXME*)
   471   using [[z3_new_extensions]]
   472   by (smt2 eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
   473 
   474 
   475 context complete_lattice
   476 begin
   477 
   478 lemma
   479   assumes "Sup {a | i::bool. True} \<le> Sup {b | i::bool. True}"
   480   and "Sup {b | i::bool. True} \<le> Sup {a | i::bool. True}"
   481   shows "Sup {a | i::bool. True} \<le> Sup {a | i::bool. True}"
   482   using assms by (smt2 order_trans)
   483 
   484 end
   485 
   486 
   487 section {* Monomorphization examples *}
   488 
   489 definition Pred :: "'a \<Rightarrow> bool" where "Pred x = True"
   490 
   491 lemma poly_Pred: "Pred x \<and> (Pred [x] \<or> \<not> Pred [x])" by (simp add: Pred_def)
   492 
   493 lemma "Pred (1::int)" by (smt2 poly_Pred)
   494 
   495 axiomatization g :: "'a \<Rightarrow> nat"
   496 axiomatization where
   497   g1: "g (Some x) = g [x]" and
   498   g2: "g None = g []" and
   499   g3: "g xs = length xs"
   500 
   501 lemma "g (Some (3::int)) = g (Some True)" by (smt2 g1 g2 g3 list.size)
   502 
   503 end