author  blanchet 
Thu, 20 Nov 2014 17:29:18 +0100  
changeset 59022  fa7c419f04b4 
parent 59017  80290f06a810 
child 59035  3a2153676705 
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 

58889  5 
section {* Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMTLIB 2 *} 
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 

58481  12 
subsection {* A skolemization tactic and proof method *} 
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 

42 
ML {* 

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)) 

58481  49 
*} 
50 

51 
method_setup moura = {* 

52 
Scan.succeed (SIMPLE_METHOD' o moura_tac) 

53 
*} "solve skolemization goals, especially those arising from Z3 proofs" 

54 

55 
hide_fact (open) choices bchoices 

56 

57 

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

58 
subsection {* Triggers for quantifier instantiation *} 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

59 

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

60 
text {* 
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. 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

73 
*} 
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 

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

91 
subsection {* Higherorder encoding *} 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

92 

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

93 
text {* 
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. 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

97 
*} 
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 

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

101 
text {* 
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. 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

105 
*} 
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 

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

110 
subsection {* Normalization *} 
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 

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

123 
subsection {* Integer division and modulo for Z3 *} 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

124 

56102  125 
text {* 
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. 

128 
*} 

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 

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

145 
subsection {* Setup *} 
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" 

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

168 
ML_file "Tools/SMT/z3_replay_literals.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 

58061  174 
method_setup smt = {* 
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)))) 
58072  178 
*} "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 

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

181 
subsection {* Configuration *} 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

182 

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

183 
text {* 
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. 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

186 
*} 
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 

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

189 
subsection {* General configuration options *} 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

190 

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

191 
text {* 
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. 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

195 

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

196 
Due to licensing restrictions, Z3 is not enabled by default. Z3 is free 
57237
bc51864c2ac4
took out broken support for Yices from SMT2 stack  see 'NEWS' for rationale
blanchet
parents:
57230
diff
changeset

197 
for noncommercial applications and can be enabled by setting Isabelle 
bc51864c2ac4
took out broken support for Yices from SMT2 stack  see 'NEWS' for rationale
blanchet
parents:
57230
diff
changeset

198 
system option @{text z3_non_commercial} to @{text yes}. 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

200 

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

202 

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

203 
text {* 
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

204 
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

205 
(given in seconds) to restrict their runtime. 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

207 

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

209 

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

210 
text {* 
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

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

212 
solvable by an SMT solver, changing the following option might help. 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

214 

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

216 

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

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

218 
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

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

220 
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

221 
a checkable certificate. This is currently only implemented for Z3. 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

223 

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

225 

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

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

227 
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

228 
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

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

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

231 

58061  232 
declare [[cvc3_options = ""]] 
59022  233 
declare [[cvc4_options = "fullsaturatequant instwhen=fulllastcall"]] 
58061  234 
declare [[veriT_options = ""]] 
235 
declare [[z3_options = ""]] 

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

236 

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

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

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

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

240 
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

241 
in the SMT solver). To turn it on, set the following option. 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

243 

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

245 

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

246 
text {* 
58360  247 
Enable the following option to use builtin support for datatypes, 
248 
codatatypes, and records in CVC4. Currently, this is implemented only 

249 
in oracle mode. 

250 
*} 

251 

252 
declare [[cvc4_extensions = false]] 

253 

254 
text {* 

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

255 
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

256 
and records in Z3. Currently, this is implemented only in oracle mode. 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

258 

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

260 

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

261 

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

262 
subsection {* Certificates *} 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

263 

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

264 
text {* 
58061  265 
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

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

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

268 
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

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

270 

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

271 
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

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

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

274 
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

275 
to avoid race conditions with other concurrent accesses. 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

277 

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

279 

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

280 
text {* 
58061  281 
The option @{text smt_read_only_certificates} controls whether only 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

282 
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

283 
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

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

285 
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

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

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

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

289 

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

291 

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

292 

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

293 
subsection {* Tracing *} 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

294 

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

295 
text {* 
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

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

297 
make it entirely silent, set the following option to @{text false}. 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

299 

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

301 

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

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

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

304 
well as the returned result of the solver, the option 
58061  305 
@{text smt_trace} should be set to @{text true}. 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

307 

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

309 

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

310 

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

311 
subsection {* Schematic rules for Z3 proof reconstruction *} 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

312 

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

313 
text {* 
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

314 
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

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

316 
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

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

318 
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

319 
the simplifier when reconstructing theoryspecific proof steps. 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

321 

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

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

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

325 
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

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

327 

58061  328 
lemma [z3_rule]: 
57169  329 
"(P \<and> Q) = (\<not> (\<not> P \<or> \<not> Q))" 
330 
"(P \<and> Q) = (\<not> (\<not> Q \<or> \<not> P))" 

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

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

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

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

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

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

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

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

338 

58061  339 
lemma [z3_rule]: 
57169  340 
"(P \<longrightarrow> Q) = (Q \<or> \<not> P)" 
341 
"(\<not> P \<longrightarrow> Q) = (P \<or> Q)" 

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

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

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

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

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

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

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

348 

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

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

352 

58061  353 
lemma [z3_rule]: 
57169  354 
"(\<not> True) = False" 
355 
"(\<not> False) = True" 

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

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

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

358 
"(True = P) = P" 
57169  359 
"(P = False) = (\<not> P)" 
360 
"(False = P) = (\<not> P)" 

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

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

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

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

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

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

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

368 
"(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

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

370 

58061  371 
lemma [z3_rule]: 
57169  372 
"(if P then P else \<not> P) = True" 
373 
"(if \<not> P then \<not> P else P) = True" 

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

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

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

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

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

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

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

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

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

384 
"(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

385 
"(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

386 
"(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

387 
"(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

388 
"(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

389 
"(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

390 
"(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

391 
"(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

392 
"(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

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

394 

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

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

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

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

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

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

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

403 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

420 
"P \<or> (if P then x else y) = y" 
57169  421 
"\<not> P \<or> x = (if P then x else y)" 
422 
"\<not> P \<or> (if P then x else y) = x" 

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

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

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

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

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

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

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

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

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

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

432 

57230  433 
hide_type (open) symb_list pattern 
434 
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

435 

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

436 
end 