products/sources/formale Sprachen/Coq/plugins/ssr/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: SMT_Tests_Verit.thy   Sprache: VDM

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

end

[ zur Elbe Produktseite wechseln0.28Quellennavigators  Analyse erneut starten  ]