author | eberlm <eberlm@in.tum.de> |
Thu, 30 Nov 2017 16:59:59 +0100 | |
changeset 67107 | cef76a19125e |
parent 67091 | 1393c2340eec |
child 67399 | eab6ce8368fa |
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 |
|
66298 | 123 |
lemma nat_int': "\<forall>n. nat (int n) = n" by simp |
124 |
lemma int_nat_nneg: "\<forall>i. i \<ge> 0 \<longrightarrow> int (nat i) = i" by simp |
|
125 |
lemma int_nat_neg: "\<forall>i. i < 0 \<longrightarrow> int (nat i) = 0" by simp |
|
126 |
||
66817 | 127 |
lemma nat_zero_as_int: |
128 |
"0 = nat 0" |
|
129 |
by simp |
|
130 |
||
131 |
lemma nat_one_as_int: |
|
132 |
"1 = nat 1" |
|
133 |
by simp |
|
134 |
||
66298 | 135 |
lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp |
136 |
lemma nat_less_as_int: "op < = (\<lambda>a b. int a < int b)" by simp |
|
137 |
lemma nat_leq_as_int: "op \<le> = (\<lambda>a b. int a \<le> int b)" by simp |
|
138 |
lemma Suc_as_int: "Suc = (\<lambda>a. nat (int a + 1))" by (rule ext) simp |
|
139 |
lemma nat_plus_as_int: "op + = (\<lambda>a b. nat (int a + int b))" by (rule ext)+ simp |
|
140 |
lemma nat_minus_as_int: "op - = (\<lambda>a b. nat (int a - int b))" by (rule ext)+ simp |
|
141 |
lemma nat_times_as_int: "op * = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib) |
|
142 |
lemma nat_div_as_int: "op div = (\<lambda>a b. nat (int a div int b))" by (simp add: nat_div_distrib) |
|
143 |
lemma nat_mod_as_int: "op mod = (\<lambda>a b. nat (int a mod int b))" by (simp add: nat_mod_distrib) |
|
144 |
||
145 |
lemma int_Suc: "int (Suc n) = int n + 1" by simp |
|
146 |
lemma int_plus: "int (n + m) = int n + int m" by (rule of_nat_add) |
|
147 |
lemma int_minus: "int (n - m) = int (nat (int n - int m))" by auto |
|
148 |
||
56103
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset
|
149 |
|
60758 | 150 |
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
|
151 |
|
60758 | 152 |
text \<open> |
61799 | 153 |
The following Z3-inspired definitions are overspecified for the case where \<open>l = 0\<close>. This |
154 |
Schönheitsfehler is corrected in the \<open>div_as_z3div\<close> and \<open>mod_as_z3mod\<close> theorems. |
|
60758 | 155 |
\<close> |
56102 | 156 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
157 |
definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where |
56102 | 158 |
"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
|
159 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
160 |
definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where |
56102 | 161 |
"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
|
162 |
|
56101 | 163 |
lemma div_as_z3div: |
56102 | 164 |
"\<forall>k l. k div l = (if l = 0 then 0 else if l > 0 then z3div k l else z3div (- k) (- l))" |
56101 | 165 |
by (simp add: z3div_def) |
166 |
||
167 |
lemma mod_as_z3mod: |
|
56102 | 168 |
"\<forall>k l. k mod l = (if l = 0 then k else if l > 0 then z3mod k l else - z3mod (- k) (- l))" |
56101 | 169 |
by (simp add: z3mod_def) |
170 |
||
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
171 |
|
60758 | 172 |
subsection \<open>Setup\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
173 |
|
58061 | 174 |
ML_file "Tools/SMT/smt_util.ML" |
175 |
ML_file "Tools/SMT/smt_failure.ML" |
|
176 |
ML_file "Tools/SMT/smt_config.ML" |
|
177 |
ML_file "Tools/SMT/smt_builtin.ML" |
|
178 |
ML_file "Tools/SMT/smt_datatypes.ML" |
|
179 |
ML_file "Tools/SMT/smt_normalize.ML" |
|
180 |
ML_file "Tools/SMT/smt_translate.ML" |
|
181 |
ML_file "Tools/SMT/smtlib.ML" |
|
182 |
ML_file "Tools/SMT/smtlib_interface.ML" |
|
183 |
ML_file "Tools/SMT/smtlib_proof.ML" |
|
184 |
ML_file "Tools/SMT/smtlib_isar.ML" |
|
185 |
ML_file "Tools/SMT/z3_proof.ML" |
|
186 |
ML_file "Tools/SMT/z3_isar.ML" |
|
187 |
ML_file "Tools/SMT/smt_solver.ML" |
|
58360 | 188 |
ML_file "Tools/SMT/cvc4_interface.ML" |
59015 | 189 |
ML_file "Tools/SMT/cvc4_proof_parse.ML" |
58360 | 190 |
ML_file "Tools/SMT/verit_proof.ML" |
191 |
ML_file "Tools/SMT/verit_isar.ML" |
|
192 |
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
|
193 |
ML_file "Tools/SMT/conj_disj_perm.ML" |
58061 | 194 |
ML_file "Tools/SMT/z3_interface.ML" |
195 |
ML_file "Tools/SMT/z3_replay_util.ML" |
|
196 |
ML_file "Tools/SMT/z3_replay_rules.ML" |
|
197 |
ML_file "Tools/SMT/z3_replay_methods.ML" |
|
198 |
ML_file "Tools/SMT/z3_replay.ML" |
|
199 |
ML_file "Tools/SMT/smt_systems.ML" |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
200 |
|
60758 | 201 |
method_setup smt = \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
202 |
Scan.optional Attrib.thms [] >> |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
203 |
(fn thms => fn ctxt => |
58061 | 204 |
METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts)))) |
60758 | 205 |
\<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
|
206 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
207 |
|
60758 | 208 |
subsection \<open>Configuration\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
209 |
|
60758 | 210 |
text \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
211 |
The current configuration can be printed by the command |
61799 | 212 |
\<open>smt_status\<close>, which shows the values of most options. |
60758 | 213 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
214 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
215 |
|
60758 | 216 |
subsection \<open>General configuration options\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
217 |
|
60758 | 218 |
text \<open> |
61799 | 219 |
The option \<open>smt_solver\<close> can be used to change the target SMT |
220 |
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
|
221 |
command. |
60758 | 222 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
223 |
|
58061 | 224 |
declare [[smt_solver = z3]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
225 |
|
60758 | 226 |
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
|
227 |
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
|
228 |
(given in seconds) to restrict their runtime. |
60758 | 229 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
230 |
|
58061 | 231 |
declare [[smt_timeout = 20]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
232 |
|
60758 | 233 |
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
|
234 |
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
|
235 |
solvable by an SMT solver, changing the following option might help. |
60758 | 236 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
237 |
|
58061 | 238 |
declare [[smt_random_seed = 1]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
239 |
|
60758 | 240 |
text \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
241 |
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
|
242 |
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
|
243 |
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
|
244 |
a checkable certificate. This is currently only implemented for Z3. |
60758 | 245 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
246 |
|
58061 | 247 |
declare [[smt_oracle = false]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
248 |
|
60758 | 249 |
text \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
250 |
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
|
251 |
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
|
252 |
options. |
60758 | 253 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
254 |
|
58061 | 255 |
declare [[cvc3_options = ""]] |
66323
c41642bc1ebb
pass option recommended by Andy Reynolds to CVC4 1.5 (released) or better
blanchet
parents:
66298
diff
changeset
|
256 |
declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]] |
66559 | 257 |
declare [[verit_options = "--index-sorts --index-fresh-sorts"]] |
58061 | 258 |
declare [[z3_options = ""]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
259 |
|
60758 | 260 |
text \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
261 |
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
|
262 |
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
|
263 |
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
|
264 |
in the SMT solver). To turn it on, set the following option. |
60758 | 265 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
266 |
|
58061 | 267 |
declare [[smt_infer_triggers = false]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
268 |
|
60758 | 269 |
text \<open> |
58360 | 270 |
Enable the following option to use built-in support for datatypes, |
271 |
codatatypes, and records in CVC4. Currently, this is implemented only |
|
272 |
in oracle mode. |
|
60758 | 273 |
\<close> |
58360 | 274 |
|
275 |
declare [[cvc4_extensions = false]] |
|
276 |
||
60758 | 277 |
text \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
278 |
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
|
279 |
and records in Z3. Currently, this is implemented only in oracle mode. |
60758 | 280 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
281 |
|
58061 | 282 |
declare [[z3_extensions = false]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
283 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
284 |
|
60758 | 285 |
subsection \<open>Certificates\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
286 |
|
60758 | 287 |
text \<open> |
61799 | 288 |
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
|
289 |
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
|
290 |
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
|
291 |
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
|
292 |
solver. An empty string disables caching certificates. |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
293 |
|
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
|
294 |
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
|
295 |
practice to use the name of the current theory (with ending |
61799 | 296 |
\<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
|
297 |
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
|
298 |
to avoid race conditions with other concurrent accesses. |
60758 | 299 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
300 |
|
58061 | 301 |
declare [[smt_certificates = ""]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
302 |
|
60758 | 303 |
text \<open> |
61799 | 304 |
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
|
305 |
stored certificates are should be used or invocation of an SMT solver |
61799 | 306 |
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
|
307 |
invoked and only the existing certificates found in the configured |
61799 | 308 |
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
|
309 |
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
|
310 |
invoked. |
60758 | 311 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
312 |
|
58061 | 313 |
declare [[smt_read_only_certificates = false]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
314 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
315 |
|
60758 | 316 |
subsection \<open>Tracing\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
317 |
|
60758 | 318 |
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
|
319 |
The SMT method, when applied, traces important information. To |
61799 | 320 |
make it entirely silent, set the following option to \<open>false\<close>. |
60758 | 321 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
322 |
|
58061 | 323 |
declare [[smt_verbose = true]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
324 |
|
60758 | 325 |
text \<open> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
326 |
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
|
327 |
well as the returned result of the solver, the option |
61799 | 328 |
\<open>smt_trace\<close> should be set to \<open>true\<close>. |
60758 | 329 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
330 |
|
58061 | 331 |
declare [[smt_trace = false]] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
332 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
333 |
|
60758 | 334 |
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
|
335 |
|
60758 | 336 |
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
|
337 |
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
|
338 |
lemma groups which can turn failing Z3 proof reconstruction attempts |
61799 | 339 |
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
|
340 |
any implemented reconstruction procedure for all uncertain Z3 proof |
61799 | 341 |
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
|
342 |
the simplifier when reconstructing theory-specific proof steps. |
60758 | 343 |
\<close> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
344 |
|
58061 | 345 |
lemmas [z3_rule] = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
346 |
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
|
347 |
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
|
348 |
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
|
349 |
NO_MATCH_def |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
350 |
|
58061 | 351 |
lemma [z3_rule]: |
57169 | 352 |
"(P \<and> Q) = (\<not> (\<not> P \<or> \<not> Q))" |
353 |
"(P \<and> Q) = (\<not> (\<not> Q \<or> \<not> P))" |
|
354 |
"(\<not> P \<and> Q) = (\<not> (P \<or> \<not> Q))" |
|
355 |
"(\<not> P \<and> Q) = (\<not> (\<not> Q \<or> P))" |
|
356 |
"(P \<and> \<not> Q) = (\<not> (\<not> P \<or> Q))" |
|
357 |
"(P \<and> \<not> Q) = (\<not> (Q \<or> \<not> P))" |
|
358 |
"(\<not> P \<and> \<not> Q) = (\<not> (P \<or> Q))" |
|
359 |
"(\<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
|
360 |
by auto |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
361 |
|
58061 | 362 |
lemma [z3_rule]: |
57169 | 363 |
"(P \<longrightarrow> Q) = (Q \<or> \<not> P)" |
364 |
"(\<not> P \<longrightarrow> Q) = (P \<or> Q)" |
|
365 |
"(\<not> P \<longrightarrow> Q) = (Q \<or> P)" |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
366 |
"(True \<longrightarrow> P) = P" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
367 |
"(P \<longrightarrow> True) = True" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
368 |
"(False \<longrightarrow> P) = True" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
369 |
"(P \<longrightarrow> P) = True" |
59037
650dcf624729
added Z3 reconstruction rule suggested by F. Maric
blanchet
parents:
59036
diff
changeset
|
370 |
"(\<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
|
371 |
by auto |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
372 |
|
58061 | 373 |
lemma [z3_rule]: |
67091 | 374 |
"((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
|
375 |
by auto |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
376 |
|
58061 | 377 |
lemma [z3_rule]: |
57169 | 378 |
"(\<not> True) = False" |
379 |
"(\<not> False) = True" |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
380 |
"(x = x) = True" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
381 |
"(P = True) = P" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
382 |
"(True = P) = P" |
57169 | 383 |
"(P = False) = (\<not> P)" |
384 |
"(False = P) = (\<not> P)" |
|
385 |
"((\<not> P) = P) = False" |
|
386 |
"(P = (\<not> P)) = False" |
|
387 |
"((\<not> P) = (\<not> Q)) = (P = Q)" |
|
388 |
"\<not> (P = (\<not> Q)) = (P = Q)" |
|
389 |
"\<not> ((\<not> P) = Q) = (P = Q)" |
|
390 |
"(P \<noteq> Q) = (Q = (\<not> P))" |
|
391 |
"(P = Q) = ((\<not> P \<or> Q) \<and> (P \<or> \<not> Q))" |
|
392 |
"(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
|
393 |
by auto |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
394 |
|
58061 | 395 |
lemma [z3_rule]: |
57169 | 396 |
"(if P then P else \<not> P) = True" |
397 |
"(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
|
398 |
"(if P then True else False) = P" |
57169 | 399 |
"(if P then False else True) = (\<not> P)" |
400 |
"(if P then Q else True) = ((\<not> P) \<or> Q)" |
|
401 |
"(if P then Q else True) = (Q \<or> (\<not> P))" |
|
402 |
"(if P then Q else \<not> Q) = (P = Q)" |
|
403 |
"(if P then Q else \<not> Q) = (Q = P)" |
|
404 |
"(if P then \<not> Q else Q) = (P = (\<not> Q))" |
|
405 |
"(if P then \<not> Q else Q) = ((\<not> Q) = P)" |
|
406 |
"(if \<not> P then x else y) = (if P then y else x)" |
|
407 |
"(if P then (if Q then x else y) else x) = (if P \<and> (\<not> Q) then y else x)" |
|
408 |
"(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
|
409 |
"(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
|
410 |
"(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
|
411 |
"(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
|
412 |
"(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
|
413 |
"(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
|
414 |
"(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
|
415 |
"(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
|
416 |
"(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
|
417 |
by auto |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
418 |
|
58061 | 419 |
lemma [z3_rule]: |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
420 |
"0 + (x::int) = x" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
421 |
"x + 0 = x" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
422 |
"x + x = 2 * x" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
423 |
"0 * x = 0" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
424 |
"1 * x = x" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
425 |
"x + y = y + x" |
57230 | 426 |
by (auto simp add: mult_2) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
427 |
|
58061 | 428 |
lemma [z3_rule]: (* for def-axiom *) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
429 |
"P = Q \<or> P \<or> Q" |
57169 | 430 |
"P = Q \<or> \<not> P \<or> \<not> Q" |
431 |
"(\<not> P) = Q \<or> \<not> P \<or> Q" |
|
432 |
"(\<not> P) = Q \<or> P \<or> \<not> Q" |
|
433 |
"P = (\<not> Q) \<or> \<not> P \<or> Q" |
|
434 |
"P = (\<not> Q) \<or> P \<or> \<not> Q" |
|
435 |
"P \<noteq> Q \<or> P \<or> \<not> Q" |
|
436 |
"P \<noteq> Q \<or> \<not> P \<or> Q" |
|
437 |
"P \<noteq> (\<not> Q) \<or> P \<or> Q" |
|
438 |
"(\<not> P) \<noteq> Q \<or> P \<or> Q" |
|
439 |
"P \<or> Q \<or> P \<noteq> (\<not> Q)" |
|
440 |
"P \<or> Q \<or> (\<not> P) \<noteq> Q" |
|
441 |
"P \<or> \<not> Q \<or> P \<noteq> Q" |
|
442 |
"\<not> P \<or> Q \<or> P \<noteq> Q" |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
443 |
"P \<or> y = (if P then x else y)" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
444 |
"P \<or> (if P then x else y) = y" |
57169 | 445 |
"\<not> P \<or> x = (if P then x else y)" |
446 |
"\<not> P \<or> (if P then x else y) = x" |
|
447 |
"P \<or> R \<or> \<not> (if P then Q else R)" |
|
448 |
"\<not> P \<or> Q \<or> \<not> (if P then Q else R)" |
|
449 |
"\<not> (if P then Q else R) \<or> \<not> P \<or> Q" |
|
450 |
"\<not> (if P then Q else R) \<or> P \<or> R" |
|
451 |
"(if P then Q else R) \<or> \<not> P \<or> \<not> Q" |
|
452 |
"(if P then Q else R) \<or> P \<or> \<not> R" |
|
453 |
"(if P then \<not> Q else R) \<or> \<not> P \<or> Q" |
|
454 |
"(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
|
455 |
by auto |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
456 |
|
57230 | 457 |
hide_type (open) symb_list pattern |
458 |
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
|
459 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
460 |
end |