author | haftmann |
Tue, 13 Oct 2015 09:21:15 +0200 | |
changeset 61424 | c3658c18b7bc |
parent 58889 | 5b7a9633cfa8 |
child 61945 | 1135b8de26c3 |
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 |
|
58889 | 5 |
section {* Tests for the SMT binding *} |
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 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
13 |
text {* Most examples are taken from various Isabelle theories and from HOL4. *} |
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 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
16 |
section {* Propositional logic *} |
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 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
84 |
section {* First-order logic with equality *} |
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 |
|
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
56859
diff
changeset
|
184 |
section {* Guidance for quantifier heuristics: patterns *} |
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 |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset
|
201 |
section {* Meta-logical connectives *} |
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 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
225 |
section {* Integers *} |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
226 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
227 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
228 |
"(0::int) = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
229 |
"(0::int) = (- 0)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
230 |
"(1::int) = 1" |
57232 | 231 |
"\<not> (-1 = (1::int))" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
232 |
"(0::int) < 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
233 |
"(0::int) \<le> 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
234 |
"-123 + 345 < (567::int)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
235 |
"(123456789::int) < 2345678901" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
236 |
"(-123456789::int) < 2345678901" |
58061 | 237 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
238 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
239 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
240 |
"(x::int) + 0 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
241 |
"0 + x = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
242 |
"x + y = y + x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
243 |
"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
|
244 |
"(x + y = 0) = (x = -y)" |
58061 | 245 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
246 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
247 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
248 |
"(-1::int) = - 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
249 |
"(-3::int) = - 3" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
250 |
"-(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
|
251 |
"x > 0 \<longrightarrow> -x < 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
252 |
"x < 0 \<longrightarrow> -x > 0" |
58061 | 253 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
254 |
|
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset
|
255 |
lemma |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
256 |
"(x::int) - 0 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
257 |
"0 - x = -x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
258 |
"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
|
259 |
"x - y = -(y - x)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
260 |
"x - y = -y + x" |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset
|
261 |
"x - y - z = x - (y + z)" |
58061 | 262 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
263 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
264 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
265 |
"(x::int) * 0 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
266 |
"0 * x = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
267 |
"x * 1 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
268 |
"1 * x = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
269 |
"x * -1 = -x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
270 |
"-1 * x = -x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
271 |
"3 * x = x * 3" |
58061 | 272 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
273 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
274 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
275 |
"(0::int) div 0 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
276 |
"(x::int) div 0 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
277 |
"(0::int) div 1 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
278 |
"(1::int) div 1 = 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
279 |
"(3::int) div 1 = 3" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
280 |
"(x::int) div 1 = x" |
37151 | 281 |
"(0::int) div -1 = 0" |
282 |
"(1::int) div -1 = -1" |
|
283 |
"(3::int) div -1 = -3" |
|
284 |
"(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
|
285 |
"(0::int) div 3 = 0" |
37151 | 286 |
"(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
|
287 |
"(1::int) div 3 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
288 |
"(3::int) div 3 = 1" |
37151 | 289 |
"(5::int) div 3 = 1" |
290 |
"(1::int) div -3 = -1" |
|
291 |
"(3::int) div -3 = -1" |
|
292 |
"(5::int) div -3 = -2" |
|
293 |
"(-1::int) div 3 = -1" |
|
294 |
"(-3::int) div 3 = -1" |
|
295 |
"(-5::int) div 3 = -2" |
|
296 |
"(-1::int) div -3 = 0" |
|
297 |
"(-3::int) div -3 = 1" |
|
298 |
"(-5::int) div -3 = 1" |
|
58061 | 299 |
using [[z3_extensions]] |
300 |
by smt+ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
301 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
302 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
303 |
"(0::int) mod 0 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
304 |
"(x::int) mod 0 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
305 |
"(0::int) mod 1 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
306 |
"(1::int) mod 1 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
307 |
"(3::int) mod 1 = 0" |
37151 | 308 |
"(x::int) mod 1 = 0" |
309 |
"(0::int) mod -1 = 0" |
|
310 |
"(1::int) mod -1 = 0" |
|
311 |
"(3::int) mod -1 = 0" |
|
312 |
"(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
|
313 |
"(0::int) mod 3 = 0" |
37151 | 314 |
"(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
|
315 |
"(1::int) mod 3 = 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
316 |
"(3::int) mod 3 = 0" |
37151 | 317 |
"(5::int) mod 3 = 2" |
318 |
"(1::int) mod -3 = -2" |
|
319 |
"(3::int) mod -3 = 0" |
|
320 |
"(5::int) mod -3 = -1" |
|
321 |
"(-1::int) mod 3 = 2" |
|
322 |
"(-3::int) mod 3 = 0" |
|
323 |
"(-5::int) mod 3 = 1" |
|
324 |
"(-1::int) mod -3 = -1" |
|
325 |
"(-3::int) mod -3 = 0" |
|
326 |
"(-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
|
327 |
"x mod 3 < 3" |
37151 | 328 |
"(x mod 3 = x) \<longrightarrow> (x < 3)" |
58061 | 329 |
using [[z3_extensions]] |
330 |
by smt+ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
331 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
332 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
333 |
"(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
|
334 |
"x = x div 3 * 3 + x mod 3" |
58061 | 335 |
using [[z3_extensions]] |
336 |
by smt+ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
337 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
338 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
339 |
"abs (x::int) \<ge> 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
340 |
"(abs x = 0) = (x = 0)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
341 |
"(x \<ge> 0) = (abs x = x)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
342 |
"(x \<le> 0) = (abs x = -x)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
343 |
"abs (abs x) = abs x" |
58061 | 344 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
345 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
346 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
347 |
"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
|
348 |
"min x y \<le> y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
349 |
"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
|
350 |
"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
|
351 |
"x \<ge> 0 \<longrightarrow> min x 0 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
352 |
"min x y \<le> abs (x + y)" |
58061 | 353 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
354 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
355 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
356 |
"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
|
357 |
"max x y \<ge> y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
358 |
"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
|
359 |
"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
|
360 |
"x \<ge> 0 \<longrightarrow> max x 0 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
361 |
"max x y \<ge> - abs x - abs 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 |
"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
|
366 |
"x \<le> x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
367 |
"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
|
368 |
"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
|
369 |
"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
|
370 |
"(x < y) = (x + 1 \<le> y)" |
57232 | 371 |
"\<not> (x < x)" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
372 |
"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
|
373 |
"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
|
374 |
"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
|
375 |
"x < y \<longrightarrow> y < z \<longrightarrow> x < z" |
57232 | 376 |
"x < y \<and> y < z \<longrightarrow> \<not> (z < x)" |
58061 | 377 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
378 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
379 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
380 |
section {* Reals *} |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
381 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
382 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
383 |
"(0::real) = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
384 |
"(0::real) = -0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
385 |
"(0::real) = (- 0)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
386 |
"(1::real) = 1" |
57232 | 387 |
"\<not> (-1 = (1::real))" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
388 |
"(0::real) < 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
389 |
"(0::real) \<le> 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
390 |
"-123 + 345 < (567::real)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
391 |
"(123456789::real) < 2345678901" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
392 |
"(-123456789::real) < 2345678901" |
58061 | 393 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
394 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
395 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
396 |
"(x::real) + 0 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
397 |
"0 + x = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
398 |
"x + y = y + x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
399 |
"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
|
400 |
"(x + y = 0) = (x = -y)" |
58061 | 401 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
402 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
403 |
lemma |
41132 | 404 |
"(-1::real) = - 1" |
405 |
"(-3::real) = - 3" |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
406 |
"-(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
|
407 |
"x > 0 \<longrightarrow> -x < 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
408 |
"x < 0 \<longrightarrow> -x > 0" |
58061 | 409 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
410 |
|
49995
3b7ad6153322
regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles
blanchet
parents:
49834
diff
changeset
|
411 |
lemma |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
412 |
"(x::real) - 0 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
413 |
"0 - x = -x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
414 |
"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
|
415 |
"x - y = -(y - x)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
416 |
"x - y = -y + x" |
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset
|
417 |
"x - y - z = x - (y + z)" |
58061 | 418 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
419 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
420 |
lemma |
41132 | 421 |
"(x::real) * 0 = 0" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
422 |
"0 * x = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
423 |
"x * 1 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
424 |
"1 * x = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
425 |
"x * -1 = -x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
426 |
"-1 * x = -x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
427 |
"3 * x = x * 3" |
58061 | 428 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
429 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
430 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
431 |
"(1/2 :: real) < 1" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
432 |
"(1::real) / 3 = 1 / 3" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
433 |
"(1::real) / -3 = - 1 / 3" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
434 |
"(-1::real) / 3 = - 1 / 3" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
435 |
"(-1::real) / -3 = 1 / 3" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
436 |
"(x::real) / 1 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
437 |
"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
|
438 |
"x < 0 \<longrightarrow> x / 3 > x" |
58061 | 439 |
using [[z3_extensions]] |
440 |
by smt+ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
441 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
442 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
443 |
"(3::real) * (x / 3) = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
444 |
"(x * 3) / 3 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
445 |
"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
|
446 |
"x < 0 \<longrightarrow> 2 * x / 3 > x" |
58061 | 447 |
using [[z3_extensions]] |
448 |
by smt+ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
449 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
450 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
451 |
"abs (x::real) \<ge> 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
452 |
"(abs x = 0) = (x = 0)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
453 |
"(x \<ge> 0) = (abs x = x)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
454 |
"(x \<le> 0) = (abs x = -x)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
455 |
"abs (abs x) = abs x" |
58061 | 456 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
457 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
458 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
459 |
"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
|
460 |
"min x y \<le> y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
461 |
"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
|
462 |
"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
|
463 |
"x \<ge> 0 \<longrightarrow> min x 0 = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
464 |
"min x y \<le> abs (x + y)" |
58061 | 465 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
466 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
467 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
468 |
"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
|
469 |
"max x y \<ge> y" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
470 |
"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
|
471 |
"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
|
472 |
"x \<ge> 0 \<longrightarrow> max x 0 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
473 |
"max x y \<ge> - abs x - abs y" |
58061 | 474 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
475 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
476 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
477 |
"x \<le> (x::real)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
478 |
"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
|
479 |
"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
|
480 |
"x < y \<longrightarrow> x \<le> y" |
57232 | 481 |
"\<not> (x < x)" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
482 |
"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
|
483 |
"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
|
484 |
"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
|
485 |
"x < y \<longrightarrow> y < z \<longrightarrow> x < z" |
57232 | 486 |
"x < y \<and> y < z \<longrightarrow> \<not> (z < x)" |
58061 | 487 |
by smt+ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
488 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
489 |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
490 |
section {* Datatypes, Records, and Typedefs *} |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
491 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
492 |
subsection {* Without support by the SMT solver *} |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
493 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
494 |
subsubsection {* Algebraic datatypes *} |
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 |
lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
497 |
"x = fst (x, y)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
498 |
"y = snd (x, y)" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
499 |
"((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
|
500 |
"((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
|
501 |
"(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
|
502 |
"(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
|
503 |
"(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
|
504 |
"(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
|
505 |
"(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
|
506 |
"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
|
507 |
"(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
|
508 |
"(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
|
509 |
using fst_conv snd_conv prod.collapse |
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 |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
512 |
lemma |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
513 |
"[x] \<noteq> Nil" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
514 |
"[x, y] \<noteq> Nil" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
515 |
"x \<noteq> y \<longrightarrow> [x] \<noteq> [y]" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
516 |
"hd (x # xs) = x" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
517 |
"tl (x # xs) = xs" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
518 |
"hd [x, y, z] = x" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
519 |
"tl [x, y, z] = [y, z]" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
520 |
"hd (tl [x, y, z]) = y" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
521 |
"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
|
522 |
using list.sel(1,3) list.simps |
58061 | 523 |
by smt+ |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
524 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
525 |
lemma |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
526 |
"fst (hd [(a, b)]) = a" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
527 |
"snd (hd [(a, b)]) = b" |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
58889
diff
changeset
|
528 |
using fst_conv snd_conv prod.collapse list.sel(1,3) list.simps |
58061 | 529 |
by smt+ |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
530 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
531 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
532 |
subsubsection {* Records *} |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
533 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
534 |
record point = |
41427 | 535 |
cx :: int |
536 |
cy :: int |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
537 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
538 |
record bw_point = point + |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
539 |
black :: bool |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
540 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
541 |
lemma |
58366 | 542 |
"\<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
|
543 |
using point.simps |
58366 | 544 |
by smt |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
545 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
546 |
lemma |
41427 | 547 |
"cx \<lparr> cx = 3, cy = 4 \<rparr> = 3" |
548 |
"cy \<lparr> cx = 3, cy = 4 \<rparr> = 4" |
|
549 |
"cx \<lparr> cx = 3, cy = 4 \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4 \<rparr>" |
|
550 |
"\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4 \<rparr>" |
|
551 |
"\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6 \<rparr>" |
|
552 |
"p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" |
|
553 |
"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
|
554 |
using point.simps |
58061 | 555 |
by smt+ |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
556 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
557 |
lemma |
41427 | 558 |
"cy (p \<lparr> cx := a \<rparr>) = cy p" |
559 |
"cx (p \<lparr> cy := a \<rparr>) = cx p" |
|
560 |
"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
|
561 |
sorry |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
562 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
563 |
lemma |
58366 | 564 |
"\<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
|
565 |
using point.simps bw_point.simps |
58366 | 566 |
by smt |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
567 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
568 |
lemma |
41427 | 569 |
"cx \<lparr> cx = 3, cy = 4, black = b \<rparr> = 3" |
570 |
"cy \<lparr> cx = 3, cy = 4, black = b \<rparr> = 4" |
|
571 |
"black \<lparr> cx = 3, cy = 4, black = b \<rparr> = b" |
|
572 |
"cx \<lparr> cx = 3, cy = 4, black = b \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4, black = b \<rparr>" |
|
573 |
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4, black = b \<rparr>" |
|
574 |
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6, black = b \<rparr>" |
|
575 |
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
576 |
p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p" |
|
577 |
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
578 |
p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p" |
|
579 |
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
580 |
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
|
581 |
using point.simps bw_point.simps |
58366 | 582 |
by smt+ |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
583 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
584 |
lemma |
41427 | 585 |
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>" |
586 |
"\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> = |
|
587 |
\<lparr> cx = 3, cy = 4, black = False \<rparr>" |
|
588 |
"p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = |
|
589 |
p \<lparr> black := True \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>" |
|
58366 | 590 |
apply (smt add_One add_inc bw_point.update_convs(1) default_unit_def inc.simps(2) one_plus_BitM |
591 |
semiring_norm(6,26)) |
|
592 |
apply (smt bw_point.update_convs(1)) |
|
593 |
apply (smt bw_point.cases_scheme bw_point.update_convs(1) point.update_convs(1,2)) |
|
594 |
done |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
595 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
596 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
597 |
subsubsection {* Type definitions *} |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
598 |
|
57214
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
599 |
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
|
600 |
|
57214
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
601 |
definition n0 where "n0 = Abs_int' 0" |
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
602 |
definition n1 where "n1 = Abs_int' 1" |
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
603 |
definition n2 where "n2 = Abs_int' 2" |
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
604 |
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
|
605 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
606 |
lemma |
57214
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
607 |
"n0 \<noteq> n1" |
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
608 |
"plus' n1 n1 = n2" |
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
609 |
"plus' n0 n2 = n2" |
58061 | 610 |
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
|
611 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
612 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
613 |
subsection {* With support by the SMT solver (but without proofs) *} |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
614 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
615 |
subsubsection {* Algebraic datatypes *} |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
616 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
617 |
lemma |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
618 |
"x = fst (x, y)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
619 |
"y = snd (x, y)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
620 |
"((x, y) = (y, x)) = (x = y)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
621 |
"((x, y) = (u, v)) = (x = u \<and> y = v)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
622 |
"(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
|
623 |
"(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
|
624 |
"(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
|
625 |
"(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
|
626 |
"(fst (x, y) = snd (x, y)) = (x = y)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
627 |
"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
|
628 |
"(fst (x, y) = snd (x, y)) = (x = y)" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
629 |
"(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
|
630 |
using fst_conv snd_conv prod.collapse |
58061 | 631 |
using [[smt_oracle, z3_extensions]] |
632 |
by smt+ |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
633 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
634 |
lemma |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
635 |
"[x] \<noteq> Nil" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
636 |
"[x, y] \<noteq> Nil" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
637 |
"x \<noteq> y \<longrightarrow> [x] \<noteq> [y]" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
638 |
"hd (x # xs) = x" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
639 |
"tl (x # xs) = xs" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
640 |
"hd [x, y, z] = x" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
641 |
"tl [x, y, z] = [y, z]" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
642 |
"hd (tl [x, y, z]) = y" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
643 |
"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
|
644 |
using list.sel(1,3) |
58061 | 645 |
using [[smt_oracle, z3_extensions]] |
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 |
lemma |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
649 |
"fst (hd [(a, b)]) = a" |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
650 |
"snd (hd [(a, b)]) = b" |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
58889
diff
changeset
|
651 |
using fst_conv snd_conv prod.collapse list.sel(1,3) |
58061 | 652 |
using [[smt_oracle, z3_extensions]] |
653 |
by smt+ |
|
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 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
656 |
subsubsection {* Records *} |
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'" |
58061 | 660 |
using [[smt_oracle, z3_extensions]] |
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 |
using [[smt_oracle, z3_extensions]] |
673 |
by smt+ |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
674 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
675 |
lemma |
41427 | 676 |
"cy (p \<lparr> cx := a \<rparr>) = cy p" |
677 |
"cx (p \<lparr> cy := a \<rparr>) = cx p" |
|
678 |
"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
|
679 |
using point.simps |
58061 | 680 |
using [[smt_oracle, z3_extensions]] |
681 |
by smt+ |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
682 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
683 |
lemma |
58366 | 684 |
"\<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 | 685 |
using [[smt_oracle, z3_extensions]] |
58366 | 686 |
by smt |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
687 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
688 |
lemma |
41427 | 689 |
"cx \<lparr> cx = 3, cy = 4, black = b \<rparr> = 3" |
690 |
"cy \<lparr> cx = 3, cy = 4, black = b \<rparr> = 4" |
|
691 |
"black \<lparr> cx = 3, cy = 4, black = b \<rparr> = b" |
|
692 |
"cx \<lparr> cx = 3, cy = 4, black = b \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4, black = b \<rparr>" |
|
693 |
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4, black = b \<rparr>" |
|
694 |
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6, black = b \<rparr>" |
|
695 |
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
696 |
p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p" |
|
697 |
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
698 |
p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p" |
|
699 |
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
|
700 |
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
|
701 |
using point.simps bw_point.simps |
58061 | 702 |
using [[smt_oracle, z3_extensions]] |
703 |
by smt+ |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
704 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
705 |
lemma |
41427 | 706 |
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>" |
707 |
"\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> = |
|
708 |
\<lparr> cx = 3, cy = 4, black = False \<rparr>" |
|
709 |
sorry |
|
710 |
||
711 |
lemma |
|
712 |
"p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = |
|
713 |
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
|
714 |
using point.simps bw_point.simps |
58061 | 715 |
using [[smt_oracle, z3_extensions]] |
716 |
by smt |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
717 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
718 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
719 |
subsubsection {* Type definitions *} |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
720 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset
|
721 |
lemma |
57214
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
722 |
"n0 \<noteq> n1" |
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
723 |
"plus' n1 n1 = n2" |
c4986877deea
adapted SMT examples to new, corrected handling of 'typedef'
blanchet
parents:
57168
diff
changeset
|
724 |
"plus' n0 n2 = n2" |
58061 | 725 |
using [[smt_oracle, z3_extensions]] |
726 |
by (smt n0_def n1_def n2_def plus'_def)+ |
|
37157 | 727 |
|
728 |
||
729 |
section {* Function updates *} |
|
730 |
||
731 |
lemma |
|
732 |
"(f (i := v)) i = v" |
|
733 |
"i1 \<noteq> i2 \<longrightarrow> (f (i1 := v)) i2 = f i2" |
|
734 |
"i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v1" |
|
735 |
"i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i2 = v2" |
|
736 |
"i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2" |
|
737 |
"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
|
738 |
"i1 \<noteq> i2 \<and>i1 \<noteq> i3 \<and> i2 \<noteq> i3 \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3" |
41132 | 739 |
using fun_upd_same fun_upd_apply |
58061 | 740 |
by smt+ |
37157 | 741 |
|
742 |
||
743 |
section {* Sets *} |
|
744 |
||
44925 | 745 |
lemma Empty: "x \<notin> {}" by simp |
746 |
||
58061 | 747 |
lemmas smt_sets = Empty UNIV_I Un_iff Int_iff |
37157 | 748 |
|
749 |
lemma |
|
750 |
"x \<notin> {}" |
|
751 |
"x \<in> UNIV" |
|
44925 | 752 |
"x \<in> A \<union> B \<longleftrightarrow> x \<in> A \<or> x \<in> B" |
753 |
"x \<in> P \<union> {} \<longleftrightarrow> x \<in> P" |
|
37157 | 754 |
"x \<in> P \<union> UNIV" |
44925 | 755 |
"x \<in> P \<union> Q \<longleftrightarrow> x \<in> Q \<union> P" |
756 |
"x \<in> P \<union> P \<longleftrightarrow> x \<in> P" |
|
757 |
"x \<in> P \<union> (Q \<union> R) \<longleftrightarrow> x \<in> (P \<union> Q) \<union> R" |
|
758 |
"x \<in> A \<inter> B \<longleftrightarrow> x \<in> A \<and> x \<in> B" |
|
37157 | 759 |
"x \<notin> P \<inter> {}" |
44925 | 760 |
"x \<in> P \<inter> UNIV \<longleftrightarrow> x \<in> P" |
761 |
"x \<in> P \<inter> Q \<longleftrightarrow> x \<in> Q \<inter> P" |
|
762 |
"x \<in> P \<inter> P \<longleftrightarrow> x \<in> P" |
|
763 |
"x \<in> P \<inter> (Q \<inter> R) \<longleftrightarrow> x \<in> (P \<inter> Q) \<inter> R" |
|
764 |
"{x. x \<in> P} = {y. y \<in> P}" |
|
58061 | 765 |
by (smt smt_sets)+ |
37157 | 766 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
767 |
end |