Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/SMT_Examples/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 14 kB

Quelle SMT_Examples.thy Sprache: Isabelle

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

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

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.