1 (* Title: HOL/Integ/cooper_proof.ML
3 Author: Amine Chaieb and Tobias Nipkow, TU Muenchen
5 File containing the implementation of the proof
6 generation for Cooper Algorithm
10 signature COOPER_PROOF =
18 val list_to_set : typ -> term list -> term
19 val qe_get_terms : thm -> term * term
20 val cooper_prv : Sign.sg -> term -> term -> thm
21 val cooper_prv2 : Sign.sg -> term -> term -> thm
22 val proof_of_evalc : Sign.sg -> term -> thm
23 val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
24 val proof_of_linform : Sign.sg -> string list -> term -> thm
25 val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
26 val prove_elementar : Sign.sg -> string -> term -> thm
27 val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
30 structure CooperProof : COOPER_PROOF =
35 val presburger_ss = simpset_of (theory "Presburger")
36 addsimps [zdiff_def] delsimps [symmetric zdiff_def];
39 val presburger_ss = simpset_of (theory "Presburger")
40 addsimps[diff_int_def] delsimps [thm"diff_int_def_symmetric"];
41 val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
43 (*Theorems that will be used later for the proofgeneration*)
45 val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
46 val unity_coeff_ex = thm "unity_coeff_ex";
48 (* Thorems for proving the adjustment of the coeffitients*)
50 val ac_lt_eq = thm "ac_lt_eq";
51 val ac_eq_eq = thm "ac_eq_eq";
52 val ac_dvd_eq = thm "ac_dvd_eq";
53 val ac_pi_eq = thm "ac_pi_eq";
55 (* The logical compination of the sythetised properties*)
56 val qe_Not = thm "qe_Not";
57 val qe_conjI = thm "qe_conjI";
58 val qe_disjI = thm "qe_disjI";
59 val qe_impI = thm "qe_impI";
60 val qe_eqI = thm "qe_eqI";
61 val qe_exI = thm "qe_exI";
62 val qe_ALLI = thm "qe_ALLI";
64 (*Modulo D property for Pminusinf an Plusinf *)
65 val fm_modd_minf = thm "fm_modd_minf";
66 val not_dvd_modd_minf = thm "not_dvd_modd_minf";
67 val dvd_modd_minf = thm "dvd_modd_minf";
69 val fm_modd_pinf = thm "fm_modd_pinf";
70 val not_dvd_modd_pinf = thm "not_dvd_modd_pinf";
71 val dvd_modd_pinf = thm "dvd_modd_pinf";
73 (* the minusinfinity proprty*)
75 val fm_eq_minf = thm "fm_eq_minf";
76 val neq_eq_minf = thm "neq_eq_minf";
77 val eq_eq_minf = thm "eq_eq_minf";
78 val le_eq_minf = thm "le_eq_minf";
79 val len_eq_minf = thm "len_eq_minf";
80 val not_dvd_eq_minf = thm "not_dvd_eq_minf";
81 val dvd_eq_minf = thm "dvd_eq_minf";
83 (* the Plusinfinity proprty*)
85 val fm_eq_pinf = thm "fm_eq_pinf";
86 val neq_eq_pinf = thm "neq_eq_pinf";
87 val eq_eq_pinf = thm "eq_eq_pinf";
88 val le_eq_pinf = thm "le_eq_pinf";
89 val len_eq_pinf = thm "len_eq_pinf";
90 val not_dvd_eq_pinf = thm "not_dvd_eq_pinf";
91 val dvd_eq_pinf = thm "dvd_eq_pinf";
93 (*Logical construction of the Property*)
94 val eq_minf_conjI = thm "eq_minf_conjI";
95 val eq_minf_disjI = thm "eq_minf_disjI";
96 val modd_minf_disjI = thm "modd_minf_disjI";
97 val modd_minf_conjI = thm "modd_minf_conjI";
99 val eq_pinf_conjI = thm "eq_pinf_conjI";
100 val eq_pinf_disjI = thm "eq_pinf_disjI";
101 val modd_pinf_disjI = thm "modd_pinf_disjI";
102 val modd_pinf_conjI = thm "modd_pinf_conjI";
104 (*Cooper Backwards...*)
106 val not_bst_p_fm = thm "not_bst_p_fm";
107 val not_bst_p_ne = thm "not_bst_p_ne";
108 val not_bst_p_eq = thm "not_bst_p_eq";
109 val not_bst_p_gt = thm "not_bst_p_gt";
110 val not_bst_p_lt = thm "not_bst_p_lt";
111 val not_bst_p_ndvd = thm "not_bst_p_ndvd";
112 val not_bst_p_dvd = thm "not_bst_p_dvd";
115 val not_ast_p_fm = thm "not_ast_p_fm";
116 val not_ast_p_ne = thm "not_ast_p_ne";
117 val not_ast_p_eq = thm "not_ast_p_eq";
118 val not_ast_p_gt = thm "not_ast_p_gt";
119 val not_ast_p_lt = thm "not_ast_p_lt";
120 val not_ast_p_ndvd = thm "not_ast_p_ndvd";
121 val not_ast_p_dvd = thm "not_ast_p_dvd";
123 (*Logical construction of the prop*)
125 val not_bst_p_conjI = thm "not_bst_p_conjI";
126 val not_bst_p_disjI = thm "not_bst_p_disjI";
127 val not_bst_p_Q_elim = thm "not_bst_p_Q_elim";
130 val not_ast_p_conjI = thm "not_ast_p_conjI";
131 val not_ast_p_disjI = thm "not_ast_p_disjI";
132 val not_ast_p_Q_elim = thm "not_ast_p_Q_elim";
135 val cppi_eq = thm "cppi_eq";
136 val cpmi_eq = thm "cpmi_eq";
139 val simp_from_to = thm "simp_from_to";
140 val P_eqtrue = thm "P_eqtrue";
141 val P_eqfalse = thm "P_eqfalse";
145 val nnf_nn = thm "nnf_nn";
146 val nnf_im = thm "nnf_im";
147 val nnf_eq = thm "nnf_eq";
148 val nnf_sdj = thm "nnf_sdj";
149 val nnf_ncj = thm "nnf_ncj";
150 val nnf_nim = thm "nnf_nim";
151 val nnf_neq = thm "nnf_neq";
152 val nnf_ndj = thm "nnf_ndj";
154 (*For Proving term linearizition*)
155 val linearize_dvd = thm "linearize_dvd";
156 val lf_lt = thm "lf_lt";
157 val lf_eq = thm "lf_eq";
158 val lf_dvd = thm "lf_dvd";
161 (* ------------------------------------------------------------------------- *)
162 (*This function norm_zero_one replaces the occurences of Numeral1 and Numeral0*)
163 (*Respectively by their abstract representation Const("1",..) and COnst("0",..)*)
164 (*this is necessary because the theorems use this representation.*)
165 (* This function should be elminated in next versions...*)
166 (* ------------------------------------------------------------------------- *)
168 fun norm_zero_one fm = case fm of
169 (Const ("op *",_) $ c $ t) =>
170 if c = one then (norm_zero_one t)
171 else if (dest_numeral c = ~1)
172 then (Const("uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
173 else (HOLogic.mk_binop "op *" (norm_zero_one c,norm_zero_one t))
174 |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
175 |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
178 (* ------------------------------------------------------------------------- *)
179 (*function list to Set, constructs a set containing all elements of a given list.*)
180 (* ------------------------------------------------------------------------- *)
181 fun list_to_set T1 l = let val T = (HOLogic.mk_setT T1) in
184 |(h::t) => Const("insert", T1 --> (T --> T)) $ h $(list_to_set T1 t)
187 (* ------------------------------------------------------------------------- *)
188 (* Returns both sides of an equvalence in the theorem*)
189 (* ------------------------------------------------------------------------- *)
190 fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end;
192 (* ------------------------------------------------------------------------- *)
193 (* Modified version of the simple version with minimal amount of checking and postprocessing*)
194 (* ------------------------------------------------------------------------- *)
196 fun simple_prove_goal_cterm2 G tacs =
198 fun check None = error "prove_goal: tactic failed"
199 | check (Some (thm, _)) = (case nprems_of thm of
201 | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
202 in check (Seq.pull (EVERY tacs (trivial G))) end;
204 (*-------------------------------------------------------------*)
205 (*-------------------------------------------------------------*)
207 fun cert_Trueprop sg t = cterm_of sg (HOLogic.mk_Trueprop t);
209 (* ------------------------------------------------------------------------- *)
210 (*This function proove elementar will be used to generate proofs at runtime*)
211 (*It is is based on the isabelle function proove_goalw_cterm and is thought to *)
212 (*prove properties such as a dvd b (essentially) that are only to make at
214 (* ------------------------------------------------------------------------- *)
215 fun prove_elementar sg s fm2 = case s of
216 (*"ss" like simplification with simpset*)
219 val ss = presburger_ss addsimps
220 [zdvd_iff_zmod_eq_0,unity_coeff_ex]
221 val ct = cert_Trueprop sg fm2
223 simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
227 (*"bl" like blast tactic*)
228 (* Is only used in the harrisons like proof procedure *)
230 let val ct = cert_Trueprop sg fm2
232 simple_prove_goal_cterm2 ct [blast_tac HOL_cs 1]
235 (*"ed" like Existence disjunctions ...*)
236 (* Is only used in the harrisons like proof procedure *)
241 val tac1 = EVERY[REPEAT(resolve_tac [disjI1,disjI2] 1), etac exI 1]
242 val tac2 = EVERY[etac exE 1, rtac exI 1,
243 REPEAT(resolve_tac [disjI1,disjI2] 1), assumption 1]
245 etac exE 1, REPEAT(EVERY[etac disjE 1, tac1]), tac1,
246 REPEAT(EVERY[etac disjE 1, tac2]), tac2]
249 val ct = cert_Trueprop sg fm2
251 simple_prove_goal_cterm2 ct ex_disj_tacs
255 let val ct = cert_Trueprop sg fm2
256 in simple_prove_goal_cterm2 ct [simple_arith_tac 1]
262 val ss = presburger_ss addsimps zadd_ac
263 val ct = cert_Trueprop sg fm2
265 simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
268 (* like Existance Conjunction *)
271 val ss = presburger_ss addsimps zadd_ac
272 val ct = cert_Trueprop sg fm2
274 simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (blast_tac HOL_cs 1)]
279 val ss = HOL_basic_ss addsimps zadd_ac
280 val ct = cert_Trueprop sg fm2
282 simple_prove_goal_cterm2 ct [simp_tac ss 1]
287 val ss = presburger_ss addsimps zadd_ac
288 val ct = cert_Trueprop sg fm2
290 simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
294 (*=============================================================*)
295 (*-------------------------------------------------------------*)
296 (* The new compact model *)
297 (*-------------------------------------------------------------*)
298 (*=============================================================*)
300 fun thm_of sg decomp t =
301 let val (ts,recomb) = decomp t
302 in recomb (map (thm_of sg decomp) ts)
305 (*==================================================*)
306 (* Compact Version for adjustcoeffeq *)
307 (*==================================================*)
309 fun decomp_adjustcoeffeq sg x l fm = case fm of
310 (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $ c $ y ) $z )))) =>
312 val m = l div (dest_numeral c)
313 val n = if (x = y) then abs (m) else 1
314 val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
316 then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
317 else HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )
318 val ck = cterm_of sg (mk_numeral n)
319 val cc = cterm_of sg c
320 val ct = cterm_of sg z
321 val cx = cterm_of sg y
322 val pre = prove_elementar sg "lf"
323 (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral n)))
324 val th1 = (pre RS (instantiate' [] [Some ck,Some cc, Some cx, Some ct] (ac_pi_eq)))
325 in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
328 |(Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $
330 if (is_arith_rel fm) andalso (x = y)
332 let val m = l div (dest_numeral c)
333 val k = (if p = "op <" then abs(m) else m)
334 val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div k)*l) ), x))
335 val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul k t) ))))
337 val ck = cterm_of sg (mk_numeral k)
338 val cc = cterm_of sg c
339 val ct = cterm_of sg t
340 val cx = cterm_of sg x
341 val ca = cterm_of sg a
346 let val pre = prove_elementar sg "lf"
347 (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
348 val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_lt_eq)))
349 in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
353 let val pre = prove_elementar sg "lf"
354 (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
355 val th1 = (pre RS(instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_eq_eq)))
356 in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
360 let val pre = prove_elementar sg "lf"
361 (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
362 val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct]) (ac_dvd_eq))
363 in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
367 else ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl)
369 |( Const ("Not", _) $ p) => ([p], fn [th] => th RS qe_Not)
370 |( Const ("op &",_) $ p $ q) => ([p,q], fn [th1,th2] => [th1,th2] MRS qe_conjI)
371 |( Const ("op |",_) $ p $ q) =>([p,q], fn [th1,th2] => [th1,th2] MRS qe_disjI)
373 |_ => ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl);
375 fun proof_of_adjustcoeffeq sg x l = thm_of sg (decomp_adjustcoeffeq sg x l);
379 (*==================================================*)
380 (* Finding rho for modd_minusinfinity *)
381 (*==================================================*)
382 fun rho_for_modd_minf x dlcm sg fm1 =
384 (*Some certified Terms*)
386 val ctrue = cterm_of sg HOLogic.true_const
387 val cfalse = cterm_of sg HOLogic.false_const
388 val fm = norm_zero_one fm1
390 (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
391 if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [Some cboolT] [Some ctrue] (fm_modd_minf))
392 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
394 |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
395 if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one)
396 then (instantiate' [Some cboolT] [Some cfalse] (fm_modd_minf))
397 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
399 |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
400 if (y=x) andalso (c1 = zero) then
401 if (pm1 = one) then (instantiate' [Some cboolT] [Some cfalse] (fm_modd_minf)) else
402 (instantiate' [Some cboolT] [Some ctrue] (fm_modd_minf))
403 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
405 |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
406 if y=x then let val cz = cterm_of sg (norm_zero_one z)
407 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
408 in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
410 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
411 |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
413 if y=x then let val cz = cterm_of sg (norm_zero_one z)
414 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
415 in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf)))
417 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
420 |_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf)
422 (*=========================================================================*)
423 (*=========================================================================*)
424 fun rho_for_eq_minf x dlcm sg fm1 =
426 val fm = norm_zero_one fm1
428 (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
429 if (x=y) andalso (c1=zero) andalso (c2=one)
430 then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
431 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
433 |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
434 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))
435 then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
436 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
438 |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
439 if (y=x) andalso (c1 =zero) then
440 if pm1 = one then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
441 (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (len_eq_minf))
442 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
443 |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
444 if y=x then let val cd = cterm_of sg (norm_zero_one d)
445 val cz = cterm_of sg (norm_zero_one z)
446 in(instantiate' [] [Some cd, Some cz] (not_dvd_eq_minf))
449 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
451 |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
452 if y=x then let val cd = cterm_of sg (norm_zero_one d)
453 val cz = cterm_of sg (norm_zero_one z)
454 in(instantiate' [] [Some cd, Some cz ] (dvd_eq_minf))
456 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
459 |_ => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
462 (*=====================================================*)
463 (*=====================================================*)
464 (*=========== minf proofs with the compact version==========*)
465 fun decomp_minf_eq x dlcm sg t = case t of
466 Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_conjI)
467 |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_disjI)
468 |_ => ([],fn [] => rho_for_eq_minf x dlcm sg t);
470 fun decomp_minf_modd x dlcm sg t = case t of
471 Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_conjI)
472 |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_disjI)
473 |_ => ([],fn [] => rho_for_modd_minf x dlcm sg t);
475 (* -------------------------------------------------------------*)
476 (* Finding rho for pinf_modd *)
477 (* -------------------------------------------------------------*)
478 fun rho_for_modd_pinf x dlcm sg fm1 =
480 (*Some certified Terms*)
482 val ctrue = cterm_of sg HOLogic.true_const
483 val cfalse = cterm_of sg HOLogic.false_const
484 val fm = norm_zero_one fm1
486 (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
487 if ((x=y) andalso (c1= zero) andalso (c2= one))
488 then (instantiate' [Some cboolT] [Some ctrue] (fm_modd_pinf))
489 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
491 |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
492 if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero) andalso (c2 = one))
493 then (instantiate' [Some cboolT] [Some cfalse] (fm_modd_pinf))
494 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
496 |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
497 if ((y=x) andalso (c1 = zero)) then
499 then (instantiate' [Some cboolT] [Some ctrue] (fm_modd_pinf))
500 else (instantiate' [Some cboolT] [Some cfalse] (fm_modd_pinf))
501 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
503 |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
504 if y=x then let val cz = cterm_of sg (norm_zero_one z)
505 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
506 in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
508 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
509 |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
511 if y=x then let val cz = cterm_of sg (norm_zero_one z)
512 val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
513 in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf)))
515 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
518 |_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf)
520 (* -------------------------------------------------------------*)
521 (* Finding rho for pinf_eq *)
522 (* -------------------------------------------------------------*)
523 fun rho_for_eq_pinf x dlcm sg fm1 =
525 val fm = norm_zero_one fm1
527 (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
528 if (x=y) andalso (c1=zero) andalso (c2=one)
529 then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
530 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
532 |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
533 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))
534 then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
535 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
537 |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
538 if (y=x) andalso (c1 =zero) then
539 if pm1 = one then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
540 (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
541 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
542 |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
543 if y=x then let val cd = cterm_of sg (norm_zero_one d)
544 val cz = cterm_of sg (norm_zero_one z)
545 in(instantiate' [] [Some cd, Some cz] (not_dvd_eq_pinf))
548 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
550 |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
551 if y=x then let val cd = cterm_of sg (norm_zero_one d)
552 val cz = cterm_of sg (norm_zero_one z)
553 in(instantiate' [] [Some cd, Some cz ] (dvd_eq_pinf))
555 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
558 |_ => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
563 fun minf_proof_of_c sg x dlcm t =
564 let val minf_eqth = thm_of sg (decomp_minf_eq x dlcm sg) t
565 val minf_moddth = thm_of sg (decomp_minf_modd x dlcm sg) t
566 in (minf_eqth, minf_moddth)
569 (*=========== pinf proofs with the compact version==========*)
570 fun decomp_pinf_eq x dlcm sg t = case t of
571 Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_conjI)
572 |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_disjI)
573 |_ =>([],fn [] => rho_for_eq_pinf x dlcm sg t) ;
575 fun decomp_pinf_modd x dlcm sg t = case t of
576 Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_conjI)
577 |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_disjI)
578 |_ => ([],fn [] => rho_for_modd_pinf x dlcm sg t);
580 fun pinf_proof_of_c sg x dlcm t =
581 let val pinf_eqth = thm_of sg (decomp_pinf_eq x dlcm sg) t
582 val pinf_moddth = thm_of sg (decomp_pinf_modd x dlcm sg) t
583 in (pinf_eqth,pinf_moddth)
587 (* ------------------------------------------------------------------------- *)
588 (* Here we generate the theorem for the Bset Property in the simple direction*)
589 (* It is just an instantiation*)
590 (* ------------------------------------------------------------------------- *)
592 fun bsetproof_of sg (x as Free(xn,xT)) fm bs dlcm =
594 val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
595 val cdlcm = cterm_of sg dlcm
596 val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs))
597 in instantiate' [] [Some cdlcm,Some cB, Some cp] (bst_thm)
600 fun asetproof_of sg (x as Free(xn,xT)) fm ast dlcm =
602 val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
603 val cdlcm = cterm_of sg dlcm
604 val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast))
605 in instantiate' [] [Some cdlcm,Some cA, Some cp] (ast_thm)
609 (* For the generation of atomic Theorems*)
610 (* Prove the premisses on runtime and then make RS*)
611 (* ------------------------------------------------------------------------- *)
613 (*========= this is rho ============*)
614 fun generate_atomic_not_bst_p sg (x as Free(xn,xT)) fm dlcm B at =
616 val cdlcm = cterm_of sg dlcm
617 val cB = cterm_of sg B
618 val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
619 val cat = cterm_of sg (norm_zero_one at)
622 (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
623 if (x=y) andalso (c1=zero) andalso (c2=one)
624 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)
625 val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
626 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
627 in (instantiate' [] [Some cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
629 else (instantiate' [] [Some cfma, Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
631 |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
632 if (is_arith_rel at) andalso (x=y)
633 then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
634 in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
635 val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("op -",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
636 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
637 in (instantiate' [] [Some cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
640 else (instantiate' [] [Some cfma, Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
642 |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
643 if (y=x) andalso (c1 =zero) then
645 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)
646 val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
647 in (instantiate' [] [Some cfma, Some cdlcm]([th1,th2] MRS (not_bst_p_gt)))
649 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
650 in (instantiate' [] [Some cfma, Some cB,Some (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt)))
652 else (instantiate' [] [Some cfma, Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
654 |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
656 let val cz = cterm_of sg (norm_zero_one z)
657 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
658 in (instantiate' [] [Some cfma, Some cB,Some cz] (th1 RS (not_bst_p_ndvd)))
660 else (instantiate' [] [Some cfma, Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
662 |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
664 let val cz = cterm_of sg (norm_zero_one z)
665 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
666 in (instantiate' [] [Some cfma,Some cB,Some cz] (th1 RS (not_bst_p_dvd)))
668 else (instantiate' [] [Some cfma, Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
670 |_ => (instantiate' [] [Some cfma, Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
675 (* ------------------------------------------------------------------------- *)
676 (* Main interpretation function for this backwards dirction*)
677 (* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
679 (* ------------------------------------------------------------------------- *)
681 (*==================== Proof with the compact version *)
683 fun decomp_nbstp sg x dlcm B fm t = case t of
684 Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_conjI )
685 |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_disjI)
686 |_ => ([], fn [] => generate_atomic_not_bst_p sg x fm dlcm B t);
688 fun not_bst_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm B t =
690 val th = thm_of sg (decomp_nbstp sg x dlcm (list_to_set xT (map norm_zero_one B)) fm) t
691 val fma = absfree (xn,xT, norm_zero_one fm)
692 in let val th1 = prove_elementar sg "ss" (HOLogic.mk_eq (fma,fma))
693 in [th,th1] MRS (not_bst_p_Q_elim)
698 (* ------------------------------------------------------------------------- *)
699 (* Protokol interpretation function for the backwards direction for cooper's Theorem*)
701 (* For the generation of atomic Theorems*)
702 (* Prove the premisses on runtime and then make RS*)
703 (* ------------------------------------------------------------------------- *)
704 (*========= this is rho ============*)
705 fun generate_atomic_not_ast_p sg (x as Free(xn,xT)) fm dlcm A at =
707 val cdlcm = cterm_of sg dlcm
708 val cA = cterm_of sg A
709 val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
710 val cat = cterm_of sg (norm_zero_one at)
713 (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
714 if (x=y) andalso (c1=zero) andalso (c2=one)
715 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)
716 val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
717 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
718 in (instantiate' [] [Some cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
720 else (instantiate' [] [Some cfma, Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
722 |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
723 if (is_arith_rel at) andalso (x=y)
724 then let val ast_z = norm_zero_one (linear_sub [] one z )
725 val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
726 val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("op +",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
727 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
728 in (instantiate' [] [Some cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
730 else (instantiate' [] [Some cfma, Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
732 |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
733 if (y=x) andalso (c1 =zero) then
734 if pm1 = (mk_numeral ~1) then
735 let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
736 val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm))
737 in (instantiate' [] [Some cfma]([th2,th1] MRS (not_ast_p_lt)))
739 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
740 in (instantiate' [] [Some cfma, Some cA,Some (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt)))
742 else (instantiate' [] [Some cfma, Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
744 |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
746 let val cz = cterm_of sg (norm_zero_one z)
747 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
748 in (instantiate' [] [Some cfma, Some cA,Some cz] (th1 RS (not_ast_p_ndvd)))
750 else (instantiate' [] [Some cfma, Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
752 |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) =>
754 let val cz = cterm_of sg (norm_zero_one z)
755 val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
756 in (instantiate' [] [Some cfma,Some cA,Some cz] (th1 RS (not_ast_p_dvd)))
758 else (instantiate' [] [Some cfma, Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
760 |_ => (instantiate' [] [Some cfma, Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
764 (* ------------------------------------------------------------------------ *)
765 (* Main interpretation function for this backwards dirction*)
766 (* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
768 (* ------------------------------------------------------------------------- *)
770 fun decomp_nastp sg x dlcm A fm t = case t of
771 Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_conjI )
772 |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_disjI)
773 |_ => ([], fn [] => generate_atomic_not_ast_p sg x fm dlcm A t);
775 fun not_ast_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm A t =
777 val th = thm_of sg (decomp_nastp sg x dlcm (list_to_set xT (map norm_zero_one A)) fm) t
778 val fma = absfree (xn,xT, norm_zero_one fm)
779 in let val th1 = prove_elementar sg "ss" (HOLogic.mk_eq (fma,fma))
780 in [th,th1] MRS (not_ast_p_Q_elim)
785 (* -------------------------------*)
786 (* Finding rho and beta for evalc *)
787 (* -------------------------------*)
789 fun rho_for_evalc sg at = case at of
790 (Const (p,_) $ s $ t) =>(
791 case assoc (operations,p) of
793 ((if (f ((dest_numeral s),(dest_numeral t)))
794 then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const))
795 else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)))
796 handle _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl)
797 | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl )
798 |Const("Not",_)$(Const (p,_) $ s $ t) =>(
799 case assoc (operations,p) of
801 ((if (f ((dest_numeral s),(dest_numeral t)))
802 then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))
803 else prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)))
804 handle _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl)
805 | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl )
806 | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl;
809 (*=========================================================*)
810 fun decomp_evalc sg t = case t of
811 (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
812 |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
813 |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
814 |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
815 |_ => ([], fn [] => rho_for_evalc sg t);
818 fun proof_of_evalc sg fm = thm_of sg (decomp_evalc sg) fm;
820 (*==================================================*)
821 (* Proof of linform with the compact model *)
822 (*==================================================*)
825 fun decomp_linform sg vars t = case t of
826 (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
827 |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
828 |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
829 |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
830 |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
831 |(Const("Divides.op dvd",_)$d$r) => ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [None , None, Some (cterm_of sg d)](linearize_dvd)))
832 |_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t)));
834 fun proof_of_linform sg vars f = thm_of sg (decomp_linform sg vars) f;
836 (* ------------------------------------------------------------------------- *)
837 (* Interpretaion of Protocols of the cooper procedure : minusinfinity version*)
838 (* ------------------------------------------------------------------------- *)
839 fun coopermi_proof_of sg (x as Free(xn,xT)) fm B dlcm =
840 (* Get the Bset thm*)
841 let val (minf_eqth, minf_moddth) = minf_proof_of_c sg x dlcm fm
842 val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
843 val nbstpthm = not_bst_p_proof_of_c sg x fm dlcm B fm
844 in (dpos,minf_eqth,nbstpthm,minf_moddth)
847 (* ------------------------------------------------------------------------- *)
848 (* Interpretaion of Protocols of the cooper procedure : plusinfinity version *)
849 (* ------------------------------------------------------------------------- *)
850 fun cooperpi_proof_of sg (x as Free(xn,xT)) fm A dlcm =
851 let val (pinf_eqth,pinf_moddth) = pinf_proof_of_c sg x dlcm fm
852 val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
853 val nastpthm = not_ast_p_proof_of_c sg x fm dlcm A fm
854 in (dpos,pinf_eqth,nastpthm,pinf_moddth)
857 (* ------------------------------------------------------------------------- *)
858 (* Interpretaion of Protocols of the cooper procedure : full version*)
859 (* ------------------------------------------------------------------------- *)
860 fun cooper_thm sg s (x as Free(xn,xT)) cfm dlcm ast bst= case s of
861 "pi" => let val (dpsthm,pinf_eqth,nbpth,pinf_moddth) = cooperpi_proof_of sg x cfm ast dlcm
862 in [dpsthm,pinf_eqth,nbpth,pinf_moddth] MRS (cppi_eq)
864 |"mi" => let val (dpsthm,minf_eqth,nbpth,minf_moddth) = coopermi_proof_of sg x cfm bst dlcm
865 in [dpsthm,minf_eqth,nbpth,minf_moddth] MRS (cpmi_eq)
867 |_ => error "parameter error";
869 (* ------------------------------------------------------------------------- *)
870 (* This function should evoluate to the end prove Procedure for one quantifier elimination for Presburger arithmetic*)
871 (* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
872 (* ------------------------------------------------------------------------- *)
874 fun cooper_prv sg (x as Free(xn,xT)) efm = let
875 (* lfm_thm : efm = linearized form of efm*)
876 val lfm_thm = proof_of_linform sg [xn] efm
877 (*efm2 is the linearized form of efm *)
878 val efm2 = snd(qe_get_terms lfm_thm)
879 (* l is the lcm of all coefficients of x *)
880 val l = formlcm x efm2
881 (*ac_thm: efm = efm2 with adjusted coefficients of x *)
882 val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
883 (* fm is efm2 with adjusted coefficients of x *)
884 val fm = snd (qe_get_terms ac_thm)
885 (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
886 val cfm = unitycoeff x fm
887 (*afm is fm where c*x is replaced by 1*x or -1*x *)
888 val afm = adjustcoeff x l fm
890 val P = absfree(xn,xT,afm)
891 (* This simpset allows the elimination of the sets in bex {1..d} *)
892 val ss = presburger_ss addsimps
893 [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
894 (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
895 val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
896 (* e_ac_thm : Ex x. efm = EX x. fm*)
897 val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
898 (* A and B set of the formula*)
901 (* the divlcm (delta) of the formula*)
902 val dlcm = mk_numeral (divlcm x cfm)
903 (* Which set is smaller to generate the (hoepfully) shorter proof*)
904 val cms = if ((length A) < (length B )) then "pi" else "mi"
905 (* synthesize the proof of cooper's theorem*)
906 (* cp_thm: EX x. cfm = Q*)
907 val cp_thm = cooper_thm sg cms x cfm dlcm A B
908 (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
909 (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
910 val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
911 (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
912 val (lsuth,rsuth) = qe_get_terms (uth)
913 (* lseacth = EX x. efm; rseacth = EX x. fm*)
914 val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
915 (* lscth = EX x. cfm; rscth = Q' *)
916 val (lscth,rscth) = qe_get_terms (exp_cp_thm)
917 (* u_c_thm: EX x. P(l*x) = Q'*)
918 val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
919 (* result: EX x. efm = Q'*)
920 in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
922 |cooper_prv _ _ _ = error "Parameters format";
924 (* ********************************** *)
925 (* cooper_prv2 is just copy and paste *)
926 (* And only generates proof with *)
927 (* bset and minusinfity *)
928 (* ********************************** *)
932 fun cooper_prv2 sg (x as Free(xn,xT)) efm = let
933 (* lfm_thm : efm = linearized form of efm*)
934 val lfm_thm = proof_of_linform sg [xn] efm
935 (*efm2 is the linearized form of efm *)
936 val efm2 = snd(qe_get_terms lfm_thm)
937 (* l is the lcm of all coefficients of x *)
938 val l = formlcm x efm2
939 (*ac_thm: efm = efm2 with adjusted coefficients of x *)
940 val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
941 (* fm is efm2 with adjusted coefficients of x *)
942 val fm = snd (qe_get_terms ac_thm)
943 (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
944 val cfm = unitycoeff x fm
945 (*afm is fm where c*x is replaced by 1*x or -1*x *)
946 val afm = adjustcoeff x l fm
948 val P = absfree(xn,xT,afm)
949 (* This simpset allows the elimination of the sets in bex {1..d} *)
950 val ss = presburger_ss addsimps
951 [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
952 (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
953 val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
954 (* e_ac_thm : Ex x. efm = EX x. fm*)
955 val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
956 (* A and B set of the formula*)
959 (* the divlcm (delta) of the formula*)
960 val dlcm = mk_numeral (divlcm x cfm)
961 (* Which set is smaller to generate the (hoepfully) shorter proof*)
963 (* synthesize the proof of cooper's theorem*)
964 (* cp_thm: EX x. cfm = Q*)
965 val cp_thm = cooper_thm sg cms x cfm dlcm A B
966 (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
967 (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
968 val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
969 (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
970 val (lsuth,rsuth) = qe_get_terms (uth)
971 (* lseacth = EX x. efm; rseacth = EX x. fm*)
972 val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
973 (* lscth = EX x. cfm; rscth = Q' *)
974 val (lscth,rscth) = qe_get_terms (exp_cp_thm)
975 (* u_c_thm: EX x. P(l*x) = Q'*)
976 val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
977 (* result: EX x. efm = Q'*)
978 in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
980 |cooper_prv2 _ _ _ = error "Parameters format";
983 (* **************************************** *)
984 (* An Other Version of cooper proving *)
985 (* by giving a withness for EX *)
986 (* **************************************** *)
990 fun cooper_prv_w sg (x as Free(xn,xT)) efm = let
991 (* lfm_thm : efm = linearized form of efm*)
992 val lfm_thm = proof_of_linform sg [xn] efm
993 (*efm2 is the linearized form of efm *)
994 val efm2 = snd(qe_get_terms lfm_thm)
995 (* l is the lcm of all coefficients of x *)
996 val l = formlcm x efm2
997 (*ac_thm: efm = efm2 with adjusted coefficients of x *)
998 val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
999 (* fm is efm2 with adjusted coefficients of x *)
1000 val fm = snd (qe_get_terms ac_thm)
1001 (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
1002 val cfm = unitycoeff x fm
1003 (*afm is fm where c*x is replaced by 1*x or -1*x *)
1004 val afm = adjustcoeff x l fm
1006 val P = absfree(xn,xT,afm)
1007 (* This simpset allows the elimination of the sets in bex {1..d} *)
1008 val ss = presburger_ss addsimps
1009 [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
1010 (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
1011 val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
1012 (* e_ac_thm : Ex x. efm = EX x. fm*)
1013 val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
1014 (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
1015 val (lsuth,rsuth) = qe_get_terms (uth)
1016 (* lseacth = EX x. efm; rseacth = EX x. fm*)
1017 val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
1019 val (w,rs) = cooper_w [] cfm
1020 val exp_cp_thm = case w of
1021 (* FIXME - e_ac_thm just tipped to test syntactical correctness of the program!!!!*)
1022 Some n => e_ac_thm (* Prove cfm (n) and use exI and then Eq_TrueI*)
1024 (* A and B set of the formula*)
1027 (* the divlcm (delta) of the formula*)
1028 val dlcm = mk_numeral (divlcm x cfm)
1029 (* Which set is smaller to generate the (hoepfully) shorter proof*)
1030 val cms = if ((length A) < (length B )) then "pi" else "mi"
1031 (* synthesize the proof of cooper's theorem*)
1032 (* cp_thm: EX x. cfm = Q*)
1033 val cp_thm = cooper_thm sg cms x cfm dlcm A B
1034 (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
1035 (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
1036 in refl RS (simplify ss (cp_thm RSN (2,trans)))
1038 (* lscth = EX x. cfm; rscth = Q' *)
1039 val (lscth,rscth) = qe_get_terms (exp_cp_thm)
1040 (* u_c_thm: EX x. P(l*x) = Q'*)
1041 val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
1042 (* result: EX x. efm = Q'*)
1043 in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
1045 |cooper_prv_w _ _ _ = error "Parameters format";
1049 fun decomp_cnnf sg lfnp P = case P of
1050 Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI )
1051 |Const ("op |",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_disjI)
1052 |Const ("Not",_) $ (Const("Not",_) $ p) => ([p], fn [th] => th RS nnf_nn)
1053 |Const("Not",_) $ (Const(opn,T) $ p $ q) =>
1056 (A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) =>
1058 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)
1060 else ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj)
1061 |(_,_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj)
1064 ("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_ncj )
1065 |("op -->",_) => ([p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_nim )
1066 |("op =",Type ("fun",[Type ("bool", []),_])) =>
1067 ([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q], fn [th1,th2] => [th1,th2] MRS nnf_neq)
1068 |(_,_) => ([], fn [] => lfnp P)
1071 |(Const ("op -->",_) $ p $ q) => ([HOLogic.Not$p,q], fn [th1,th2] => [th1,th2] MRS nnf_im)
1073 |(Const ("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q) =>
1074 ([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], fn [th1,th2] =>[th1,th2] MRS nnf_eq )
1075 |_ => ([], fn [] => lfnp P);
1080 fun proof_of_cnnf sg p lfnp =
1081 let val th1 = thm_of sg (decomp_cnnf sg lfnp) p
1082 val rs = snd(qe_get_terms th1)
1083 val th2 = prove_elementar sg "ss" (HOLogic.mk_eq(rs,simpl rs))
1084 in [th1,th2] MRS trans