author | nipkow |
Tue, 05 Nov 2019 21:07:03 +0100 | |
changeset 71044 | cb504351d058 |
parent 67226 | ec32cdaab97b |
permissions | -rw-r--r-- |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
1 |
(* Title: HOL/SMT_Examples/SMT_Tests.thy |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
3 |
*) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
4 |
|
63167 | 5 |
section \<open>Tests for the SMT binding\<close> |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
6 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
7 |
theory SMT_Tests |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
8 |
imports Complex_Main |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
9 |
begin |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
10 |
|
58061 | 11 |
smt_status |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
12 |
|
63167 | 13 |
text \<open>Most examples are taken from various Isabelle theories and from HOL4.\<close> |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
14 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
15 |
|
63167 | 16 |
section \<open>Propositional logic\<close> |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
17 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
18 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
19 |
"True" |
57232 | 20 |
"\<not> False" |
21 |
"\<not> \<not> True" |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
22 |
"True \<and> True" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
23 |
"True \<or> False" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
24 |
"False \<longrightarrow> True" |
57232 | 25 |
"\<not> (False \<longleftrightarrow> True)" |
58061 | 26 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
27 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
28 |
lemma |
57232 | 29 |
"P \<or> \<not> P" |
30 |
"\<not> (P \<and> \<not> P)" |
|
31 |
"(True \<and> P) \<or> \<not> P \<or> (False \<and> P) \<or> P" |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
32 |
"P \<longrightarrow> P" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
33 |
"P \<and> \<not> P \<longrightarrow> False" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
34 |
"P \<and> Q \<longrightarrow> Q \<and> P" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
35 |
"P \<or> Q \<longrightarrow> Q \<or> P" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
36 |
"P \<and> Q \<longrightarrow> P \<or> Q" |
57232 | 37 |
"\<not> (P \<or> Q) \<longrightarrow> \<not> P" |
38 |
"\<not> (P \<or> Q) \<longrightarrow> \<not> Q" |
|
39 |
"\<not> P \<longrightarrow> \<not> (P \<and> Q)" |
|
40 |
"\<not> Q \<longrightarrow> \<not> (P \<and> Q)" |
|
41 |
"(P \<and> Q) \<longleftrightarrow> (\<not> (\<not> P \<or> \<not> Q))" |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
42 |
"(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
43 |
"(P \<or> Q) \<or> R \<longrightarrow> P \<or> (Q \<or> R)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
44 |
"(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
45 |
"(P \<or> R) \<and> (Q \<or> R) \<longrightarrow> (P \<and> Q) \<or> R" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
46 |
"(P \<or> Q) \<and> R \<longrightarrow> (P \<and> R) \<or> (Q \<and> R)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
47 |
"(P \<and> R) \<or> (Q \<and> R) \<longrightarrow> (P \<or> Q) \<and> R" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
48 |
"((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
49 |
"(P \<longrightarrow> R) \<and> (Q \<longrightarrow> R) \<longleftrightarrow> (P \<or> Q \<longrightarrow> R)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
50 |
"(P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
51 |
"((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> ((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<longrightarrow> R) \<longrightarrow> R" |
57232 | 52 |
"\<not> (P \<longrightarrow> R) \<longrightarrow> \<not> (Q \<longrightarrow> R) \<longrightarrow> \<not> (P \<and> Q \<longrightarrow> R)" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
53 |
"(P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
54 |
"P \<longrightarrow> (Q \<longrightarrow> P)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
55 |
"(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q)\<longrightarrow> (P \<longrightarrow> R)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
56 |
"(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
57 |
"((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q" |
57232 | 58 |
"(P \<longrightarrow> Q) \<longrightarrow> (\<not> Q \<longrightarrow> \<not> P)" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
59 |
"(P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
60 |
"(P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P) \<longrightarrow> (P \<longleftrightarrow> Q)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
61 |
"(P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)" |
57232 | 62 |
"\<not> (P \<longleftrightarrow> \<not> P)" |
63 |
"(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P)" |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
64 |
"P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P" |
58061 | 65 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
66 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
67 |
lemma |
57232 | 68 |
"(if P then Q1 else Q2) \<longleftrightarrow> ((P \<longrightarrow> Q1) \<and> (\<not> P \<longrightarrow> Q2))" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
69 |
"if P then (Q \<longrightarrow> P) else (P \<longrightarrow> Q)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
70 |
"(if P1 \<or> P2 then Q1 else Q2) \<longleftrightarrow> (if P1 then Q1 else if P2 then Q1 else Q2)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
71 |
"(if P1 \<and> P2 then Q1 else Q2) \<longleftrightarrow> (if P1 then if P2 then Q1 else Q2 else Q2)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
72 |
"(P1 \<longrightarrow> (if P2 then Q1 else Q2)) \<longleftrightarrow> |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
73 |
(if P1 \<longrightarrow> P2 then P1 \<longrightarrow> Q1 else P1 \<longrightarrow> Q2)" |
58061 | 74 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
75 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
76 |
lemma |
57232 | 77 |
"case P of True \<Rightarrow> P | False \<Rightarrow> \<not> P" |
78 |
"case P of False \<Rightarrow> \<not> P | True \<Rightarrow> P" |
|
79 |
"case \<not> P of True \<Rightarrow> \<not> P | False \<Rightarrow> P" |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
80 |
"case P of True \<Rightarrow> (Q \<longrightarrow> P) | False \<Rightarrow> (P \<longrightarrow> Q)" |
58061 | 81 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
82 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
83 |
|
63167 | 84 |
section \<open>First-order logic with equality\<close> |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
85 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
86 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
87 |
"x = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
88 |
"x = y \<longrightarrow> y = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
89 |
"x = y \<and> y = z \<longrightarrow> x = z" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
90 |
"x = y \<longrightarrow> f x = f y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
91 |
"x = y \<longrightarrow> g x y = g y x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
92 |
"f (f x) = x \<and> f (f (f (f (f x)))) = x \<longrightarrow> f x = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
93 |
"((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))" |
58061 | 94 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
95 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
96 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
97 |
"\<forall>x. x = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
98 |
"(\<forall>x. P x) \<longleftrightarrow> (\<forall>y. P y)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
99 |
"\<forall>x. P x \<longrightarrow> (\<forall>y. P x \<or> P y)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
100 |
"(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
101 |
"(\<forall>x. P x) \<or> R \<longleftrightarrow> (\<forall>x. P x \<or> R)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
102 |
"(\<forall>x y z. S x z) \<longleftrightarrow> (\<forall>x z. S x z)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
103 |
"(\<forall>x y. S x y \<longrightarrow> S y x) \<longrightarrow> (\<forall>x. S x y) \<longrightarrow> S y x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
104 |
"(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P d \<longrightarrow> P (f(f(f(d))))" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
105 |
"(\<forall>x y. s x y = s y x) \<longrightarrow> a = a \<and> s a b = s b a" |
57232 | 106 |
"(\<forall>s. q s \<longrightarrow> r s) \<and> \<not> r s \<and> (\<forall>s. \<not> r s \<and> \<not> q s \<longrightarrow> p t \<or> q t) \<longrightarrow> p t \<or> r t" |
58061 | 107 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
108 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
109 |
lemma |
50662
b1f4291eb916
regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents:
49995
diff
changeset
|
110 |
"(\<forall>x. P x) \<and> R \<longleftrightarrow> (\<forall>x. P x \<and> R)" |
58061 | 111 |
by smt |
50662
b1f4291eb916
regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents:
49995
diff
changeset
|
112 |
|
b1f4291eb916
regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents:
49995
diff
changeset
|
113 |
lemma |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
114 |
"\<exists>x. x = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
115 |
"(\<exists>x. P x) \<longleftrightarrow> (\<exists>y. P y)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
116 |
"(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
117 |
"(\<exists>x. P x) \<and> R \<longleftrightarrow> (\<exists>x. P x \<and> R)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
118 |
"(\<exists>x y z. S x z) \<longleftrightarrow> (\<exists>x z. S x z)" |
57232 | 119 |
"\<not> ((\<exists>x. \<not> P x) \<and> ((\<exists>x. P x) \<or> (\<exists>x. P x \<and> Q x)) \<and> \<not> (\<exists>x. P x))" |
58061 | 120 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
121 |
|
49995
3b7ad6153322
regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles
blanchet
parents:
49834
diff
changeset
|
122 |
lemma |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
123 |
"\<exists>x y. x = y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
124 |
"\<exists>x. P x \<longrightarrow> (\<exists>y. P x \<and> P y)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
125 |
"(\<exists>x. P x) \<or> R \<longleftrightarrow> (\<exists>x. P x \<or> R)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
126 |
"\<exists>x. P x \<longrightarrow> P a \<and> P b" |
49995
3b7ad6153322
regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles
blanchet
parents:
49834
diff
changeset
|
127 |
"\<exists>x. (\<exists>y. P y) \<longrightarrow> P x" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
128 |
"(\<exists>x. Q \<longrightarrow> P x) \<longleftrightarrow> (Q \<longrightarrow> (\<exists>x. P x))" |
58061 | 129 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
130 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
131 |
lemma |
57232 | 132 |
"(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
133 |
"(\<exists>x. P x \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x) \<longrightarrow> Q" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
134 |
"(\<forall>x y. R x y = x) \<longrightarrow> (\<exists>y. R x y) = R x c" |
57232 | 135 |
"(if P x then \<not> (\<exists>y. P y) else (\<forall>y. \<not> P y)) \<longrightarrow> P x \<longrightarrow> P y" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
136 |
"(\<forall>x y. R x y = x) \<and> (\<forall>x. \<exists>y. R x y) = (\<forall>x. R x c) \<longrightarrow> (\<exists>y. R x y) = R x c" |
58061 | 137 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
138 |
|
49995
3b7ad6153322
regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles
blanchet
parents:
49834
diff
changeset
|
139 |
lemma |
41132 | 140 |
"\<forall>x. \<exists>y. f x y = f x (g x)" |
57232 | 141 |
"(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
142 |
"\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
143 |
"\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x) else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
144 |
"\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x) else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
145 |
"(\<exists>x. \<forall>y. P x \<longleftrightarrow> P y) \<longrightarrow> ((\<exists>x. P x) \<longleftrightarrow> (\<forall>y. P y))" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
146 |
"\<exists>z. P z \<longrightarrow> (\<forall>x. P x)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
147 |
"(\<exists>y. \<forall>x. R x y) \<longrightarrow> (\<forall>x. \<exists>y. R x y)" |
58061 | 148 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
149 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
150 |
lemma |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset
|
151 |
"(\<exists>!x. P x) \<longrightarrow> (\<exists>x. P x)" |
57232 | 152 |
"(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x \<and> (\<forall>y. y \<noteq> x \<longrightarrow> \<not> P y))" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
153 |
"P a \<longrightarrow> (\<forall>x. P x \<longrightarrow> x = a) \<longrightarrow> (\<exists>!x. P x)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
154 |
"(\<exists>x. P x) \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> x = y) \<longrightarrow> (\<exists>!x. P x)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
155 |
"(\<exists>!x. P x) \<and> (\<forall>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> R) \<longrightarrow> R" |
58061 | 156 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
157 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
158 |
lemma |
37786
4eb98849c5c0
fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
boehmes
parents:
37157
diff
changeset
|
159 |
"(\<forall>x\<in>M. P x) \<and> c \<in> M \<longrightarrow> P c" |
57232 | 160 |
"(\<exists>x\<in>M. P x) \<or> \<not> (P c \<and> c \<in> M)" |
58061 | 161 |
by smt+ |
37786
4eb98849c5c0
fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
boehmes
parents:
37157
diff
changeset
|
162 |
|
4eb98849c5c0
fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
boehmes
parents:
37157
diff
changeset
|
163 |
lemma |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
164 |
"let P = True in P" |
57232 | 165 |
"let P = P1 \<or> P2 in P \<or> \<not> P" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
166 |
"let P1 = True; P2 = False in P1 \<and> P2 \<longrightarrow> P2 \<or> P1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
167 |
"(let x = y in x) = y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
168 |
"(let x = y in Q x) \<longleftrightarrow> (let z = y in Q z)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
169 |
"(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y2; x = y1 in R x z)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
170 |
"(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y1; x = y2 in R z x)" |
57232 | 171 |
"let P = (\<forall>x. Q x) in if P then P else \<not> P" |
58061 | 172 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
173 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
174 |
lemma |
47155
ade3fc826af3
dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
boehmes
parents:
47152
diff
changeset
|
175 |
"a \<noteq> b \<and> a \<noteq> c \<and> b \<noteq> c \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b" |
58061 | 176 |
by smt |
41899
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41601
diff
changeset
|
177 |
|
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41601
diff
changeset
|
178 |
lemma |
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41601
diff
changeset
|
179 |
"(\<forall>x y z. f x y = f x z \<longrightarrow> y = z) \<and> b \<noteq> c \<longrightarrow> f a b \<noteq> f a c" |
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41601
diff
changeset
|
180 |
"(\<forall>x y z. f x y = f z y \<longrightarrow> x = z) \<and> a \<noteq> d \<longrightarrow> f a b \<noteq> f d b" |
58061 | 181 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
182 |
|
44753
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset
|
183 |
|
63167 | 184 |
section \<open>Guidance for quantifier heuristics: patterns\<close> |
44753
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset
|
185 |
|
37124 | 186 |
lemma |
57232 | 187 |
assumes "\<forall>x. |
58061 | 188 |
SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat (f x)) SMT.Symb_Nil) SMT.Symb_Nil) |
57232 | 189 |
(f x = x)" |
37124 | 190 |
shows "f 1 = 1" |
58061 | 191 |
using assms using [[smt_trace]] by smt |
37124 | 192 |
|
193 |
lemma |
|
57232 | 194 |
assumes "\<forall>x y. |
58061 | 195 |
SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat (f x)) |
196 |
(SMT.Symb_Cons (SMT.pat (g y)) SMT.Symb_Nil)) SMT.Symb_Nil) (f x = g y)" |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45694
diff
changeset
|
197 |
shows "f a = g b" |
58061 | 198 |
using assms by smt |
37124 | 199 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
200 |
|
63167 | 201 |
section \<open>Meta-logical connectives\<close> |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
202 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
203 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
204 |
"True \<Longrightarrow> True" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
205 |
"False \<Longrightarrow> True" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
206 |
"False \<Longrightarrow> False" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
207 |
"P' x \<Longrightarrow> P' x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
208 |
"P \<Longrightarrow> P \<or> Q" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
209 |
"Q \<Longrightarrow> P \<or> Q" |
57232 | 210 |
"\<not> P \<Longrightarrow> P \<longrightarrow> Q" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
211 |
"Q \<Longrightarrow> P \<longrightarrow> Q" |
57232 | 212 |
"\<lbrakk>P; \<not> Q\<rbrakk> \<Longrightarrow> \<not> (P \<longrightarrow> Q)" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
213 |
"P' x \<equiv> P' x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
214 |
"P' x \<equiv> Q' x \<Longrightarrow> P' x = Q' x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
215 |
"P' x = Q' x \<Longrightarrow> P' x \<equiv> Q' x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
216 |
"x \<equiv> y \<Longrightarrow> y \<equiv> z \<Longrightarrow> x \<equiv> (z::'a::type)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
217 |
"x \<equiv> y \<Longrightarrow> (f x :: 'b::type) \<equiv> f y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
218 |
"(\<And>x. g x) \<Longrightarrow> g a \<or> a" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
219 |
"(\<And>x y. h x y \<and> h y x) \<Longrightarrow> \<forall>x. h x x" |
57232 | 220 |
"(p \<or> q) \<and> \<not> p \<Longrightarrow> q" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
221 |
"(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)" |
58061 | 222 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
223 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
224 |
|
67226 | 225 |
section \<open>Natural numbers\<close> |
66298 | 226 |
|
227 |
declare [[smt_nat_as_int]] |
|
228 |
||
229 |
lemma |
|
230 |
"(0::nat) = 0" |
|
231 |
"(1::nat) = 1" |
|
232 |
"(0::nat) < 1" |
|
233 |
"(0::nat) \<le> 1" |
|
234 |
"(123456789::nat) < 2345678901" |
|
235 |
by smt+ |
|
236 |
||
237 |
lemma |
|
238 |
"Suc 0 = 1" |
|
239 |
"Suc x = x + 1" |
|
240 |
"x < Suc x" |
|
241 |
"(Suc x = Suc y) = (x = y)" |
|
242 |
"Suc (x + y) < Suc x + Suc y" |
|
243 |
by smt+ |
|
244 |
||
245 |
lemma |
|
246 |
"(x::nat) + 0 = x" |
|
247 |
"0 + x = x" |
|
248 |
"x + y = y + x" |
|
249 |
"x + (y + z) = (x + y) + z" |
|
250 |
"(x + y = 0) = (x = 0 \<and> y = 0)" |
|
251 |
by smt+ |
|
252 |
||
253 |
lemma |
|
254 |
"(x::nat) - 0 = x" |
|
255 |
"x < y \<longrightarrow> x - y = 0" |
|
256 |
"x - y = 0 \<or> y - x = 0" |
|
257 |
"(x - y) + y = (if x < y then y else x)" |
|
258 |
"x - y - z = x - (y + z)" |
|
259 |
by smt+ |
|
260 |
||
261 |
lemma |
|
262 |
"(x::nat) * 0 = 0" |
|
263 |
"0 * x = 0" |
|
264 |
"x * 1 = x" |
|
265 |
"1 * x = x" |
|
266 |
"3 * x = x * 3" |
|
267 |
by smt+ |
|
268 |
||
269 |
lemma |
|
270 |
"(0::nat) div 0 = 0" |
|
271 |
"(x::nat) div 0 = 0" |
|
272 |
"(0::nat) div 1 = 0" |
|
273 |
"(1::nat) div 1 = 1" |
|
274 |
"(3::nat) div 1 = 3" |
|
275 |
"(x::nat) div 1 = x" |
|
276 |
"(0::nat) div 3 = 0" |
|
277 |
"(1::nat) div 3 = 0" |
|
278 |
"(3::nat) div 3 = 1" |
|
279 |
"(x::nat) div 3 \<le> x" |
|
280 |
"(x div 3 = x) = (x = 0)" |
|
281 |
using [[z3_extensions]] |
|
282 |
by smt+ |
|
283 |
||
284 |
lemma |
|
285 |
"(0::nat) mod 0 = 0" |
|
286 |
"(x::nat) mod 0 = x" |
|
287 |
"(0::nat) mod 1 = 0" |
|
288 |
"(1::nat) mod 1 = 0" |
|
289 |
"(3::nat) mod 1 = 0" |
|
290 |
"(x::nat) mod 1 = 0" |
|
291 |
"(0::nat) mod 3 = 0" |
|
292 |
"(1::nat) mod 3 = 1" |
|
293 |
"(3::nat) mod 3 = 0" |
|
294 |
"x mod 3 < 3" |
|
295 |
"(x mod 3 = x) = (x < 3)" |
|
296 |
using [[z3_extensions]] |
|
297 |
by smt+ |
|
298 |
||
299 |
lemma |
|
300 |
"(x::nat) = x div 1 * 1 + x mod 1" |
|
301 |
"x = x div 3 * 3 + x mod 3" |
|
302 |
using [[z3_extensions]] |
|
303 |
by smt+ |
|
304 |
||
305 |
lemma |
|
306 |
"min (x::nat) y \<le> x" |
|
307 |
"min x y \<le> y" |
|
308 |
"min x y \<le> x + y" |
|
309 |
"z < x \<and> z < y \<longrightarrow> z < min x y" |
|
310 |
"min x y = min y x" |
|
311 |
"min x 0 = 0" |
|
312 |
by smt+ |
|
313 |
||
314 |
lemma |
|
315 |
"max (x::nat) y \<ge> x" |
|
316 |
"max x y \<ge> y" |
|
317 |
"max x y \<ge> (x - y) + (y - x)" |
|
318 |
"z > x \<and> z > y \<longrightarrow> z > max x y" |
|
319 |
"max x y = max y x" |
|
320 |
"max x 0 = x" |
|
321 |
by smt+ |
|
322 |
||
323 |
lemma |
|
324 |
"0 \<le> (x::nat)" |
|
325 |
"0 < x \<and> x \<le> 1 \<longrightarrow> x = 1" |
|
326 |
"x \<le> x" |
|
327 |
"x \<le> y \<longrightarrow> 3 * x \<le> 3 * y" |
|
328 |
"x < y \<longrightarrow> 3 * x < 3 * y" |
|
329 |
"x < y \<longrightarrow> x \<le> y" |
|
330 |
"(x < y) = (x + 1 \<le> y)" |
|
331 |
"\<not> (x < x)" |
|
332 |
"x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" |
|
333 |
"x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" |
|
334 |
"x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z" |
|
335 |
"x < y \<longrightarrow> y < z \<longrightarrow> x < z" |
|
336 |
"x < y \<and> y < z \<longrightarrow> \<not> (z < x)" |
|
337 |
by smt+ |
|
338 |
||
339 |
declare [[smt_nat_as_int = false]] |
|
340 |
||
341 |
||
63167 | 342 |
section \<open>Integers\<close> |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
343 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
344 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
345 |
"(0::int) = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
346 |
"(0::int) = (- 0)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
347 |
"(1::int) = 1" |
57232 | 348 |
"\<not> (-1 = (1::int))" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
349 |
"(0::int) < 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
350 |
"(0::int) \<le> 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
351 |
"-123 + 345 < (567::int)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
352 |
"(123456789::int) < 2345678901" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
353 |
"(-123456789::int) < 2345678901" |
58061 | 354 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
355 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
356 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
357 |
"(x::int) + 0 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
358 |
"0 + x = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
359 |
"x + y = y + x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
360 |
"x + (y + z) = (x + y) + z" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
361 |
"(x + y = 0) = (x = -y)" |
58061 | 362 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
363 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
364 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
365 |
"(-1::int) = - 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
366 |
"(-3::int) = - 3" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
367 |
"-(x::int) < 0 \<longleftrightarrow> x > 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
368 |
"x > 0 \<longrightarrow> -x < 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
369 |
"x < 0 \<longrightarrow> -x > 0" |
58061 | 370 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
371 |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset
|
372 |
lemma |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
373 |
"(x::int) - 0 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
374 |
"0 - x = -x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
375 |
"x < y \<longrightarrow> x - y < 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
376 |
"x - y = -(y - x)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
377 |
"x - y = -y + x" |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset
|
378 |
"x - y - z = x - (y + z)" |
58061 | 379 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
380 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
381 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
382 |
"(x::int) * 0 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
383 |
"0 * x = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
384 |
"x * 1 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
385 |
"1 * x = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
386 |
"x * -1 = -x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
387 |
"-1 * x = -x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
388 |
"3 * x = x * 3" |
58061 | 389 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
390 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
391 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
392 |
"(0::int) div 0 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
393 |
"(x::int) div 0 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
394 |
"(0::int) div 1 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
395 |
"(1::int) div 1 = 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
396 |
"(3::int) div 1 = 3" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
397 |
"(x::int) div 1 = x" |
37151 | 398 |
"(0::int) div -1 = 0" |
399 |
"(1::int) div -1 = -1" |
|
400 |
"(3::int) div -1 = -3" |
|
401 |
"(x::int) div -1 = -x" |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
402 |
"(0::int) div 3 = 0" |
37151 | 403 |
"(0::int) div -3 = 0" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
404 |
"(1::int) div 3 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
405 |
"(3::int) div 3 = 1" |
37151 | 406 |
"(5::int) div 3 = 1" |
407 |
"(1::int) div -3 = -1" |
|
408 |
"(3::int) div -3 = -1" |
|
409 |
"(5::int) div -3 = -2" |
|
410 |
"(-1::int) div 3 = -1" |
|
411 |
"(-3::int) div 3 = -1" |
|
412 |
"(-5::int) div 3 = -2" |
|
413 |
"(-1::int) div -3 = 0" |
|
414 |
"(-3::int) div -3 = 1" |
|
415 |
"(-5::int) div -3 = 1" |
|
58061 | 416 |
using [[z3_extensions]] |
417 |
by smt+ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
418 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
419 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
420 |
"(0::int) mod 0 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
421 |
"(x::int) mod 0 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
422 |
"(0::int) mod 1 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
423 |
"(1::int) mod 1 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
424 |
"(3::int) mod 1 = 0" |
37151 | 425 |
"(x::int) mod 1 = 0" |
426 |
"(0::int) mod -1 = 0" |
|
427 |
"(1::int) mod -1 = 0" |
|
428 |
"(3::int) mod -1 = 0" |
|
429 |
"(x::int) mod -1 = 0" |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
430 |
"(0::int) mod 3 = 0" |
37151 | 431 |
"(0::int) mod -3 = 0" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
432 |
"(1::int) mod 3 = 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
433 |
"(3::int) mod 3 = 0" |
37151 | 434 |
"(5::int) mod 3 = 2" |
435 |
"(1::int) mod -3 = -2" |
|
436 |
"(3::int) mod -3 = 0" |
|
437 |
"(5::int) mod -3 = -1" |
|
438 |
"(-1::int) mod 3 = 2" |
|
439 |
"(-3::int) mod 3 = 0" |
|
440 |
"(-5::int) mod 3 = 1" |
|
441 |
"(-1::int) mod -3 = -1" |
|
442 |
"(-3::int) mod -3 = 0" |
|
443 |
"(-5::int) mod -3 = -2" |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
444 |
"x mod 3 < 3" |
37151 | 445 |
"(x mod 3 = x) \<longrightarrow> (x < 3)" |
58061 | 446 |
using [[z3_extensions]] |
447 |
by smt+ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
448 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
449 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
450 |
"(x::int) = x div 1 * 1 + x mod 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
451 |
"x = x div 3 * 3 + x mod 3" |
58061 | 452 |
using [[z3_extensions]] |
453 |
by smt+ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
454 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
455 |
lemma |
61945 | 456 |
"\<bar>x::int\<bar> \<ge> 0" |
457 |
"(\<bar>x\<bar> = 0) = (x = 0)" |
|
458 |
"(x \<ge> 0) = (\<bar>x\<bar> = x)" |
|
459 |
"(x \<le> 0) = (\<bar>x\<bar> = -x)" |
|
460 |
"\<bar>\<bar>x\<bar>\<bar> = \<bar>x\<bar>" |
|
58061 | 461 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
462 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
463 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
464 |
"min (x::int) y \<le> x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
465 |
"min x y \<le> y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
466 |
"z < x \<and> z < y \<longrightarrow> z < min x y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
467 |
"min x y = min y x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
468 |
"x \<ge> 0 \<longrightarrow> min x 0 = 0" |
61945 | 469 |
"min x y \<le> \<bar>x + y\<bar>" |
58061 | 470 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
471 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
472 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
473 |
"max (x::int) y \<ge> x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
474 |
"max x y \<ge> y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
475 |
"z > x \<and> z > y \<longrightarrow> z > max x y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
476 |
"max x y = max y x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
477 |
"x \<ge> 0 \<longrightarrow> max x 0 = x" |
61945 | 478 |
"max x y \<ge> - \<bar>x\<bar> - \<bar>y\<bar>" |
58061 | 479 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
480 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
481 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
482 |
"0 < (x::int) \<and> x \<le> 1 \<longrightarrow> x = 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
483 |
"x \<le> x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
484 |
"x \<le> y \<longrightarrow> 3 * x \<le> 3 * y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
485 |
"x < y \<longrightarrow> 3 * x < 3 * y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
486 |
"x < y \<longrightarrow> x \<le> y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
487 |
"(x < y) = (x + 1 \<le> y)" |
57232 | 488 |
"\<not> (x < x)" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
489 |
"x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
490 |
"x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
491 |
"x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
492 |
"x < y \<longrightarrow> y < z \<longrightarrow> x < z" |
57232 | 493 |
"x < y \<and> y < z \<longrightarrow> \<not> (z < x)" |
58061 | 494 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
495 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
496 |
|
63167 | 497 |
section \<open>Reals\<close> |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
498 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
499 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
500 |
"(0::real) = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
501 |
"(0::real) = -0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
502 |
"(0::real) = (- 0)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
503 |
"(1::real) = 1" |
57232 | 504 |
"\<not> (-1 = (1::real))" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
505 |
"(0::real) < 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
506 |
"(0::real) \<le> 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
507 |
"-123 + 345 < (567::real)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
508 |
"(123456789::real) < 2345678901" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
509 |
"(-123456789::real) < 2345678901" |
58061 | 510 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
511 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
512 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
513 |
"(x::real) + 0 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
514 |
"0 + x = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
515 |
"x + y = y + x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
516 |
"x + (y + z) = (x + y) + z" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
517 |
"(x + y = 0) = (x = -y)" |
58061 | 518 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
519 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
520 |
lemma |
41132 | 521 |
"(-1::real) = - 1" |
522 |
"(-3::real) = - 3" |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
523 |
"-(x::real) < 0 \<longleftrightarrow> x > 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
524 |
"x > 0 \<longrightarrow> -x < 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
525 |
"x < 0 \<longrightarrow> -x > 0" |
58061 | 526 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
527 |
|
49995
3b7ad6153322
regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles
blanchet
parents:
49834
diff
changeset
|
528 |
lemma |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
529 |
"(x::real) - 0 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
530 |
"0 - x = -x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
531 |
"x < y \<longrightarrow> x - y < 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
532 |
"x - y = -(y - x)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
533 |
"x - y = -y + x" |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset
|
534 |
"x - y - z = x - (y + z)" |
58061 | 535 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
536 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
537 |
lemma |
41132 | 538 |
"(x::real) * 0 = 0" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
539 |
"0 * x = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
540 |
"x * 1 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
541 |
"1 * x = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
542 |
"x * -1 = -x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
543 |
"-1 * x = -x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
544 |
"3 * x = x * 3" |
58061 | 545 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
546 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
547 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
548 |
"(1/2 :: real) < 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
549 |
"(1::real) / 3 = 1 / 3" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
550 |
"(1::real) / -3 = - 1 / 3" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
551 |
"(-1::real) / 3 = - 1 / 3" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
552 |
"(-1::real) / -3 = 1 / 3" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
553 |
"(x::real) / 1 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
554 |
"x > 0 \<longrightarrow> x / 3 < x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
555 |
"x < 0 \<longrightarrow> x / 3 > x" |
58061 | 556 |
using [[z3_extensions]] |
557 |
by smt+ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
558 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
559 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
560 |
"(3::real) * (x / 3) = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
561 |
"(x * 3) / 3 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
562 |
"x > 0 \<longrightarrow> 2 * x / 3 < x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
563 |
"x < 0 \<longrightarrow> 2 * x / 3 > x" |
58061 | 564 |
using [[z3_extensions]] |
565 |
by smt+ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
566 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
567 |
lemma |
61945 | 568 |
"\<bar>x::real\<bar> \<ge> 0" |
569 |
"(\<bar>x\<bar> = 0) = (x = 0)" |
|
570 |
"(x \<ge> 0) = (\<bar>x\<bar> = x)" |
|
571 |
"(x \<le> 0) = (\<bar>x\<bar> = -x)" |
|
572 |
"\<bar>\<bar>x\<bar>\<bar> = \<bar>x\<bar>" |
|
58061 | 573 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
574 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
575 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
576 |
"min (x::real) y \<le> x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
577 |
"min x y \<le> y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
578 |
"z < x \<and> z < y \<longrightarrow> z < min x y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
579 |
"min x y = min y x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
580 |
"x \<ge> 0 \<longrightarrow> min x 0 = 0" |
61945 | 581 |
"min x y \<le> \<bar>x + y\<bar>" |
58061 | 582 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
583 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
584 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
585 |
"max (x::real) y \<ge> x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
586 |
"max x y \<ge> y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
587 |
"z > x \<and> z > y \<longrightarrow> z > max x y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
588 |
"max x y = max y x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
589 |
"x \<ge> 0 \<longrightarrow> max x 0 = x" |
61945 | 590 |
"max x y \<ge> - \<bar>x\<bar> - \<bar>y\<bar>" |
58061 | 591 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
592 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
593 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
594 |
"x \<le> (x::real)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
595 |
"x \<le> y \<longrightarrow> 3 * x \<le> 3 * y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
596 |
"x < y \<longrightarrow> 3 * x < 3 * y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
597 |
"x < y \<longrightarrow> x \<le> y" |
57232 | 598 |
"\<not> (x < x)" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
599 |
"x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
600 |
"x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
601 |
"x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
602 |
"x < y \<longrightarrow> y < z \<longrightarrow> x < z" |
57232 | 603 |
"x < y \<and> y < z \<longrightarrow> \<not> (z < x)" |
58061 | 604 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
605 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
606 |
|
66738
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66298
diff
changeset
|
607 |
section \<open>Datatypes, records, and typedefs\<close> |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
608 |
|
63167 | 609 |
subsection \<open>Without support by the SMT solver\<close> |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
610 |
|
63167 | 611 |
subsubsection \<open>Algebraic datatypes\<close> |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
612 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
613 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
614 |
"x = fst (x, y)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
615 |
"y = snd (x, y)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
616 |
"((x, y) = (y, x)) = (x = y)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
617 |
"((x, y) = (u, v)) = (x = u \<and> y = v)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
618 |
"(fst (x, y, z) = fst (u, v, w)) = (x = u)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
619 |
"(snd (x, y, z) = snd (u, v, w)) = (y = v \<and> z = w)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
620 |
"(fst (snd (x, y, z)) = fst (snd (u, v, w))) = (y = v)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
621 |
"(snd (snd (x, y, z)) = snd (snd (u, v, w))) = (z = w)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
622 |
"(fst (x, y) = snd (x, y)) = (x = y)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
623 |
"p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
624 |
"(fst (x, y) = snd (x, y)) = (x = y)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
625 |
"(fst p = snd p) = (p = (snd p, fst p))" |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
58889
diff
changeset
|
626 |
using fst_conv snd_conv prod.collapse |
58061 | 627 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
628 |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
629 |
lemma |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
630 |
"[x] \<noteq> Nil" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
631 |
"[x, y] \<noteq> Nil" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
632 |
"x \<noteq> y \<longrightarrow> [x] \<noteq> [y]" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
633 |
"hd (x # xs) = x" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
634 |
"tl (x # xs) = xs" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
635 |
"hd [x, y, z] = x" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
636 |
"tl [x, y, z] = [y, z]" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
637 |
"hd (tl [x, y, z]) = y" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
638 |
"tl (tl [x, y, z]) = [z]" |
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
54489
diff
changeset
|
639 |
using list.sel(1,3) list.simps |
58061 | 640 |
by smt+ |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
641 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
642 |
lemma |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
643 |
"fst (hd [(a, b)]) = a" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
644 |
"snd (hd [(a, b)]) = b" |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
58889
diff
changeset
|
645 |
using fst_conv snd_conv prod.collapse list.sel(1,3) list.simps |
58061 | 646 |
by smt+ |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
647 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
648 |
|
63167 | 649 |
subsubsection \<open>Records\<close> |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
650 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
651 |
record point = |
41427 | 652 |
cx :: int |
653 |
cy :: int |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
654 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
655 |
record bw_point = point + |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
656 |
black :: bool |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
657 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
658 |
lemma |
58366 | 659 |
"\<lparr>cx = x, cy = y\<rparr> = \<lparr>cx = x', cy = y'\<rparr> \<Longrightarrow> x = x' \<and> y = y'" |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
660 |
using point.simps |
58366 | 661 |
by smt |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
662 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
663 |
lemma |
41427 | 664 |
"cx \<lparr> cx = 3, cy = 4 \<rparr> = 3" |
665 |
"cy \<lparr> cx = 3, cy = 4 \<rparr> = 4" |
|
666 |
"cx \<lparr> cx = 3, cy = 4 \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4 \<rparr>" |
|
667 |
"\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4 \<rparr>" |
|
668 |
"\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6 \<rparr>" |
|
669 |
"p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" |
|
670 |
"p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr> = p" |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
671 |
using point.simps |
58061 | 672 |
by smt+ |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
673 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
674 |
lemma |
41427 | 675 |
"cy (p \<lparr> cx := a \<rparr>) = cy p" |
676 |
"cx (p \<lparr> cy := a \<rparr>) = cx p" |
|
677 |
"p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>" |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
678 |
sorry |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
679 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
680 |
lemma |
58366 | 681 |
"\<lparr>cx = x, cy = y, black = b\<rparr> = \<lparr>cx = x', cy = y', black = b'\<rparr> \<Longrightarrow> x = x' \<and> y = y' \<and> b = b'" |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
682 |
using point.simps bw_point.simps |
58366 | 683 |
by smt |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
684 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
685 |
lemma |
41427 | 686 |
"cx \<lparr> cx = 3, cy = 4, black = b \<rparr> = 3" |
687 |
"cy \<lparr> cx = 3, cy = 4, black = b \<rparr> = 4" |
|
688 |
"black \<lparr> cx = 3, cy = 4, black = b \<rparr> = b" |
|
689 |
"cx \<lparr> cx = 3, cy = 4, black = b \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4, black = b \<rparr>" |
|
690 |
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4, black = b \<rparr>" |
|
691 |
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6, black = b \<rparr>" |
|
692 |
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
693 |
p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p" |
|
694 |
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
695 |
p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p" |
|
696 |
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
697 |
p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
698 |
using point.simps bw_point.simps |
58366 | 699 |
by smt+ |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
700 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
701 |
lemma |
41427 | 702 |
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>" |
703 |
"\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> = |
|
704 |
\<lparr> cx = 3, cy = 4, black = False \<rparr>" |
|
705 |
"p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = |
|
706 |
p \<lparr> black := True \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>" |
|
58366 | 707 |
apply (smt add_One add_inc bw_point.update_convs(1) default_unit_def inc.simps(2) one_plus_BitM |
708 |
semiring_norm(6,26)) |
|
709 |
apply (smt bw_point.update_convs(1)) |
|
710 |
apply (smt bw_point.cases_scheme bw_point.update_convs(1) point.update_convs(1,2)) |
|
711 |
done |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
712 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
713 |
|
63167 | 714 |
subsubsection \<open>Type definitions\<close> |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
715 |
|
57214
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
716 |
typedef int' = "UNIV::int set" by (rule UNIV_witness) |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
717 |
|
57214
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
718 |
definition n0 where "n0 = Abs_int' 0" |
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
719 |
definition n1 where "n1 = Abs_int' 1" |
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
720 |
definition n2 where "n2 = Abs_int' 2" |
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
721 |
definition plus' where "plus' n m = Abs_int' (Rep_int' n + Rep_int' m)" |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
722 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
723 |
lemma |
57214
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
724 |
"n0 \<noteq> n1" |
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
725 |
"plus' n1 n1 = n2" |
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
726 |
"plus' n0 n2 = n2" |
58061 | 727 |
by (smt n0_def n1_def n2_def plus'_def Abs_int'_inverse Rep_int'_inverse UNIV_I)+ |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
728 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
729 |
|
63167 | 730 |
subsection \<open>With support by the SMT solver (but without proofs)\<close> |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
731 |
|
63167 | 732 |
subsubsection \<open>Algebraic datatypes\<close> |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
733 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
734 |
lemma |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
735 |
"x = fst (x, y)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
736 |
"y = snd (x, y)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
737 |
"((x, y) = (y, x)) = (x = y)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
738 |
"((x, y) = (u, v)) = (x = u \<and> y = v)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
739 |
"(fst (x, y, z) = fst (u, v, w)) = (x = u)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
740 |
"(snd (x, y, z) = snd (u, v, w)) = (y = v \<and> z = w)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
741 |
"(fst (snd (x, y, z)) = fst (snd (u, v, w))) = (y = v)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
742 |
"(snd (snd (x, y, z)) = snd (snd (u, v, w))) = (z = w)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
743 |
"(fst (x, y) = snd (x, y)) = (x = y)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
744 |
"p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
745 |
"(fst (x, y) = snd (x, y)) = (x = y)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
746 |
"(fst p = snd p) = (p = (snd p, fst p))" |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
58889
diff
changeset
|
747 |
using fst_conv snd_conv prod.collapse |
58061 | 748 |
using [[smt_oracle, z3_extensions]] |
749 |
by smt+ |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
750 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
751 |
lemma |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
752 |
"[x] \<noteq> Nil" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
753 |
"[x, y] \<noteq> Nil" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
754 |
"x \<noteq> y \<longrightarrow> [x] \<noteq> [y]" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
755 |
"hd (x # xs) = x" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
756 |
"tl (x # xs) = xs" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
757 |
"hd [x, y, z] = x" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
758 |
"tl [x, y, z] = [y, z]" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
759 |
"hd (tl [x, y, z]) = y" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
760 |
"tl (tl [x, y, z]) = [z]" |
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
54489
diff
changeset
|
761 |
using list.sel(1,3) |
58061 | 762 |
using [[smt_oracle, z3_extensions]] |
763 |
by smt+ |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
764 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
765 |
lemma |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
766 |
"fst (hd [(a, b)]) = a" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
767 |
"snd (hd [(a, b)]) = b" |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
58889
diff
changeset
|
768 |
using fst_conv snd_conv prod.collapse list.sel(1,3) |
58061 | 769 |
using [[smt_oracle, z3_extensions]] |
770 |
by smt+ |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
771 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
772 |
|
63167 | 773 |
subsubsection \<open>Records\<close> |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
774 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
775 |
lemma |
58366 | 776 |
"\<lparr>cx = x, cy = y\<rparr> = \<lparr>cx = x', cy = y'\<rparr> \<Longrightarrow> x = x' \<and> y = y'" |
58061 | 777 |
using [[smt_oracle, z3_extensions]] |
778 |
by smt+ |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
779 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
780 |
lemma |
41427 | 781 |
"cx \<lparr> cx = 3, cy = 4 \<rparr> = 3" |
782 |
"cy \<lparr> cx = 3, cy = 4 \<rparr> = 4" |
|
783 |
"cx \<lparr> cx = 3, cy = 4 \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4 \<rparr>" |
|
784 |
"\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4 \<rparr>" |
|
785 |
"\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6 \<rparr>" |
|
786 |
"p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" |
|
787 |
"p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr> = p" |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
788 |
using point.simps |
58061 | 789 |
using [[smt_oracle, z3_extensions]] |
790 |
by smt+ |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
791 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
792 |
lemma |
41427 | 793 |
"cy (p \<lparr> cx := a \<rparr>) = cy p" |
794 |
"cx (p \<lparr> cy := a \<rparr>) = cx p" |
|
795 |
"p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>" |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
796 |
using point.simps |
58061 | 797 |
using [[smt_oracle, z3_extensions]] |
798 |
by smt+ |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
799 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
800 |
lemma |
58366 | 801 |
"\<lparr>cx = x, cy = y, black = b\<rparr> = \<lparr>cx = x', cy = y', black = b'\<rparr> \<Longrightarrow> x = x' \<and> y = y' \<and> b = b'" |
58061 | 802 |
using [[smt_oracle, z3_extensions]] |
58366 | 803 |
by smt |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
804 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
805 |
lemma |
41427 | 806 |
"cx \<lparr> cx = 3, cy = 4, black = b \<rparr> = 3" |
807 |
"cy \<lparr> cx = 3, cy = 4, black = b \<rparr> = 4" |
|
808 |
"black \<lparr> cx = 3, cy = 4, black = b \<rparr> = b" |
|
809 |
"cx \<lparr> cx = 3, cy = 4, black = b \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4, black = b \<rparr>" |
|
810 |
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4, black = b \<rparr>" |
|
811 |
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6, black = b \<rparr>" |
|
812 |
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
813 |
p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p" |
|
814 |
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
815 |
p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p" |
|
816 |
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
817 |
p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
818 |
using point.simps bw_point.simps |
58061 | 819 |
using [[smt_oracle, z3_extensions]] |
820 |
by smt+ |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
821 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
822 |
lemma |
41427 | 823 |
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>" |
824 |
"\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> = |
|
825 |
\<lparr> cx = 3, cy = 4, black = False \<rparr>" |
|
826 |
sorry |
|
827 |
||
828 |
lemma |
|
829 |
"p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = |
|
830 |
p \<lparr> black := True \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>" |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
831 |
using point.simps bw_point.simps |
58061 | 832 |
using [[smt_oracle, z3_extensions]] |
833 |
by smt |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
834 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
835 |
|
63167 | 836 |
subsubsection \<open>Type definitions\<close> |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
837 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
838 |
lemma |
57214
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
839 |
"n0 \<noteq> n1" |
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
840 |
"plus' n1 n1 = n2" |
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
841 |
"plus' n0 n2 = n2" |
58061 | 842 |
using [[smt_oracle, z3_extensions]] |
843 |
by (smt n0_def n1_def n2_def plus'_def)+ |
|
37157 | 844 |
|
845 |
||
66738
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66298
diff
changeset
|
846 |
section \<open>Functions\<close> |
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66298
diff
changeset
|
847 |
|
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66298
diff
changeset
|
848 |
lemma "\<exists>f. map_option f (Some x) = Some (y + x)" |
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66298
diff
changeset
|
849 |
by (smt option.map(2)) |
37157 | 850 |
|
851 |
lemma |
|
852 |
"(f (i := v)) i = v" |
|
853 |
"i1 \<noteq> i2 \<longrightarrow> (f (i1 := v)) i2 = f i2" |
|
854 |
"i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v1" |
|
855 |
"i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i2 = v2" |
|
856 |
"i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2" |
|
857 |
"i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2" |
|
47155
ade3fc826af3
dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
boehmes
parents:
47152
diff
changeset
|
858 |
"i1 \<noteq> i2 \<and>i1 \<noteq> i3 \<and> i2 \<noteq> i3 \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3" |
41132 | 859 |
using fun_upd_same fun_upd_apply |
58061 | 860 |
by smt+ |
37157 | 861 |
|
862 |
||
63167 | 863 |
section \<open>Sets\<close> |
37157 | 864 |
|
44925 | 865 |
lemma Empty: "x \<notin> {}" by simp |
866 |
||
58061 | 867 |
lemmas smt_sets = Empty UNIV_I Un_iff Int_iff |
37157 | 868 |
|
869 |
lemma |
|
870 |
"x \<notin> {}" |
|
871 |
"x \<in> UNIV" |
|
44925 | 872 |
"x \<in> A \<union> B \<longleftrightarrow> x \<in> A \<or> x \<in> B" |
873 |
"x \<in> P \<union> {} \<longleftrightarrow> x \<in> P" |
|
37157 | 874 |
"x \<in> P \<union> UNIV" |
44925 | 875 |
"x \<in> P \<union> Q \<longleftrightarrow> x \<in> Q \<union> P" |
876 |
"x \<in> P \<union> P \<longleftrightarrow> x \<in> P" |
|
877 |
"x \<in> P \<union> (Q \<union> R) \<longleftrightarrow> x \<in> (P \<union> Q) \<union> R" |
|
878 |
"x \<in> A \<inter> B \<longleftrightarrow> x \<in> A \<and> x \<in> B" |
|
37157 | 879 |
"x \<notin> P \<inter> {}" |
44925 | 880 |
"x \<in> P \<inter> UNIV \<longleftrightarrow> x \<in> P" |
881 |
"x \<in> P \<inter> Q \<longleftrightarrow> x \<in> Q \<inter> P" |
|
882 |
"x \<in> P \<inter> P \<longleftrightarrow> x \<in> P" |
|
883 |
"x \<in> P \<inter> (Q \<inter> R) \<longleftrightarrow> x \<in> (P \<inter> Q) \<inter> R" |
|
884 |
"{x. x \<in> P} = {y. y \<in> P}" |
|
58061 | 885 |
by (smt smt_sets)+ |
37157 | 886 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
887 |
end |