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