# Theory SMT_Tests

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

section ‹Tests for the SMT binding›

theory SMT_Tests
imports Complex_Main
begin

smt_status

text ‹Most examples are taken from various Isabelle theories and from HOL4.›

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 ⟶ (∃y. P x ∧ P y)"
"(∃x. P x) ∨ R ⟷ (∃x. P x ∨ R)"
"∃x. P x ⟶ P a ∧ P b"
"∃x. (∃y. P y) ⟶ P x"
"(∃x. Q ⟶ P x) ⟷ (Q ⟶ (∃x. P x))"
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))"
"∃z. P z ⟶ (∀x. P x)"
"(∃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 using [[smt_trace]] 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
"(0::nat) div 0 = 0"
"(x::nat) div 0 = 0"
"(0::nat) div 1 = 0"
"(1::nat) div 1 = 1"
"(3::nat) div 1 = 3"
"(x::nat) div 1 = x"
"(0::nat) div 3 = 0"
"(1::nat) div 3 = 0"
"(3::nat) div 3 = 1"
"(x::nat) div 3 ≤ x"
"(x div 3 = x) = (x = 0)"
using [[z3_extensions]]
by smt+

lemma
"(0::nat) mod 0 = 0"
"(x::nat) mod 0 = x"
"(0::nat) mod 1 = 0"
"(1::nat) mod 1 = 0"
"(3::nat) mod 1 = 0"
"(x::nat) mod 1 = 0"
"(0::nat) mod 3 = 0"
"(1::nat) mod 3 = 1"
"(3::nat) mod 3 = 0"
"x mod 3 < 3"
"(x mod 3 = x) = (x < 3)"
using [[z3_extensions]]
by smt+

lemma
"(x::nat) = x div 1 * 1 + x mod 1"
"x = x div 3 * 3 + x mod 3"
using [[z3_extensions]]
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
"(0::int) div 0 = 0"
"(x::int) div 0 = 0"
"(0::int) div 1 = 0"
"(1::int) div 1 = 1"
"(3::int) div 1 = 3"
"(x::int) div 1 = x"
"(0::int) div -1 = 0"
"(1::int) div -1 = -1"
"(3::int) div -1 = -3"
"(x::int) div -1 = -x"
"(0::int) div 3 = 0"
"(0::int) div -3 = 0"
"(1::int) div 3 = 0"
"(3::int) div 3 = 1"
"(5::int) div 3 = 1"
"(1::int) div -3 = -1"
"(3::int) div -3 = -1"
"(5::int) div -3 = -2"
"(-1::int) div 3 = -1"
"(-3::int) div 3 = -1"
"(-5::int) div 3 = -2"
"(-1::int) div -3 = 0"
"(-3::int) div -3 = 1"
"(-5::int) div -3 = 1"
using [[z3_extensions]]
by smt+

lemma
"(0::int) mod 0 = 0"
"(x::int) mod 0 = x"
"(0::int) mod 1 = 0"
"(1::int) mod 1 = 0"
"(3::int) mod 1 = 0"
"(x::int) mod 1 = 0"
"(0::int) mod -1 = 0"
"(1::int) mod -1 = 0"
"(3::int) mod -1 = 0"
"(x::int) mod -1 = 0"
"(0::int) mod 3 = 0"
"(0::int) mod -3 = 0"
"(1::int) mod 3 = 1"
"(3::int) mod 3 = 0"
"(5::int) mod 3 = 2"
"(1::int) mod -3 = -2"
"(3::int) mod -3 = 0"
"(5::int) mod -3 = -1"
"(-1::int) mod 3 = 2"
"(-3::int) mod 3 = 0"
"(-5::int) mod 3 = 1"
"(-1::int) mod -3 = -1"
"(-3::int) mod -3 = 0"
"(-5::int) mod -3 = -2"
"x mod 3 < 3"
"(x mod 3 = x) ⟶ (x < 3)"
using [[z3_extensions]]
by smt+

lemma
"(x::int) = x div 1 * 1 + x mod 1"
"x = x div 3 * 3 + x mod 3"
using [[z3_extensions]]
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
"(1/2 :: real) < 1"
"(1::real) / 3 = 1 / 3"
"(1::real) / -3 = - 1 / 3"
"(-1::real) / 3 = - 1 / 3"
"(-1::real) / -3 = 1 / 3"
"(x::real) / 1 = x"
"x > 0 ⟶ x / 3 < x"
"x < 0 ⟶ x / 3 > x"
using [[z3_extensions]]
by smt+

lemma
"(3::real) * (x / 3) = x"
"(x * 3) / 3 = x"
"x > 0 ⟶ 2 * x / 3 < x"
"x < 0 ⟶ 2 * x / 3 > x"
using [[z3_extensions]]
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
"cy (p ⦇ cx := a ⦈) = cy p"
"cx (p ⦇ cy := a ⦈) = cx p"
"p ⦇ cx := 3 ⦈ ⦇ cy := 4 ⦈ = p ⦇ cy := 4 ⦈ ⦇ cx := 3 ⦈"
sorry

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 ⦈"
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
using [[smt_oracle, z3_extensions]]
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)
using [[smt_oracle, z3_extensions]]
by smt+

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

subsubsection ‹Records›

lemma
"⦇cx = x, cy = y⦈ = ⦇cx = x', cy = y'⦈ ⟹ x = x' ∧ y = y'"
using [[smt_oracle, z3_extensions]]
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
using [[smt_oracle, z3_extensions]]
by smt+

lemma
"cy (p ⦇ cx := a ⦈) = cy p"
"cx (p ⦇ cy := a ⦈) = cx p"
"p ⦇ cx := 3 ⦈ ⦇ cy := 4 ⦈ = p ⦇ cy := 4 ⦈ ⦇ cx := 3 ⦈"
using point.simps
using [[smt_oracle, z3_extensions]]
by smt+

lemma
"⦇cx = x, cy = y, black = b⦈ = ⦇cx = x', cy = y', black = b'⦈ ⟹ x = x' ∧ y = y' ∧ b = b'"
using [[smt_oracle, z3_extensions]]
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
using [[smt_oracle, z3_extensions]]
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 ⦈"
sorry

lemma
"p ⦇ cx := 3 ⦈ ⦇ cy := 4 ⦈ ⦇ black := True ⦈ =
p ⦇ black := True ⦈ ⦇ cy := 4 ⦈ ⦇ cx := 3 ⦈"
using point.simps bw_point.simps
using [[smt_oracle, z3_extensions]]
by smt

subsubsection ‹Type definitions›

lemma
"n0 ≠ n1"
"plus' n1 n1 = n2"
"plus' n0 n2 = n2"
using [[smt_oracle, z3_extensions]]
by (smt n0_def n1_def n2_def plus'_def)+

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)+

end
```