author  blanchet 
Mon, 06 Oct 2014 19:19:16 +0200  
changeset 58598  d9892c88cb56 
parent 58481  62bc7c79212b 
child 58776  95e58e04e534 
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 

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

5 
header {* Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMTLIB 2 *} 
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" 
162 
ML_file "Tools/SMT/verit_proof.ML" 

163 
ML_file "Tools/SMT/verit_isar.ML" 

164 
ML_file "Tools/SMT/verit_proof_parse.ML" 

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

167 
ML_file "Tools/SMT/z3_replay_literals.ML" 

168 
ML_file "Tools/SMT/z3_replay_rules.ML" 

169 
ML_file "Tools/SMT/z3_replay_methods.ML" 

170 
ML_file "Tools/SMT/z3_replay.ML" 

171 
ML_file "Tools/SMT/smt_systems.ML" 

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

172 

58061  173 
method_setup smt = {* 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

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

178 

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

181 

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

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

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

185 
*} 
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 
subsection {* General configuration options *} 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

189 

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

190 
text {* 
58061  191 
The option @{text smt_solver} can be used to change the target SMT 
192 
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

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

194 

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

195 
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

196 
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

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

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

199 

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

201 

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

202 
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

203 
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

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

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

206 

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

208 

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

209 
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

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

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

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

213 

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

215 

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

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

217 
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

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

219 
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

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

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

222 

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

224 

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

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

226 
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

227 
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

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

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

230 

58061  231 
declare [[cvc3_options = ""]] 
58441  232 
declare [[cvc4_options = "fullsaturatequant quantcf"]] 
58061  233 
declare [[veriT_options = ""]] 
234 
declare [[z3_options = ""]] 

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

235 

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

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

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

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

239 
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

240 
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

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

242 

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

244 

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

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

248 
in oracle mode. 

249 
*} 

250 

251 
declare [[cvc4_extensions = false]] 

252 

253 
text {* 

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

254 
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

255 
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

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

257 

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

259 

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

262 

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

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

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

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

267 
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

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

269 

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

270 
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

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

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

273 
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

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

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

276 

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

278 

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

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

281 
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

282 
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

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

284 
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

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

286 
invoked. 
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 

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

290 

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

293 

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

294 
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

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

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

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

298 

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

300 

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

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

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

303 
well as the returned result of the solver, the option 
58061  304 
@{text smt_trace} should be set to @{text true}. 
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 

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

308 

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 
subsection {* Schematic rules for Z3 proof reconstruction *} 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

311 

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

312 
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

313 
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

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

315 
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

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

317 
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

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

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

320 

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

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

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

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

325 

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

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

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

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

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

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

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

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

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

336 

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

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

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

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

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

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

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

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

346 

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

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

350 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

368 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

392 

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

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

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

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

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

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

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

401 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

430 

57230  431 
hide_type (open) symb_list pattern 
432 
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

433 

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

434 
end 