author  blanchet 
Tue, 03 Jun 2014 16:02:42 +0200  
changeset 57169  6abda9b6b9c1 
parent 57165  7b1bf424ec5f 
child 57209  7ffa0f7e2775 
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 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

8 
imports Record 
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 

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

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

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

15 

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

16 

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

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

18 

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

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

20 
Some SMT solvers support patterns as a quantifier instantiation 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

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

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

24 
quantifier accordingly  or negative terms (tagged by "nopat") 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

26 
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

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

28 
A list of multipatterns is called a trigger, and their multipatterns 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

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

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

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

33 

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

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

35 

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

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

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

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

39 

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

40 
definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" where "trigger _ P = P" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

41 

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

42 

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

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

46 
Application is made explicit for constants occurring with varying 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

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

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

50 

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

51 
definition fun_app :: "'a \<Rightarrow> 'a" where "fun_app f = f" 
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 
text {* 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

54 
Some solvers support a theory of arrays which can be used to encode 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

56 
properties of such (extensional) arrays. 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

58 

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

59 
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

60 

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

61 

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

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

63 

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

64 
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

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

66 

56107  67 
lemma nat_int': "\<forall>n. nat (int n) = n" by simp 
56103
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

68 
lemma int_nat_nneg: "\<forall>i. i \<ge> 0 \<longrightarrow> int (nat i) = i" by simp 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

69 
lemma int_nat_neg: "\<forall>i. i < 0 \<longrightarrow> int (nat i) = 0" by simp 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

70 

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

71 
lemma nat_zero_as_int: "0 = nat 0" by (rule transfer_nat_int_numerals(1)) 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

72 
lemma nat_one_as_int: "1 = nat 1" by (rule transfer_nat_int_numerals(2)) 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

73 
lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

74 
lemma nat_less_as_int: "op < = (\<lambda>a b. int a < int b)" by simp 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

75 
lemma nat_leq_as_int: "op \<le> = (\<lambda>a b. int a <= int b)" by simp 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

76 
lemma Suc_as_int: "Suc = (\<lambda>a. nat (int a + 1))" by (rule ext) simp 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

77 
lemma nat_plus_as_int: "op + = (\<lambda>a b. nat (int a + int b))" by (rule ext)+ simp 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

78 
lemma nat_minus_as_int: "op  = (\<lambda>a b. nat (int a  int b))" by (rule ext)+ simp 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

79 
lemma nat_times_as_int: "op * = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib) 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

80 
lemma nat_div_as_int: "op div = (\<lambda>a b. nat (int a div int b))" by (simp add: nat_div_distrib) 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

81 
lemma nat_mod_as_int: "op mod = (\<lambda>a b. nat (int a mod int b))" by (simp add: nat_mod_distrib) 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

82 

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

83 
lemma int_Suc: "int (Suc n) = int n + 1" by simp 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

84 
lemma int_plus: "int (n + m) = int n + int m" by (rule of_nat_add) 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

85 
lemma int_minus: "int (n  m) = int (nat (int n  int m))" by auto 
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56102
diff
changeset

86 

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

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

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

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

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

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

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

93 

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

94 

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

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

96 

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

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

100 
*} 

101 

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

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

104 

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

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

107 

56101  108 
lemma div_as_z3div: 
56102  109 
"\<forall>k l. k div l = (if l = 0 then 0 else if l > 0 then z3div k l else z3div ( k) ( l))" 
56101  110 
by (simp add: z3div_def) 
111 

112 
lemma mod_as_z3mod: 

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

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

116 

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

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

118 

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

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

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

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

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

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

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

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

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

128 
ML_file "Tools/SMT2/z3_new_interface.ML" 
56090  129 
ML_file "Tools/SMT2/z3_new_replay_util.ML" 
130 
ML_file "Tools/SMT2/z3_new_replay_literals.ML" 

131 
ML_file "Tools/SMT2/z3_new_replay_rules.ML" 

132 
ML_file "Tools/SMT2/z3_new_replay_methods.ML" 

133 
ML_file "Tools/SMT2/z3_new_replay.ML" 

134 
ML_file "Tools/SMT2/smt2_systems.ML" 

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

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

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

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

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

141 

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

142 

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

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

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

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

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

149 

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 

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

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

153 

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

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

155 
The option @{text smt2_solver} can be used to change the target SMT 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

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

158 

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

159 
Due to licensing restrictions, Yices and Z3 are not installed/enabled 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

160 
by default. Z3 is free for noncommercial applications and can be enabled 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

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

163 

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

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

165 

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

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

167 
Since SMT solvers are potentially nonterminating, there is a timeout 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

168 
(given in seconds) to restrict their runtime. A value greater than 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

169 
120 (seconds) is in most cases not advisable. 
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 

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

172 
declare [[ smt2_timeout = 20 ]] 
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 
SMT solvers apply randomized heuristics. In case a problem is not 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

177 
*} 
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 
declare [[ smt2_random_seed = 1 ]] 
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 
text {* 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

182 
In general, the binding to SMT solvers runs as an oracle, i.e, the SMT 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

184 
option can cause the SMT solver to run in proofproducing mode, giving 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

185 
a checkable certificate. This is currently only implemented for Z3. 
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 
declare [[ smt2_oracle = false ]] 
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 {* 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

191 
Each SMT solver provides several commandline options to tweak its 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

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

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

195 

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

196 
(* declare [[ cvc3_options = "" ]] TODO *) 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

197 
(* declare [[ yices_options = "" ]] TODO *) 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

198 
(* declare [[ z3_options = "" ]] TODO *) 
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 
text {* 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

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

203 
solvable by SMT solvers (note: triggers guide quantifier instantiations 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

204 
in the SMT solver). To turn it on, set the following option. 
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 

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

207 
declare [[ smt2_infer_triggers = false ]] 
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 {* 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

210 
Enable the following option to use builtin support for div/mod, datatypes, 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

211 
and records in Z3. Currently, this is implemented only in oracle mode. 
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 

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

214 
declare [[ z3_new_extensions = false ]] 
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 
The SMT method monomorphizes the given facts, that is, it tries to 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

218 
instantiate all schematic type variables with fixed types occurring 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

219 
in the problem. This is a (possibly nonterminating) fixedpoint 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

220 
construction whose cycles are limited by the following option. 
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 

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

223 
declare [[ monomorph_max_rounds = 5 ]] 
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 
In addition, the number of generated monomorphic instances is limited 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

227 
by the following option. 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

228 
*} 
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 
declare [[ monomorph_max_new_instances = 500 ]] 
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 

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

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

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

240 
configuration) reuses the cached certificate instead of invoking the 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

241 
solver. An empty string disables caching certificates. 
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 
The filename should be given as an explicit path. It is good 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

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

246 
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

247 
to avoid race conditions with other concurrent accesses. 
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 
declare [[ smt2_certificates = "" ]] 
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 {* 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

254 
stored certificates are should be used or invocation of an SMT solver 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

255 
is allowed. When set to @{text true}, no SMT solver will ever be 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

257 
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

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

259 
invoked. 
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 
declare [[ smt2_read_only_certificates = false ]] 
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 

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

267 

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

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

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

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

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

272 

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

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

274 

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

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

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

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

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

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

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

282 

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

283 

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

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

285 

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

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

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

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

289 
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

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

291 
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

292 
the simplifier when reconstructing theoryspecific proof steps. 
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 

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

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

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

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

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

299 

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

300 
lemma [z3_new_rule]: 
57169  301 
"(P \<and> Q) = (\<not> (\<not> P \<or> \<not> Q))" 
302 
"(P \<and> Q) = (\<not> (\<not> Q \<or> \<not> P))" 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

319 
by auto 
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 
lemma [z3_new_rule]: 
57169  322 
"((P = Q) \<longrightarrow> R) = (R  (Q = (\<not> P)))" 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

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

324 

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

325 
lemma [z3_new_rule]: 
57169  326 
"(\<not> True) = False" 
327 
"(\<not> False) = True" 

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

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

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

330 
"(True = P) = P" 
57169  331 
"(P = False) = (\<not> P)" 
332 
"(False = P) = (\<not> P)" 

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

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

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

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

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

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

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

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

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

342 

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

343 
lemma [z3_new_rule]: 
57169  344 
"(if P then P else \<not> P) = True" 
345 
"(if \<not> P then \<not> P else P) = True" 

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

346 
"(if P then True else False) = P" 
57169  347 
"(if P then False else True) = (\<not> P)" 
348 
"(if P then Q else True) = ((\<not> P) \<or> Q)" 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

366 

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

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

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

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

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

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

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

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

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

375 

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

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

377 
"P = Q \<or> P \<or> Q" 
57169  378 
"P = Q \<or> \<not> P \<or> \<not> Q" 
379 
"(\<not> P) = Q \<or> \<not> P \<or> Q" 

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

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

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

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

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

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

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

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

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

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

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

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

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

392 
"P \<or> (if P then x else y) = y" 
57169  393 
"\<not> P \<or> x = (if P then x else y)" 
394 
"\<not> P \<or> (if P then x else y) = x" 

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

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

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

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

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

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

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

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

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

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

404 

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

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

406 
hide_const fun_app z3div z3mod 
57165
7b1bf424ec5f
removed SMT weights  their impact was very inconclusive anyway
blanchet
parents:
57159
diff
changeset

407 
hide_const (open) trigger pat nopat 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
diff
changeset

408 

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

409 
end 