author  blanchet 
Sun, 27 Jul 2014 21:11:35 +0200  
changeset 57696  fb71c6f100f8 
parent 57246  62746a41cc0c 
child 57704  c0da3fc313e3 
permissions  rwrr 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

1 
(* Title: HOL/SMT2.thy 
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 

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

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

9 
keywords "smt2_status" :: diag 
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 

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

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

13 

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

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

15 
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

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

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

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

19 
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

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

21 
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

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

23 
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

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

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

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

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

28 

57230  29 
typedecl 'a symb_list 
30 

31 
consts 

32 
Symb_Nil :: "'a symb_list" 

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

34 

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

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

36 

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

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

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

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

40 

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

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

43 

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

44 

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

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

46 

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

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

48 
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

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

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

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

52 

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

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

54 

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

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

56 
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

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

58 
properties of such (extensional) arrays. 
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 

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

61 
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

62 

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

63 

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

64 
subsection {* Normalization *} 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

65 

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

66 
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

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

68 

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

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

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

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

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

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

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

75 

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

76 

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

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

78 

56102  79 
text {* 
80 
The following Z3inspired definitions are overspecified for the case where @{text "l = 0"}. This 

81 
SchĂ¶nheitsfehler is corrected in the @{text div_as_z3div} and @{text mod_as_z3mod} theorems. 

82 
*} 

83 

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

84 
definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where 
56102  85 
"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

86 

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

87 
definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where 
56102  88 
"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

89 

56101  90 
lemma div_as_z3div: 
56102  91 
"\<forall>k l. k div l = (if l = 0 then 0 else if l > 0 then z3div k l else z3div ( k) ( l))" 
56101  92 
by (simp add: z3div_def) 
93 

94 
lemma mod_as_z3mod: 

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

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

100 

57230  101 
ML_file "Tools/SMT2/smt2_util.ML" 
102 
ML_file "Tools/SMT2/smt2_failure.ML" 

103 
ML_file "Tools/SMT2/smt2_config.ML" 

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

104 
ML_file "Tools/SMT2/smt2_builtin.ML" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

105 
ML_file "Tools/SMT2/smt2_datatypes.ML" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

106 
ML_file "Tools/SMT2/smt2_normalize.ML" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

107 
ML_file "Tools/SMT2/smt2_translate.ML" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

108 
ML_file "Tools/SMT2/smtlib2.ML" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

109 
ML_file "Tools/SMT2/smtlib2_interface.ML" 
57219
34018603e0d0
factor out SMTLIB 2 type/term parsing from Z3specific code
blanchet
parents:
57209
diff
changeset

110 
ML_file "Tools/SMT2/smtlib2_proof.ML" 
56083
b5d1d9c60341
have Sledgehammer generate Isar proofs from Z3 proofs
blanchet
parents:
56078
diff
changeset

111 
ML_file "Tools/SMT2/z3_new_proof.ML" 
57159  112 
ML_file "Tools/SMT2/z3_new_isar.ML" 
56083
b5d1d9c60341
have Sledgehammer generate Isar proofs from Z3 proofs
blanchet
parents:
56078
diff
changeset

113 
ML_file "Tools/SMT2/smt2_solver.ML" 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

114 
ML_file "Tools/SMT2/z3_new_interface.ML" 
56090  115 
ML_file "Tools/SMT2/z3_new_replay_util.ML" 
116 
ML_file "Tools/SMT2/z3_new_replay_literals.ML" 

117 
ML_file "Tools/SMT2/z3_new_replay_rules.ML" 

118 
ML_file "Tools/SMT2/z3_new_replay_methods.ML" 

119 
ML_file "Tools/SMT2/z3_new_replay.ML" 

120 
ML_file "Tools/SMT2/smt2_systems.ML" 

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

121 

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

122 
method_setup smt2 = {* 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

124 
(fn thms => fn ctxt => 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

125 
METHOD (fn facts => HEADGOAL (SMT2_Solver.smt2_tac ctxt (thms @ facts)))) 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

126 
*} "apply an SMT solver to the current goal (based on SMTLIB 2)" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

127 

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

128 

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

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

130 

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

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

132 
The current configuration can be printed by the command 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

133 
@{text smt2_status}, which shows the values of most options. 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

135 

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

136 

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

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

138 

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

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

140 
The option @{text smt2_solver} can be used to change the target 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

141 
solver. The possible values can be obtained from the @{text smt2_status} 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

143 

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

144 
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

145 
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

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

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

148 

57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57169
diff
changeset

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

150 

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

151 
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

152 
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

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

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

155 

57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57169
diff
changeset

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

157 

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

158 
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

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

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

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

162 

57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57169
diff
changeset

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

164 

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

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

166 
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

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

168 
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

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

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

171 

57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57169
diff
changeset

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

173 

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

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

175 
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

176 
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

177 
options. 
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 

57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57169
diff
changeset

180 
declare [[cvc3_new_options = ""]] 
57246  181 
declare [[cvc4_new_options = ""]] 
57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57169
diff
changeset

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

183 

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

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

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

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

187 
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

188 
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

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

190 

57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57169
diff
changeset

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

192 

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

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

194 
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

195 
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

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

197 

57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57169
diff
changeset

198 
declare [[z3_new_extensions = false]] 
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 

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

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

204 
By setting the option @{text smt2_certificates} to the name of a file, 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

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

207 
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

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

209 

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

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

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

213 
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

214 
to avoid race conditions with other concurrent accesses. 
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 

57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57169
diff
changeset

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

218 

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

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

220 
The option @{text smt2_read_only_certificates} controls whether only 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

221 
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

222 
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

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

224 
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

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

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

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

228 

57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57169
diff
changeset

229 
declare [[smt2_read_only_certificates = false]] 
56078
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 

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

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

233 

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

234 
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

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

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

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

238 

57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57169
diff
changeset

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

240 

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

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

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

243 
well as the returned result of the solver, the option 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

244 
@{text smt2_trace} should be set to @{text true}. 
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 

57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57169
diff
changeset

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

248 

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

249 

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

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

251 

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

252 
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

253 
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

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

255 
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

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

257 
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

258 
the simplifier when reconstructing theoryspecific proof steps. 
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 
lemmas [z3_new_rule] = 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

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

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

265 

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

266 
lemma [z3_new_rule]: 
57169  267 
"(P \<and> Q) = (\<not> (\<not> P \<or> \<not> Q))" 
268 
"(P \<and> Q) = (\<not> (\<not> Q \<or> \<not> P))" 

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

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

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

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

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

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

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

275 
by auto 
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 
lemma [z3_new_rule]: 
57169  278 
"(P \<longrightarrow> Q) = (Q \<or> \<not> P)" 
279 
"(\<not> P \<longrightarrow> Q) = (P \<or> Q)" 

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

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

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

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

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

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

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

286 

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

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

289 
by auto 
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 
lemma [z3_new_rule]: 
57169  292 
"(\<not> True) = False" 
293 
"(\<not> False) = True" 

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

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

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

296 
"(True = P) = P" 
57169  297 
"(P = False) = (\<not> P)" 
298 
"(False = P) = (\<not> P)" 

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

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

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

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

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

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

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

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

307 
by auto 
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 
lemma [z3_new_rule]: 
57169  310 
"(if P then P else \<not> P) = True" 
311 
"(if \<not> P then \<not> P else P) = True" 

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

312 
"(if P then True else False) = P" 
57169  313 
"(if P then False else True) = (\<not> P)" 
314 
"(if P then Q else True) = ((\<not> P) \<or> Q)" 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

332 

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

333 
lemma [z3_new_rule]: 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

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

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

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

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

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

341 

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

342 
lemma [z3_new_rule]: (* for defaxiom *) 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

343 
"P = Q \<or> P \<or> Q" 
57169  344 
"P = Q \<or> \<not> P \<or> \<not> Q" 
345 
"(\<not> P) = Q \<or> \<not> P \<or> Q" 

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

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

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

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

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

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

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

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

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

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

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

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

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

358 
"P \<or> (if P then x else y) = y" 
57169  359 
"\<not> P \<or> x = (if P then x else y)" 
360 
"\<not> P \<or> (if P then x else y) = x" 

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

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

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

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

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

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

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

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

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 

57230  371 
hide_type (open) symb_list pattern 
372 
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

373 

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

374 
end 