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