author  wenzelm 
Sat, 18 Jul 2015 22:58:50 +0200  
changeset 60758  d8d85a8172b5 
parent 60201  90e88e521e0e 
child 61611  a9c0572109af 
permissions  rwrr 
58061  1 
(* Title: HOL/SMT.thy 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

2 
Author: Sascha Boehme, TU Muenchen 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

3 
*) 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

4 

60758  5 
section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMTLIB 2\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

6 

58061  7 
theory SMT 
57230  8 
imports Divides 
58061  9 
keywords "smt_status" :: diag 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

10 
begin 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

11 

60758  12 
subsection \<open>A skolemization tactic and proof method\<close> 
58481  13 

14 
lemma choices: 

15 
"\<And>Q. \<forall>x. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x. Q x (f x) (fa x)" 

16 
"\<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)" 

17 
"\<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  18 
"\<And>Q. \<forall>x. \<exists>y ya yb yc yd. Q x y ya yb yc yd \<Longrightarrow> 
19 
\<exists>f fa fb fc fd. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x)" 

20 
"\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye. Q x y ya yb yc yd ye \<Longrightarrow> 

21 
\<exists>f fa fb fc fd fe. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" 

22 
"\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \<Longrightarrow> 

23 
\<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)" 

24 
"\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \<Longrightarrow> 

25 
\<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  26 
by metis+ 
27 

28 
lemma bchoices: 

29 
"\<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)" 

30 
"\<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)" 

31 
"\<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  32 
"\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd. Q x y ya yb yc yd \<Longrightarrow> 
33 
\<exists>f fa fb fc fd. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x)" 

34 
"\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye. Q x y ya yb yc yd ye \<Longrightarrow> 

35 
\<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)" 

36 
"\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \<Longrightarrow> 

37 
\<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)" 

38 
"\<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> 

39 
\<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  40 
by metis+ 
41 

60758  42 
ML \<open> 
58481  43 
fun moura_tac ctxt = 
44 
Atomize_Elim.atomize_elim_tac ctxt THEN' 

45 
SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice choices bchoice bchoices}) THEN 

58598  46 
ALLGOALS (Metis_Tactic.metis_tac (take 1 ATP_Proof_Reconstruct.partial_type_encs) 
47 
ATP_Proof_Reconstruct.default_metis_lam_trans ctxt [] ORELSE' 

48 
blast_tac ctxt)) 

60758  49 
\<close> 
58481  50 

60758  51 
method_setup moura = \<open> 
60201  52 
Scan.succeed (SIMPLE_METHOD' o moura_tac) 
60758  53 
\<close> "solve skolemization goals, especially those arising from Z3 proofs" 
58481  54 

55 
hide_fact (open) choices bchoices 

56 

57 

60758  58 
subsection \<open>Triggers for quantifier instantiation\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

59 

60758  60 
text \<open> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

61 
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

62 
heuristics. Patterns may either be positive terms (tagged by "pat") 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

63 
triggering quantifier instantiations  when the solver finds a 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

64 
term matching a positive pattern, it instantiates the corresponding 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

65 
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

66 
inhibiting quantifier instantiations. A list of patterns 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

67 
of the same kind is called a multipattern, and all patterns in a 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

68 
multipattern are considered conjunctively for quantifier instantiation. 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

69 
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

70 
act disjunctively during quantifier instantiation. Each multipattern 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

71 
should mention at least all quantified variables of the preceding 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

72 
quantifier block. 
60758  73 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

74 

57230  75 
typedecl 'a symb_list 
76 

77 
consts 

78 
Symb_Nil :: "'a symb_list" 

79 
Symb_Cons :: "'a \<Rightarrow> 'a symb_list \<Rightarrow> 'a symb_list" 

80 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

81 
typedecl pattern 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

82 

624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

83 
consts 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

84 
pat :: "'a \<Rightarrow> pattern" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

85 
nopat :: "'a \<Rightarrow> pattern" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

86 

57230  87 
definition trigger :: "pattern symb_list symb_list \<Rightarrow> bool \<Rightarrow> bool" where 
88 
"trigger _ P = P" 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

89 

624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

90 

60758  91 
subsection \<open>Higherorder encoding\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

92 

60758  93 
text \<open> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

94 
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

95 
numbers of arguments. This is achieved by the introduction of the 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

96 
following constant. 
60758  97 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

98 

624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

99 
definition fun_app :: "'a \<Rightarrow> 'a" where "fun_app f = f" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

100 

60758  101 
text \<open> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

102 
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

103 
higherorder functions. The following set of lemmas specifies the 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

104 
properties of such (extensional) arrays. 
60758  105 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

106 

624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

107 
lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other fun_upd_upd fun_app_def 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

108 

624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

109 

60758  110 
subsection \<open>Normalization\<close> 
56103
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

111 

6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

112 
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

113 
by simp 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

114 

6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

115 
lemmas Ex1_def_raw = Ex1_def[abs_def] 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

116 
lemmas Ball_def_raw = Ball_def[abs_def] 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

117 
lemmas Bex_def_raw = Bex_def[abs_def] 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

118 
lemmas abs_if_raw = abs_if[abs_def] 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

119 
lemmas min_def_raw = min_def[abs_def] 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

120 
lemmas max_def_raw = max_def[abs_def] 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

121 

6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

122 

60758  123 
subsection \<open>Integer division and modulo for Z3\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

124 

60758  125 
text \<open> 
56102  126 
The following Z3inspired definitions are overspecified for the case where @{text "l = 0"}. This 
127 
SchÃ¶nheitsfehler is corrected in the @{text div_as_z3div} and @{text mod_as_z3mod} theorems. 

60758  128 
\<close> 
56102  129 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

130 
definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where 
56102  131 
"z3div k l = (if l \<ge> 0 then k div l else  (k div  l))" 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

132 

624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

133 
definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where 
56102  134 
"z3mod k l = k mod (if l \<ge> 0 then l else  l)" 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

135 

56101  136 
lemma div_as_z3div: 
56102  137 
"\<forall>k l. k div l = (if l = 0 then 0 else if l > 0 then z3div k l else z3div ( k) ( l))" 
56101  138 
by (simp add: z3div_def) 
139 

140 
lemma mod_as_z3mod: 

56102  141 
"\<forall>k l. k mod l = (if l = 0 then k else if l > 0 then z3mod k l else  z3mod ( k) ( l))" 
56101  142 
by (simp add: z3mod_def) 
143 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

144 

60758  145 
subsection \<open>Setup\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

146 

58061  147 
ML_file "Tools/SMT/smt_util.ML" 
148 
ML_file "Tools/SMT/smt_failure.ML" 

149 
ML_file "Tools/SMT/smt_config.ML" 

150 
ML_file "Tools/SMT/smt_builtin.ML" 

151 
ML_file "Tools/SMT/smt_datatypes.ML" 

152 
ML_file "Tools/SMT/smt_normalize.ML" 

153 
ML_file "Tools/SMT/smt_translate.ML" 

154 
ML_file "Tools/SMT/smtlib.ML" 

155 
ML_file "Tools/SMT/smtlib_interface.ML" 

156 
ML_file "Tools/SMT/smtlib_proof.ML" 

157 
ML_file "Tools/SMT/smtlib_isar.ML" 

158 
ML_file "Tools/SMT/z3_proof.ML" 

159 
ML_file "Tools/SMT/z3_isar.ML" 

160 
ML_file "Tools/SMT/smt_solver.ML" 

58360  161 
ML_file "Tools/SMT/cvc4_interface.ML" 
59015  162 
ML_file "Tools/SMT/cvc4_proof_parse.ML" 
58360  163 
ML_file "Tools/SMT/verit_proof.ML" 
164 
ML_file "Tools/SMT/verit_isar.ML" 

165 
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

166 
ML_file "Tools/SMT/conj_disj_perm.ML" 
58061  167 
ML_file "Tools/SMT/z3_interface.ML" 
168 
ML_file "Tools/SMT/z3_replay_util.ML" 

169 
ML_file "Tools/SMT/z3_replay_rules.ML" 

170 
ML_file "Tools/SMT/z3_replay_methods.ML" 

171 
ML_file "Tools/SMT/z3_replay.ML" 

172 
ML_file "Tools/SMT/smt_systems.ML" 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

173 

60758  174 
method_setup smt = \<open> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

175 
Scan.optional Attrib.thms [] >> 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

176 
(fn thms => fn ctxt => 
58061  177 
METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts)))) 
60758  178 
\<close> "apply an SMT solver to the current goal" 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

179 

624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

180 

60758  181 
subsection \<open>Configuration\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

182 

60758  183 
text \<open> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

184 
The current configuration can be printed by the command 
58061  185 
@{text smt_status}, which shows the values of most options. 
60758  186 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

187 

624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

188 

60758  189 
subsection \<open>General configuration options\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

190 

60758  191 
text \<open> 
58061  192 
The option @{text smt_solver} can be used to change the target SMT 
193 
solver. The possible values can be obtained from the @{text smt_status} 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

194 
command. 
60758  195 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

196 

58061  197 
declare [[smt_solver = z3]] 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

198 

60758  199 
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

200 
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

201 
(given in seconds) to restrict their runtime. 
60758  202 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

203 

58061  204 
declare [[smt_timeout = 20]] 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

205 

60758  206 
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

207 
SMT solvers apply randomized heuristics. In case a problem is not 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

208 
solvable by an SMT solver, changing the following option might help. 
60758  209 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

210 

58061  211 
declare [[smt_random_seed = 1]] 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

212 

60758  213 
text \<open> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

214 
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

215 
solvers are fully trusted without additional checks. The following 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

216 
option can cause the SMT solver to run in proofproducing 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

217 
a checkable certificate. This is currently only implemented for Z3. 
60758  218 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

219 

58061  220 
declare [[smt_oracle = false]] 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

221 

60758  222 
text \<open> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

223 
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

224 
behaviour. They can be passed to the solver by setting the following 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

225 
options. 
60758  226 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

227 

58061  228 
declare [[cvc3_options = ""]] 
59045
1da9b8045026
added one more CVC4 option that helps Judgment Day (10 theory version)
blanchet
parents:
59037
diff
changeset

229 
declare [[cvc4_options = "fullsaturatequant instwhen=fulllastcall instnoentail termdbmode=relevant"]] 
59035
3a2153676705
renamed 'veriT' to 'verit', to stick to alllowercase rule for prover names
blanchet
parents:
59022
diff
changeset

230 
declare [[verit_options = ""]] 
58061  231 
declare [[z3_options = ""]] 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

232 

60758  233 
text \<open> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

234 
The SMT method provides an inference mechanism to detect simple triggers 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

235 
in quantified formulas, which might increase the number of problems 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

236 
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

237 
in the SMT solver). To turn it on, set the following option. 
60758  238 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

239 

58061  240 
declare [[smt_infer_triggers = false]] 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

241 

60758  242 
text \<open> 
58360  243 
Enable the following option to use builtin support for datatypes, 
244 
codatatypes, and records in CVC4. Currently, this is implemented only 

245 
in oracle mode. 

60758  246 
\<close> 
58360  247 

248 
declare [[cvc4_extensions = false]] 

249 

60758  250 
text \<open> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

251 
Enable the following option to use builtin 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

252 
and records in Z3. Currently, this is implemented only in oracle mode. 
60758  253 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

254 

58061  255 
declare [[z3_extensions = false]] 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

256 

624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

257 

60758  258 
subsection \<open>Certificates\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

259 

60758  260 
text \<open> 
58061  261 
By setting the option @{text smt_certificates} to the name of a file, 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

262 
all following applications of an SMT solver a cached in that file. 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

263 
Any further application of the same SMT solver (using the very same 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

264 
configuration) reuses 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

265 
solver. An empty string disables caching certificates. 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

266 

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

267 
The filename should be given as an explicit path. It is good 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

268 
practice to use the name of the current theory (with ending 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

269 
@{text ".certs"} instead of @{text ".thy"}) as the certificates file. 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

270 
Certificate files should be used at most once in a certain theory context, 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

271 
to avoid race conditions with other concurrent accesses. 
60758  272 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

273 

58061  274 
declare [[smt_certificates = ""]] 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

275 

60758  276 
text \<open> 
58061  277 
The option @{text smt_read_only_certificates} controls whether only 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

278 
stored certificates are should be used or invocation of an SMT solver 
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 
is allowed. When set to @{text true}, no SMT solver will ever be 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

280 
invoked and only the existing certificates found in the configured 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

281 
cache are used; when set to @{text false} and there is no cached 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

282 
certificate for some proposition, then the configured SMT solver is 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

283 
invoked. 
60758  284 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

285 

58061  286 
declare [[smt_read_only_certificates = false]] 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

287 

624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

288 

60758  289 
subsection \<open>Tracing\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

290 

60758  291 
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

292 
The SMT method, when applied, traces important information. To 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

293 
make it entirely silent, set the following option to @{text false}. 
60758  294 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

295 

58061  296 
declare [[smt_verbose = true]] 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

297 

60758  298 
text \<open> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

299 
For tracing the generated problem file given to the SMT solver as 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

300 
well as the returned result of the solver, the option 
58061  301 
@{text smt_trace} should be set to @{text true}. 
60758  302 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

303 

58061  304 
declare [[smt_trace = false]] 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

305 

624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

306 

60758  307 
subsection \<open>Schematic rules for Z3 proof reconstruction\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

308 

60758  309 
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

310 
Several prof rules of Z3 are not very well documented. There are two 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

311 
lemma groups which can turn failing Z3 proof reconstruction attempts 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

312 
into succeeding ones: the facts in @{text z3_rule} are tried prior to 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

313 
any implemented reconstruction procedure for all uncertain Z3 proof 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

314 
rules; the facts in @{text z3_simp} are only fed to invocations of 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

315 
the simplifier when reconstructing theoryspecific proof steps. 
60758  316 
\<close> 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

317 

58061  318 
lemmas [z3_rule] = 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

319 
refl eq_commute conj_commute disj_commute simp_thms nnf_simps 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

320 
ring_distribs field_simps times_divide_eq_right times_divide_eq_left 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

321 
if_True if_False not_not 
58776
95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58598
diff
changeset

322 
NO_MATCH_def 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

323 

58061  324 
lemma [z3_rule]: 
57169  325 
"(P \<and> Q) = (\<not> (\<not> P \<or> \<not> Q))" 
326 
"(P \<and> Q) = (\<not> (\<not> Q \<or> \<not> P))" 

327 
"(\<not> P \<and> Q) = (\<not> (P \<or> \<not> Q))" 

328 
"(\<not> P \<and> Q) = (\<not> (\<not> Q \<or> P))" 

329 
"(P \<and> \<not> Q) = (\<not> (\<not> P \<or> Q))" 

330 
"(P \<and> \<not> Q) = (\<not> (Q \<or> \<not> P))" 

331 
"(\<not> P \<and> \<not> Q) = (\<not> (P \<or> Q))" 

332 
"(\<not> P \<and> \<not> Q) = (\<not> (Q \<or> P))" 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

333 
by auto 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

334 

58061  335 
lemma [z3_rule]: 
57169  336 
"(P \<longrightarrow> Q) = (Q \<or> \<not> P)" 
337 
"(\<not> P \<longrightarrow> Q) = (P \<or> Q)" 

338 
"(\<not> P \<longrightarrow> Q) = (Q \<or> P)" 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

339 
"(True \<longrightarrow> P) = P" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

340 
"(P \<longrightarrow> True) = True" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

341 
"(False \<longrightarrow> P) = True" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

342 
"(P \<longrightarrow> P) = True" 
59037
650dcf624729
added Z3 reconstruction rule suggested by F. Maric
blanchet
parents:
59036
diff
changeset

343 
"(\<not> (A \<longleftrightarrow> \<not> B)) \<longleftrightarrow> (A \<longleftrightarrow> B)" 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

344 
by auto 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

345 

58061  346 
lemma [z3_rule]: 
57169  347 
"((P = Q) \<longrightarrow> R) = (R  (Q = (\<not> P)))" 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

348 
by auto 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

349 

58061  350 
lemma [z3_rule]: 
57169  351 
"(\<not> True) = False" 
352 
"(\<not> False) = True" 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

353 
"(x = x) = True" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

354 
"(P = True) = P" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

355 
"(True = P) = P" 
57169  356 
"(P = False) = (\<not> P)" 
357 
"(False = P) = (\<not> P)" 

358 
"((\<not> P) = P) = False" 

359 
"(P = (\<not> P)) = False" 

360 
"((\<not> P) = (\<not> Q)) = (P = Q)" 

361 
"\<not> (P = (\<not> Q)) = (P = Q)" 

362 
"\<not> ((\<not> P) = Q) = (P = Q)" 

363 
"(P \<noteq> Q) = (Q = (\<not> P))" 

364 
"(P = Q) = ((\<not> P \<or> Q) \<and> (P \<or> \<not> Q))" 

365 
"(P \<noteq> Q) = ((\<not> P \<or> \<not> Q) \<and> (P \<or> Q))" 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

366 
by auto 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

367 

58061  368 
lemma [z3_rule]: 
57169  369 
"(if P then P else \<not> P) = True" 
370 
"(if \<not> P then \<not> P else P) = True" 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

371 
"(if P then True else False) = P" 
57169  372 
"(if P then False else True) = (\<not> P)" 
373 
"(if P then Q else True) = ((\<not> P) \<or> Q)" 

374 
"(if P then Q else True) = (Q \<or> (\<not> P))" 

375 
"(if P then Q else \<not> Q) = (P = Q)" 

376 
"(if P then Q else \<not> Q) = (Q = P)" 

377 
"(if P then \<not> Q else Q) = (P = (\<not> Q))" 

378 
"(if P then \<not> Q else Q) = ((\<not> Q) = P)" 

379 
"(if \<not> P then x else y) = (if P then y else x)" 

380 
"(if P then (if Q then x else y) else x) = (if P \<and> (\<not> Q) then y else x)" 

381 
"(if P then (if Q then x else y) else x) = (if (\<not> Q) \<and> P then y else x)" 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

382 
"(if P then (if Q then x else y) else y) = (if P \<and> Q then x else y)" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

383 
"(if P then (if Q then x else y) else y) = (if Q \<and> P then x else y)" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

384 
"(if P then x else if P then y else z) = (if P then x else z)" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

385 
"(if P then x else if Q then x else y) = (if P \<or> Q then x else y)" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

386 
"(if P then x else if Q then x else y) = (if Q \<or> P then x else y)" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

387 
"(if P then x = y else x = z) = (x = (if P then y else z))" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

388 
"(if P then x = y else y = z) = (y = (if P then x else z))" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

389 
"(if P then x = y else z = y) = (y = (if P then x else z))" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

390 
by auto 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

391 

58061  392 
lemma [z3_rule]: 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

393 
"0 + (x::int) = x" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

394 
"x + 0 = x" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

395 
"x + x = 2 * x" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

396 
"0 * x = 0" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

397 
"1 * x = x" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

398 
"x + y = y + x" 
57230  399 
by (auto simp add: mult_2) 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

400 

58061  401 
lemma [z3_rule]: (* for defaxiom *) 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

402 
"P = Q \<or> P \<or> Q" 
57169  403 
"P = Q \<or> \<not> P \<or> \<not> Q" 
404 
"(\<not> P) = Q \<or> \<not> P \<or> Q" 

405 
"(\<not> P) = Q \<or> P \<or> \<not> Q" 

406 
"P = (\<not> Q) \<or> \<not> P \<or> Q" 

407 
"P = (\<not> Q) \<or> P \<or> \<not> Q" 

408 
"P \<noteq> Q \<or> P \<or> \<not> Q" 

409 
"P \<noteq> Q \<or> \<not> P \<or> Q" 

410 
"P \<noteq> (\<not> Q) \<or> P \<or> Q" 

411 
"(\<not> P) \<noteq> Q \<or> P \<or> Q" 

412 
"P \<or> Q \<or> P \<noteq> (\<not> Q)" 

413 
"P \<or> Q \<or> (\<not> P) \<noteq> Q" 

414 
"P \<or> \<not> Q \<or> P \<noteq> Q" 

415 
"\<not> P \<or> Q \<or> P \<noteq> Q" 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

416 
"P \<or> y = (if P then x else y)" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

417 
"P \<or> (if P then x else y) = y" 
57169  418 
"\<not> P \<or> x = (if P then x else y)" 
419 
"\<not> P \<or> (if P then x else y) = x" 

420 
"P \<or> R \<or> \<not> (if P then Q else R)" 

421 
"\<not> P \<or> Q \<or> \<not> (if P then Q else R)" 

422 
"\<not> (if P then Q else R) \<or> \<not> P \<or> Q" 

423 
"\<not> (if P then Q else R) \<or> P \<or> R" 

424 
"(if P then Q else R) \<or> \<not> P \<or> \<not> Q" 

425 
"(if P then Q else R) \<or> P \<or> \<not> R" 

426 
"(if P then \<not> Q else R) \<or> \<not> P \<or> Q" 

427 
"(if P then Q else \<not> R) \<or> P \<or> R" 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

428 
by auto 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

429 

57230  430 
hide_type (open) symb_list pattern 
431 
hide_const (open) Symb_Nil Symb_Cons trigger pat nopat fun_app z3div z3mod 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

432 

624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

433 
end 