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 \ (\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 \<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 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 \<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+
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+
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 "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+
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>
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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
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.
