author  boehmes 
Wed, 15 Dec 2010 10:12:48 +0100  
changeset 41130  130771a48c70 
parent 41127  2ea84c8535c6 
child 41131  fc9d503c3d67 
permissions  rwrr 
36898  1 
(* Title: HOL/Tools/SMT/z3_proof_reconstruction.ML 
2 
Author: Sascha Boehme, TU Muenchen 

3 

4 
Proof reconstruction for proofs found by Z3. 

5 
*) 

6 

7 
signature Z3_PROOF_RECONSTRUCTION = 

8 
sig 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

9 
val add_z3_rule: thm > Context.generic > Context.generic 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

10 
val reconstruct: Proof.context > SMT_Translate.recon > string list > 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

11 
int list * thm 
36898  12 
val setup: theory > theory 
13 
end 

14 

15 
structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION = 

16 
struct 

17 

18 
structure P = Z3_Proof_Parser 

19 
structure T = Z3_Proof_Tools 

20 
structure L = Z3_Proof_Literals 

40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset

21 
structure M = Z3_Proof_Methods 
36898  22 

40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40274
diff
changeset

23 
fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

24 
("Z3 proof reconstruction: " ^ msg)) 
36898  25 

26 

27 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

28 
(* net of schematic rules *) 
36898  29 

30 
val z3_ruleN = "z3_rule" 

31 

32 
local 

33 
val description = "declaration of Z3 proof rules" 

34 

35 
val eq = Thm.eq_thm 

36 

37 
structure Z3_Rules = Generic_Data 

38 
( 

39 
type T = thm Net.net 

40 
val empty = Net.empty 

41 
val extend = I 

42 
val merge = Net.merge eq 

43 
) 

44 

45 
val prep = `Thm.prop_of o Simplifier.rewrite_rule [L.rewrite_true] 

46 

47 
fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net 

48 
fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net 

49 

50 
val add = Thm.declaration_attribute (Z3_Rules.map o ins) 

51 
val del = Thm.declaration_attribute (Z3_Rules.map o del) 

52 
in 

53 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

54 
val add_z3_rule = Z3_Rules.map o ins 
36898  55 

56 
fun by_schematic_rule ctxt ct = 

57 
the (T.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct) 

58 

59 
val z3_rules_setup = 

60 
Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #> 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39020
diff
changeset

61 
Global_Theory.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get) 
36898  62 

63 
end 

64 

65 

66 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

67 
(* proof tools *) 
36898  68 

69 
fun named ctxt name prover ct = 

40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40274
diff
changeset

70 
let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...") 
36898  71 
in prover ct end 
72 

73 
fun NAMED ctxt name tac i st = 

40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40274
diff
changeset

74 
let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...") 
36898  75 
in tac i st end 
76 

77 
fun pretty_goal ctxt thms t = 

78 
[Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]] 

79 
> not (null thms) ? cons (Pretty.big_list "assumptions:" 

80 
(map (Display.pretty_thm ctxt) thms)) 

81 

82 
fun try_apply ctxt thms = 

83 
let 

84 
fun try_apply_err ct = Pretty.string_of (Pretty.chunks [ 

85 
Pretty.big_list ("Z3 found a proof," ^ 

86 
" but proof reconstruction failed at the following subgoal:") 

87 
(pretty_goal ctxt thms (Thm.term_of ct)), 

88 
Pretty.str ("Adding a rule to the lemma group " ^ quote z3_ruleN ^ 

89 
" might solve this problem.")]) 

90 

91 
fun apply [] ct = error (try_apply_err ct) 

92 
 apply (prover :: provers) ct = 

93 
(case try prover ct of 

40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40274
diff
changeset

94 
SOME thm => (SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm) 
36898  95 
 NONE => apply provers ct) 
96 

97 
in apply o cons (named ctxt "schematic rules" (by_schematic_rule ctxt)) end 

98 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

99 
local 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

100 
val rewr_if = 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

101 
@{lemma "(if P then Q1 else Q2) = ((P > Q1) & (~P > Q2))" by simp} 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

102 
in 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

103 
val simp_fast_tac = 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

104 
Simplifier.simp_tac (HOL_ss addsimps [rewr_if]) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

105 
THEN_ALL_NEW Classical.fast_tac HOL_cs 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

106 
end 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

107 

36898  108 

109 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

110 
(* theorems and proofs *) 
36898  111 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

112 
(** theorem incarnations **) 
36898  113 

114 
datatype theorem = 

115 
Thm of thm  (* theorem without special features *) 

116 
MetaEq of thm  (* meta equality "t == s" *) 

117 
Literals of thm * L.littab 

118 
(* "P1 & ... & Pn" and table of all literals P1, ..., Pn *) 

119 

120 
fun thm_of (Thm thm) = thm 

121 
 thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq} 

122 
 thm_of (Literals (thm, _)) = thm 

123 

124 
fun meta_eq_of (MetaEq thm) = thm 

125 
 meta_eq_of p = mk_meta_eq (thm_of p) 

126 

127 
fun literals_of (Literals (_, lits)) = lits 

128 
 literals_of p = L.make_littab [thm_of p] 

129 

130 

131 

132 
(** core proof rules **) 

133 

134 
(* assumption *) 

135 
local 

136 
val remove_trigger = @{lemma "trigger t p == p" 

137 
by (rule eq_reflection, rule trigger_def)} 

138 

40664  139 
val remove_weight = @{lemma "weight w p == p" 
140 
by (rule eq_reflection, rule weight_def)} 

141 

142 
val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight, 

143 
L.rewrite_true] 

36898  144 

145 
fun rewrite_conv ctxt eqs = Simplifier.full_rewrite 

146 
(Simplifier.context ctxt Simplifier.empty_ss addsimps eqs) 

147 

40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

148 
fun rewrites f ctxt eqs = map (f (Conv.fconv_rule (rewrite_conv ctxt eqs))) 
36898  149 

40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

150 
fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm) 
36898  151 
fun lookup_assm ctxt assms ct = 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

152 
(case T.net_instance' burrow_snd_option assms ct of 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

153 
SOME ithm => ithm 
36898  154 
 _ => z3_exn ("not asserted: " ^ 
155 
quote (Syntax.string_of_term ctxt (Thm.term_of ct)))) 

156 
in 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

157 
fun prepare_assms ctxt rewrite_rules assms = 
36898  158 
let 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

159 
val eqs = rewrites I ctxt [L.rewrite_true] rewrite_rules 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

160 
val assms' = 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

161 
assms 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

162 
> rewrites apsnd ctxt (union Thm.eq_thm eqs prep_rules) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

163 
> map (apsnd (Conv.fconv_rule Thm.eta_conversion)) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

164 
in (eqs, T.thm_net_of snd assms') end 
36898  165 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

166 
fun asserted ctxt (eqs, assms) ct = 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

167 
let val revert_conv = rewrite_conv ctxt eqs then_conv Thm.eta_conversion 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

168 
in Thm (T.with_conv revert_conv (snd o lookup_assm ctxt assms) ct) end 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

169 

57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

170 
fun find_assm ctxt (unfolds, assms) ct = 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

171 
fst (lookup_assm ctxt assms (Thm.rhs_of (rewrite_conv ctxt unfolds ct))) 
36898  172 
end 
173 

174 

175 
(* P = Q ==> P ==> Q or P > Q ==> P ==> Q *) 

176 
local 

177 
val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp} 

178 
val meta_iffD1_c = T.precompose2 Thm.dest_binop meta_iffD1 

179 

180 
val iffD1_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm iffD1} 

181 
val mp_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm mp} 

182 
in 

183 
fun mp (MetaEq thm) p = Thm (Thm.implies_elim (T.compose meta_iffD1_c thm) p) 

184 
 mp p_q p = 

185 
let 

186 
val pq = thm_of p_q 

187 
val thm = T.compose iffD1_c pq handle THM _ => T.compose mp_c pq 

188 
in Thm (Thm.implies_elim thm p) end 

189 
end 

190 

191 

192 
(* and_elim: P1 & ... & Pn ==> Pi *) 

193 
(* not_or_elim: ~(P1  ...  Pn) ==> ~Pi *) 

194 
local 

195 
fun is_sublit conj t = L.exists_lit conj (fn u => u aconv t) 

196 

197 
fun derive conj t lits idx ptab = 

198 
let 

199 
val lit = the (L.get_first_lit (is_sublit conj t) lits) 

200 
val ls = L.explode conj false false [t] lit 

201 
val lits' = fold L.insert_lit ls (L.delete_lit lit lits) 

202 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

203 
fun upd thm = Literals (thm_of thm, lits') 
36898  204 
in (the (L.lookup_lit lits' t), Inttab.map_entry idx upd ptab) end 
205 

206 
fun lit_elim conj (p, idx) ct ptab = 

207 
let val lits = literals_of p 

208 
in 

209 
(case L.lookup_lit lits (T.term_of ct) of 

210 
SOME lit => (Thm lit, ptab) 

211 
 NONE => apfst Thm (derive conj (T.term_of ct) lits idx ptab)) 

212 
end 

213 
in 

214 
val and_elim = lit_elim true 

215 
val not_or_elim = lit_elim false 

216 
end 

217 

218 

219 
(* P1, ..., Pn  False ==>  ~P1  ...  ~Pn *) 

220 
local 

221 
fun step lit thm = 

222 
Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit 

223 
val explode_disj = L.explode false false false 

224 
fun intro hyps thm th = fold step (explode_disj hyps th) thm 

225 

226 
fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))] 

227 
val ccontr = T.precompose dest_ccontr @{thm ccontr} 

228 
in 

229 
fun lemma thm ct = 

230 
let 

40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

231 
val cu = L.negate (Thm.dest_arg ct) 
36898  232 
val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm)) 
233 
in Thm (T.compose ccontr (T.under_assumption (intro hyps thm) cu)) end 

234 
end 

235 

236 

237 
(* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *) 

238 
local 

239 
val explode_disj = L.explode false true false 

240 
val join_disj = L.join false 

241 
fun unit thm thms th = 

40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

242 
let val t = @{const Not} $ T.prop_of thm and ts = map T.prop_of thms 
36898  243 
in join_disj (L.make_littab (thms @ explode_disj ts th)) t end 
244 

245 
fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct) 

246 
fun dest ct = pairself dest_arg2 (Thm.dest_binop ct) 

247 
val contrapos = T.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast} 

248 
in 

249 
fun unit_resolution thm thms ct = 

40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

250 
L.negate (Thm.dest_arg ct) 
36898  251 
> T.under_assumption (unit thm thms) 
252 
> Thm o T.discharge thm o T.compose contrapos 

253 
end 

254 

255 

256 
(* P ==> P == True or P ==> P == False *) 

257 
local 

258 
val iff1 = @{lemma "P ==> P == (~ False)" by simp} 

259 
val iff2 = @{lemma "~P ==> P == False" by simp} 

260 
in 

261 
fun iff_true thm = MetaEq (thm COMP iff1) 

262 
fun iff_false thm = MetaEq (thm COMP iff2) 

263 
end 

264 

265 

266 
(* distributivity of  over & *) 

267 
fun distributivity ctxt = Thm o try_apply ctxt [] [ 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

268 
named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))] 
36898  269 
(* FIXME: not very well tested *) 
270 

271 

272 
(* Tseitinlike axioms *) 

273 
local 

274 
val disjI1 = @{lemma "(P ==> Q) ==> ~P  Q" by fast} 

275 
val disjI2 = @{lemma "(~P ==> Q) ==> P  Q" by fast} 

276 
val disjI3 = @{lemma "(~Q ==> P) ==> P  Q" by fast} 

277 
val disjI4 = @{lemma "(Q ==> P) ==> P  ~Q" by fast} 

278 

279 
fun prove' conj1 conj2 ct2 thm = 

280 
let val lits = L.true_thm :: L.explode conj1 true (conj1 <> conj2) [] thm 

281 
in L.join conj2 (L.make_littab lits) (Thm.term_of ct2) end 

282 

283 
fun prove rule (ct1, conj1) (ct2, conj2) = 

284 
T.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule 

285 

286 
fun prove_def_axiom ct = 

287 
let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct) 

288 
in 

289 
(case Thm.term_of ct1 of 

40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

290 
@{const Not} $ (@{const HOL.conj} $ _ $ _) => 
36898  291 
prove disjI1 (Thm.dest_arg ct1, true) (ct2, true) 
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

292 
 @{const HOL.conj} $ _ $ _ => 
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

293 
prove disjI3 (L.negate ct2, false) (ct1, true) 
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

294 
 @{const Not} $ (@{const HOL.disj} $ _ $ _) => 
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

295 
prove disjI3 (L.negate ct2, false) (ct1, false) 
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

296 
 @{const HOL.disj} $ _ $ _ => 
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

297 
prove disjI2 (L.negate ct1, false) (ct2, true) 
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as builtin
boehmes
parents:
40680
diff
changeset

298 
 Const (@{const_name distinct}, _) $ _ => 
36898  299 
let 
300 
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv) 

301 
fun prv cu = 

302 
let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) 

303 
in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end 

304 
in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end 

40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as builtin
boehmes
parents:
40680
diff
changeset

305 
 @{const Not} $ (Const (@{const_name distinct}, _) $ _) => 
36898  306 
let 
307 
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv)) 

308 
fun prv cu = 

309 
let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) 

310 
in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end 

311 
in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end 

312 
 _ => raise CTERM ("prove_def_axiom", [ct])) 

313 
end 

314 
in 

315 
fun def_axiom ctxt = Thm o try_apply ctxt [] [ 

316 
named ctxt "conj/disj/distinct" prove_def_axiom, 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

317 
T.by_abstraction (true, false) ctxt [] (fn ctxt' => 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

318 
named ctxt' "simp+fast" (T.by_tac simp_fast_tac))] 
36898  319 
end 
320 

321 

322 
(* local definitions *) 

323 
local 

324 
val intro_rules = [ 

325 
@{lemma "n == P ==> (~n  P) & (n  ~P)" by simp}, 

326 
@{lemma "n == (if P then s else t) ==> (~P  n = s) & (P  n = t)" 

327 
by simp}, 

328 
@{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ] 

329 

330 
val apply_rules = [ 

331 
@{lemma "(~n  P) & (n  ~P) ==> P == n" by (atomize(full)) fast}, 

332 
@{lemma "(~P  n = s) & (P  n = t) ==> (if P then s else t) == n" 

333 
by (atomize(full)) fastsimp} ] 

334 

335 
val inst_rule = T.match_instantiate Thm.dest_arg 

336 

337 
fun apply_rule ct = 

338 
(case get_first (try (inst_rule ct)) intro_rules of 

339 
SOME thm => thm 

340 
 NONE => raise CTERM ("intro_def", [ct])) 

341 
in 

342 
fun intro_def ct = T.make_hyp_def (apply_rule ct) #>> Thm 

343 

344 
fun apply_def thm = 

345 
get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules 

346 
> the_default (Thm thm) 

347 
end 

348 

349 

350 
(* negation normal form *) 

351 
local 

352 
val quant_rules1 = ([ 

353 
@{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp}, 

354 
@{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [ 

355 
@{lemma "(!!x. P x == Q x) ==> ALL x. P x == ALL x. Q x" by simp}, 

356 
@{lemma "(!!x. P x == Q x) ==> EX x. P x == EX x. Q x" by simp}]) 

357 

358 
val quant_rules2 = ([ 

359 
@{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp}, 

360 
@{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [ 

361 
@{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp}, 

362 
@{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}]) 

363 

364 
fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = ( 

365 
Tactic.rtac thm ORELSE' 

366 
(Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE' 

367 
(Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st 

368 

369 
fun nnf_quant vars qs p ct = 

370 
T.as_meta_eq ct 

371 
> T.by_tac (nnf_quant_tac (T.varify vars (meta_eq_of p)) qs) 

372 

373 
fun prove_nnf ctxt = try_apply ctxt [] [ 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

374 
named ctxt "conj/disj" L.prove_conj_disj_eq, 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

375 
T.by_abstraction (true, false) ctxt [] (fn ctxt' => 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

376 
named ctxt' "simp+fast" (T.by_tac simp_fast_tac))] 
36898  377 
in 
378 
fun nnf ctxt vars ps ct = 

379 
(case T.term_of ct of 

380 
_ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) => 

381 
if l aconv r 

382 
then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) 

383 
else MetaEq (nnf_quant vars quant_rules1 (hd ps) ct) 

40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

384 
 _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) => 
36898  385 
MetaEq (nnf_quant vars quant_rules2 (hd ps) ct) 
386 
 _ => 

387 
let 

388 
val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv 

389 
(T.unfold_eqs ctxt (map (Thm.symmetric o meta_eq_of) ps))) 

390 
in Thm (T.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end) 

391 
end 

392 

393 

394 

395 
(** equality proof rules **) 

396 

397 
(*  t = t *) 

398 
fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) 

399 

400 

401 
(* s = t ==> t = s *) 

402 
local 

403 
val symm_rule = @{lemma "s = t ==> t == s" by simp} 

404 
in 

405 
fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm) 

406 
 symm p = MetaEq (thm_of p COMP symm_rule) 

407 
end 

408 

409 

410 
(* s = t ==> t = u ==> s = u *) 

411 
local 

412 
val trans1 = @{lemma "s == t ==> t = u ==> s == u" by simp} 

413 
val trans2 = @{lemma "s = t ==> t == u ==> s == u" by simp} 

414 
val trans3 = @{lemma "s = t ==> t = u ==> s == u" by simp} 

415 
in 

416 
fun trans (MetaEq thm1) (MetaEq thm2) = MetaEq (Thm.transitive thm1 thm2) 

417 
 trans (MetaEq thm) q = MetaEq (thm_of q COMP (thm COMP trans1)) 

418 
 trans p (MetaEq thm) = MetaEq (thm COMP (thm_of p COMP trans2)) 

419 
 trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans3)) 

420 
end 

421 

422 

423 
(* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn 

424 
(reflexive antecendents are droppped) *) 

425 
local 

426 
exception MONO 

427 

428 
fun prove_refl (ct, _) = Thm.reflexive ct 

429 
fun prove_comb f g cp = 

430 
let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp 

431 
in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end 

432 
fun prove_arg f = prove_comb prove_refl f 

433 

434 
fun prove f cp = prove_comb (prove f) f cp handle CTERM _ => prove_refl cp 

435 

436 
fun prove_nary is_comb f = 

437 
let 

438 
fun prove (cp as (ct, _)) = f cp handle MONO => 

439 
if is_comb (Thm.term_of ct) 

440 
then prove_comb (prove_arg prove) prove cp 

441 
else prove_refl cp 

442 
in prove end 

443 

444 
fun prove_list f n cp = 

445 
if n = 0 then prove_refl cp 

446 
else prove_comb (prove_arg f) (prove_list f (n1)) cp 

447 

448 
fun with_length f (cp as (cl, _)) = 

449 
f (length (HOLogic.dest_list (Thm.term_of cl))) cp 

450 

451 
fun prove_distinct f = prove_arg (with_length (prove_list f)) 

452 

453 
fun prove_eq exn lookup cp = 

454 
(case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of 

455 
SOME eq => eq 

456 
 NONE => if exn then raise MONO else prove_refl cp) 

457 

458 
val prove_eq_exn = prove_eq true 

459 
and prove_eq_safe = prove_eq false 

460 

461 
fun mono f (cp as (cl, _)) = 

462 
(case Term.head_of (Thm.term_of cl) of 

40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

463 
@{const HOL.conj} => prove_nary L.is_conj (prove_eq_exn f) 
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

464 
 @{const HOL.disj} => prove_nary L.is_disj (prove_eq_exn f) 
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as builtin
boehmes
parents:
40680
diff
changeset

465 
 Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f) 
36898  466 
 _ => prove (prove_eq_safe f)) cp 
467 
in 

468 
fun monotonicity eqs ct = 

469 
let 

40680
02caa72cb950
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
boehmes
parents:
40664
diff
changeset

470 
fun and_symmetric (t, thm) = [(t, thm), (t, Thm.symmetric thm)] 
02caa72cb950
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
boehmes
parents:
40664
diff
changeset

471 
val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs 
02caa72cb950
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
boehmes
parents:
40664
diff
changeset

472 
val lookup = AList.lookup (op aconv) teqs 
36898  473 
val cp = Thm.dest_binop (Thm.dest_arg ct) 
474 
in MetaEq (prove_eq_exn lookup cp handle MONO => mono lookup cp) end 

475 
end 

476 

477 

478 
(*  f a b = f b a (where f is equality) *) 

479 
local 

480 
val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)} 

481 
in 

482 
fun commutativity ct = MetaEq (T.match_instantiate I (T.as_meta_eq ct) rule) 

483 
end 

484 

485 

486 

487 
(** quantifier proof rules **) 

488 

489 
(* P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x) 

490 
P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x) *) 

491 
local 

492 
val rules = [ 

493 
@{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp}, 

494 
@{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}] 

495 
in 

496 
fun quant_intro vars p ct = 

497 
let 

498 
val thm = meta_eq_of p 

499 
val rules' = T.varify vars thm :: rules 

500 
val cu = T.as_meta_eq ct 

501 
in MetaEq (T.by_tac (REPEAT_ALL_NEW (Tactic.match_tac rules')) cu) end 

502 
end 

503 

504 

505 
(*  ((ALL x. P x)  Q) = (ALL x. P x  Q) *) 

506 
fun pull_quant ctxt = Thm o try_apply ctxt [] [ 

507 
named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))] 

508 
(* FIXME: not very well tested *) 

509 

510 

511 
(*  (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *) 

512 
fun push_quant ctxt = Thm o try_apply ctxt [] [ 

513 
named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))] 

514 
(* FIXME: not very well tested *) 

515 

516 

517 
(*  (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *) 

518 
local 

519 
val elim_all = @{lemma "(ALL x. P) == P" by simp} 

520 
val elim_ex = @{lemma "(EX x. P) == P" by simp} 

521 

522 
fun elim_unused_conv ctxt = 

523 
Conv.params_conv ~1 (K (Conv.arg_conv (Conv.arg1_conv 

36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36899
diff
changeset

524 
(Conv.rewrs_conv [elim_all, elim_ex])))) ctxt 
36898  525 

526 
fun elim_unused_tac ctxt = 

527 
REPEAT_ALL_NEW ( 

528 
Tactic.match_tac [@{thm refl}, @{thm iff_allI}, @{thm iff_exI}] 

529 
ORELSE' CONVERSION (elim_unused_conv ctxt)) 

530 
in 

531 
fun elim_unused_vars ctxt = Thm o T.by_tac (elim_unused_tac ctxt) 

532 
end 

533 

534 

535 
(*  (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn)  P x1 ... xn) = P t1 ... tn *) 

536 
fun dest_eq_res ctxt = Thm o try_apply ctxt [] [ 

537 
named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))] 

538 
(* FIXME: not very well tested *) 

539 

540 

541 
(*  ~(ALL x1...xn. P x1...xn)  P a1...an *) 

542 
local 

543 
val rule = @{lemma "~ P x  Q ==> ~(ALL x. P x)  Q" by fast} 

544 
in 

545 
val quant_inst = Thm o T.by_tac ( 

546 
REPEAT_ALL_NEW (Tactic.match_tac [rule]) 

547 
THEN' Tactic.rtac @{thm excluded_middle}) 

548 
end 

549 

550 

551 
(* c = SOME x. P x  (EX x. P x) = P c 

552 
c = SOME x. ~ P x  ~(ALL x. P x) = ~ P c *) 

553 
local 

554 
val elim_ex = @{lemma "EX x. P == P" by simp} 

555 
val elim_all = @{lemma "~ (ALL x. P) == ~P" by simp} 

556 
val sk_ex = @{lemma "c == SOME x. P x ==> EX x. P x == P c" 

557 
by simp (intro eq_reflection some_eq_ex[symmetric])} 

558 
val sk_all = @{lemma "c == SOME x. ~ P x ==> ~(ALL x. P x) == ~ P c" 

559 
by (simp only: not_all) (intro eq_reflection some_eq_ex[symmetric])} 

560 
val sk_ex_rule = ((sk_ex, I), elim_ex) 

561 
and sk_all_rule = ((sk_all, Thm.dest_arg), elim_all) 

562 

563 
fun dest f sk_rule = 

564 
Thm.dest_comb (f (Thm.dest_arg (Thm.dest_arg (Thm.cprop_of sk_rule)))) 

565 
fun type_of f sk_rule = Thm.ctyp_of_term (snd (dest f sk_rule)) 

566 
fun pair2 (a, b) (c, d) = [(a, c), (b, d)] 

567 
fun inst_sk (sk_rule, f) p c = 

568 
Thm.instantiate ([(type_of f sk_rule, Thm.ctyp_of_term c)], []) sk_rule 

569 
> (fn sk' => Thm.instantiate ([], (pair2 (dest f sk') (p, c))) sk') 

570 
> Conv.fconv_rule (Thm.beta_conversion true) 

571 

572 
fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I) 

40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

573 
 kind (@{const Not} $ (Const (@{const_name All}, _) $ _)) = 
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

574 
(sk_all_rule, Thm.dest_arg, L.negate) 
36898  575 
 kind t = raise TERM ("skolemize", [t]) 
576 

577 
fun dest_abs_type (Abs (_, T, _)) = T 

578 
 dest_abs_type t = raise TERM ("dest_abs_type", [t]) 

579 

580 
fun bodies_of thy lhs rhs = 

581 
let 

582 
val (rule, dest, make) = kind (Thm.term_of lhs) 

583 

584 
fun dest_body idx cbs ct = 

585 
let 

586 
val cb = Thm.dest_arg (dest ct) 

587 
val T = dest_abs_type (Thm.term_of cb) 

588 
val cv = Thm.cterm_of thy (Var (("x", idx), T)) 

589 
val cu = make (Drule.beta_conv cb cv) 

590 
val cbs' = (cv, cb) :: cbs 

591 
in 

592 
(snd (Thm.first_order_match (cu, rhs)), rev cbs') 

593 
handle Pattern.MATCH => dest_body (idx+1) cbs' cu 

594 
end 

595 
in (rule, dest_body 1 [] lhs) end 

596 

597 
fun transitive f thm = Thm.transitive thm (f (Thm.rhs_of thm)) 

598 

599 
fun sk_step (rule, elim) (cv, mct, cb) ((is, thm), ctxt) = 

600 
(case mct of 

601 
SOME ct => 

602 
ctxt 

603 
> T.make_hyp_def (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct) 

604 
>> pair ((cv, ct) :: is) o Thm.transitive thm 

605 
 NONE => ((is, transitive (Conv.rewr_conv elim) thm), ctxt)) 

606 
in 

607 
fun skolemize ct ctxt = 

608 
let 

609 
val (lhs, rhs) = Thm.dest_binop (Thm.dest_arg ct) 

610 
val (rule, (ctab, cbs)) = bodies_of (ProofContext.theory_of ctxt) lhs rhs 

611 
fun lookup_var (cv, cb) = (cv, AList.lookup (op aconvc) ctab cv, cb) 

612 
in 

613 
(([], Thm.reflexive lhs), ctxt) 

614 
> fold (sk_step rule) (map lookup_var cbs) 

615 
>> MetaEq o snd 

616 
end 

617 
end 

618 

619 

620 
(** theory proof rules **) 

621 

622 
(* theory lemmas: linear arithmetic, arrays *) 

623 
fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [ 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

624 
T.by_abstraction (false, true) ctxt thms (fn ctxt' => T.by_tac ( 
36898  625 
NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt') 
626 
ORELSE' NAMED ctxt' "simp+arith" (Simplifier.simp_tac simpset THEN_ALL_NEW 

627 
Arith_Data.arith_tac ctxt')))] 

628 

629 

630 
(* rewriting: prove equalities: 

631 
* ACI of conjunction/disjunction 

632 
* contradiction, excluded middle 

633 
* logical rewriting rules (for negation, implication, equivalence, 

634 
distinct) 

635 
* normal forms for polynoms (integer/real arithmetic) 

636 
* quantifier elimination over linear arithmetic 

637 
* ... ? **) 

638 
structure Z3_Simps = Named_Thms 

639 
( 

640 
val name = "z3_simp" 

641 
val description = "simplification rules for Z3 proof reconstruction" 

642 
) 

643 

644 
local 

645 
fun spec_meta_eq_of thm = 

646 
(case try (fn th => th RS @{thm spec}) thm of 

647 
SOME thm' => spec_meta_eq_of thm' 

648 
 NONE => mk_meta_eq thm) 

649 

650 
fun prep (Thm thm) = spec_meta_eq_of thm 

651 
 prep (MetaEq thm) = thm 

652 
 prep (Literals (thm, _)) = spec_meta_eq_of thm 

653 

654 
fun unfold_conv ctxt ths = 

655 
Conv.arg_conv (Conv.binop_conv (T.unfold_eqs ctxt (map prep ths))) 

656 

657 
fun with_conv _ [] prv = prv 

658 
 with_conv ctxt ths prv = T.with_conv (unfold_conv ctxt ths) prv 

659 

660 
val unfold_conv = 

661 
Conv.arg_conv (Conv.binop_conv (Conv.try_conv T.unfold_distinct_conv)) 

662 
val prove_conj_disj_eq = T.with_conv unfold_conv L.prove_conj_disj_eq 

40663  663 

664 
fun assume_prems ctxt thm = 

665 
Assumption.add_assumes (Drule.cprems_of thm) ctxt 

666 
>> (fn thms => fold Thm.elim_implies thms thm) 

36898  667 
in 
668 

40663  669 
fun rewrite simpset ths ct ctxt = 
670 
apfst Thm (assume_prems ctxt (with_conv ctxt ths (try_apply ctxt [] [ 

671 
named ctxt "conj/disj/distinct" prove_conj_disj_eq, 

672 
T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac ( 

673 
NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset) 

674 
THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))), 

675 
T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac ( 

676 
NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset) 

677 
THEN_ALL_NEW ( 

678 
NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs) 

679 
ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))), 

680 
T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac ( 

681 
NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset) 

682 
THEN_ALL_NEW ( 

683 
NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs) 

684 
ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))), 

685 
named ctxt "injectivity" (M.prove_injectivity ctxt)]) ct)) 

36898  686 

687 
end 

688 

689 

690 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

691 
(* proof reconstruction *) 
36898  692 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

693 
(** tracing and checking **) 
36898  694 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

695 
fun trace_before ctxt idx = SMT_Config.trace_msg ctxt (fn r => 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

696 
"Z3: #" ^ string_of_int idx ^ ": " ^ P.string_of_rule r) 
36898  697 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

698 
fun check_after idx r ps ct (p, (ctxt, _)) = 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

699 
if not (Config.get ctxt SMT_Config.trace) then () 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

700 
else 
36898  701 
let val thm = thm_of p > tap (Thm.join_proofs o single) 
702 
in 

703 
if (Thm.cprop_of thm) aconvc ct then () 

704 
else z3_exn (Pretty.string_of (Pretty.big_list ("proof step failed: " ^ 

705 
quote (P.string_of_rule r) ^ " (#" ^ string_of_int idx ^ ")") 

706 
(pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @ 

707 
[Pretty.block [Pretty.str "expected: ", 

708 
Syntax.pretty_term ctxt (Thm.term_of ct)]]))) 

709 
end 

710 

711 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

712 
(** overall reconstruction procedure **) 
36898  713 

40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

714 
local 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

715 
fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^ 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

716 
quote (P.string_of_rule r)) 
36898  717 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

718 
fun prove_step assms simpset vars r ps ct (cxp as (cx, ptab)) = 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

719 
(case (r, ps) of 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

720 
(* core rules *) 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

721 
(P.True_Axiom, _) => (Thm L.true_thm, cxp) 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

722 
 (P.Asserted, _) => (asserted cx assms ct, cxp) 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

723 
 (P.Goal, _) => (asserted cx assms ct, cxp) 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

724 
 (P.Modus_Ponens, [(p, _), (q, _)]) => (mp q (thm_of p), cxp) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

725 
 (P.Modus_Ponens_Oeq, [(p, _), (q, _)]) => (mp q (thm_of p), cxp) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

726 
 (P.And_Elim, [(p, i)]) => and_elim (p, i) ct ptab > pair cx 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

727 
 (P.Not_Or_Elim, [(p, i)]) => not_or_elim (p, i) ct ptab > pair cx 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

728 
 (P.Hypothesis, _) => (Thm (Thm.assume ct), cxp) 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

729 
 (P.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp) 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

730 
 (P.Unit_Resolution, (p, _) :: ps) => 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

731 
(unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp) 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

732 
 (P.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

733 
 (P.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp) 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

734 
 (P.Distributivity, _) => (distributivity cx ct, cxp) 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

735 
 (P.Def_Axiom, _) => (def_axiom cx ct, cxp) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

736 
 (P.Intro_Def, _) => intro_def ct cx > rpair ptab 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

737 
 (P.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

738 
 (P.Iff_Oeq, [(p, _)]) => (p, cxp) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

739 
 (P.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

740 
 (P.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp) 
36898  741 

40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

742 
(* equality rules *) 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

743 
 (P.Reflexivity, _) => (refl ct, cxp) 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

744 
 (P.Symmetry, [(p, _)]) => (symm p, cxp) 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

745 
 (P.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp) 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

746 
 (P.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp) 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

747 
 (P.Commutativity, _) => (commutativity ct, cxp) 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

748 

57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

749 
(* quantifier rules *) 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

750 
 (P.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

751 
 (P.Pull_Quant, _) => (pull_quant cx ct, cxp) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

752 
 (P.Push_Quant, _) => (push_quant cx ct, cxp) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

753 
 (P.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

754 
 (P.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

755 
 (P.Quant_Inst, _) => (quant_inst ct, cxp) 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

756 
 (P.Skolemize, _) => skolemize ct cx > rpair ptab 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

757 

57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

758 
(* theory rules *) 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

759 
 (P.Th_Lemma _, _) => (* FIXME: use arguments *) 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

760 
(th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp) 
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset

761 
 (P.Rewrite, _) => rewrite simpset [] ct cx > rpair ptab 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

762 
 (P.Rewrite_Star, ps) => rewrite simpset (map fst ps) ct cx > rpair ptab 
36898  763 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

764 
 (P.Nnf_Star, _) => not_supported r 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

765 
 (P.Cnf_Star, _) => not_supported r 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

766 
 (P.Transitivity_Star, _) => not_supported r 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

767 
 (P.Pull_Quant_Star, _) => not_supported r 
36898  768 

40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

769 
 _ => raise Fail ("Z3: proof rule " ^ quote (P.string_of_rule r) ^ 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

770 
" has an unexpected number of arguments.")) 
36898  771 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

772 
fun lookup_proof ptab idx = 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

773 
(case Inttab.lookup ptab idx of 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

774 
SOME p => (p, idx) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

775 
 NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx))) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

776 

130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

777 
fun prove assms simpset vars (idx, step) (_, cxp as (ctxt, ptab)) = 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

778 
let 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

779 
val P.Proof_Step {rule=r, prems, prop, ...} = step 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

780 
val ps = map (lookup_proof ptab) prems 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

781 
val _ = trace_before ctxt idx r 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

782 
val (thm, (ctxt', ptab')) = 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

783 
cxp 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

784 
> prove_step assms simpset vars r ps prop 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

785 
> tap (check_after idx r ps prop) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

786 
in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end 
36898  787 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

788 
val disch_rules = map (pair false) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

789 
[@{thm allI}, @{thm refl}, @{thm reflexive}] 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

790 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

791 
fun disch_assm thm = 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

792 
if Thm.nprems_of thm = 0 then Drule.flexflex_unique thm 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

793 
else 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

794 
(case Seq.pull (Thm.biresolution false disch_rules 1 thm) of 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

795 
SOME (thm', _) => disch_assm thm' 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

796 
 NONE => raise THM ("failed to discharge premise", 1, [thm])) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

797 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

798 
fun discharge outer_ctxt (p, (inner_ctxt, _)) = 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

799 
thm_of p 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

800 
> singleton (ProofContext.export inner_ctxt outer_ctxt) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

801 
> disch_assm 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

802 

41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

803 
fun filter_assms ctxt assms = 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

804 
let 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

805 
fun add_assm r ct = 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

806 
(case r of 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

807 
P.Asserted => insert (op =) (find_assm ctxt assms ct) 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

808 
 P.Goal => insert (op =) (find_assm ctxt assms ct) 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

809 
 _ => I) 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

810 
in fold (fn (_, P.Proof_Step {rule, prop, ...}) => add_assm rule prop) end 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

811 
in 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

812 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

813 
fun reconstruct outer_ctxt recon output = 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

814 
let 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

815 
val {context=ctxt, typs, terms, rewrite_rules, assms} = recon 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

816 
val (steps, vars, ctxt') = P.parse ctxt typs terms output 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

817 
val assms' = prepare_assms ctxt' rewrite_rules assms 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

818 
val simpset = T.make_simpset ctxt' (Z3_Simps.get ctxt') 
36898  819 
in 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

820 
if Config.get ctxt' SMT_Config.filter_only_facts then 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

821 
(filter_assms ctxt' assms' steps [], @{thm TrueI}) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

822 
else 
41130
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

823 
(Thm @{thm TrueI}, (ctxt', Inttab.empty)) 
130771a48c70
adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents:
41127
diff
changeset

824 
> fold (prove assms' simpset vars) steps 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

825 
> discharge outer_ctxt 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
40681
diff
changeset

826 
> pair [] 
36898  827 
end 
828 

40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

829 
end 
36898  830 

40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

831 
val setup = z3_rules_setup #> Z3_Simps.setup 
36898  832 

833 
end 