Theory SMT_Tests_Verit

(*  Title:      HOL/SMT_Examples/SMT_Tests.thy
    Author:     Sascha Boehme, TU Muenchen
    Author:     Mathias Fleury, MPII, JKU
*)

section ‹Tests for the SMT binding›

theory SMT_Tests_Verit
imports Complex_Main
begin

declare [[smt_solver=verit]]
smt_status

text ‹Most examples are taken from the equivalent Z3 theory called 🗏‹SMT_Tests.thy›,
and have been taken from various Isabelle and HOL4 developments.›


section ‹Propositional logic›

lemma
  "True"
  "¬ False"
  "¬ ¬ True"
  "True ∧ True"
  "True ∨ False"
  "False ⟶ True"
  "¬ (False ⟷ True)"
  by smt+

lemma
  "P ∨ ¬ P"
  "¬ (P ∧ ¬ P)"
  "(True ∧ P) ∨ ¬ P ∨ (False ∧ P) ∨ P"
  "P ⟶ P"
  "P ∧ ¬ P ⟶ False"
  "P ∧ Q ⟶ Q ∧ P"
  "P ∨ Q ⟶ Q ∨ P"
  "P ∧ Q ⟶ P ∨ Q"
  "¬ (P ∨ Q) ⟶ ¬ P"
  "¬ (P ∨ Q) ⟶ ¬ Q"
  "¬ P ⟶ ¬ (P ∧ Q)"
  "¬ Q ⟶ ¬ (P ∧ Q)"
  "(P ∧ Q) ⟷ (¬ (¬ P ∨ ¬ Q))"
  "(P ∧ Q) ∧ R ⟶ P ∧ (Q ∧ R)"
  "(P ∨ Q) ∨ R ⟶ P ∨ (Q ∨ R)"
  "(P ∧ Q) ∨ R  ⟶ (P ∨ R) ∧ (Q ∨ R)"
  "(P ∨ R) ∧ (Q ∨ R) ⟶ (P ∧ Q) ∨ R"
  "(P ∨ Q) ∧ R ⟶ (P ∧ R) ∨ (Q ∧ R)"
  "(P ∧ R) ∨ (Q ∧ R) ⟶ (P ∨ Q) ∧ R"
  "((P ⟶ Q) ⟶ P) ⟶ P"
  "(P ⟶ R) ∧ (Q ⟶ R) ⟷ (P ∨ Q ⟶ R)"
  "(P ∧ Q ⟶ R) ⟷ (P ⟶ (Q ⟶ R))"
  "((P ⟶ R) ⟶ R) ⟶  ((Q ⟶ R) ⟶ R) ⟶ (P ∧ Q ⟶ R) ⟶ R"
  "¬ (P ⟶ R) ⟶  ¬ (Q ⟶ R) ⟶ ¬ (P ∧ Q ⟶ R)"
  "(P ⟶ Q ∧ R) ⟷ (P ⟶ Q) ∧ (P ⟶ R)"
  "P ⟶ (Q ⟶ P)"
  "(P ⟶ Q ⟶ R) ⟶ (P ⟶ Q)⟶ (P ⟶ R)"
  "(P ⟶ Q) ∨ (P ⟶ R) ⟶ (P ⟶ Q ∨ R)"
  "((((P ⟶ Q) ⟶ P) ⟶ P) ⟶ Q) ⟶ Q"
  "(P ⟶ Q) ⟶ (¬ Q ⟶ ¬ P)"
  "(P ⟶ Q ∨ R) ⟶ (P ⟶ Q) ∨ (P ⟶ R)"
  "(P ⟶ Q) ∧ (Q  ⟶ P) ⟶ (P ⟷ Q)"
  "(P ⟷ Q) ⟷ (Q ⟷ P)"
  "¬ (P ⟷ ¬ P)"
  "(P ⟶ Q) ⟷ (¬ Q ⟶ ¬ P)"
  "P ⟷ P ⟷ P ⟷ P ⟷ P ⟷ P ⟷ P ⟷ P ⟷ P ⟷ P"
  by smt+

lemma
  "(if P then Q1 else Q2) ⟷ ((P ⟶ Q1) ∧ (¬ P ⟶ Q2))"
  "if P then (Q ⟶ P) else (P ⟶ Q)"
  "(if P1 ∨ P2 then Q1 else Q2) ⟷ (if P1 then Q1 else if P2 then Q1 else Q2)"
  "(if P1 ∧ P2 then Q1 else Q2) ⟷ (if P1 then if P2 then Q1 else Q2 else Q2)"
  "(P1 ⟶ (if P2 then Q1 else Q2)) ⟷
   (if P1 ⟶ P2 then P1 ⟶ Q1 else P1 ⟶ Q2)"
  by smt+

lemma
  "case P of True ⇒ P | False ⇒ ¬ P"
  "case P of False ⇒ ¬ P | True ⇒ P"
  "case ¬ P of True ⇒ ¬ P | False ⇒ P"
  "case P of True ⇒ (Q ⟶ P) | False ⇒ (P ⟶ Q)"
  by smt+


section ‹First-order logic with equality›

lemma
  "x = x"
  "x = y ⟶ y = x"
  "x = y ∧ y = z ⟶ x = z"
  "x = y ⟶ f x = f y"
  "x = y ⟶ g x y = g y x"
  "f (f x) = x ∧ f (f (f (f (f x)))) = x ⟶ f x = x"
  "((if a then b else c) = d) = ((a ⟶ (b = d)) ∧ (¬ a ⟶ (c = d)))"
  by smt+

lemma
  "∀x. x = x"
  "(∀x. P x) ⟷ (∀y. P y)"
  "∀x. P x ⟶ (∀y. P x ∨ P y)"
  "(∀x. P x ∧ Q x) ⟷ (∀x. P x) ∧ (∀x. Q x)"
  "(∀x. P x) ∨ R ⟷ (∀x. P x ∨ R)"
  "(∀x y z. S x z) ⟷ (∀x z. S x z)"
  "(∀x y. S x y ⟶ S y x) ⟶ (∀x. S x y) ⟶ S y x"
  "(∀x. P x ⟶ P (f x)) ∧ P d ⟶ P (f(f(f(d))))"
  "(∀x y. s x y = s y x) ⟶ a = a ∧ s a b = s b a"
  "(∀s. q s ⟶ r s) ∧ ¬ r s ∧ (∀s. ¬ r s ∧ ¬ q s ⟶ p t ∨ q t) ⟶ p t ∨ r t"
  by smt+

lemma
  "(∀x. P x) ∧ R ⟷ (∀x. P x ∧ R)"
  by smt

lemma
  "∃x. x = x"
  "(∃x. P x) ⟷ (∃y. P y)"
  "(∃x. P x ∨ Q x) ⟷ (∃x. P x) ∨ (∃x. Q x)"
  "(∃x. P x) ∧ R ⟷ (∃x. P x ∧ R)"
  "(∃x y z. S x z) ⟷ (∃x z. S x z)"
  "¬ ((∃x. ¬ P x) ∧ ((∃x. P x) ∨ (∃x. P x ∧ Q x)) ∧ ¬ (∃x. P x))"
  by smt+

lemma
  "∃x y. x = y"
  "(∃x. P x) ∨ R ⟷ (∃x. P x ∨ R)"
  "∃x. P x ⟶ P a ∧ P b"
  "(∃x. Q ⟶ P x) ⟷ (Q ⟶ (∃x. P x))"
  by smt+

lemma
  "(P False ∨ P True) ∨ ¬ P False"
  by smt

lemma
  "(¬ (∃x. P x)) ⟷ (∀x. ¬ P x)"
  "(∃x. P x ⟶ Q) ⟷ (∀x. P x) ⟶ Q"
  "(∀x y. R x y = x) ⟶ (∃y. R x y) = R x c"
  "(if P x then ¬ (∃y. P y) else (∀y. ¬ P y)) ⟶ P x ⟶ P y"
  "(∀x y. R x y = x) ∧ (∀x. ∃y. R x y) = (∀x. R x c) ⟶ (∃y. R x y) = R x c"
  by smt+

lemma
  "∀x. ∃y. f x y = f x (g x)"
  "(¬ ¬ (∃x. P x)) ⟷ (¬ (∀x. ¬ P x))"
  "∀u. ∃v. ∀w. ∃x. f u v w x = f u (g u) w (h u w)"
  "∃x. if x = y then (∀y. y = x ∨ y ≠ x) else (∀y. y = (x, x) ∨ y ≠ (x, x))"
  "∃x. if x = y then (∃y. y = x ∨ y ≠ x) else (∃y. y = (x, x) ∨ y ≠ (x, x))"
  "(∃x. ∀y. P x ⟷ P y) ⟶ ((∃x. P x) ⟷ (∀y. P y))"
  "(∃y. ∀x. R x y) ⟶ (∀x. ∃y. R x y)"
  by smt+

lemma
  "(∃!x. P x) ⟶ (∃x. P x)"
  "(∃!x. P x) ⟷ (∃x. P x ∧ (∀y. y ≠ x ⟶ ¬ P y))"
  "P a ⟶ (∀x. P x ⟶ x = a) ⟶ (∃!x. P x)"
  "(∃x. P x) ∧ (∀x y. P x ∧ P y ⟶ x = y) ⟶ (∃!x. P x)"
  "(∃!x. P x) ∧ (∀x. P x ∧ (∀y. P y ⟶ y = x) ⟶ R) ⟶ R"
  by smt+

lemma
  "(∀x∈M. P x) ∧ c ∈ M ⟶ P c"
  "(∃x∈M. P x) ∨ ¬ (P c ∧ c ∈ M)"
  by smt+

lemma
  "let P = True in P"
  "let P = P1 ∨ P2 in P ∨ ¬ P"
  "let P1 = True; P2 = False in P1 ∧ P2 ⟶ P2 ∨ P1"
  "(let x = y in x) = y"
  "(let x = y in Q x) ⟷ (let z = y in Q z)"
  "(let x = y1; z = y2 in R x z) ⟷ (let z = y2; x = y1 in R x z)"
  "(let x = y1; z = y2 in R x z) ⟷ (let z = y1; x = y2 in R z x)"
  "let P = (∀x. Q x) in if P then P else ¬ P"
  by smt+

lemma
  "a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀x y. f x = f y ⟶ y = x) ⟶ f a ≠ f b"
  by smt

lemma
  "(∀x y z. f x y = f x z ⟶ y = z) ∧ b ≠ c ⟶ f a b ≠ f a c"
  "(∀x y z. f x y = f z y ⟶ x = z) ∧ a ≠ d ⟶ f a b ≠ f d b"
  by smt+


section ‹Guidance for quantifier heuristics: patterns›

lemma
  assumes "∀x.
    SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat (f x)) SMT.Symb_Nil) SMT.Symb_Nil)
    (f x = x)"
  shows "f 1 = 1"
  using assms by smt

lemma
  assumes "∀x y.
    SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat (f x))
      (SMT.Symb_Cons (SMT.pat (g y)) SMT.Symb_Nil)) SMT.Symb_Nil) (f x = g y)"
  shows "f a = g b"
  using assms by smt


section ‹Meta-logical connectives›

lemma
  "True ⟹ True"
  "False ⟹ True"
  "False ⟹ False"
  "P' x ⟹ P' x"
  "P ⟹ P ∨ Q"
  "Q ⟹ P ∨ Q"
  "¬ P ⟹ P ⟶ Q"
  "Q ⟹ P ⟶ Q"
  "⟦P; ¬ Q⟧ ⟹ ¬ (P ⟶ Q)"
  "P' x ≡ P' x"
  "P' x ≡ Q' x ⟹ P' x = Q' x"
  "P' x = Q' x ⟹ P' x ≡ Q' x"
  "x ≡ y ⟹ y ≡ z ⟹ x ≡ (z::'a::type)"
  "x ≡ y ⟹ (f x :: 'b::type) ≡ f y"
  "(⋀x. g x) ⟹ g a ∨ a"
  "(⋀x y. h x y ∧ h y x) ⟹ ∀x. h x x"
  "(p ∨ q) ∧ ¬ p ⟹ q"
  "(a ∧ b) ∨ (c ∧ d) ⟹ (a ∧ b) ∨ (c ∧ d)"
  by smt+


section ‹Natural numbers›

declare [[smt_nat_as_int]]

lemma
  "(0::nat) = 0"
  "(1::nat) = 1"
  "(0::nat) < 1"
  "(0::nat) ≤ 1"
  "(123456789::nat) < 2345678901"
  by smt+

lemma
  "Suc 0 = 1"
  "Suc x = x + 1"
  "x < Suc x"
  "(Suc x = Suc y) = (x = y)"
  "Suc (x + y) < Suc x + Suc y"
  by smt+

lemma
  "(x::nat) + 0 = x"
  "0 + x = x"
  "x + y = y + x"
  "x + (y + z) = (x + y) + z"
  "(x + y = 0) = (x = 0 ∧ y = 0)"
  by smt+

lemma
  "(x::nat) - 0 = x"
  "x < y ⟶ x - y = 0"
  "x - y = 0 ∨ y - x = 0"
  "(x - y) + y = (if x < y then y else x)"
   "x - y - z = x - (y + z)"
  by smt+

lemma
  "(x::nat) * 0 = 0"
  "0 * x = 0"
  "x * 1 = x"
  "1 * x = x"
  "3 * x = x * 3"
  by smt+

lemma
  "min (x::nat) y ≤ x"
  "min x y ≤ y"
  "min x y ≤ x + y"
  "z < x ∧ z < y ⟶ z < min x y"
  "min x y = min y x"
  "min x 0 = 0"
  by smt+

lemma
  "max (x::nat) y ≥ x"
  "max x y ≥ y"
  "max x y ≥ (x - y) + (y - x)"
  "z > x ∧ z > y ⟶ z > max x y"
  "max x y = max y x"
  "max x 0 = x"
  by smt+

lemma
  "0 ≤ (x::nat)"
  "0 < x ∧ x ≤ 1 ⟶ x = 1"
  "x ≤ x"
  "x ≤ y ⟶ 3 * x ≤ 3 * y"
  "x < y ⟶ 3 * x < 3 * y"
  "x < y ⟶ x ≤ y"
  "(x < y) = (x + 1 ≤ y)"
  "¬ (x < x)"
  "x ≤ y ⟶ y ≤ z ⟶ x ≤ z"
  "x < y ⟶ y ≤ z ⟶ x ≤ z"
  "x ≤ y ⟶ y < z ⟶ x ≤ z"
  "x < y ⟶ y < z ⟶ x < z"
  "x < y ∧ y < z ⟶ ¬ (z < x)"
  by smt+

declare [[smt_nat_as_int = false]]


section ‹Integers›

lemma
  "(0::int) = 0"
  "(0::int) = (- 0)"
  "(1::int) = 1"
  "¬ (-1 = (1::int))"
  "(0::int) < 1"
  "(0::int) ≤ 1"
  "-123 + 345 < (567::int)"
  "(123456789::int) < 2345678901"
  "(-123456789::int) < 2345678901"
  by smt+

lemma
  "(x::int) + 0 = x"
  "0 + x = x"
  "x + y = y + x"
  "x + (y + z) = (x + y) + z"
  "(x + y = 0) = (x = -y)"
  by smt+

lemma
  "(-1::int) = - 1"
  "(-3::int) = - 3"
  "-(x::int) < 0 ⟷ x > 0"
  "x > 0 ⟶ -x < 0"
  "x < 0 ⟶ -x > 0"
  by smt+

lemma
  "(x::int) - 0 = x"
  "0 - x = -x"
  "x < y ⟶ x - y < 0"
  "x - y = -(y - x)"
  "x - y = -y + x"
  "x - y - z = x - (y + z)"
  by smt+

lemma
  "(x::int) * 0 = 0"
  "0 * x = 0"
  "x * 1 = x"
  "1 * x = x"
  "x * -1 = -x"
  "-1 * x = -x"
  "3 * x = x * 3"
  by smt+

lemma
  "¦x::int¦ ≥ 0"
  "(¦x¦ = 0) = (x = 0)"
  "(x ≥ 0) = (¦x¦ = x)"
  "(x ≤ 0) = (¦x¦ = -x)"
  "¦¦x¦¦ = ¦x¦"
  by smt+

lemma
  "min (x::int) y ≤ x"
  "min x y ≤ y"
  "z < x ∧ z < y ⟶ z < min x y"
  "min x y = min y x"
  "x ≥ 0 ⟶ min x 0 = 0"
  "min x y ≤ ¦x + y¦"
  by smt+

lemma
  "max (x::int) y ≥ x"
  "max x y ≥ y"
  "z > x ∧ z > y ⟶ z > max x y"
  "max x y = max y x"
  "x ≥ 0 ⟶ max x 0 = x"
  "max x y ≥ - ¦x¦ - ¦y¦"
  by smt+

lemma
  "0 < (x::int) ∧ x ≤ 1 ⟶ x = 1"
  "x ≤ x"
  "x ≤ y ⟶ 3 * x ≤ 3 * y"
  "x < y ⟶ 3 * x < 3 * y"
  "x < y ⟶ x ≤ y"
  "(x < y) = (x + 1 ≤ y)"
  "¬ (x < x)"
  "x ≤ y ⟶ y ≤ z ⟶ x ≤ z"
  "x < y ⟶ y ≤ z ⟶ x ≤ z"
  "x ≤ y ⟶ y < z ⟶ x ≤ z"
  "x < y ⟶ y < z ⟶ x < z"
  "x < y ∧ y < z ⟶ ¬ (z < x)"
  by smt+


section ‹Reals›

lemma
  "(0::real) = 0"
  "(0::real) = -0"
  "(0::real) = (- 0)"
  "(1::real) = 1"
  "¬ (-1 = (1::real))"
  "(0::real) < 1"
  "(0::real) ≤ 1"
  "-123 + 345 < (567::real)"
  "(123456789::real) < 2345678901"
  "(-123456789::real) < 2345678901"
  by smt+

lemma
  "(x::real) + 0 = x"
  "0 + x = x"
  "x + y = y + x"
  "x + (y + z) = (x + y) + z"
  "(x + y = 0) = (x = -y)"
  by smt+

lemma
  "(-1::real) = - 1"
  "(-3::real) = - 3"
  "-(x::real) < 0 ⟷ x > 0"
  "x > 0 ⟶ -x < 0"
  "x < 0 ⟶ -x > 0"
  by smt+

lemma
  "(x::real) - 0 = x"
  "0 - x = -x"
  "x < y ⟶ x - y < 0"
  "x - y = -(y - x)"
  "x - y = -y + x"
  "x - y - z = x - (y + z)"
  by smt+

lemma
  "(x::real) * 0 = 0"
  "0 * x = 0"
  "x * 1 = x"
  "1 * x = x"
  "x * -1 = -x"
  "-1 * x = -x"
  "3 * x = x * 3"
  by smt+

lemma
  "¦x::real¦ ≥ 0"
  "(¦x¦ = 0) = (x = 0)"
  "(x ≥ 0) = (¦x¦ = x)"
  "(x ≤ 0) = (¦x¦ = -x)"
  "¦¦x¦¦ = ¦x¦"
  by smt+

lemma
  "min (x::real) y ≤ x"
  "min x y ≤ y"
  "z < x ∧ z < y ⟶ z < min x y"
  "min x y = min y x"
  "x ≥ 0 ⟶ min x 0 = 0"
  "min x y ≤ ¦x + y¦"
  by smt+

lemma
  "max (x::real) y ≥ x"
  "max x y ≥ y"
  "z > x ∧ z > y ⟶ z > max x y"
  "max x y = max y x"
  "x ≥ 0 ⟶ max x 0 = x"
  "max x y ≥ - ¦x¦ - ¦y¦"
  by smt+

lemma
  "x ≤ (x::real)"
  "x ≤ y ⟶ 3 * x ≤ 3 * y"
  "x < y ⟶ 3 * x < 3 * y"
  "x < y ⟶ x ≤ y"
  "¬ (x < x)"
  "x ≤ y ⟶ y ≤ z ⟶ x ≤ z"
  "x < y ⟶ y ≤ z ⟶ x ≤ z"
  "x ≤ y ⟶ y < z ⟶ x ≤ z"
  "x < y ⟶ y < z ⟶ x < z"
  "x < y ∧ y < z ⟶ ¬ (z < x)"
  by smt+


section ‹Datatypes, records, and typedefs›

subsection ‹Without support by the SMT solver›

subsubsection ‹Algebraic datatypes›

lemma
  "x = fst (x, y)"
  "y = snd (x, y)"
  "((x, y) = (y, x)) = (x = y)"
  "((x, y) = (u, v)) = (x = u ∧ y = v)"
  "(fst (x, y, z) = fst (u, v, w)) = (x = u)"
  "(snd (x, y, z) = snd (u, v, w)) = (y = v ∧ z = w)"
  "(fst (snd (x, y, z)) = fst (snd (u, v, w))) = (y = v)"
  "(snd (snd (x, y, z)) = snd (snd (u, v, w))) = (z = w)"
  "(fst (x, y) = snd (x, y)) = (x = y)"
  "p1 = (x, y) ∧ p2 = (y, x) ⟶ fst p1 = snd p2"
  "(fst (x, y) = snd (x, y)) = (x = y)"
  "(fst p = snd p) = (p = (snd p, fst p))"
  using fst_conv snd_conv prod.collapse
  by smt+

lemma
  "[x] ≠ Nil"
  "[x, y] ≠ Nil"
  "x ≠ y ⟶ [x] ≠ [y]"
  "hd (x # xs) = x"
  "tl (x # xs) = xs"
  "hd [x, y, z] = x"
  "tl [x, y, z] = [y, z]"
  "hd (tl [x, y, z]) = y"
  "tl (tl [x, y, z]) = [z]"
  using list.sel(1,3) list.simps
  by smt+

lemma
  "fst (hd [(a, b)]) = a"
  "snd (hd [(a, b)]) = b"
  using fst_conv snd_conv prod.collapse list.sel(1,3) list.simps
  by smt+


subsubsection ‹Records›

record point =
  cx :: int
  cy :: int

record bw_point = point +
  black :: bool

lemma
  "⦇cx = x, cy = y⦈ = ⦇cx = x', cy = y'⦈ ⟹ x = x' ∧ y = y'"
  using point.simps
  by smt

lemma
  "cx ⦇ cx = 3, cy = 4 ⦈ = 3"
  "cy ⦇ cx = 3, cy = 4 ⦈ = 4"
  "cx ⦇ cx = 3, cy = 4 ⦈ ≠ cy ⦇ cx = 3, cy = 4 ⦈"
  "⦇ cx = 3, cy = 4 ⦈ ⦇ cx := 5 ⦈ = ⦇ cx = 5, cy = 4 ⦈"
  "⦇ cx = 3, cy = 4 ⦈ ⦇ cy := 6 ⦈ = ⦇ cx = 3, cy = 6 ⦈"
  "p = ⦇ cx = 3, cy = 4 ⦈ ⟶ p ⦇ cx := 3 ⦈ ⦇ cy := 4 ⦈ = p"
  "p = ⦇ cx = 3, cy = 4 ⦈ ⟶ p ⦇ cy := 4 ⦈ ⦇ cx := 3 ⦈ = p"
  using point.simps
  by smt+

lemma
  "⦇cx = x, cy = y, black = b⦈ = ⦇cx = x', cy = y', black = b'⦈ ⟹ x = x' ∧ y = y' ∧ b = b'"
  using point.simps bw_point.simps
  by smt

lemma
  "cx ⦇ cx = 3, cy = 4, black = b ⦈ = 3"
  "cy ⦇ cx = 3, cy = 4, black = b ⦈ = 4"
  "black ⦇ cx = 3, cy = 4, black = b ⦈ = b"
  "cx ⦇ cx = 3, cy = 4, black = b ⦈ ≠ cy ⦇ cx = 3, cy = 4, black = b ⦈"
  "⦇ cx = 3, cy = 4, black = b ⦈ ⦇ cx := 5 ⦈ = ⦇ cx = 5, cy = 4, black = b ⦈"
  "⦇ cx = 3, cy = 4, black = b ⦈ ⦇ cy := 6 ⦈ = ⦇ cx = 3, cy = 6, black = b ⦈"
  "p = ⦇ cx = 3, cy = 4, black = True ⦈ ⟶
     p ⦇ cx := 3 ⦈ ⦇ cy := 4 ⦈ ⦇ black := True ⦈ = p"
  "p = ⦇ cx = 3, cy = 4, black = True ⦈ ⟶
     p ⦇ cy := 4 ⦈ ⦇ black := True ⦈ ⦇ cx := 3 ⦈ = p"
  "p = ⦇ cx = 3, cy = 4, black = True ⦈ ⟶
     p ⦇ black := True ⦈ ⦇ cx := 3 ⦈ ⦇ cy := 4 ⦈ = p"
  using point.simps bw_point.simps
  by smt+

lemma
  "⦇ cx = 3, cy = 4, black = b ⦈ ⦇ black := w ⦈ = ⦇ cx = 3, cy = 4, black = w ⦈"
  "⦇ cx = 3, cy = 4, black = True ⦈ ⦇ black := False ⦈ =
     ⦇ cx = 3, cy = 4, black = False ⦈"
  "p ⦇ cx := 3 ⦈ ⦇ cy := 4 ⦈ ⦇ black := True ⦈ =
     p ⦇ black := True ⦈ ⦇ cy := 4 ⦈ ⦇ cx := 3 ⦈"
    apply (smt add_One add_inc bw_point.update_convs(1) default_unit_def inc.simps(2) one_plus_BitM
      semiring_norm(6,26))
   apply (smt bw_point.update_convs(1))
  apply (smt bw_point.cases_scheme bw_point.update_convs(1) point.update_convs(1,2))
  done


subsubsection ‹Type definitions›

typedef int' = "UNIV::int set" by (rule UNIV_witness)

definition n0 where "n0 = Abs_int' 0"
definition n1 where "n1 = Abs_int' 1"
definition n2 where "n2 = Abs_int' 2"
definition plus' where "plus' n m = Abs_int' (Rep_int' n + Rep_int' m)"

lemma
  "n0 ≠ n1"
  "plus' n1 n1 = n2"
  "plus' n0 n2 = n2"
  by (smt n0_def n1_def n2_def plus'_def Abs_int'_inverse Rep_int'_inverse UNIV_I)+


subsection ‹With support by the SMT solver (but without proofs)›

subsubsection ‹Algebraic datatypes›

lemma
  "x = fst (x, y)"
  "y = snd (x, y)"
  "((x, y) = (y, x)) = (x = y)"
  "((x, y) = (u, v)) = (x = u ∧ y = v)"
  "(fst (x, y, z) = fst (u, v, w)) = (x = u)"
  "(snd (x, y, z) = snd (u, v, w)) = (y = v ∧ z = w)"
  "(fst (snd (x, y, z)) = fst (snd (u, v, w))) = (y = v)"
  "(snd (snd (x, y, z)) = snd (snd (u, v, w))) = (z = w)"
  "(fst (x, y) = snd (x, y)) = (x = y)"
  "p1 = (x, y) ∧ p2 = (y, x) ⟶ fst p1 = snd p2"
  "(fst (x, y) = snd (x, y)) = (x = y)"
  "(fst p = snd p) = (p = (snd p, fst p))"
  using fst_conv snd_conv prod.collapse
  by smt+

lemma
  "x ≠ y ⟶ [x] ≠ [y]"
  "hd (x # xs) = x"
  "tl (x # xs) = xs"
  "hd [x, y, z] = x"
  "tl [x, y, z] = [y, z]"
  "hd (tl [x, y, z]) = y"
  "tl (tl [x, y, z]) = [z]"
  using list.sel(1,3)
  by smt+

lemma
  "fst (hd [(a, b)]) = a"
  "snd (hd [(a, b)]) = b"
  using fst_conv snd_conv prod.collapse list.sel(1,3)
  by smt+


subsubsection ‹Records›
text ‹The equivalent theory for Z3 contains more example, but unlike Z3, we are able
to reconstruct the proofs.›

lemma
  "cx ⦇ cx = 3, cy = 4 ⦈ = 3"
  "cy ⦇ cx = 3, cy = 4 ⦈ = 4"
  "cx ⦇ cx = 3, cy = 4 ⦈ ≠ cy ⦇ cx = 3, cy = 4 ⦈"
  "⦇ cx = 3, cy = 4 ⦈ ⦇ cx := 5 ⦈ = ⦇ cx = 5, cy = 4 ⦈"
  "⦇ cx = 3, cy = 4 ⦈ ⦇ cy := 6 ⦈ = ⦇ cx = 3, cy = 6 ⦈"
  "p = ⦇ cx = 3, cy = 4 ⦈ ⟶ p ⦇ cx := 3 ⦈ ⦇ cy := 4 ⦈ = p"
  "p = ⦇ cx = 3, cy = 4 ⦈ ⟶ p ⦇ cy := 4 ⦈ ⦇ cx := 3 ⦈ = p"
  using point.simps
  by smt+


lemma
  "cx ⦇ cx = 3, cy = 4, black = b ⦈ = 3"
  "cy ⦇ cx = 3, cy = 4, black = b ⦈ = 4"
  "black ⦇ cx = 3, cy = 4, black = b ⦈ = b"
  "cx ⦇ cx = 3, cy = 4, black = b ⦈ ≠ cy ⦇ cx = 3, cy = 4, black = b ⦈"
  "⦇ cx = 3, cy = 4, black = b ⦈ ⦇ cx := 5 ⦈ = ⦇ cx = 5, cy = 4, black = b ⦈"
  "⦇ cx = 3, cy = 4, black = b ⦈ ⦇ cy := 6 ⦈ = ⦇ cx = 3, cy = 6, black = b ⦈"
  "p = ⦇ cx = 3, cy = 4, black = True ⦈ ⟶
     p ⦇ cx := 3 ⦈ ⦇ cy := 4 ⦈ ⦇ black := True ⦈ = p"
  "p = ⦇ cx = 3, cy = 4, black = True ⦈ ⟶
     p ⦇ cy := 4 ⦈ ⦇ black := True ⦈ ⦇ cx := 3 ⦈ = p"
  "p = ⦇ cx = 3, cy = 4, black = True ⦈ ⟶
     p ⦇ black := True ⦈ ⦇ cx := 3 ⦈ ⦇ cy := 4 ⦈ = p"
  using point.simps bw_point.simps
  by smt+


section ‹Functions›

lemma "∃f. map_option f (Some x) = Some (y + x)"
  by (smt option.map(2))

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


section ‹Sets›

lemma Empty: "x ∉ {}" by simp

lemmas smt_sets = Empty UNIV_I Un_iff Int_iff

lemma
  "x ∉ {}"
  "x ∈ UNIV"
  "x ∈ A ∪ B ⟷ x ∈ A ∨ x ∈ B"
  "x ∈ P ∪ {} ⟷ x ∈ P"
  "x ∈ P ∪ UNIV"
  "x ∈ P ∪ Q ⟷ x ∈ Q ∪ P"
  "x ∈ P ∪ P ⟷ x ∈ P"
  "x ∈ P ∪ (Q ∪ R) ⟷ x ∈ (P ∪ Q) ∪ R"
  "x ∈ A ∩ B ⟷ x ∈ A ∧ x ∈ B"
  "x ∉ P ∩ {}"
  "x ∈ P ∩ UNIV ⟷ x ∈ P"
  "x ∈ P ∩ Q ⟷ x ∈ Q ∩ P"
  "x ∈ P ∩ P ⟷ x ∈ P"
  "x ∈ P ∩ (Q ∩ R) ⟷ x ∈ (P ∩ Q) ∩ R"
  "{x. x ∈ P} = {y. y ∈ P}"
  by (smt smt_sets)+


context
  fixes in_multiset :: "'d ⇒ 'd_multiset ⇒ bool" and
    add_mset :: "'d ⇒ 'd_multiset ⇒ 'd_multiset" and
    set_mset :: "'d_multiset ⇒ 'd set"
begin
lemma
  assumes "⋀a b A. ((a::'d) ∈ insert b A) = (a = b ∨ a ∈ A)"
    "⋀a A. set_mset (add_mset (a::'d) A) = insert a (set_mset A)"
    "⋀r. transp (r::'d ⇒ 'd ⇒ bool) = (∀x y z. r x y ⟶ r y z ⟶ r x z)"
  shows
    "transp (λx y. (x::'d) ∈ set_mset (add_mset m M) ∧ y ∈ set_mset (add_mset m M) ∧ R x y) ⟹
     transp (λx y. x ∈ set_mset M ∧ y ∈ set_mset M ∧ R x y)"
   by (smt (verit) assms)
end

end