author | nipkow |
Mon, 24 Sep 2018 14:30:09 +0200 | |
changeset 69064 | 5840724b1d71 |
parent 67972 | 959b0aed2ce5 |
child 69204 | d5ab1636660b |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/SMT.thy |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
66551 | 3 |
Author: Jasmin Blanchette, VU Amsterdam |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
4 |
*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
5 |
|
61626 | 6 |
section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
7 |
|
58061 | 8 |
theory SMT |
66551 | 9 |
imports Divides |
10 |
keywords "smt_status" :: diag |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
11 |
begin |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
12 |
|
60758 | 13 |
subsection \<open>A skolemization tactic and proof method\<close> |
58481 | 14 |
|
15 |
lemma choices: |
|
16 |
"\<And>Q. \<forall>x. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x. Q x (f x) (fa x)" |
|
17 |
"\<And>Q. \<forall>x. \<exists>y ya yb. Q x y ya yb \<Longrightarrow> \<exists>f fa fb. \<forall>x. Q x (f x) (fa x) (fb x)" |
|
18 |
"\<And>Q. \<forall>x. \<exists>y ya yb yc. Q x y ya yb yc \<Longrightarrow> \<exists>f fa fb fc. \<forall>x. Q x (f x) (fa x) (fb x) (fc x)" |
|
58598 | 19 |
"\<And>Q. \<forall>x. \<exists>y ya yb yc yd. Q x y ya yb yc yd \<Longrightarrow> |
20 |
\<exists>f fa fb fc fd. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x)" |
|
21 |
"\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye. Q x y ya yb yc yd ye \<Longrightarrow> |
|
22 |
\<exists>f fa fb fc fd fe. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" |
|
23 |
"\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \<Longrightarrow> |
|
24 |
\<exists>f fa fb fc fd fe ff. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" |
|
25 |
"\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \<Longrightarrow> |
|
26 |
\<exists>f fa fb fc fd fe ff fg. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)" |
|
58481 | 27 |
by metis+ |
28 |
||
29 |
lemma bchoices: |
|
30 |
"\<And>Q. \<forall>x \<in> S. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x \<in> S. Q x (f x) (fa x)" |
|
31 |
"\<And>Q. \<forall>x \<in> S. \<exists>y ya yb. Q x y ya yb \<Longrightarrow> \<exists>f fa fb. \<forall>x \<in> S. Q x (f x) (fa x) (fb x)" |
|
32 |
"\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc. Q x y ya yb yc \<Longrightarrow> \<exists>f fa fb fc. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x)" |
|
58598 | 33 |
"\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd. Q x y ya yb yc yd \<Longrightarrow> |
34 |
\<exists>f fa fb fc fd. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x)" |
|
35 |
"\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye. Q x y ya yb yc yd ye \<Longrightarrow> |
|
36 |
\<exists>f fa fb fc fd fe. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" |
|
37 |
"\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \<Longrightarrow> |
|
38 |
\<exists>f fa fb fc fd fe ff. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" |
|
39 |
"\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \<Longrightarrow> |
|
40 |
\<exists>f fa fb fc fd fe ff fg. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)" |
|
58481 | 41 |
by metis+ |
42 |
||
60758 | 43 |
ML \<open> |
58481 | 44 |
fun moura_tac ctxt = |
45 |
Atomize_Elim.atomize_elim_tac ctxt THEN' |
|
46 |
SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice choices bchoice bchoices}) THEN |
|
58598 | 47 |
ALLGOALS (Metis_Tactic.metis_tac (take 1 ATP_Proof_Reconstruct.partial_type_encs) |
48 |
ATP_Proof_Reconstruct.default_metis_lam_trans ctxt [] ORELSE' |
|
49 |
blast_tac ctxt)) |
|
60758 | 50 |
\<close> |
58481 | 51 |
|
60758 | 52 |
method_setup moura = \<open> |
60201 | 53 |
Scan.succeed (SIMPLE_METHOD' o moura_tac) |
60758 | 54 |
\<close> "solve skolemization goals, especially those arising from Z3 proofs" |
58481 | 55 |
|
56 |
hide_fact (open) choices bchoices |
|
57 |
||
58 |
||
60758 | 59 |
subsection \<open>Triggers for quantifier instantiation\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
60 |
|
60758 | 61 |
text \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
62 |
Some SMT solvers support patterns as a quantifier instantiation |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
63 |
heuristics. Patterns may either be positive terms (tagged by "pat") |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
64 |
triggering quantifier instantiations -- when the solver finds a |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
65 |
term matching a positive pattern, it instantiates the corresponding |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
66 |
quantifier accordingly -- or negative terms (tagged by "nopat") |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
67 |
inhibiting quantifier instantiations. A list of patterns |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
68 |
of the same kind is called a multipattern, and all patterns in a |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
69 |
multipattern are considered conjunctively for quantifier instantiation. |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
70 |
A list of multipatterns is called a trigger, and their multipatterns |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
71 |
act disjunctively during quantifier instantiation. Each multipattern |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
72 |
should mention at least all quantified variables of the preceding |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
73 |
quantifier block. |
60758 | 74 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
75 |
|
57230 | 76 |
typedecl 'a symb_list |
77 |
||
78 |
consts |
|
79 |
Symb_Nil :: "'a symb_list" |
|
80 |
Symb_Cons :: "'a \<Rightarrow> 'a symb_list \<Rightarrow> 'a symb_list" |
|
81 |
||
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
82 |
typedecl pattern |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
83 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
84 |
consts |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
85 |
pat :: "'a \<Rightarrow> pattern" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
86 |
nopat :: "'a \<Rightarrow> pattern" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
87 |
|
57230 | 88 |
definition trigger :: "pattern symb_list symb_list \<Rightarrow> bool \<Rightarrow> bool" where |
89 |
"trigger _ P = P" |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
90 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
91 |
|
60758 | 92 |
subsection \<open>Higher-order encoding\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
93 |
|
60758 | 94 |
text \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
95 |
Application is made explicit for constants occurring with varying |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
96 |
numbers of arguments. This is achieved by the introduction of the |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
97 |
following constant. |
60758 | 98 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
99 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
100 |
definition fun_app :: "'a \<Rightarrow> 'a" where "fun_app f = f" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
101 |
|
60758 | 102 |
text \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
103 |
Some solvers support a theory of arrays which can be used to encode |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
104 |
higher-order functions. The following set of lemmas specifies the |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
105 |
properties of such (extensional) arrays. |
60758 | 106 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
107 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
108 |
lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other fun_upd_upd fun_app_def |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
109 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
110 |
|
60758 | 111 |
subsection \<open>Normalization\<close> |
56103
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset
|
112 |
|
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset
|
113 |
lemma case_bool_if[abs_def]: "case_bool x y P = (if P then x else y)" |
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset
|
114 |
by simp |
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset
|
115 |
|
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset
|
116 |
lemmas Ex1_def_raw = Ex1_def[abs_def] |
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset
|
117 |
lemmas Ball_def_raw = Ball_def[abs_def] |
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset
|
118 |
lemmas Bex_def_raw = Bex_def[abs_def] |
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset
|
119 |
lemmas abs_if_raw = abs_if[abs_def] |
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset
|
120 |
lemmas min_def_raw = min_def[abs_def] |
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset
|
121 |
lemmas max_def_raw = max_def[abs_def] |
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset
|
122 |
|
66817 | 123 |
lemma nat_zero_as_int: |
124 |
"0 = nat 0" |
|
125 |
by simp |
|
126 |
||
127 |
lemma nat_one_as_int: |
|
128 |
"1 = nat 1" |
|
129 |
by simp |
|
130 |
||
66298 | 131 |
lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp |
67399 | 132 |
lemma nat_less_as_int: "(<) = (\<lambda>a b. int a < int b)" by simp |
133 |
lemma nat_leq_as_int: "(\<le>) = (\<lambda>a b. int a \<le> int b)" by simp |
|
66298 | 134 |
lemma Suc_as_int: "Suc = (\<lambda>a. nat (int a + 1))" by (rule ext) simp |
67399 | 135 |
lemma nat_plus_as_int: "(+) = (\<lambda>a b. nat (int a + int b))" by (rule ext)+ simp |
136 |
lemma nat_minus_as_int: "(-) = (\<lambda>a b. nat (int a - int b))" by (rule ext)+ simp |
|
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
67972
diff
changeset
|
137 |
lemma nat_times_as_int: "(*) = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib) |
67399 | 138 |
lemma nat_div_as_int: "(div) = (\<lambda>a b. nat (int a div int b))" by (simp add: nat_div_distrib) |
139 |
lemma nat_mod_as_int: "(mod) = (\<lambda>a b. nat (int a mod int b))" by (simp add: nat_mod_distrib) |
|
66298 | 140 |
|
141 |
lemma int_Suc: "int (Suc n) = int n + 1" by simp |
|
142 |
lemma int_plus: "int (n + m) = int n + int m" by (rule of_nat_add) |
|
143 |
lemma int_minus: "int (n - m) = int (nat (int n - int m))" by auto |
|
144 |
||
67972
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
145 |
lemma nat_int_comparison: |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
146 |
fixes a b :: nat |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
147 |
shows "(a = b) = (int a = int b)" |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
148 |
and "(a < b) = (int a < int b)" |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
149 |
and "(a \<le> b) = (int a \<le> int b)" |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
150 |
by simp_all |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
151 |
|
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
152 |
lemma int_ops: |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
153 |
fixes a b :: nat |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
154 |
shows "int 0 = 0" |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
155 |
and "int 1 = 1" |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
156 |
and "int (numeral n) = numeral n" |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
157 |
and "int (Suc a) = int a + 1" |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
158 |
and "int (a + b) = int a + int b" |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
159 |
and "int (a - b) = (if int a < int b then 0 else int a - int b)" |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
160 |
and "int (a * b) = int a * int b" |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
161 |
and "int (a div b) = int a div int b" |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
162 |
and "int (a mod b) = int a mod int b" |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
163 |
by (auto intro: zdiv_int zmod_int) |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
164 |
|
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
165 |
lemma int_if: |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
166 |
fixes a b :: nat |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
167 |
shows "int (if P then a else b) = (if P then int a else int b)" |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
168 |
by simp |
959b0aed2ce5
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
boehmes
parents:
67399
diff
changeset
|
169 |
|
56103
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset
|
170 |
|
60758 | 171 |
subsection \<open>Integer division and modulo for Z3\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
172 |
|
60758 | 173 |
text \<open> |
61799 | 174 |
The following Z3-inspired definitions are overspecified for the case where \<open>l = 0\<close>. This |
175 |
Schönheitsfehler is corrected in the \<open>div_as_z3div\<close> and \<open>mod_as_z3mod\<close> theorems. |
|
60758 | 176 |
\<close> |
56102 | 177 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
178 |
definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where |
56102 | 179 |
"z3div k l = (if l \<ge> 0 then k div l else - (k div - l))" |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
180 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
181 |
definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where |
56102 | 182 |
"z3mod k l = k mod (if l \<ge> 0 then l else - l)" |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
183 |
|
56101 | 184 |
lemma div_as_z3div: |
56102 | 185 |
"\<forall>k l. k div l = (if l = 0 then 0 else if l > 0 then z3div k l else z3div (- k) (- l))" |
56101 | 186 |
by (simp add: z3div_def) |
187 |
||
188 |
lemma mod_as_z3mod: |
|
56102 | 189 |
"\<forall>k l. k mod l = (if l = 0 then k else if l > 0 then z3mod k l else - z3mod (- k) (- l))" |
56101 | 190 |
by (simp add: z3mod_def) |
191 |
||
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
192 |
|
60758 | 193 |
subsection \<open>Setup\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
194 |
|
58061 | 195 |
ML_file "Tools/SMT/smt_util.ML" |
196 |
ML_file "Tools/SMT/smt_failure.ML" |
|
197 |
ML_file "Tools/SMT/smt_config.ML" |
|
198 |
ML_file "Tools/SMT/smt_builtin.ML" |
|
199 |
ML_file "Tools/SMT/smt_datatypes.ML" |
|
200 |
ML_file "Tools/SMT/smt_normalize.ML" |
|
201 |
ML_file "Tools/SMT/smt_translate.ML" |
|
202 |
ML_file "Tools/SMT/smtlib.ML" |
|
203 |
ML_file "Tools/SMT/smtlib_interface.ML" |
|
204 |
ML_file "Tools/SMT/smtlib_proof.ML" |
|
205 |
ML_file "Tools/SMT/smtlib_isar.ML" |
|
206 |
ML_file "Tools/SMT/z3_proof.ML" |
|
207 |
ML_file "Tools/SMT/z3_isar.ML" |
|
208 |
ML_file "Tools/SMT/smt_solver.ML" |
|
58360 | 209 |
ML_file "Tools/SMT/cvc4_interface.ML" |
59015 | 210 |
ML_file "Tools/SMT/cvc4_proof_parse.ML" |
58360 | 211 |
ML_file "Tools/SMT/verit_proof.ML" |
212 |
ML_file "Tools/SMT/verit_isar.ML" |
|
213 |
ML_file "Tools/SMT/verit_proof_parse.ML" |
|
59381
de4218223e00
more efficient Z3 proof reconstruction for rewrite steps with conjunctions and disjunctions, similar to Old_SMT
boehmes
parents:
59045
diff
changeset
|
214 |
ML_file "Tools/SMT/conj_disj_perm.ML" |
58061 | 215 |
ML_file "Tools/SMT/z3_interface.ML" |
216 |
ML_file "Tools/SMT/z3_replay_util.ML" |
|
217 |
ML_file "Tools/SMT/z3_replay_rules.ML" |
|
218 |
ML_file "Tools/SMT/z3_replay_methods.ML" |
|
219 |
ML_file "Tools/SMT/z3_replay.ML" |
|
220 |
ML_file "Tools/SMT/smt_systems.ML" |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
221 |
|
60758 | 222 |
method_setup smt = \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
223 |
Scan.optional Attrib.thms [] >> |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
224 |
(fn thms => fn ctxt => |
58061 | 225 |
METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts)))) |
60758 | 226 |
\<close> "apply an SMT solver to the current goal" |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
227 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
228 |
|
60758 | 229 |
subsection \<open>Configuration\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
230 |
|
60758 | 231 |
text \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
232 |
The current configuration can be printed by the command |
61799 | 233 |
\<open>smt_status\<close>, which shows the values of most options. |
60758 | 234 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
235 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
236 |
|
60758 | 237 |
subsection \<open>General configuration options\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
238 |
|
60758 | 239 |
text \<open> |
61799 | 240 |
The option \<open>smt_solver\<close> can be used to change the target SMT |
241 |
solver. The possible values can be obtained from the \<open>smt_status\<close> |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
242 |
command. |
60758 | 243 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
244 |
|
58061 | 245 |
declare [[smt_solver = z3]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
246 |
|
60758 | 247 |
text \<open> |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
248 |
Since SMT solvers are potentially nonterminating, there is a timeout |
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
249 |
(given in seconds) to restrict their runtime. |
60758 | 250 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
251 |
|
58061 | 252 |
declare [[smt_timeout = 20]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
253 |
|
60758 | 254 |
text \<open> |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
255 |
SMT solvers apply randomized heuristics. In case a problem is not |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
256 |
solvable by an SMT solver, changing the following option might help. |
60758 | 257 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
258 |
|
58061 | 259 |
declare [[smt_random_seed = 1]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
260 |
|
60758 | 261 |
text \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
262 |
In general, the binding to SMT solvers runs as an oracle, i.e, the SMT |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
263 |
solvers are fully trusted without additional checks. The following |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
264 |
option can cause the SMT solver to run in proof-producing mode, giving |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
265 |
a checkable certificate. This is currently only implemented for Z3. |
60758 | 266 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
267 |
|
58061 | 268 |
declare [[smt_oracle = false]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
269 |
|
60758 | 270 |
text \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
271 |
Each SMT solver provides several commandline options to tweak its |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
272 |
behaviour. They can be passed to the solver by setting the following |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
273 |
options. |
60758 | 274 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
275 |
|
58061 | 276 |
declare [[cvc3_options = ""]] |
66323
c41642bc1ebb
pass option recommended by Andy Reynolds to CVC4 1.5 (released) or better
blanchet
parents:
66298
diff
changeset
|
277 |
declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]] |
66559 | 278 |
declare [[verit_options = "--index-sorts --index-fresh-sorts"]] |
58061 | 279 |
declare [[z3_options = ""]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
280 |
|
60758 | 281 |
text \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
282 |
The SMT method provides an inference mechanism to detect simple triggers |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
283 |
in quantified formulas, which might increase the number of problems |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
284 |
solvable by SMT solvers (note: triggers guide quantifier instantiations |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
285 |
in the SMT solver). To turn it on, set the following option. |
60758 | 286 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
287 |
|
58061 | 288 |
declare [[smt_infer_triggers = false]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
289 |
|
60758 | 290 |
text \<open> |
58360 | 291 |
Enable the following option to use built-in support for datatypes, |
292 |
codatatypes, and records in CVC4. Currently, this is implemented only |
|
293 |
in oracle mode. |
|
60758 | 294 |
\<close> |
58360 | 295 |
|
296 |
declare [[cvc4_extensions = false]] |
|
297 |
||
60758 | 298 |
text \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
299 |
Enable the following option to use built-in support for div/mod, datatypes, |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
300 |
and records in Z3. Currently, this is implemented only in oracle mode. |
60758 | 301 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
302 |
|
58061 | 303 |
declare [[z3_extensions = false]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
304 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
305 |
|
60758 | 306 |
subsection \<open>Certificates\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
307 |
|
60758 | 308 |
text \<open> |
61799 | 309 |
By setting the option \<open>smt_certificates\<close> to the name of a file, |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
310 |
all following applications of an SMT solver a cached in that file. |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
311 |
Any further application of the same SMT solver (using the very same |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
312 |
configuration) re-uses the cached certificate instead of invoking the |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
313 |
solver. An empty string disables caching certificates. |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
314 |
|
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
315 |
The filename should be given as an explicit path. It is good |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
316 |
practice to use the name of the current theory (with ending |
61799 | 317 |
\<open>.certs\<close> instead of \<open>.thy\<close>) as the certificates file. |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
318 |
Certificate files should be used at most once in a certain theory context, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
319 |
to avoid race conditions with other concurrent accesses. |
60758 | 320 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
321 |
|
58061 | 322 |
declare [[smt_certificates = ""]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
323 |
|
60758 | 324 |
text \<open> |
61799 | 325 |
The option \<open>smt_read_only_certificates\<close> controls whether only |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
326 |
stored certificates are should be used or invocation of an SMT solver |
61799 | 327 |
is allowed. When set to \<open>true\<close>, no SMT solver will ever be |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
328 |
invoked and only the existing certificates found in the configured |
61799 | 329 |
cache are used; when set to \<open>false\<close> and there is no cached |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
330 |
certificate for some proposition, then the configured SMT solver is |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
331 |
invoked. |
60758 | 332 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
333 |
|
58061 | 334 |
declare [[smt_read_only_certificates = false]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
335 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
336 |
|
60758 | 337 |
subsection \<open>Tracing\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
338 |
|
60758 | 339 |
text \<open> |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
340 |
The SMT method, when applied, traces important information. To |
61799 | 341 |
make it entirely silent, set the following option to \<open>false\<close>. |
60758 | 342 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
343 |
|
58061 | 344 |
declare [[smt_verbose = true]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
345 |
|
60758 | 346 |
text \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
347 |
For tracing the generated problem file given to the SMT solver as |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
348 |
well as the returned result of the solver, the option |
61799 | 349 |
\<open>smt_trace\<close> should be set to \<open>true\<close>. |
60758 | 350 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
351 |
|
58061 | 352 |
declare [[smt_trace = false]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
353 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
354 |
|
60758 | 355 |
subsection \<open>Schematic rules for Z3 proof reconstruction\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
356 |
|
60758 | 357 |
text \<open> |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57246
diff
changeset
|
358 |
Several prof rules of Z3 are not very well documented. There are two |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
359 |
lemma groups which can turn failing Z3 proof reconstruction attempts |
61799 | 360 |
into succeeding ones: the facts in \<open>z3_rule\<close> are tried prior to |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
361 |
any implemented reconstruction procedure for all uncertain Z3 proof |
61799 | 362 |
rules; the facts in \<open>z3_simp\<close> are only fed to invocations of |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
363 |
the simplifier when reconstructing theory-specific proof steps. |
60758 | 364 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
365 |
|
58061 | 366 |
lemmas [z3_rule] = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
367 |
refl eq_commute conj_commute disj_commute simp_thms nnf_simps |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
368 |
ring_distribs field_simps times_divide_eq_right times_divide_eq_left |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
369 |
if_True if_False not_not |
58776
95e58e04e534
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
hoelzl
parents:
58598
diff
changeset
|
370 |
NO_MATCH_def |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
371 |
|
58061 | 372 |
lemma [z3_rule]: |
57169 | 373 |
"(P \<and> Q) = (\<not> (\<not> P \<or> \<not> Q))" |
374 |
"(P \<and> Q) = (\<not> (\<not> Q \<or> \<not> P))" |
|
375 |
"(\<not> P \<and> Q) = (\<not> (P \<or> \<not> Q))" |
|
376 |
"(\<not> P \<and> Q) = (\<not> (\<not> Q \<or> P))" |
|
377 |
"(P \<and> \<not> Q) = (\<not> (\<not> P \<or> Q))" |
|
378 |
"(P \<and> \<not> Q) = (\<not> (Q \<or> \<not> P))" |
|
379 |
"(\<not> P \<and> \<not> Q) = (\<not> (P \<or> Q))" |
|
380 |
"(\<not> P \<and> \<not> Q) = (\<not> (Q \<or> P))" |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
381 |
by auto |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
382 |
|
58061 | 383 |
lemma [z3_rule]: |
57169 | 384 |
"(P \<longrightarrow> Q) = (Q \<or> \<not> P)" |
385 |
"(\<not> P \<longrightarrow> Q) = (P \<or> Q)" |
|
386 |
"(\<not> P \<longrightarrow> Q) = (Q \<or> P)" |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
387 |
"(True \<longrightarrow> P) = P" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
388 |
"(P \<longrightarrow> True) = True" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
389 |
"(False \<longrightarrow> P) = True" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
390 |
"(P \<longrightarrow> P) = True" |
59037
650dcf624729
added Z3 reconstruction rule suggested by F. Maric
blanchet
parents:
59036
diff
changeset
|
391 |
"(\<not> (A \<longleftrightarrow> \<not> B)) \<longleftrightarrow> (A \<longleftrightarrow> B)" |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
392 |
by auto |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
393 |
|
58061 | 394 |
lemma [z3_rule]: |
67091 | 395 |
"((P = Q) \<longrightarrow> R) = (R \<or> (Q = (\<not> P)))" |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
396 |
by auto |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
397 |
|
58061 | 398 |
lemma [z3_rule]: |
57169 | 399 |
"(\<not> True) = False" |
400 |
"(\<not> False) = True" |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
401 |
"(x = x) = True" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
402 |
"(P = True) = P" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
403 |
"(True = P) = P" |
57169 | 404 |
"(P = False) = (\<not> P)" |
405 |
"(False = P) = (\<not> P)" |
|
406 |
"((\<not> P) = P) = False" |
|
407 |
"(P = (\<not> P)) = False" |
|
408 |
"((\<not> P) = (\<not> Q)) = (P = Q)" |
|
409 |
"\<not> (P = (\<not> Q)) = (P = Q)" |
|
410 |
"\<not> ((\<not> P) = Q) = (P = Q)" |
|
411 |
"(P \<noteq> Q) = (Q = (\<not> P))" |
|
412 |
"(P = Q) = ((\<not> P \<or> Q) \<and> (P \<or> \<not> Q))" |
|
413 |
"(P \<noteq> Q) = ((\<not> P \<or> \<not> Q) \<and> (P \<or> Q))" |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
414 |
by auto |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
415 |
|
58061 | 416 |
lemma [z3_rule]: |
57169 | 417 |
"(if P then P else \<not> P) = True" |
418 |
"(if \<not> P then \<not> P else P) = True" |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
419 |
"(if P then True else False) = P" |
57169 | 420 |
"(if P then False else True) = (\<not> P)" |
421 |
"(if P then Q else True) = ((\<not> P) \<or> Q)" |
|
422 |
"(if P then Q else True) = (Q \<or> (\<not> P))" |
|
423 |
"(if P then Q else \<not> Q) = (P = Q)" |
|
424 |
"(if P then Q else \<not> Q) = (Q = P)" |
|
425 |
"(if P then \<not> Q else Q) = (P = (\<not> Q))" |
|
426 |
"(if P then \<not> Q else Q) = ((\<not> Q) = P)" |
|
427 |
"(if \<not> P then x else y) = (if P then y else x)" |
|
428 |
"(if P then (if Q then x else y) else x) = (if P \<and> (\<not> Q) then y else x)" |
|
429 |
"(if P then (if Q then x else y) else x) = (if (\<not> Q) \<and> P then y else x)" |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
430 |
"(if P then (if Q then x else y) else y) = (if P \<and> Q then x else y)" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
431 |
"(if P then (if Q then x else y) else y) = (if Q \<and> P then x else y)" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
432 |
"(if P then x else if P then y else z) = (if P then x else z)" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
433 |
"(if P then x else if Q then x else y) = (if P \<or> Q then x else y)" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
434 |
"(if P then x else if Q then x else y) = (if Q \<or> P then x else y)" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
435 |
"(if P then x = y else x = z) = (x = (if P then y else z))" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
436 |
"(if P then x = y else y = z) = (y = (if P then x else z))" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
437 |
"(if P then x = y else z = y) = (y = (if P then x else z))" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
438 |
by auto |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
439 |
|
58061 | 440 |
lemma [z3_rule]: |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
441 |
"0 + (x::int) = x" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
442 |
"x + 0 = x" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
443 |
"x + x = 2 * x" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
444 |
"0 * x = 0" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
445 |
"1 * x = x" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
446 |
"x + y = y + x" |
57230 | 447 |
by (auto simp add: mult_2) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
448 |
|
58061 | 449 |
lemma [z3_rule]: (* for def-axiom *) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
450 |
"P = Q \<or> P \<or> Q" |
57169 | 451 |
"P = Q \<or> \<not> P \<or> \<not> Q" |
452 |
"(\<not> P) = Q \<or> \<not> P \<or> Q" |
|
453 |
"(\<not> P) = Q \<or> P \<or> \<not> Q" |
|
454 |
"P = (\<not> Q) \<or> \<not> P \<or> Q" |
|
455 |
"P = (\<not> Q) \<or> P \<or> \<not> Q" |
|
456 |
"P \<noteq> Q \<or> P \<or> \<not> Q" |
|
457 |
"P \<noteq> Q \<or> \<not> P \<or> Q" |
|
458 |
"P \<noteq> (\<not> Q) \<or> P \<or> Q" |
|
459 |
"(\<not> P) \<noteq> Q \<or> P \<or> Q" |
|
460 |
"P \<or> Q \<or> P \<noteq> (\<not> Q)" |
|
461 |
"P \<or> Q \<or> (\<not> P) \<noteq> Q" |
|
462 |
"P \<or> \<not> Q \<or> P \<noteq> Q" |
|
463 |
"\<not> P \<or> Q \<or> P \<noteq> Q" |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
464 |
"P \<or> y = (if P then x else y)" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
465 |
"P \<or> (if P then x else y) = y" |
57169 | 466 |
"\<not> P \<or> x = (if P then x else y)" |
467 |
"\<not> P \<or> (if P then x else y) = x" |
|
468 |
"P \<or> R \<or> \<not> (if P then Q else R)" |
|
469 |
"\<not> P \<or> Q \<or> \<not> (if P then Q else R)" |
|
470 |
"\<not> (if P then Q else R) \<or> \<not> P \<or> Q" |
|
471 |
"\<not> (if P then Q else R) \<or> P \<or> R" |
|
472 |
"(if P then Q else R) \<or> \<not> P \<or> \<not> Q" |
|
473 |
"(if P then Q else R) \<or> P \<or> \<not> R" |
|
474 |
"(if P then \<not> Q else R) \<or> \<not> P \<or> Q" |
|
475 |
"(if P then Q else \<not> R) \<or> P \<or> R" |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
476 |
by auto |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
477 |
|
57230 | 478 |
hide_type (open) symb_list pattern |
479 |
hide_const (open) Symb_Nil Symb_Cons trigger pat nopat fun_app z3div z3mod |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
480 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
481 |
end |