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