Theory SMT_Examples

(*  Title:      HOL/SMT_Examples/SMT_Examples.thy
    Author:     Sascha Boehme, TU Muenchen
*)

section ‹Examples for the SMT binding›

theory SMT_Examples
imports Complex_Main
begin

external_file ‹SMT_Examples.certs›
declare [[smt_certificates = "SMT_Examples.certs"]]
declare [[smt_read_only_certificates = true]]


section ‹Propositional and first-order logic›

lemma "True" by smt
lemma "p ∨ ¬p" by smt
lemma "(p ∧ True) = p" by smt
lemma "(p ∨ q) ∧ ¬p ⟹ q" by smt
lemma "(a ∧ b) ∨ (c ∧ d) ⟹ (a ∧ b) ∨ (c ∧ d)" by smt
lemma "(p1 ∧ p2) ∨ p3 ⟶ (p1 ⟶ (p3 ∧ p2) ∨ (p1 ∧ p3)) ∨ p1" by smt
lemma "P = P = P = P = P = P = P = P = P = P" by smt

lemma
  assumes "a ∨ b ∨ c ∨ d"
      and "e ∨ f ∨ (a ∧ d)"
      and "¬ (a ∨ (c ∧ ~c)) ∨ b"
      and "¬ (b ∧ (x ∨ ¬ x)) ∨ c"
      and "¬ (d ∨ False) ∨ c"
      and "¬ (c ∨ (¬ p ∧ (p ∨ (q ∧ ¬ q))))"
  shows False
  using assms by smt

axiomatization symm_f :: "'a ⇒ 'a ⇒ 'a" where
  symm_f: "symm_f x y = symm_f y x"

lemma "a = a ∧ symm_f a b = symm_f b a"
  by (smt symm_f)

(*
Taken from ~~/src/HOL/ex/SAT_Examples.thy.
Translated from TPTP problem library: PUZ015-2.006.dimacs
*)
lemma
  assumes "~x0"
  and "~x30"
  and "~x29"
  and "~x59"
  and "x1 ∨ x31 ∨ x0"
  and "x2 ∨ x32 ∨ x1"
  and "x3 ∨ x33 ∨ x2"
  and "x4 ∨ x34 ∨ x3"
  and "x35 ∨ x4"
  and "x5 ∨ x36 ∨ x30"
  and "x6 ∨ x37 ∨ x5 ∨ x31"
  and "x7 ∨ x38 ∨ x6 ∨ x32"
  and "x8 ∨ x39 ∨ x7 ∨ x33"
  and "x9 ∨ x40 ∨ x8 ∨ x34"
  and "x41 ∨ x9 ∨ x35"
  and "x10 ∨ x42 ∨ x36"
  and "x11 ∨ x43 ∨ x10 ∨ x37"
  and "x12 ∨ x44 ∨ x11 ∨ x38"
  and "x13 ∨ x45 ∨ x12 ∨ x39"
  and "x14 ∨ x46 ∨ x13 ∨ x40"
  and "x47 ∨ x14 ∨ x41"
  and "x15 ∨ x48 ∨ x42"
  and "x16 ∨ x49 ∨ x15 ∨ x43"
  and "x17 ∨ x50 ∨ x16 ∨ x44"
  and "x18 ∨ x51 ∨ x17 ∨ x45"
  and "x19 ∨ x52 ∨ x18 ∨ x46"
  and "x53 ∨ x19 ∨ x47"
  and "x20 ∨ x54 ∨ x48"
  and "x21 ∨ x55 ∨ x20 ∨ x49"
  and "x22 ∨ x56 ∨ x21 ∨ x50"
  and "x23 ∨ x57 ∨ x22 ∨ x51"
  and "x24 ∨ x58 ∨ x23 ∨ x52"
  and "x59 ∨ x24 ∨ x53"
  and "x25 ∨ x54"
  and "x26 ∨ x25 ∨ x55"
  and "x27 ∨ x26 ∨ x56"
  and "x28 ∨ x27 ∨ x57"
  and "x29 ∨ x28 ∨ x58"
  and "~x1 ∨ ~x31"
  and "~x1 ∨ ~x0"
  and "~x31 ∨ ~x0"
  and "~x2 ∨ ~x32"
  and "~x2 ∨ ~x1"
  and "~x32 ∨ ~x1"
  and "~x3 ∨ ~x33"
  and "~x3 ∨ ~x2"
  and "~x33 ∨ ~x2"
  and "~x4 ∨ ~x34"
  and "~x4 ∨ ~x3"
  and "~x34 ∨ ~x3"
  and "~x35 ∨ ~x4"
  and "~x5 ∨ ~x36"
  and "~x5 ∨ ~x30"
  and "~x36 ∨ ~x30"
  and "~x6 ∨ ~x37"
  and "~x6 ∨ ~x5"
  and "~x6 ∨ ~x31"
  and "~x37 ∨ ~x5"
  and "~x37 ∨ ~x31"
  and "~x5 ∨ ~x31"
  and "~x7 ∨ ~x38"
  and "~x7 ∨ ~x6"
  and "~x7 ∨ ~x32"
  and "~x38 ∨ ~x6"
  and "~x38 ∨ ~x32"
  and "~x6 ∨ ~x32"
  and "~x8 ∨ ~x39"
  and "~x8 ∨ ~x7"
  and "~x8 ∨ ~x33"
  and "~x39 ∨ ~x7"
  and "~x39 ∨ ~x33"
  and "~x7 ∨ ~x33"
  and "~x9 ∨ ~x40"
  and "~x9 ∨ ~x8"
  and "~x9 ∨ ~x34"
  and "~x40 ∨ ~x8"
  and "~x40 ∨ ~x34"
  and "~x8 ∨ ~x34"
  and "~x41 ∨ ~x9"
  and "~x41 ∨ ~x35"
  and "~x9 ∨ ~x35"
  and "~x10 ∨ ~x42"
  and "~x10 ∨ ~x36"
  and "~x42 ∨ ~x36"
  and "~x11 ∨ ~x43"
  and "~x11 ∨ ~x10"
  and "~x11 ∨ ~x37"
  and "~x43 ∨ ~x10"
  and "~x43 ∨ ~x37"
  and "~x10 ∨ ~x37"
  and "~x12 ∨ ~x44"
  and "~x12 ∨ ~x11"
  and "~x12 ∨ ~x38"
  and "~x44 ∨ ~x11"
  and "~x44 ∨ ~x38"
  and "~x11 ∨ ~x38"
  and "~x13 ∨ ~x45"
  and "~x13 ∨ ~x12"
  and "~x13 ∨ ~x39"
  and "~x45 ∨ ~x12"
  and "~x45 ∨ ~x39"
  and "~x12 ∨ ~x39"
  and "~x14 ∨ ~x46"
  and "~x14 ∨ ~x13"
  and "~x14 ∨ ~x40"
  and "~x46 ∨ ~x13"
  and "~x46 ∨ ~x40"
  and "~x13 ∨ ~x40"
  and "~x47 ∨ ~x14"
  and "~x47 ∨ ~x41"
  and "~x14 ∨ ~x41"
  and "~x15 ∨ ~x48"
  and "~x15 ∨ ~x42"
  and "~x48 ∨ ~x42"
  and "~x16 ∨ ~x49"
  and "~x16 ∨ ~x15"
  and "~x16 ∨ ~x43"
  and "~x49 ∨ ~x15"
  and "~x49 ∨ ~x43"
  and "~x15 ∨ ~x43"
  and "~x17 ∨ ~x50"
  and "~x17 ∨ ~x16"
  and "~x17 ∨ ~x44"
  and "~x50 ∨ ~x16"
  and "~x50 ∨ ~x44"
  and "~x16 ∨ ~x44"
  and "~x18 ∨ ~x51"
  and "~x18 ∨ ~x17"
  and "~x18 ∨ ~x45"
  and "~x51 ∨ ~x17"
  and "~x51 ∨ ~x45"
  and "~x17 ∨ ~x45"
  and "~x19 ∨ ~x52"
  and "~x19 ∨ ~x18"
  and "~x19 ∨ ~x46"
  and "~x52 ∨ ~x18"
  and "~x52 ∨ ~x46"
  and "~x18 ∨ ~x46"
  and "~x53 ∨ ~x19"
  and "~x53 ∨ ~x47"
  and "~x19 ∨ ~x47"
  and "~x20 ∨ ~x54"
  and "~x20 ∨ ~x48"
  and "~x54 ∨ ~x48"
  and "~x21 ∨ ~x55"
  and "~x21 ∨ ~x20"
  and "~x21 ∨ ~x49"
  and "~x55 ∨ ~x20"
  and "~x55 ∨ ~x49"
  and "~x20 ∨ ~x49"
  and "~x22 ∨ ~x56"
  and "~x22 ∨ ~x21"
  and "~x22 ∨ ~x50"
  and "~x56 ∨ ~x21"
  and "~x56 ∨ ~x50"
  and "~x21 ∨ ~x50"
  and "~x23 ∨ ~x57"
  and "~x23 ∨ ~x22"
  and "~x23 ∨ ~x51"
  and "~x57 ∨ ~x22"
  and "~x57 ∨ ~x51"
  and "~x22 ∨ ~x51"
  and "~x24 ∨ ~x58"
  and "~x24 ∨ ~x23"
  and "~x24 ∨ ~x52"
  and "~x58 ∨ ~x23"
  and "~x58 ∨ ~x52"
  and "~x23 ∨ ~x52"
  and "~x59 ∨ ~x24"
  and "~x59 ∨ ~x53"
  and "~x24 ∨ ~x53"
  and "~x25 ∨ ~x54"
  and "~x26 ∨ ~x25"
  and "~x26 ∨ ~x55"
  and "~x25 ∨ ~x55"
  and "~x27 ∨ ~x26"
  and "~x27 ∨ ~x56"
  and "~x26 ∨ ~x56"
  and "~x28 ∨ ~x27"
  and "~x28 ∨ ~x57"
  and "~x27 ∨ ~x57"
  and "~x29 ∨ ~x28"
  and "~x29 ∨ ~x58"
  and "~x28 ∨ ~x58"
  shows False
  using assms by smt

lemma "∀x::int. P x ⟶ (∀y::int. P x ∨ P y)"
  by smt

lemma
  assumes "(∀x y. P x y = x)"
  shows "(∃y. P x y) = P x c"
  using assms by smt

lemma
  assumes "(∀x y. P x y = x)"
  and "(∀x. ∃y. P x y) = (∀x. P x c)"
  shows "(∃y. P x y) = P x c"
  using assms by smt

lemma
  assumes "if P x then ¬(∃y. P y) else (∀y. ¬P y)"
  shows "P x ⟶ P y"
  using assms by smt


section ‹Arithmetic›

subsection ‹Linear arithmetic over integers and reals›

lemma "(3::int) = 3" by smt
lemma "(3::real) = 3" by smt
lemma "(3 :: int) + 1 = 4" by smt
lemma "x + (y + z) = y + (z + (x::int))" by smt
lemma "max (3::int) 8 > 5" by smt
lemma "¦x :: real¦ + ¦y¦ ≥ ¦x + y¦" by smt
lemma "P ((2::int) < 3) = P True" by smt
lemma "x + 3 ≥ 4 ∨ x < (1::int)" by smt

lemma
  assumes "x ≥ (3::int)" and "y = x + 4"
  shows "y - x > 0"
  using assms by smt

lemma "let x = (2 :: int) in x + x ≠ 5" by smt

lemma
  fixes x :: real
  assumes "3 * x + 7 * a < 4" and "3 < 2 * x"
  shows "a < 0"
  using assms by smt

lemma "(0 ≤ y + -1 * x ∨ ¬ 0 ≤ x ∨ 0 ≤ (x::int)) = (¬ False)" by smt

lemma "
  (n < m ∧ m < n') ∨ (n < m ∧ m = n') ∨ (n < n' ∧ n' < m) ∨
  (n = n' ∧ n' < m) ∨ (n = m ∧ m < n') ∨
  (n' < m ∧ m < n) ∨ (n' < m ∧ m = n) ∨
  (n' < n ∧ n < m) ∨ (n' = n ∧ n < m) ∨ (n' = m ∧ m < n) ∨
  (m < n ∧ n < n') ∨ (m < n ∧ n' = n) ∨ (m < n' ∧ n' < n) ∨
  (m = n ∧ n < n') ∨ (m = n' ∧ n' < n) ∨
  (n' = m ∧ m = (n::int))"
  by smt

text‹
The following example was taken from HOL/ex/PresburgerEx.thy, where it says:

  This following theorem proves that all solutions to the
  recurrence relation $x_{i+2} = |x_{i+1}| - x_i$ are periodic with
  period 9.  The example was brought to our attention by John
  Harrison. It does does not require Presburger arithmetic but merely
  quantifier-free linear arithmetic and holds for the rationals as well.

  Warning: it takes (in 2006) over 4.2 minutes!

There, it is proved by "arith". SMT is able to prove this within a fraction
of one second. With proof reconstruction, it takes about 13 seconds on a Core2
processor.
›

lemma "⟦ x3 = ¦x2¦ - x1; x4 = ¦x3¦ - x2; x5 = ¦x4¦ - x3;
         x6 = ¦x5¦ - x4; x7 = ¦x6¦ - x5; x8 = ¦x7¦ - x6;
         x9 = ¦x8¦ - x7; x10 = ¦x9¦ - x8; x11 = ¦x10¦ - x9 ⟧
 ⟹ x1 = x10 ∧ x2 = (x11::int)"
  by smt


lemma "let P = 2 * x + 1 > x + (x::real) in P ∨ False ∨ P" by smt

lemma "x + (let y = x mod 2 in 2 * y + 1) ≥ x + (1::int)"
  using [[z3_extensions]] by smt

lemma "x + (let y = x mod 2 in y + y) < x + (3::int)"
  using [[z3_extensions]] by smt

lemma
  assumes "x ≠ (0::real)"
  shows "x + x ≠ (let P = (¦x¦ > 1) in if P ∨ ¬ P then 4 else 2) * x"
  using assms [[z3_extensions]] by smt


subsection ‹Linear arithmetic with quantifiers›

lemma "~ (∃x::int. False)" by smt
lemma "~ (∃x::real. False)" by smt

lemma "∃x::int. 0 < x" by smt

lemma "∃x::real. 0 < x"
  using [[smt_oracle=true]] (* no Z3 proof *)
  by smt

lemma "∀x::int. ∃y. y > x" by smt

lemma "∀x y::int. (x = 0 ∧ y = 1) ⟶ x ≠ y" by smt
lemma "∃x::int. ∀y. x < y ⟶ y < 0 ∨ y >= 0" by smt
lemma "∀x y::int. x < y ⟶ (2 * x + 1) < (2 * y)" by smt
lemma "∀x y::int. (2 * x + 1) ≠ (2 * y)" by smt
lemma "∀x y::int. x + y > 2 ∨ x + y = 2 ∨ x + y < 2" by smt
lemma "∀x::int. if x > 0 then x + 1 > 0 else 1 > x" by smt
lemma "if (∀x::int. x < 0 ∨ x > 0) then False else True" by smt
lemma "(if (∀x::int. x < 0 ∨ x > 0) then -1 else 3) > (0::int)" by smt
lemma "~ (∃x y z::int. 4 * x + -6 * y = (1::int))" by smt
lemma "∃x::int. ∀x y. 0 < x ∧ 0 < y ⟶ (0::int) < x + y" by smt
lemma "∃u::int. ∀(x::int) y::real. 0 < x ∧ 0 < y ⟶ -1 < x" by smt
lemma "∃x::int. (∀y. y ≥ x ⟶ y > 0) ⟶ x > 0" by smt
lemma "∀(a::int) b::int. 0 < b ∨ b < 1" by smt


subsection ‹Non-linear arithmetic over integers and reals›

lemma "a > (0::int) ⟹ a*b > 0 ⟹ b > 0"
  using [[smt_oracle, z3_extensions]]
  by smt

lemma  "(a::int) * (x + 1 + y) = a * x + a * (y + 1)"
  using [[z3_extensions]]
  by smt

lemma "((x::real) * (1 + y) - x * (1 - y)) = (2 * x * y)"
  using [[z3_extensions]]
  by smt

lemma
  "(U::int) + (1 + p) * (b + e) + p * d =
   U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)"
  using [[z3_extensions]] by smt

lemma [z3_rule]:
  fixes x :: "int"
  assumes "x * y ≤ 0" and "¬ y ≤ 0" and "¬ x ≤ 0"
  shows False
  using assms by (metis mult_le_0_iff)


subsection ‹Linear arithmetic for natural numbers›

declare [[smt_nat_as_int]]

lemma "2 * (x::nat) ≠ 1" by smt

lemma "a < 3 ⟹ (7::nat) > 2 * a" by smt

lemma "let x = (1::nat) + y in x - y > 0 * x" by smt

lemma
  "let x = (1::nat) + y in
   let P = (if x > 0 then True else False) in
   False ∨ P = (x - 1 = y) ∨ (¬P ⟶ False)"
  by smt

lemma "int (nat ¦x::int¦) = ¦x¦" by (smt int_nat_eq)

definition prime_nat :: "nat ⇒ bool" where
  "prime_nat p = (1 < p ∧ (∀m. m dvd p --> m = 1 ∨ m = p))"

lemma "prime_nat (4*m + 1) ⟹ m ≥ (1::nat)" by (smt prime_nat_def)

declare [[smt_nat_as_int = false]]


section ‹Pairs›

lemma "fst (x, y) = a ⟹ x = a"
  using fst_conv by smt

lemma "p1 = (x, y) ∧ p2 = (y, x) ⟹ fst p1 = snd p2"
  using fst_conv snd_conv by smt


section ‹Higher-order problems and recursion›

lemma "i ≠ i1 ∧ i ≠ i2 ⟹ (f (i1 := v1, i2 := v2)) i = f i"
  using fun_upd_same fun_upd_apply by smt

lemma "(f g (x::'a::type) = (g x ∧ True)) ∨ (f g x = True) ∨ (g x = True)"
  by smt

lemma "id x = x ∧ id True = True"
  by (smt id_def)

lemma "i ≠ i1 ∧ i ≠ i2 ⟹ ((f (i1 := v1)) (i2 := v2)) i = f i"
  using fun_upd_same fun_upd_apply by smt

lemma
  "f (∃x. g x) ⟹ True"
  "f (∀x. g x) ⟹ True"
  by smt+

lemma True using let_rsp by smt
lemma "le = (≤) ⟹ le (3::int) 42" by smt
lemma "map (λi::int. i + 1) [0, 1] = [1, 2]" by (smt list.map)
lemma "(∀x. P x) ∨ ¬ All P" by smt

fun dec_10 :: "int ⇒ int" where
  "dec_10 n = (if n < 10 then n else dec_10 (n - 10))"

lemma "dec_10 (4 * dec_10 4) = 6" by (smt dec_10.simps)

axiomatization
  eval_dioph :: "int list ⇒ int list ⇒ int"
where
  eval_dioph_mod: "eval_dioph ks xs mod n = eval_dioph ks (map (λx. x mod n) xs) mod n"
and
  eval_dioph_div_mult:
  "eval_dioph ks (map (λx. x div n) xs) * n +
   eval_dioph ks (map (λx. x mod n) xs) = eval_dioph ks xs"

lemma
  "(eval_dioph ks xs = l) =
   (eval_dioph ks (map (λx. x mod 2) xs) mod 2 = l mod 2 ∧
    eval_dioph ks (map (λx. x div 2) xs) = (l - eval_dioph ks (map (λx. x mod 2) xs)) div 2)"
  using [[smt_oracle = true]] (*FIXME*)
  using [[z3_extensions]]
  by (smt eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])


context complete_lattice
begin

lemma
  assumes "Sup {a | i::bool. True} ≤ Sup {b | i::bool. True}"
  and "Sup {b | i::bool. True} ≤ Sup {a | i::bool. True}"
  shows "Sup {a | i::bool. True} ≤ Sup {a | i::bool. True}"
  using assms by (smt order_trans)

end


section ‹Monomorphization examples›

definition Pred :: "'a ⇒ bool" where
  "Pred x = True"

lemma poly_Pred: "Pred x ∧ (Pred [x] ∨ ¬ Pred [x])"
  by (simp add: Pred_def)

lemma "Pred (1::int)"
  by (smt poly_Pred)

axiomatization g :: "'a ⇒ nat"
axiomatization where
  g1: "g (Some x) = g [x]" and
  g2: "g None = g []" and
  g3: "g xs = length xs"

lemma "g (Some (3::int)) = g (Some True)" by (smt g1 g2 g3 list.size)

end