36898
|
1 |
(* Title: HOL/Tools/SMT/z3_proof_literals.ML
|
|
2 |
Author: Sascha Boehme, TU Muenchen
|
|
3 |
|
|
4 |
Proof tools related to conjunctions and disjunctions.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature Z3_PROOF_LITERALS =
|
|
8 |
sig
|
|
9 |
(* literal table *)
|
|
10 |
type littab = thm Termtab.table
|
|
11 |
val make_littab: thm list -> littab
|
|
12 |
val insert_lit: thm -> littab -> littab
|
|
13 |
val delete_lit: thm -> littab -> littab
|
|
14 |
val lookup_lit: littab -> term -> thm option
|
|
15 |
val get_first_lit: (term -> bool) -> littab -> thm option
|
|
16 |
|
|
17 |
(* rules *)
|
|
18 |
val true_thm: thm
|
|
19 |
val rewrite_true: thm
|
|
20 |
|
|
21 |
(* properties *)
|
|
22 |
val is_conj: term -> bool
|
|
23 |
val is_disj: term -> bool
|
|
24 |
val exists_lit: bool -> (term -> bool) -> term -> bool
|
|
25 |
|
|
26 |
(* proof tools *)
|
|
27 |
val explode: bool -> bool -> bool -> term list -> thm -> thm list
|
|
28 |
val join: bool -> littab -> term -> thm
|
|
29 |
val prove_conj_disj_eq: cterm -> thm
|
|
30 |
end
|
|
31 |
|
|
32 |
structure Z3_Proof_Literals: Z3_PROOF_LITERALS =
|
|
33 |
struct
|
|
34 |
|
|
35 |
structure T = Z3_Proof_Tools
|
|
36 |
|
|
37 |
|
|
38 |
|
|
39 |
(** literal table **)
|
|
40 |
|
|
41 |
type littab = thm Termtab.table
|
|
42 |
|
|
43 |
fun make_littab thms = fold (Termtab.update o `T.prop_of) thms Termtab.empty
|
|
44 |
|
|
45 |
fun insert_lit thm = Termtab.update (`T.prop_of thm)
|
|
46 |
fun delete_lit thm = Termtab.delete (T.prop_of thm)
|
|
47 |
fun lookup_lit lits = Termtab.lookup lits
|
|
48 |
fun get_first_lit f =
|
|
49 |
Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE)
|
|
50 |
|
|
51 |
|
|
52 |
|
|
53 |
(** rules **)
|
|
54 |
|
|
55 |
val true_thm = @{lemma "~False" by simp}
|
|
56 |
val rewrite_true = @{lemma "True == ~ False" by simp}
|
|
57 |
|
|
58 |
|
|
59 |
|
|
60 |
(** properties and term operations **)
|
|
61 |
|
|
62 |
val is_neg = (fn @{term Not} $ _ => true | _ => false)
|
|
63 |
fun is_neg' f = (fn @{term Not} $ t => f t | _ => false)
|
|
64 |
val is_dneg = is_neg' is_neg
|
|
65 |
val is_conj = (fn @{term "op &"} $ _ $ _ => true | _ => false)
|
|
66 |
val is_disj = (fn @{term "op |"} $ _ $ _ => true | _ => false)
|
|
67 |
|
|
68 |
fun dest_disj_term' f = (fn
|
|
69 |
@{term Not} $ (@{term "op |"} $ t $ u) => SOME (f t, f u)
|
|
70 |
| _ => NONE)
|
|
71 |
|
|
72 |
val dest_conj_term = (fn @{term "op &"} $ t $ u => SOME (t, u) | _ => NONE)
|
|
73 |
val dest_disj_term =
|
|
74 |
dest_disj_term' (fn @{term Not} $ t => t | t => @{term Not} $ t)
|
|
75 |
|
|
76 |
fun exists_lit is_conj P =
|
|
77 |
let
|
|
78 |
val dest = if is_conj then dest_conj_term else dest_disj_term
|
|
79 |
fun exists t = P t orelse
|
|
80 |
(case dest t of
|
|
81 |
SOME (t1, t2) => exists t1 orelse exists t2
|
|
82 |
| NONE => false)
|
|
83 |
in exists end
|
|
84 |
|
|
85 |
|
|
86 |
|
|
87 |
(** proof tools **)
|
|
88 |
|
|
89 |
(* explosion of conjunctions and disjunctions *)
|
|
90 |
|
|
91 |
local
|
|
92 |
fun destc ct = Thm.dest_binop (Thm.dest_arg ct)
|
|
93 |
val dest_conj1 = T.precompose2 destc @{thm conjunct1}
|
|
94 |
val dest_conj2 = T.precompose2 destc @{thm conjunct2}
|
|
95 |
fun dest_conj_rules t =
|
|
96 |
dest_conj_term t |> Option.map (K (dest_conj1, dest_conj2))
|
|
97 |
|
|
98 |
fun destd f ct = f (Thm.dest_binop (Thm.dest_arg (Thm.dest_arg ct)))
|
|
99 |
val dn1 = apfst Thm.dest_arg and dn2 = apsnd Thm.dest_arg
|
|
100 |
val dest_disj1 = T.precompose2 (destd I) @{lemma "~(P | Q) ==> ~P" by fast}
|
|
101 |
val dest_disj2 = T.precompose2 (destd dn1) @{lemma "~(~P | Q) ==> P" by fast}
|
|
102 |
val dest_disj3 = T.precompose2 (destd I) @{lemma "~(P | Q) ==> ~Q" by fast}
|
|
103 |
val dest_disj4 = T.precompose2 (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast}
|
|
104 |
|
|
105 |
fun dest_disj_rules t =
|
|
106 |
(case dest_disj_term' is_neg t of
|
|
107 |
SOME (true, true) => SOME (dest_disj2, dest_disj4)
|
|
108 |
| SOME (true, false) => SOME (dest_disj2, dest_disj3)
|
|
109 |
| SOME (false, true) => SOME (dest_disj1, dest_disj4)
|
|
110 |
| SOME (false, false) => SOME (dest_disj1, dest_disj3)
|
|
111 |
| NONE => NONE)
|
|
112 |
|
|
113 |
fun destn ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg ct))]
|
|
114 |
val dneg_rule = T.precompose destn @{thm notnotD}
|
|
115 |
in
|
|
116 |
|
|
117 |
(* explode a term into literals and collect all rules to be able to deduce
|
|
118 |
particular literals afterwards *)
|
|
119 |
fun explode_term is_conj =
|
|
120 |
let
|
|
121 |
val dest = if is_conj then dest_conj_term else dest_disj_term
|
|
122 |
val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules
|
|
123 |
|
|
124 |
fun add (t, rs) = Termtab.map_default (t, rs)
|
|
125 |
(fn rs' => if length rs' < length rs then rs' else rs)
|
|
126 |
|
|
127 |
fun explode1 rules t =
|
|
128 |
(case dest t of
|
|
129 |
SOME (t1, t2) =>
|
|
130 |
let val (rule1, rule2) = the (dest_rules t)
|
|
131 |
in
|
|
132 |
explode1 (rule1 :: rules) t1 #>
|
|
133 |
explode1 (rule2 :: rules) t2 #>
|
|
134 |
add (t, rev rules)
|
|
135 |
end
|
|
136 |
| NONE => add (t, rev rules))
|
|
137 |
|
|
138 |
fun explode0 (@{term Not} $ (@{term Not} $ t)) =
|
|
139 |
Termtab.make [(t, [dneg_rule])]
|
|
140 |
| explode0 t = explode1 [] t Termtab.empty
|
|
141 |
|
|
142 |
in explode0 end
|
|
143 |
|
|
144 |
(* extract a literal by applying previously collected rules *)
|
|
145 |
fun extract_lit thm rules = fold T.compose rules thm
|
|
146 |
|
|
147 |
|
|
148 |
(* explode a theorem into its literals *)
|
|
149 |
fun explode is_conj full keep_intermediate stop_lits =
|
|
150 |
let
|
|
151 |
val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules
|
|
152 |
val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty
|
|
153 |
|
|
154 |
fun explode1 thm =
|
|
155 |
if Termtab.defined tab (T.prop_of thm) then cons thm
|
|
156 |
else
|
|
157 |
(case dest_rules (T.prop_of thm) of
|
|
158 |
SOME (rule1, rule2) =>
|
|
159 |
explode2 rule1 thm #>
|
|
160 |
explode2 rule2 thm #>
|
|
161 |
keep_intermediate ? cons thm
|
|
162 |
| NONE => cons thm)
|
|
163 |
|
|
164 |
and explode2 dest_rule thm =
|
|
165 |
if full orelse exists_lit is_conj (Termtab.defined tab) (T.prop_of thm)
|
|
166 |
then explode1 (T.compose dest_rule thm)
|
|
167 |
else cons (T.compose dest_rule thm)
|
|
168 |
|
|
169 |
fun explode0 thm =
|
|
170 |
if not is_conj andalso is_dneg (T.prop_of thm)
|
|
171 |
then [T.compose dneg_rule thm]
|
|
172 |
else explode1 thm []
|
|
173 |
|
|
174 |
in explode0 end
|
|
175 |
|
|
176 |
end
|
|
177 |
|
|
178 |
|
|
179 |
|
|
180 |
(* joining of literals to conjunctions or disjunctions *)
|
|
181 |
|
|
182 |
local
|
|
183 |
fun on_cprem i f thm = f (Thm.cprem_of thm i)
|
|
184 |
fun on_cprop f thm = f (Thm.cprop_of thm)
|
|
185 |
fun precomp2 f g thm = (on_cprem 1 f thm, on_cprem 2 g thm, f, g, thm)
|
|
186 |
fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 =
|
|
187 |
Thm.instantiate ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule
|
|
188 |
|> T.discharge thm1 |> T.discharge thm2
|
|
189 |
|
|
190 |
fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct)
|
|
191 |
|
|
192 |
val conj_rule = precomp2 d1 d1 @{thm conjI}
|
|
193 |
fun comp_conj ((_, thm1), (_, thm2)) = comp2 conj_rule thm1 thm2
|
|
194 |
|
|
195 |
val disj1 = precomp2 d2 d2 @{lemma "~P ==> ~Q ==> ~(P | Q)" by fast}
|
|
196 |
val disj2 = precomp2 d2 d1 @{lemma "~P ==> Q ==> ~(P | ~Q)" by fast}
|
|
197 |
val disj3 = precomp2 d1 d2 @{lemma "P ==> ~Q ==> ~(~P | Q)" by fast}
|
|
198 |
val disj4 = precomp2 d1 d1 @{lemma "P ==> Q ==> ~(~P | ~Q)" by fast}
|
|
199 |
|
|
200 |
fun comp_disj ((false, thm1), (false, thm2)) = comp2 disj1 thm1 thm2
|
|
201 |
| comp_disj ((false, thm1), (true, thm2)) = comp2 disj2 thm1 thm2
|
|
202 |
| comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
|
|
203 |
| comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2
|
|
204 |
|
|
205 |
fun dest_conj (@{term "op &"} $ t $ u) = ((false, t), (false, u))
|
|
206 |
| dest_conj t = raise TERM ("dest_conj", [t])
|
|
207 |
|
|
208 |
val neg = (fn @{term Not} $ t => (true, t) | t => (false, @{term Not} $ t))
|
|
209 |
fun dest_disj (@{term Not} $ (@{term "op |"} $ t $ u)) = (neg t, neg u)
|
|
210 |
| dest_disj t = raise TERM ("dest_disj", [t])
|
|
211 |
|
|
212 |
val dnegE = T.precompose (single o d2 o d1) @{thm notnotD}
|
|
213 |
val dnegI = T.precompose (single o d1) @{lemma "P ==> ~~P" by fast}
|
|
214 |
fun as_dneg f t = f (@{term Not} $ (@{term Not} $ t))
|
|
215 |
|
|
216 |
fun dni f = apsnd f o Thm.dest_binop o f o d1
|
|
217 |
val negIffE = T.precompose2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
|
|
218 |
val negIffI = T.precompose2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
|
|
219 |
val iff_const = @{term "op = :: bool => _"}
|
|
220 |
fun as_negIff f (@{term "op = :: bool => _"} $ t $ u) =
|
|
221 |
f (@{term Not} $ (iff_const $ u $ (@{term Not} $ t)))
|
|
222 |
| as_negIff _ _ = NONE
|
|
223 |
in
|
|
224 |
|
|
225 |
fun join is_conj littab t =
|
|
226 |
let
|
|
227 |
val comp = if is_conj then comp_conj else comp_disj
|
|
228 |
val dest = if is_conj then dest_conj else dest_disj
|
|
229 |
|
|
230 |
val lookup = lookup_lit littab
|
|
231 |
|
|
232 |
fun lookup_rule t =
|
|
233 |
(case t of
|
|
234 |
@{term Not} $ (@{term Not} $ t) => (T.compose dnegI, lookup t)
|
|
235 |
| @{term Not} $ (@{term "op = :: bool => _"} $ t $ (@{term Not} $ u)) =>
|
|
236 |
(T.compose negIffI, lookup (iff_const $ u $ t))
|
|
237 |
| @{term Not} $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u) =>
|
|
238 |
let fun rewr lit = lit COMP @{thm not_sym}
|
|
239 |
in (rewr, lookup (@{term Not} $ (eq $ u $ t))) end
|
|
240 |
| _ =>
|
|
241 |
(case as_dneg lookup t of
|
|
242 |
NONE => (T.compose negIffE, as_negIff lookup t)
|
|
243 |
| x => (T.compose dnegE, x)))
|
|
244 |
|
|
245 |
fun join1 (s, t) =
|
|
246 |
(case lookup t of
|
|
247 |
SOME lit => (s, lit)
|
|
248 |
| NONE =>
|
|
249 |
(case lookup_rule t of
|
|
250 |
(rewrite, SOME lit) => (s, rewrite lit)
|
|
251 |
| (_, NONE) => (s, comp (pairself join1 (dest t)))))
|
|
252 |
|
|
253 |
in snd (join1 (if is_conj then (false, t) else (true, t))) end
|
|
254 |
|
|
255 |
end
|
|
256 |
|
|
257 |
|
|
258 |
|
|
259 |
(* proving equality of conjunctions or disjunctions *)
|
|
260 |
|
|
261 |
fun iff_intro thm1 thm2 = thm2 COMP (thm1 COMP @{thm iffI})
|
|
262 |
|
|
263 |
local
|
|
264 |
val cp1 = @{lemma "(~P) = (~Q) ==> P = Q" by simp}
|
|
265 |
val cp2 = @{lemma "(~P) = Q ==> P = (~Q)" by fastsimp}
|
|
266 |
val cp3 = @{lemma "P = (~Q) ==> (~P) = Q" by simp}
|
|
267 |
val neg = Thm.capply @{cterm Not}
|
|
268 |
in
|
|
269 |
fun contrapos1 prove (ct, cu) = prove (neg ct, neg cu) COMP cp1
|
|
270 |
fun contrapos2 prove (ct, cu) = prove (neg ct, Thm.dest_arg cu) COMP cp2
|
|
271 |
fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, neg cu) COMP cp3
|
|
272 |
end
|
|
273 |
|
|
274 |
|
|
275 |
local
|
|
276 |
val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)}
|
|
277 |
fun contra_left conj thm =
|
|
278 |
let
|
|
279 |
val rules = explode_term conj (T.prop_of thm)
|
|
280 |
fun contra_lits (t, rs) =
|
|
281 |
(case t of
|
|
282 |
@{term Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
|
|
283 |
| _ => NONE)
|
|
284 |
in
|
|
285 |
(case Termtab.lookup rules @{term False} of
|
|
286 |
SOME rs => extract_lit thm rs
|
|
287 |
| NONE =>
|
|
288 |
the (Termtab.get_first contra_lits rules)
|
|
289 |
|> pairself (extract_lit thm)
|
|
290 |
|> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule)))
|
|
291 |
end
|
|
292 |
|
|
293 |
val falseE_v = Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE}))
|
|
294 |
fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE}
|
|
295 |
in
|
|
296 |
fun contradict conj ct =
|
|
297 |
iff_intro (T.under_assumption (contra_left conj) ct) (contra_right ct)
|
|
298 |
end
|
|
299 |
|
|
300 |
|
|
301 |
local
|
|
302 |
fun prove_eq l r (cl, cr) =
|
|
303 |
let
|
|
304 |
fun explode' is_conj = explode is_conj true (l <> r) []
|
|
305 |
fun make_tab is_conj thm = make_littab (true_thm :: explode' is_conj thm)
|
|
306 |
fun prove is_conj ct tab = join is_conj tab (Thm.term_of ct)
|
|
307 |
|
|
308 |
val thm1 = T.under_assumption (prove r cr o make_tab l) cl
|
|
309 |
val thm2 = T.under_assumption (prove l cl o make_tab r) cr
|
|
310 |
in iff_intro thm1 thm2 end
|
|
311 |
|
|
312 |
datatype conj_disj = CONJ | DISJ | NCON | NDIS
|
|
313 |
fun kind_of t =
|
|
314 |
if is_conj t then SOME CONJ
|
|
315 |
else if is_disj t then SOME DISJ
|
|
316 |
else if is_neg' is_conj t then SOME NCON
|
|
317 |
else if is_neg' is_disj t then SOME NDIS
|
|
318 |
else NONE
|
|
319 |
in
|
|
320 |
|
|
321 |
fun prove_conj_disj_eq ct =
|
|
322 |
let val cp as (cl, cr) = Thm.dest_binop (Thm.dest_arg ct)
|
|
323 |
in
|
|
324 |
(case (kind_of (Thm.term_of cl), Thm.term_of cr) of
|
|
325 |
(SOME CONJ, @{term False}) => contradict true cl
|
|
326 |
| (SOME DISJ, @{term "~False"}) => contrapos2 (contradict false o fst) cp
|
|
327 |
| (kl, _) =>
|
|
328 |
(case (kl, kind_of (Thm.term_of cr)) of
|
|
329 |
(SOME CONJ, SOME CONJ) => prove_eq true true cp
|
|
330 |
| (SOME CONJ, SOME NDIS) => prove_eq true false cp
|
|
331 |
| (SOME CONJ, _) => prove_eq true true cp
|
|
332 |
| (SOME DISJ, SOME DISJ) => contrapos1 (prove_eq false false) cp
|
|
333 |
| (SOME DISJ, SOME NCON) => contrapos2 (prove_eq false true) cp
|
|
334 |
| (SOME DISJ, _) => contrapos1 (prove_eq false false) cp
|
|
335 |
| (SOME NCON, SOME NCON) => contrapos1 (prove_eq true true) cp
|
|
336 |
| (SOME NCON, SOME DISJ) => contrapos3 (prove_eq true false) cp
|
|
337 |
| (SOME NCON, NONE) => contrapos3 (prove_eq true false) cp
|
|
338 |
| (SOME NDIS, SOME NDIS) => prove_eq false false cp
|
|
339 |
| (SOME NDIS, SOME CONJ) => prove_eq false true cp
|
|
340 |
| (SOME NDIS, NONE) => prove_eq false true cp
|
|
341 |
| _ => raise CTERM ("prove_conj_disj_eq", [ct])))
|
|
342 |
end
|
|
343 |
|
|
344 |
end
|
|
345 |
|
|
346 |
end
|