src/HOL/SMT_Examples/SMT_Examples.thy
author huffman
Sun Mar 25 20:15:39 2012 +0200 (2012-03-25)
changeset 47108 2a1953f0d20d
parent 46084 dd7fb9e651ad
child 47111 a4476e55a241
permissions -rw-r--r--
merged fork with new numeral representation (see NEWS)
     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_fixed=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 "distinct [x < (3::int), 3 \<le> x]" by smt
   296 
   297 lemma
   298   assumes "a > (0::int)"
   299   shows "distinct [a, a * 2, a - a]"
   300   using assms by smt
   301 
   302 lemma "
   303   (n < m & m < n') | (n < m & m = n') | (n < n' & n' < m) |
   304   (n = n' & n' < m) | (n = m & m < n') |
   305   (n' < m & m < n) | (n' < m & m = n) |
   306   (n' < n & n < m) | (n' = n & n < m) | (n' = m & m < n) |
   307   (m < n & n < n') | (m < n & n' = n) | (m < n' & n' < n) |
   308   (m = n & n < n') | (m = n' & n' < n) |
   309   (n' = m & m = (n::int))"
   310   by smt
   311 
   312 text{*
   313 The following example was taken from HOL/ex/PresburgerEx.thy, where it says:
   314 
   315   This following theorem proves that all solutions to the
   316   recurrence relation $x_{i+2} = |x_{i+1}| - x_i$ are periodic with
   317   period 9.  The example was brought to our attention by John
   318   Harrison. It does does not require Presburger arithmetic but merely
   319   quantifier-free linear arithmetic and holds for the rationals as well.
   320 
   321   Warning: it takes (in 2006) over 4.2 minutes!
   322 
   323 There, it is proved by "arith". SMT is able to prove this within a fraction
   324 of one second. With proof reconstruction, it takes about 13 seconds on a Core2
   325 processor.
   326 *}
   327 
   328 lemma "\<lbrakk> x3 = abs x2 - x1; x4 = abs x3 - x2; x5 = abs x4 - x3;
   329          x6 = abs x5 - x4; x7 = abs x6 - x5; x8 = abs x7 - x6;
   330          x9 = abs x8 - x7; x10 = abs x9 - x8; x11 = abs x10 - x9 \<rbrakk>
   331  \<Longrightarrow> x1 = x10 & x2 = (x11::int)"
   332   by smt
   333 
   334 
   335 lemma "let P = 2 * x + 1 > x + (x::real) in P \<or> False \<or> P" by smt
   336 
   337 lemma "x + (let y = x mod 2 in 2 * y + 1) \<ge> x + (1::int)" by smt
   338 
   339 lemma "x + (let y = x mod 2 in y + y) < x + (3::int)" by smt
   340 
   341 lemma
   342   assumes "x \<noteq> (0::real)"
   343   shows "x + x \<noteq> (let P = (abs x > 1) in if P \<or> \<not>P then 4 else 2) * x"
   344   using assms by smt
   345 
   346 lemma
   347   assumes "(n + m) mod 2 = 0" and "n mod 4 = 3"
   348   shows "n mod 2 = 1 & m mod 2 = (1::int)"
   349   using assms by smt
   350 
   351 
   352 
   353 subsection {* Linear arithmetic with quantifiers *}
   354 
   355 lemma "~ (\<exists>x::int. False)" by smt
   356 
   357 lemma "~ (\<exists>x::real. False)" by smt
   358 
   359 lemma "\<exists>x::int. 0 < x"
   360   using [[smt_oracle=true]] (* no Z3 proof *)
   361   by smt
   362 
   363 lemma "\<exists>x::real. 0 < x"
   364   using [[smt_oracle=true]] (* no Z3 proof *)
   365   by smt
   366 
   367 lemma "\<forall>x::int. \<exists>y. y > x"
   368   using [[smt_oracle=true]] (* no Z3 proof *)
   369   by smt
   370 
   371 lemma "\<forall>x y::int. (x = 0 \<and> y = 1) \<longrightarrow> x \<noteq> y" by smt
   372 
   373 lemma "\<exists>x::int. \<forall>y. x < y \<longrightarrow> y < 0 \<or> y >= 0" by smt
   374 
   375 lemma "\<forall>x y::int. x < y \<longrightarrow> (2 * x + 1) < (2 * y)" by smt
   376 
   377 lemma "\<forall>x y::int. (2 * x + 1) \<noteq> (2 * y)" by smt
   378 
   379 lemma "\<forall>x y::int. x + y > 2 \<or> x + y = 2 \<or> x + y < 2" by smt
   380 
   381 lemma "\<forall>x::int. if x > 0 then x + 1 > 0 else 1 > x" by smt
   382 
   383 lemma "if (ALL x::int. x < 0 \<or> x > 0) then False else True" by smt
   384 
   385 lemma "(if (ALL x::int. x < 0 \<or> x > 0) then -1 else 3) > (0::int)" by smt
   386 
   387 lemma "~ (\<exists>x y z::int. 4 * x + -6 * y = (1::int))" by smt
   388 
   389 lemma "\<exists>x::int. \<forall>x y. 0 < x \<and> 0 < y \<longrightarrow> (0::int) < x + y" by smt
   390 
   391 lemma "\<exists>u::int. \<forall>(x::int) y::real. 0 < x \<and> 0 < y \<longrightarrow> -1 < x" by smt
   392 
   393 lemma "\<exists>x::int. (\<forall>y. y \<ge> x \<longrightarrow> y > 0) \<longrightarrow> x > 0" by smt
   394 
   395 lemma "\<forall>x::int. SMT.trigger [[SMT.pat x]] (x < a \<longrightarrow> 2 * x < 2 * a)" by smt
   396 
   397 lemma "\<forall>(a::int) b::int. 0 < b \<or> b < 1" by smt
   398 
   399 
   400 subsection {* Non-linear arithmetic over integers and reals *}
   401 
   402 lemma "a > (0::int) \<Longrightarrow> a*b > 0 \<Longrightarrow> b > 0"
   403   using [[smt_oracle=true]]
   404   by smt
   405 
   406 lemma  "(a::int) * (x + 1 + y) = a * x + a * (y + 1)"
   407   by smt
   408 
   409 lemma "((x::real) * (1 + y) - x * (1 - y)) = (2 * x * y)"
   410   by smt
   411 
   412 lemma
   413   "(U::int) + (1 + p) * (b + e) + p * d =
   414    U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)"
   415   by smt
   416 
   417 lemma [z3_rule]:
   418   fixes x :: "int"
   419   assumes "x * y \<le> 0" and "\<not> y \<le> 0" and "\<not> x \<le> 0"
   420   shows False
   421   using assms by (metis mult_le_0_iff)
   422 
   423 lemma "x * y \<le> (0 :: int) \<Longrightarrow> x \<le> 0 \<or> y \<le> 0" by smt
   424 
   425 
   426 
   427 subsection {* Linear arithmetic for natural numbers *}
   428 
   429 lemma "2 * (x::nat) ~= 1" by smt
   430 
   431 lemma "a < 3 \<Longrightarrow> (7::nat) > 2 * a" by smt
   432 
   433 lemma "let x = (1::nat) + y in x - y > 0 * x" by smt
   434 
   435 lemma
   436   "let x = (1::nat) + y in
   437    let P = (if x > 0 then True else False) in
   438    False \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> False)"
   439   by smt
   440 
   441 lemma "distinct [a + (1::nat), a * 2 + 3, a - a]" by smt
   442 
   443 lemma "int (nat \<bar>x::int\<bar>) = \<bar>x\<bar>" by smt
   444 
   445 definition prime_nat :: "nat \<Rightarrow> bool" where
   446   "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
   447 lemma "prime_nat (4*m + 1) \<Longrightarrow> m \<ge> (1::nat)" by (smt prime_nat_def)
   448 
   449 
   450 section {* Pairs *}
   451 
   452 lemma "fst (x, y) = a \<Longrightarrow> x = a"
   453   using fst_conv
   454   by smt
   455 
   456 lemma "p1 = (x, y) \<and> p2 = (y, x) \<Longrightarrow> fst p1 = snd p2"
   457   using fst_conv snd_conv
   458   by smt
   459 
   460 
   461 section {* Higher-order problems and recursion *}
   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 "(f g (x::'a::type) = (g x \<and> True)) \<or> (f g x = True) \<or> (g x = True)"
   468   by smt
   469 
   470 lemma "id x = x \<and> id True = True" (* BROKEN by (smt id_def) *) oops
   471 
   472 lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> ((f (i1 := v1)) (i2 := v2)) i = f i"
   473   using fun_upd_same fun_upd_apply
   474   by smt
   475 
   476 lemma
   477   "f (\<exists>x. g x) \<Longrightarrow> True"
   478   "f (\<forall>x. g x) \<Longrightarrow> True"
   479   by smt+
   480 
   481 lemma True using let_rsp by smt
   482 
   483 lemma "le = op \<le> \<Longrightarrow> le (3::int) 42" by smt
   484 
   485 lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]" by (smt map.simps)
   486 
   487 
   488 lemma "(ALL x. P x) | ~ All P" by smt
   489 
   490 fun dec_10 :: "nat \<Rightarrow> nat" where
   491   "dec_10 n = (if n < 10 then n else dec_10 (n - 10))"
   492 lemma "dec_10 (4 * dec_10 4) = 6" by (smt dec_10.simps)
   493 
   494 
   495 axiomatization
   496   eval_dioph :: "int list \<Rightarrow> nat list \<Rightarrow> int"
   497   where
   498   eval_dioph_mod:
   499   "eval_dioph ks xs mod int n = eval_dioph ks (map (\<lambda>x. x mod n) xs) mod int n"
   500   and
   501   eval_dioph_div_mult:
   502   "eval_dioph ks (map (\<lambda>x. x div n) xs) * int n +
   503    eval_dioph ks (map (\<lambda>x. x mod n) xs) = eval_dioph ks xs"
   504 lemma
   505   "(eval_dioph ks xs = l) =
   506    (eval_dioph ks (map (\<lambda>x. x mod 2) xs) mod 2 = l mod 2 \<and>
   507     eval_dioph ks (map (\<lambda>x. x div 2) xs) =
   508       (l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)"
   509   using [[smt_oracle=true]] (*FIXME*)
   510   by (smt eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
   511 
   512 
   513 context complete_lattice
   514 begin
   515 
   516 lemma
   517   assumes "Sup { a | i::bool . True } \<le> Sup { b | i::bool . True }"
   518   and     "Sup { b | i::bool . True } \<le> Sup { a | i::bool . True }"
   519   shows   "Sup { a | i::bool . True } \<le> Sup { a | i::bool . True }"
   520   using assms by (smt order_trans)
   521 
   522 end
   523 
   524 
   525 
   526 section {* Monomorphization examples *}
   527 
   528 definition Pred :: "'a \<Rightarrow> bool" where "Pred x = True"
   529 lemma poly_Pred: "Pred x \<and> (Pred [x] \<or> \<not>Pred[x])" by (simp add: Pred_def)
   530 lemma "Pred (1::int)" by (smt poly_Pred)
   531 
   532 axiomatization g :: "'a \<Rightarrow> nat"
   533 axiomatization where
   534   g1: "g (Some x) = g [x]" and
   535   g2: "g None = g []" and
   536   g3: "g xs = length xs"
   537 lemma "g (Some (3::int)) = g (Some True)" by (smt g1 g2 g3 list.size)
   538 
   539 end