(* Title: HOL/SMT_Examples/SMT_Examples.thy
Author: Sascha Boehme, TU Muenchen
*)
section \<open>Examples for the SMT binding\<close>
theory SMT_Examples
imports Complex_Main
begin
external_file \<open>SMT_Examples.certs\<close>
declare [[smt_certificates = "SMT_Examples.certs"]]
declare [[smt_read_only_certificates = true]]
section \<open>Propositional and first-order logic\<close>
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 \<open>Arithmetic\<close>
subsection \<open>Linear arithmetic over integers and reals\<close>
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 \<and> m < n') \<or> (n < m \<and> m = n') \<or> (n < n' \<and> n' < m) \<or>
(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 \<and> n < n') \<or> (m < n \<and> n' = n) \<or> (m < n' \<and> n' < n) \<or>
(m = n \<and> n < n') \<or> (m = n' \<and> n' < n) \<or>
(n' = m \ m = (n::int))"
by smt
text\<open>
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.
\<close>
lemma "\ x3 = \x2\ - x1; x4 = \x3\ - x2; x5 = \x4\ - x3;
x6 = \<bar>x5\<bar> - x4; x7 = \<bar>x6\<bar> - x5; x8 = \<bar>x7\<bar> - x6;
x9 = \<bar>x8\<bar> - x7; x10 = \<bar>x9\<bar> - x8; x11 = \<bar>x10\<bar> - x9 \<rbrakk>
\<Longrightarrow> x1 = x10 \<and> 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 \<open>Linear arithmetic with quantifiers\<close>
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 \<open>Non-linear arithmetic over integers and reals\<close>
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 \<open>Linear arithmetic for natural numbers\<close>
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 \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> 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 \<open>Pairs\<close>
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 \<open>Higher-order problems and recursion\<close>
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 (\<lambda>x. x mod n) xs) = eval_dioph ks xs"
lemma
"(eval_dioph ks xs = l) =
(eval_dioph ks (map (\<lambda>x. x mod 2) xs) mod 2 = l mod 2 \<and>
eval_dioph ks (map (\<lambda>x. x div 2) xs) = (l - eval_dioph ks (map (\<lambda>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 \<open>Monomorphization examples\<close>
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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
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.
|
