Quelle SMT_Tests_Verit.thy Sprache: Isabelle

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

section \<open>Tests for the SMT binding\<close>

theory SMT_Tests_Verit
imports Complex_Main
begin

declare [[smt_solver=verit]]
smt_status

text \<open>Most examples are taken from the equivalent Z3 theory called \<^file>\<open>SMT_Tests.thy\<close>,
and have been taken from various Isabelle and HOL4 developments.\<close>

section \<open>Propositional logic\<close>

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 \<longrightarrow> P2 then P1 \<longrightarrow> Q1 else P1 \<longrightarrow> 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 \<open>First-order logic with equality\<close>

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 \<open>Guidance for quantifier heuristics: patterns\<close>

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 \<open>Meta-logical connectives\<close>

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 \<open>Natural numbers\<close>

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 \<open>Integers\<close>

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 \<open>Reals\<close>

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 \<open>Datatypes, records, and typedefs\<close>

subsection \<open>Without support by the SMT solver\<close>

subsubsection \<open>Algebraic datatypes\<close>

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 \<open>Records\<close>

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 \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p"
  "p = \ cx = 3, cy = 4, black = True \ \
     p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p"
  "p = \ cx = 3, cy = 4, black = True \ \
     p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = 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 \ =
     \<lparr> cx = 3, cy = 4, black = False \<rparr>"
  "p \ cx := 3 \ \ cy := 4 \ \ black := True \ =
     p \<lparr> black := True \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>"
    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 \<open>Type definitions\<close>

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 \<open>With support by the SMT solver (but without proofs)\<close>

subsubsection \<open>Algebraic datatypes\<close>

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 \<open>Records\<close>
text \<open>The equivalent theory for Z3 contains more example, but unlike Z3, we are able
to reconstruct the proofs.\<close>

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 \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p"
  "p = \ cx = 3, cy = 4, black = True \ \
     p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p"
  "p = \ cx = 3, cy = 4, black = True \ \
     p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
  using point.simps bw_point.simps
  by smt+

section \<open>Functions\<close>

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 \<open>Sets\<close>

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 (\<lambda>x y. x \<in> set_mset M \<and> y \<in> set_mset M \<and> R x y)"
   by (smt (verit) assms)
end

end

quality99%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.19Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.