1 (* Title: HOL/Integ/cooper_proof.ML |
|
2 ID: $Id$ |
|
3 Author: Amine Chaieb and Tobias Nipkow, TU Muenchen |
|
4 |
|
5 File containing the implementation of the proof |
|
6 generation for Cooper Algorithm |
|
7 *) |
|
8 |
|
9 |
|
10 signature COOPER_PROOF = |
|
11 sig |
|
12 val qe_Not : thm |
|
13 val qe_conjI : thm |
|
14 val qe_disjI : thm |
|
15 val qe_impI : thm |
|
16 val qe_eqI : thm |
|
17 val qe_exI : thm |
|
18 val list_to_set : typ -> term list -> term |
|
19 val qe_get_terms : thm -> term * term |
|
20 val cooper_prv : theory -> term -> term -> thm |
|
21 val proof_of_evalc : theory -> term -> thm |
|
22 val proof_of_cnnf : theory -> term -> (term -> thm) -> thm |
|
23 val proof_of_linform : theory -> string list -> term -> thm |
|
24 val proof_of_adjustcoeffeq : theory -> term -> IntInf.int -> term -> thm |
|
25 val prove_elementar : theory -> string -> term -> thm |
|
26 val thm_of : theory -> (term -> (term list * (thm list -> thm))) -> term -> thm |
|
27 end; |
|
28 |
|
29 structure CooperProof : COOPER_PROOF = |
|
30 struct |
|
31 open CooperDec; |
|
32 |
|
33 val presburger_ss = simpset () |
|
34 addsimps [diff_int_def] delsimps [thm "diff_int_def_symmetric"]; |
|
35 |
|
36 val cboolT = ctyp_of HOL.thy HOLogic.boolT; |
|
37 |
|
38 (*Theorems that will be used later for the proofgeneration*) |
|
39 |
|
40 val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0"; |
|
41 val unity_coeff_ex = thm "unity_coeff_ex"; |
|
42 |
|
43 (* Theorems for proving the adjustment of the coefficients*) |
|
44 |
|
45 val ac_lt_eq = thm "ac_lt_eq"; |
|
46 val ac_eq_eq = thm "ac_eq_eq"; |
|
47 val ac_dvd_eq = thm "ac_dvd_eq"; |
|
48 val ac_pi_eq = thm "ac_pi_eq"; |
|
49 |
|
50 (* The logical compination of the sythetised properties*) |
|
51 val qe_Not = thm "qe_Not"; |
|
52 val qe_conjI = thm "qe_conjI"; |
|
53 val qe_disjI = thm "qe_disjI"; |
|
54 val qe_impI = thm "qe_impI"; |
|
55 val qe_eqI = thm "qe_eqI"; |
|
56 val qe_exI = thm "qe_exI"; |
|
57 val qe_ALLI = thm "qe_ALLI"; |
|
58 |
|
59 (*Modulo D property for Pminusinf an Plusinf *) |
|
60 val fm_modd_minf = thm "fm_modd_minf"; |
|
61 val not_dvd_modd_minf = thm "not_dvd_modd_minf"; |
|
62 val dvd_modd_minf = thm "dvd_modd_minf"; |
|
63 |
|
64 val fm_modd_pinf = thm "fm_modd_pinf"; |
|
65 val not_dvd_modd_pinf = thm "not_dvd_modd_pinf"; |
|
66 val dvd_modd_pinf = thm "dvd_modd_pinf"; |
|
67 |
|
68 (* the minusinfinity proprty*) |
|
69 |
|
70 val fm_eq_minf = thm "fm_eq_minf"; |
|
71 val neq_eq_minf = thm "neq_eq_minf"; |
|
72 val eq_eq_minf = thm "eq_eq_minf"; |
|
73 val le_eq_minf = thm "le_eq_minf"; |
|
74 val len_eq_minf = thm "len_eq_minf"; |
|
75 val not_dvd_eq_minf = thm "not_dvd_eq_minf"; |
|
76 val dvd_eq_minf = thm "dvd_eq_minf"; |
|
77 |
|
78 (* the Plusinfinity proprty*) |
|
79 |
|
80 val fm_eq_pinf = thm "fm_eq_pinf"; |
|
81 val neq_eq_pinf = thm "neq_eq_pinf"; |
|
82 val eq_eq_pinf = thm "eq_eq_pinf"; |
|
83 val le_eq_pinf = thm "le_eq_pinf"; |
|
84 val len_eq_pinf = thm "len_eq_pinf"; |
|
85 val not_dvd_eq_pinf = thm "not_dvd_eq_pinf"; |
|
86 val dvd_eq_pinf = thm "dvd_eq_pinf"; |
|
87 |
|
88 (*Logical construction of the Property*) |
|
89 val eq_minf_conjI = thm "eq_minf_conjI"; |
|
90 val eq_minf_disjI = thm "eq_minf_disjI"; |
|
91 val modd_minf_disjI = thm "modd_minf_disjI"; |
|
92 val modd_minf_conjI = thm "modd_minf_conjI"; |
|
93 |
|
94 val eq_pinf_conjI = thm "eq_pinf_conjI"; |
|
95 val eq_pinf_disjI = thm "eq_pinf_disjI"; |
|
96 val modd_pinf_disjI = thm "modd_pinf_disjI"; |
|
97 val modd_pinf_conjI = thm "modd_pinf_conjI"; |
|
98 |
|
99 (*Cooper Backwards...*) |
|
100 (*Bset*) |
|
101 val not_bst_p_fm = thm "not_bst_p_fm"; |
|
102 val not_bst_p_ne = thm "not_bst_p_ne"; |
|
103 val not_bst_p_eq = thm "not_bst_p_eq"; |
|
104 val not_bst_p_gt = thm "not_bst_p_gt"; |
|
105 val not_bst_p_lt = thm "not_bst_p_lt"; |
|
106 val not_bst_p_ndvd = thm "not_bst_p_ndvd"; |
|
107 val not_bst_p_dvd = thm "not_bst_p_dvd"; |
|
108 |
|
109 (*Aset*) |
|
110 val not_ast_p_fm = thm "not_ast_p_fm"; |
|
111 val not_ast_p_ne = thm "not_ast_p_ne"; |
|
112 val not_ast_p_eq = thm "not_ast_p_eq"; |
|
113 val not_ast_p_gt = thm "not_ast_p_gt"; |
|
114 val not_ast_p_lt = thm "not_ast_p_lt"; |
|
115 val not_ast_p_ndvd = thm "not_ast_p_ndvd"; |
|
116 val not_ast_p_dvd = thm "not_ast_p_dvd"; |
|
117 |
|
118 (*Logical construction of the prop*) |
|
119 (*Bset*) |
|
120 val not_bst_p_conjI = thm "not_bst_p_conjI"; |
|
121 val not_bst_p_disjI = thm "not_bst_p_disjI"; |
|
122 val not_bst_p_Q_elim = thm "not_bst_p_Q_elim"; |
|
123 |
|
124 (*Aset*) |
|
125 val not_ast_p_conjI = thm "not_ast_p_conjI"; |
|
126 val not_ast_p_disjI = thm "not_ast_p_disjI"; |
|
127 val not_ast_p_Q_elim = thm "not_ast_p_Q_elim"; |
|
128 |
|
129 (*Cooper*) |
|
130 val cppi_eq = thm "cppi_eq"; |
|
131 val cpmi_eq = thm "cpmi_eq"; |
|
132 |
|
133 (*Others*) |
|
134 val simp_from_to = thm "simp_from_to"; |
|
135 val P_eqtrue = thm "P_eqtrue"; |
|
136 val P_eqfalse = thm "P_eqfalse"; |
|
137 |
|
138 (*For Proving NNF*) |
|
139 |
|
140 val nnf_nn = thm "nnf_nn"; |
|
141 val nnf_im = thm "nnf_im"; |
|
142 val nnf_eq = thm "nnf_eq"; |
|
143 val nnf_sdj = thm "nnf_sdj"; |
|
144 val nnf_ncj = thm "nnf_ncj"; |
|
145 val nnf_nim = thm "nnf_nim"; |
|
146 val nnf_neq = thm "nnf_neq"; |
|
147 val nnf_ndj = thm "nnf_ndj"; |
|
148 |
|
149 (*For Proving term linearizition*) |
|
150 val linearize_dvd = thm "linearize_dvd"; |
|
151 val lf_lt = thm "lf_lt"; |
|
152 val lf_eq = thm "lf_eq"; |
|
153 val lf_dvd = thm "lf_dvd"; |
|
154 |
|
155 |
|
156 (* ------------------------------------------------------------------------- *) |
|
157 (*This function norm_zero_one replaces the occurences of Numeral1 and Numeral0*) |
|
158 (*Respectively by their abstract representation Const(@{const_name HOL.one},..) and Const(@{const_name HOL.zero},..)*) |
|
159 (*this is necessary because the theorems use this representation.*) |
|
160 (* This function should be elminated in next versions...*) |
|
161 (* ------------------------------------------------------------------------- *) |
|
162 |
|
163 fun norm_zero_one fm = case fm of |
|
164 (Const (@{const_name HOL.times},_) $ c $ t) => |
|
165 if c = one then (norm_zero_one t) |
|
166 else if (dest_number c = ~1) |
|
167 then (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t)) |
|
168 else (HOLogic.mk_binop @{const_name HOL.times} (norm_zero_one c,norm_zero_one t)) |
|
169 |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest)) |
|
170 |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p))) |
|
171 |_ => fm; |
|
172 |
|
173 (* ------------------------------------------------------------------------- *) |
|
174 (*function list to Set, constructs a set containing all elements of a given list.*) |
|
175 (* ------------------------------------------------------------------------- *) |
|
176 fun list_to_set T1 l = let val T = (HOLogic.mk_setT T1) in |
|
177 case l of |
|
178 [] => Const ("{}",T) |
|
179 |(h::t) => Const("insert", T1 --> (T --> T)) $ h $(list_to_set T1 t) |
|
180 end; |
|
181 |
|
182 (* ------------------------------------------------------------------------- *) |
|
183 (* Returns both sides of an equvalence in the theorem*) |
|
184 (* ------------------------------------------------------------------------- *) |
|
185 fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end; |
|
186 |
|
187 (* ------------------------------------------------------------------------- *) |
|
188 (*This function proove elementar will be used to generate proofs at |
|
189 runtime*) (*It is thought to prove properties such as a dvd b |
|
190 (essentially) that are only to make at runtime.*) |
|
191 (* ------------------------------------------------------------------------- *) |
|
192 fun prove_elementar thy s fm2 = |
|
193 Goal.prove (ProofContext.init thy) [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY |
|
194 (case s of |
|
195 (*"ss" like simplification with simpset*) |
|
196 "ss" => |
|
197 let val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0,unity_coeff_ex] |
|
198 in [simp_tac ss 1, TRY (simple_arith_tac 1)] end |
|
199 |
|
200 (*"bl" like blast tactic*) |
|
201 (* Is only used in the harrisons like proof procedure *) |
|
202 | "bl" => [blast_tac HOL_cs 1] |
|
203 |
|
204 (*"ed" like Existence disjunctions ...*) |
|
205 (* Is only used in the harrisons like proof procedure *) |
|
206 | "ed" => |
|
207 let |
|
208 val ex_disj_tacs = |
|
209 let |
|
210 val tac1 = EVERY[REPEAT(resolve_tac [disjI1,disjI2] 1), etac exI 1] |
|
211 val tac2 = EVERY[etac exE 1, rtac exI 1, |
|
212 REPEAT(resolve_tac [disjI1,disjI2] 1), assumption 1] |
|
213 in [rtac iffI 1, |
|
214 etac exE 1, REPEAT(EVERY[etac disjE 1, tac1]), tac1, |
|
215 REPEAT(EVERY[etac disjE 1, tac2]), tac2] |
|
216 end |
|
217 in ex_disj_tacs end |
|
218 |
|
219 | "fa" => [simple_arith_tac 1] |
|
220 |
|
221 | "sa" => |
|
222 let val ss = presburger_ss addsimps zadd_ac |
|
223 in [simp_tac ss 1, TRY (simple_arith_tac 1)] end |
|
224 |
|
225 (* like Existance Conjunction *) |
|
226 | "ec" => |
|
227 let val ss = presburger_ss addsimps zadd_ac |
|
228 in [simp_tac ss 1, TRY (blast_tac HOL_cs 1)] end |
|
229 |
|
230 | "ac" => |
|
231 let val ss = HOL_basic_ss addsimps zadd_ac |
|
232 in [simp_tac ss 1] end |
|
233 |
|
234 | "lf" => |
|
235 let val ss = presburger_ss addsimps zadd_ac |
|
236 in [simp_tac ss 1, TRY (simple_arith_tac 1)] end)); |
|
237 |
|
238 (*=============================================================*) |
|
239 (*-------------------------------------------------------------*) |
|
240 (* The new compact model *) |
|
241 (*-------------------------------------------------------------*) |
|
242 (*=============================================================*) |
|
243 |
|
244 fun thm_of sg decomp t = |
|
245 let val (ts,recomb) = decomp t |
|
246 in recomb (map (thm_of sg decomp) ts) |
|
247 end; |
|
248 |
|
249 (*==================================================*) |
|
250 (* Compact Version for adjustcoeffeq *) |
|
251 (*==================================================*) |
|
252 |
|
253 fun decomp_adjustcoeffeq sg x l fm = case fm of |
|
254 (Const("Not",_)$(Const(@{const_name Orderings.less},_) $ zero $(rt as (Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ c $ y ) $z )))) => |
|
255 let |
|
256 val m = l div (dest_number c) |
|
257 val n = if (x = y) then abs (m) else 1 |
|
258 val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div n)*l) ), x)) |
|
259 val rs = if (x = y) |
|
260 then (HOLogic.mk_binrel @{const_name Orderings.less} (zero,linear_sub [] (mk_number n) (HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) )))) |
|
261 else HOLogic.mk_binrel @{const_name Orderings.less} (zero,linear_sub [] one rt ) |
|
262 val ck = cterm_of sg (mk_number n) |
|
263 val cc = cterm_of sg c |
|
264 val ct = cterm_of sg z |
|
265 val cx = cterm_of sg y |
|
266 val pre = prove_elementar sg "lf" |
|
267 (HOLogic.mk_binrel @{const_name Orderings.less} (zero, mk_number n)) |
|
268 val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq))) |
|
269 in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans) |
|
270 end |
|
271 |
|
272 |(Const(p,_) $a $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ |
|
273 c $ y ) $t )) => |
|
274 if (is_arith_rel fm) andalso (x = y) |
|
275 then |
|
276 let val m = l div (dest_number c) |
|
277 val k = (if p = @{const_name Orderings.less} then abs(m) else m) |
|
278 val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div k)*l) ), x)) |
|
279 val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul k t) )))) |
|
280 |
|
281 val ck = cterm_of sg (mk_number k) |
|
282 val cc = cterm_of sg c |
|
283 val ct = cterm_of sg t |
|
284 val cx = cterm_of sg x |
|
285 val ca = cterm_of sg a |
|
286 |
|
287 in |
|
288 case p of |
|
289 @{const_name Orderings.less} => |
|
290 let val pre = prove_elementar sg "lf" |
|
291 (HOLogic.mk_binrel @{const_name Orderings.less} (zero, mk_number k)) |
|
292 val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq))) |
|
293 in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans) |
|
294 end |
|
295 |
|
296 |"op =" => |
|
297 let val pre = prove_elementar sg "lf" |
|
298 (HOLogic.Not $ (HOLogic.mk_binrel "op =" (zero, mk_number k))) |
|
299 val th1 = (pre RS(instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_eq_eq))) |
|
300 in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans) |
|
301 end |
|
302 |
|
303 |"Divides.dvd" => |
|
304 let val pre = prove_elementar sg "lf" |
|
305 (HOLogic.Not $ (HOLogic.mk_binrel "op =" (zero, mk_number k))) |
|
306 val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq)) |
|
307 in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans) |
|
308 |
|
309 end |
|
310 end |
|
311 else ([], fn [] => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] refl) |
|
312 |
|
313 |( Const ("Not", _) $ p) => ([p], fn [th] => th RS qe_Not) |
|
314 |( Const ("op &",_) $ p $ q) => ([p,q], fn [th1,th2] => [th1,th2] MRS qe_conjI) |
|
315 |( Const ("op |",_) $ p $ q) =>([p,q], fn [th1,th2] => [th1,th2] MRS qe_disjI) |
|
316 |
|
317 |_ => ([], fn [] => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] refl); |
|
318 |
|
319 fun proof_of_adjustcoeffeq sg x l = thm_of sg (decomp_adjustcoeffeq sg x l); |
|
320 |
|
321 |
|
322 |
|
323 (*==================================================*) |
|
324 (* Finding rho for modd_minusinfinity *) |
|
325 (*==================================================*) |
|
326 fun rho_for_modd_minf x dlcm sg fm1 = |
|
327 let |
|
328 (*Some certified Terms*) |
|
329 |
|
330 val ctrue = cterm_of sg HOLogic.true_const |
|
331 val cfalse = cterm_of sg HOLogic.false_const |
|
332 val fm = norm_zero_one fm1 |
|
333 in case fm1 of |
|
334 (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => |
|
335 if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf)) |
|
336 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) |
|
337 |
|
338 |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => |
|
339 if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one) |
|
340 then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) |
|
341 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) |
|
342 |
|
343 |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) => |
|
344 if (y=x) andalso (c1 = zero) then |
|
345 if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else |
|
346 (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf)) |
|
347 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) |
|
348 |
|
349 |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => |
|
350 if y=x then let val cz = cterm_of sg (norm_zero_one z) |
|
351 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero) |
|
352 in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf))) |
|
353 end |
|
354 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) |
|
355 |(Const("Divides.dvd",_)$ d $ (db as (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ |
|
356 c $ y ) $ z))) => |
|
357 if y=x then let val cz = cterm_of sg (norm_zero_one z) |
|
358 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero) |
|
359 in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf))) |
|
360 end |
|
361 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) |
|
362 |
|
363 |
|
364 |_ => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf) |
|
365 end; |
|
366 (*=========================================================================*) |
|
367 (*=========================================================================*) |
|
368 fun rho_for_eq_minf x dlcm sg fm1 = |
|
369 let |
|
370 val fm = norm_zero_one fm1 |
|
371 in case fm1 of |
|
372 (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => |
|
373 if (x=y) andalso (c1=zero) andalso (c2=one) |
|
374 then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_minf)) |
|
375 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) |
|
376 |
|
377 |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => |
|
378 if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one)) |
|
379 then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf)) |
|
380 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) |
|
381 |
|
382 |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) => |
|
383 if (y=x) andalso (c1 =zero) then |
|
384 if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else |
|
385 (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf)) |
|
386 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) |
|
387 |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => |
|
388 if y=x then let val cd = cterm_of sg (norm_zero_one d) |
|
389 val cz = cterm_of sg (norm_zero_one z) |
|
390 in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_minf)) |
|
391 end |
|
392 |
|
393 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) |
|
394 |
|
395 |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => |
|
396 if y=x then let val cd = cterm_of sg (norm_zero_one d) |
|
397 val cz = cterm_of sg (norm_zero_one z) |
|
398 in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf)) |
|
399 end |
|
400 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) |
|
401 |
|
402 |
|
403 |_ => (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) |
|
404 end; |
|
405 |
|
406 (*=====================================================*) |
|
407 (*=====================================================*) |
|
408 (*=========== minf proofs with the compact version==========*) |
|
409 fun decomp_minf_eq x dlcm sg t = case t of |
|
410 Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_conjI) |
|
411 |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_disjI) |
|
412 |_ => ([],fn [] => rho_for_eq_minf x dlcm sg t); |
|
413 |
|
414 fun decomp_minf_modd x dlcm sg t = case t of |
|
415 Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_conjI) |
|
416 |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_disjI) |
|
417 |_ => ([],fn [] => rho_for_modd_minf x dlcm sg t); |
|
418 |
|
419 (* -------------------------------------------------------------*) |
|
420 (* Finding rho for pinf_modd *) |
|
421 (* -------------------------------------------------------------*) |
|
422 fun rho_for_modd_pinf x dlcm sg fm1 = |
|
423 let |
|
424 (*Some certified Terms*) |
|
425 |
|
426 val ctrue = cterm_of sg HOLogic.true_const |
|
427 val cfalse = cterm_of sg HOLogic.false_const |
|
428 val fm = norm_zero_one fm1 |
|
429 in case fm1 of |
|
430 (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => |
|
431 if ((x=y) andalso (c1= zero) andalso (c2= one)) |
|
432 then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf)) |
|
433 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)) |
|
434 |
|
435 |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => |
|
436 if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero) andalso (c2 = one)) |
|
437 then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf)) |
|
438 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)) |
|
439 |
|
440 |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) => |
|
441 if ((y=x) andalso (c1 = zero)) then |
|
442 if (pm1 = one) |
|
443 then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf)) |
|
444 else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf)) |
|
445 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)) |
|
446 |
|
447 |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => |
|
448 if y=x then let val cz = cterm_of sg (norm_zero_one z) |
|
449 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero) |
|
450 in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf))) |
|
451 end |
|
452 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)) |
|
453 |(Const("Divides.dvd",_)$ d $ (db as (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ |
|
454 c $ y ) $ z))) => |
|
455 if y=x then let val cz = cterm_of sg (norm_zero_one z) |
|
456 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero) |
|
457 in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf))) |
|
458 end |
|
459 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)) |
|
460 |
|
461 |
|
462 |_ => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf) |
|
463 end; |
|
464 (* -------------------------------------------------------------*) |
|
465 (* Finding rho for pinf_eq *) |
|
466 (* -------------------------------------------------------------*) |
|
467 fun rho_for_eq_pinf x dlcm sg fm1 = |
|
468 let |
|
469 val fm = norm_zero_one fm1 |
|
470 in case fm1 of |
|
471 (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => |
|
472 if (x=y) andalso (c1=zero) andalso (c2=one) |
|
473 then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_pinf)) |
|
474 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) |
|
475 |
|
476 |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => |
|
477 if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one)) |
|
478 then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf)) |
|
479 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) |
|
480 |
|
481 |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) => |
|
482 if (y=x) andalso (c1 =zero) then |
|
483 if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else |
|
484 (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf)) |
|
485 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) |
|
486 |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => |
|
487 if y=x then let val cd = cterm_of sg (norm_zero_one d) |
|
488 val cz = cterm_of sg (norm_zero_one z) |
|
489 in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_pinf)) |
|
490 end |
|
491 |
|
492 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) |
|
493 |
|
494 |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => |
|
495 if y=x then let val cd = cterm_of sg (norm_zero_one d) |
|
496 val cz = cterm_of sg (norm_zero_one z) |
|
497 in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf)) |
|
498 end |
|
499 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) |
|
500 |
|
501 |
|
502 |_ => (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) |
|
503 end; |
|
504 |
|
505 |
|
506 |
|
507 fun minf_proof_of_c sg x dlcm t = |
|
508 let val minf_eqth = thm_of sg (decomp_minf_eq x dlcm sg) t |
|
509 val minf_moddth = thm_of sg (decomp_minf_modd x dlcm sg) t |
|
510 in (minf_eqth, minf_moddth) |
|
511 end; |
|
512 |
|
513 (*=========== pinf proofs with the compact version==========*) |
|
514 fun decomp_pinf_eq x dlcm sg t = case t of |
|
515 Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_conjI) |
|
516 |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_disjI) |
|
517 |_ =>([],fn [] => rho_for_eq_pinf x dlcm sg t) ; |
|
518 |
|
519 fun decomp_pinf_modd x dlcm sg t = case t of |
|
520 Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_conjI) |
|
521 |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_disjI) |
|
522 |_ => ([],fn [] => rho_for_modd_pinf x dlcm sg t); |
|
523 |
|
524 fun pinf_proof_of_c sg x dlcm t = |
|
525 let val pinf_eqth = thm_of sg (decomp_pinf_eq x dlcm sg) t |
|
526 val pinf_moddth = thm_of sg (decomp_pinf_modd x dlcm sg) t |
|
527 in (pinf_eqth,pinf_moddth) |
|
528 end; |
|
529 |
|
530 |
|
531 (* ------------------------------------------------------------------------- *) |
|
532 (* Here we generate the theorem for the Bset Property in the simple direction*) |
|
533 (* It is just an instantiation*) |
|
534 (* ------------------------------------------------------------------------- *) |
|
535 (* |
|
536 fun bsetproof_of sg (x as Free(xn,xT)) fm bs dlcm = |
|
537 let |
|
538 val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm))) |
|
539 val cdlcm = cterm_of sg dlcm |
|
540 val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs)) |
|
541 in instantiate' [] [SOME cdlcm,SOME cB, SOME cp] (bst_thm) |
|
542 end; |
|
543 |
|
544 fun asetproof_of sg (x as Free(xn,xT)) fm ast dlcm = |
|
545 let |
|
546 val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm))) |
|
547 val cdlcm = cterm_of sg dlcm |
|
548 val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast)) |
|
549 in instantiate' [] [SOME cdlcm,SOME cA, SOME cp] (ast_thm) |
|
550 end; |
|
551 *) |
|
552 |
|
553 (* For the generation of atomic Theorems*) |
|
554 (* Prove the premisses on runtime and then make RS*) |
|
555 (* ------------------------------------------------------------------------- *) |
|
556 |
|
557 (*========= this is rho ============*) |
|
558 fun generate_atomic_not_bst_p sg (x as Free(xn,xT)) fm dlcm B at = |
|
559 let |
|
560 val cdlcm = cterm_of sg dlcm |
|
561 val cB = cterm_of sg B |
|
562 val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm))) |
|
563 val cat = cterm_of sg (norm_zero_one at) |
|
564 in |
|
565 case at of |
|
566 (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => |
|
567 if (x=y) andalso (c1=zero) andalso (c2=one) |
|
568 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B) |
|
569 val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z))) |
|
570 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero ,dlcm)) |
|
571 in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne))) |
|
572 end |
|
573 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) |
|
574 |
|
575 |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, T) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => |
|
576 if (is_arith_rel at) andalso (x=y) |
|
577 then let |
|
578 val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_number 1))) |
|
579 in |
|
580 let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B) |
|
581 val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const(@{const_name HOL.minus},T) $ (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $ norm_zero_one z) $ HOLogic.mk_number HOLogic.intT 1)) |
|
582 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm)) |
|
583 in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq))) |
|
584 end |
|
585 end |
|
586 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) |
|
587 |
|
588 |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) => |
|
589 if (y=x) andalso (c1 =zero) then |
|
590 if pm1 = one then |
|
591 let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B) |
|
592 val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z))) |
|
593 in (instantiate' [] [SOME cfma, SOME cdlcm]([th1,th2] MRS (not_bst_p_gt))) |
|
594 end |
|
595 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm)) |
|
596 in (instantiate' [] [SOME cfma, SOME cB,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt))) |
|
597 end |
|
598 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) |
|
599 |
|
600 |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => |
|
601 if y=x then |
|
602 let val cz = cterm_of sg (norm_zero_one z) |
|
603 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) |
|
604 in (instantiate' [] [SOME cfma, SOME cB,SOME cz] (th1 RS (not_bst_p_ndvd))) |
|
605 end |
|
606 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) |
|
607 |
|
608 |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => |
|
609 if y=x then |
|
610 let val cz = cterm_of sg (norm_zero_one z) |
|
611 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) |
|
612 in (instantiate' [] [SOME cfma,SOME cB,SOME cz] (th1 RS (not_bst_p_dvd))) |
|
613 end |
|
614 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) |
|
615 |
|
616 |_ => (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) |
|
617 |
|
618 end; |
|
619 |
|
620 |
|
621 (* ------------------------------------------------------------------------- *) |
|
622 (* Main interpretation function for this backwards dirction*) |
|
623 (* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*) |
|
624 (*Help Function*) |
|
625 (* ------------------------------------------------------------------------- *) |
|
626 |
|
627 (*==================== Proof with the compact version *) |
|
628 |
|
629 fun decomp_nbstp sg x dlcm B fm t = case t of |
|
630 Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_conjI ) |
|
631 |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_disjI) |
|
632 |_ => ([], fn [] => generate_atomic_not_bst_p sg x fm dlcm B t); |
|
633 |
|
634 fun not_bst_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm B t = |
|
635 let |
|
636 val th = thm_of sg (decomp_nbstp sg x dlcm (list_to_set xT (map norm_zero_one B)) fm) t |
|
637 val fma = absfree (xn,xT, norm_zero_one fm) |
|
638 in let val th1 = prove_elementar sg "ss" (HOLogic.mk_eq (fma,fma)) |
|
639 in [th,th1] MRS (not_bst_p_Q_elim) |
|
640 end |
|
641 end; |
|
642 |
|
643 |
|
644 (* ------------------------------------------------------------------------- *) |
|
645 (* Protokol interpretation function for the backwards direction for cooper's Theorem*) |
|
646 |
|
647 (* For the generation of atomic Theorems*) |
|
648 (* Prove the premisses on runtime and then make RS*) |
|
649 (* ------------------------------------------------------------------------- *) |
|
650 (*========= this is rho ============*) |
|
651 fun generate_atomic_not_ast_p sg (x as Free(xn,xT)) fm dlcm A at = |
|
652 let |
|
653 val cdlcm = cterm_of sg dlcm |
|
654 val cA = cterm_of sg A |
|
655 val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm))) |
|
656 val cat = cterm_of sg (norm_zero_one at) |
|
657 in |
|
658 case at of |
|
659 (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => |
|
660 if (x=y) andalso (c1=zero) andalso (c2=one) |
|
661 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A) |
|
662 val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z))) |
|
663 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm)) |
|
664 in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne))) |
|
665 end |
|
666 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) |
|
667 |
|
668 |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, T) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => |
|
669 if (is_arith_rel at) andalso (x=y) |
|
670 then let val ast_z = norm_zero_one (linear_sub [] one z ) |
|
671 val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A) |
|
672 val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const(@{const_name HOL.plus},T) $ (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ one)) |
|
673 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm)) |
|
674 in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq))) |
|
675 end |
|
676 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) |
|
677 |
|
678 |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) => |
|
679 if (y=x) andalso (c1 =zero) then |
|
680 if pm1 = (mk_number ~1) then |
|
681 let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A) |
|
682 val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm)) |
|
683 in (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt))) |
|
684 end |
|
685 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm)) |
|
686 in (instantiate' [] [SOME cfma, SOME cA,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt))) |
|
687 end |
|
688 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) |
|
689 |
|
690 |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => |
|
691 if y=x then |
|
692 let val cz = cterm_of sg (norm_zero_one z) |
|
693 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) |
|
694 in (instantiate' [] [SOME cfma, SOME cA,SOME cz] (th1 RS (not_ast_p_ndvd))) |
|
695 end |
|
696 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) |
|
697 |
|
698 |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => |
|
699 if y=x then |
|
700 let val cz = cterm_of sg (norm_zero_one z) |
|
701 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) |
|
702 in (instantiate' [] [SOME cfma,SOME cA,SOME cz] (th1 RS (not_ast_p_dvd))) |
|
703 end |
|
704 else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) |
|
705 |
|
706 |_ => (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) |
|
707 |
|
708 end; |
|
709 |
|
710 (* ------------------------------------------------------------------------ *) |
|
711 (* Main interpretation function for this backwards dirction*) |
|
712 (* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*) |
|
713 (*Help Function*) |
|
714 (* ------------------------------------------------------------------------- *) |
|
715 |
|
716 fun decomp_nastp sg x dlcm A fm t = case t of |
|
717 Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_conjI ) |
|
718 |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_disjI) |
|
719 |_ => ([], fn [] => generate_atomic_not_ast_p sg x fm dlcm A t); |
|
720 |
|
721 fun not_ast_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm A t = |
|
722 let |
|
723 val th = thm_of sg (decomp_nastp sg x dlcm (list_to_set xT (map norm_zero_one A)) fm) t |
|
724 val fma = absfree (xn,xT, norm_zero_one fm) |
|
725 in let val th1 = prove_elementar sg "ss" (HOLogic.mk_eq (fma,fma)) |
|
726 in [th,th1] MRS (not_ast_p_Q_elim) |
|
727 end |
|
728 end; |
|
729 |
|
730 |
|
731 (* -------------------------------*) |
|
732 (* Finding rho and beta for evalc *) |
|
733 (* -------------------------------*) |
|
734 |
|
735 fun rho_for_evalc sg at = case at of |
|
736 (Const (p,_) $ s $ t) =>( |
|
737 case AList.lookup (op =) operations p of |
|
738 SOME f => |
|
739 ((if (f ((dest_number s),(dest_number t))) |
|
740 then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)) |
|
741 else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))) |
|
742 handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl) |
|
743 | _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl ) |
|
744 |Const("Not",_)$(Const (p,_) $ s $ t) =>( |
|
745 case AList.lookup (op =) operations p of |
|
746 SOME f => |
|
747 ((if (f ((dest_number s),(dest_number t))) |
|
748 then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)) |
|
749 else prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const))) |
|
750 handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl) |
|
751 | _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl ) |
|
752 | _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl; |
|
753 |
|
754 |
|
755 (*=========================================================*) |
|
756 fun decomp_evalc sg t = case t of |
|
757 (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI) |
|
758 |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI) |
|
759 |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI) |
|
760 |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI) |
|
761 |_ => ([], fn [] => rho_for_evalc sg t); |
|
762 |
|
763 |
|
764 fun proof_of_evalc sg fm = thm_of sg (decomp_evalc sg) fm; |
|
765 |
|
766 (*==================================================*) |
|
767 (* Proof of linform with the compact model *) |
|
768 (*==================================================*) |
|
769 |
|
770 |
|
771 fun decomp_linform sg vars t = case t of |
|
772 (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI) |
|
773 |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI) |
|
774 |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI) |
|
775 |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI) |
|
776 |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not) |
|
777 |(Const("Divides.dvd",_)$d$r) => |
|
778 if is_number d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd))) |
|
779 else (warning "Nonlinear Term --- Non numeral leftside at dvd"; |
|
780 raise COOPER) |
|
781 |_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t))); |
|
782 |
|
783 fun proof_of_linform sg vars f = thm_of sg (decomp_linform sg vars) f; |
|
784 |
|
785 (* ------------------------------------------------------------------------- *) |
|
786 (* Interpretaion of Protocols of the cooper procedure : minusinfinity version*) |
|
787 (* ------------------------------------------------------------------------- *) |
|
788 fun coopermi_proof_of sg (x as Free(xn,xT)) fm B dlcm = |
|
789 (* Get the Bset thm*) |
|
790 let val (minf_eqth, minf_moddth) = minf_proof_of_c sg x dlcm fm |
|
791 val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm)); |
|
792 val nbstpthm = not_bst_p_proof_of_c sg x fm dlcm B fm |
|
793 in (dpos,minf_eqth,nbstpthm,minf_moddth) |
|
794 end; |
|
795 |
|
796 (* ------------------------------------------------------------------------- *) |
|
797 (* Interpretaion of Protocols of the cooper procedure : plusinfinity version *) |
|
798 (* ------------------------------------------------------------------------- *) |
|
799 fun cooperpi_proof_of sg (x as Free(xn,xT)) fm A dlcm = |
|
800 let val (pinf_eqth,pinf_moddth) = pinf_proof_of_c sg x dlcm fm |
|
801 val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm)); |
|
802 val nastpthm = not_ast_p_proof_of_c sg x fm dlcm A fm |
|
803 in (dpos,pinf_eqth,nastpthm,pinf_moddth) |
|
804 end; |
|
805 |
|
806 (* ------------------------------------------------------------------------- *) |
|
807 (* Interpretaion of Protocols of the cooper procedure : full version*) |
|
808 (* ------------------------------------------------------------------------- *) |
|
809 fun cooper_thm sg s (x as Free(xn,xT)) cfm dlcm ast bst= case s of |
|
810 "pi" => let val (dpsthm,pinf_eqth,nbpth,pinf_moddth) = cooperpi_proof_of sg x cfm ast dlcm |
|
811 in [dpsthm,pinf_eqth,nbpth,pinf_moddth] MRS (cppi_eq) |
|
812 end |
|
813 |"mi" => let val (dpsthm,minf_eqth,nbpth,minf_moddth) = coopermi_proof_of sg x cfm bst dlcm |
|
814 in [dpsthm,minf_eqth,nbpth,minf_moddth] MRS (cpmi_eq) |
|
815 end |
|
816 |_ => error "parameter error"; |
|
817 |
|
818 (* ------------------------------------------------------------------------- *) |
|
819 (* This function should evoluate to the end prove Procedure for one quantifier elimination for Presburger arithmetic*) |
|
820 (* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*) |
|
821 (* ------------------------------------------------------------------------- *) |
|
822 |
|
823 (* val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();*) |
|
824 (* val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer(); *) |
|
825 |
|
826 fun cooper_prv sg (x as Free(xn,xT)) efm = let |
|
827 (* lfm_thm : efm = linearized form of efm*) |
|
828 val lfm_thm = proof_of_linform sg [xn] efm |
|
829 (*efm2 is the linearized form of efm *) |
|
830 val efm2 = snd(qe_get_terms lfm_thm) |
|
831 (* l is the lcm of all coefficients of x *) |
|
832 val l = formlcm x efm2 |
|
833 (*ac_thm: efm = efm2 with adjusted coefficients of x *) |
|
834 val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans |
|
835 (* fm is efm2 with adjusted coefficients of x *) |
|
836 val fm = snd (qe_get_terms ac_thm) |
|
837 (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*) |
|
838 val cfm = unitycoeff x fm |
|
839 (*afm is fm where c*x is replaced by 1*x or -1*x *) |
|
840 val afm = adjustcoeff x l fm |
|
841 (* P = %x.afm*) |
|
842 val P = absfree(xn,xT,afm) |
|
843 (* This simpset allows the elimination of the sets in bex {1..d} *) |
|
844 val ss = presburger_ss addsimps |
|
845 [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff] |
|
846 (* uth : EX x.P(l*x) = EX x. l dvd x & P x*) |
|
847 val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_number l))] (unity_coeff_ex) |
|
848 (* e_ac_thm : Ex x. efm = EX x. fm*) |
|
849 val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI) |
|
850 (* A and B set of the formula*) |
|
851 val A = aset x cfm |
|
852 val B = bset x cfm |
|
853 (* the divlcm (delta) of the formula*) |
|
854 val dlcm = mk_number (divlcm x cfm) |
|
855 (* Which set is smaller to generate the (hoepfully) shorter proof*) |
|
856 val cms = if ((length A) < (length B )) then "pi" else "mi" |
|
857 (* val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"*) |
|
858 (* synthesize the proof of cooper's theorem*) |
|
859 (* cp_thm: EX x. cfm = Q*) |
|
860 val cp_thm = cooper_thm sg cms x cfm dlcm A B |
|
861 (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*) |
|
862 (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*) |
|
863 (* |
|
864 val _ = prth cp_thm |
|
865 val _ = writeln "Expanding the bounded EX..." |
|
866 *) |
|
867 val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans))) |
|
868 (* |
|
869 val _ = writeln "Expanded" *) |
|
870 (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*) |
|
871 val (lsuth,rsuth) = qe_get_terms (uth) |
|
872 (* lseacth = EX x. efm; rseacth = EX x. fm*) |
|
873 val (lseacth,rseacth) = qe_get_terms(e_ac_thm) |
|
874 (* lscth = EX x. cfm; rscth = Q' *) |
|
875 val (lscth,rscth) = qe_get_terms (exp_cp_thm) |
|
876 (* u_c_thm: EX x. P(l*x) = Q'*) |
|
877 val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans |
|
878 (* result: EX x. efm = Q'*) |
|
879 in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans) |
|
880 end |
|
881 |cooper_prv _ _ _ = error "Parameters format"; |
|
882 |
|
883 (* **************************************** *) |
|
884 (* An Other Version of cooper proving *) |
|
885 (* by giving a withness for EX *) |
|
886 (* **************************************** *) |
|
887 |
|
888 |
|
889 |
|
890 fun cooper_prv_w sg (x as Free(xn,xT)) efm = let |
|
891 (* lfm_thm : efm = linearized form of efm*) |
|
892 val lfm_thm = proof_of_linform sg [xn] efm |
|
893 (*efm2 is the linearized form of efm *) |
|
894 val efm2 = snd(qe_get_terms lfm_thm) |
|
895 (* l is the lcm of all coefficients of x *) |
|
896 val l = formlcm x efm2 |
|
897 (*ac_thm: efm = efm2 with adjusted coefficients of x *) |
|
898 val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans |
|
899 (* fm is efm2 with adjusted coefficients of x *) |
|
900 val fm = snd (qe_get_terms ac_thm) |
|
901 (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*) |
|
902 val cfm = unitycoeff x fm |
|
903 (*afm is fm where c*x is replaced by 1*x or -1*x *) |
|
904 val afm = adjustcoeff x l fm |
|
905 (* P = %x.afm*) |
|
906 val P = absfree(xn,xT,afm) |
|
907 (* This simpset allows the elimination of the sets in bex {1..d} *) |
|
908 val ss = presburger_ss addsimps |
|
909 [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff] |
|
910 (* uth : EX x.P(l*x) = EX x. l dvd x & P x*) |
|
911 val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_number l))] (unity_coeff_ex) |
|
912 (* e_ac_thm : Ex x. efm = EX x. fm*) |
|
913 val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI) |
|
914 (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*) |
|
915 val (lsuth,rsuth) = qe_get_terms (uth) |
|
916 (* lseacth = EX x. efm; rseacth = EX x. fm*) |
|
917 val (lseacth,rseacth) = qe_get_terms(e_ac_thm) |
|
918 |
|
919 val (w,rs) = cooper_w [] cfm |
|
920 val exp_cp_thm = case w of |
|
921 (* FIXME - e_ac_thm just tipped to test syntactical correctness of the program!!!!*) |
|
922 SOME n => e_ac_thm (* Prove cfm (n) and use exI and then Eq_TrueI*) |
|
923 |_ => let |
|
924 (* A and B set of the formula*) |
|
925 val A = aset x cfm |
|
926 val B = bset x cfm |
|
927 (* the divlcm (delta) of the formula*) |
|
928 val dlcm = mk_number (divlcm x cfm) |
|
929 (* Which set is smaller to generate the (hoepfully) shorter proof*) |
|
930 val cms = if ((length A) < (length B )) then "pi" else "mi" |
|
931 (* synthesize the proof of cooper's theorem*) |
|
932 (* cp_thm: EX x. cfm = Q*) |
|
933 val cp_thm = cooper_thm sg cms x cfm dlcm A B |
|
934 (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*) |
|
935 (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*) |
|
936 in refl RS (simplify ss (cp_thm RSN (2,trans))) |
|
937 end |
|
938 (* lscth = EX x. cfm; rscth = Q' *) |
|
939 val (lscth,rscth) = qe_get_terms (exp_cp_thm) |
|
940 (* u_c_thm: EX x. P(l*x) = Q'*) |
|
941 val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans |
|
942 (* result: EX x. efm = Q'*) |
|
943 in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans) |
|
944 end |
|
945 |cooper_prv_w _ _ _ = error "Parameters format"; |
|
946 |
|
947 |
|
948 |
|
949 fun decomp_cnnf sg lfnp P = case P of |
|
950 Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI ) |
|
951 |Const ("op |",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_disjI) |
|
952 |Const ("Not",_) $ (Const("Not",_) $ p) => ([p], fn [th] => th RS nnf_nn) |
|
953 |Const("Not",_) $ (Const(opn,T) $ p $ q) => |
|
954 if opn = "op |" |
|
955 then case (p,q) of |
|
956 (A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) => |
|
957 if r1 = negate r |
|
958 then ([r,HOLogic.Not$s,r1,HOLogic.Not$t],fn [th1_1,th1_2,th2_1,th2_2] => [[th1_1,th1_1] MRS qe_conjI,[th2_1,th2_2] MRS qe_conjI] MRS nnf_sdj) |
|
959 |
|
960 else ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj) |
|
961 |(_,_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj) |
|
962 else ( |
|
963 case (opn,T) of |
|
964 ("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_ncj ) |
|
965 |("op -->",_) => ([p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_nim ) |
|
966 |("op =",Type ("fun",[Type ("bool", []),_])) => |
|
967 ([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q], fn [th1,th2] => [th1,th2] MRS nnf_neq) |
|
968 |(_,_) => ([], fn [] => lfnp P) |
|
969 ) |
|
970 |
|
971 |(Const ("op -->",_) $ p $ q) => ([HOLogic.Not$p,q], fn [th1,th2] => [th1,th2] MRS nnf_im) |
|
972 |
|
973 |(Const ("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q) => |
|
974 ([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], fn [th1,th2] =>[th1,th2] MRS nnf_eq ) |
|
975 |_ => ([], fn [] => lfnp P); |
|
976 |
|
977 |
|
978 |
|
979 |
|
980 fun proof_of_cnnf sg p lfnp = |
|
981 let val th1 = thm_of sg (decomp_cnnf sg lfnp) p |
|
982 val rs = snd(qe_get_terms th1) |
|
983 val th2 = prove_elementar sg "ss" (HOLogic.mk_eq(rs,simpl rs)) |
|
984 in [th1,th2] MRS trans |
|
985 end; |
|
986 |
|
987 end; |
|
988 |
|