13 val qe_conjI : thm |
13 val qe_conjI : thm |
14 val qe_disjI : thm |
14 val qe_disjI : thm |
15 val qe_impI : thm |
15 val qe_impI : thm |
16 val qe_eqI : thm |
16 val qe_eqI : thm |
17 val qe_exI : thm |
17 val qe_exI : thm |
|
18 val list_to_set : typ -> term list -> term |
18 val qe_get_terms : thm -> term * term |
19 val qe_get_terms : thm -> term * term |
19 val cooper_prv : Sign.sg -> term -> term -> thm |
20 val cooper_prv : Sign.sg -> term -> term -> thm |
20 val proof_of_evalc : Sign.sg -> term -> thm |
21 val proof_of_evalc : Sign.sg -> term -> thm |
21 val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm |
22 val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm |
22 val proof_of_linform : Sign.sg -> string list -> term -> thm |
23 val proof_of_linform : Sign.sg -> string list -> term -> thm |
|
24 val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm |
23 val prove_elementar : Sign.sg -> string -> term -> thm |
25 val prove_elementar : Sign.sg -> string -> term -> thm |
24 val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm |
26 val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm |
25 end; |
27 end; |
26 |
28 |
27 structure CooperProof : COOPER_PROOF = |
29 structure CooperProof : COOPER_PROOF = |
362 |( Const ("Not", _) $ p) => ([p], fn [th] => th RS qe_Not) |
364 |( Const ("Not", _) $ p) => ([p], fn [th] => th RS qe_Not) |
363 |( Const ("op &",_) $ p $ q) => ([p,q], fn [th1,th2] => [th1,th2] MRS qe_conjI) |
365 |( Const ("op &",_) $ p $ q) => ([p,q], fn [th1,th2] => [th1,th2] MRS qe_conjI) |
364 |( Const ("op |",_) $ p $ q) =>([p,q], fn [th1,th2] => [th1,th2] MRS qe_disjI) |
366 |( Const ("op |",_) $ p $ q) =>([p,q], fn [th1,th2] => [th1,th2] MRS qe_disjI) |
365 |
367 |
366 |_ => ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl); |
368 |_ => ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl); |
|
369 |
|
370 fun proof_of_adjustcoeffeq sg x l = thm_of sg (decomp_adjustcoeffeq sg x l); |
|
371 |
|
372 |
367 |
373 |
368 (*==================================================*) |
374 (*==================================================*) |
369 (* Finding rho for modd_minusinfinity *) |
375 (* Finding rho for modd_minusinfinity *) |
370 (*==================================================*) |
376 (*==================================================*) |
371 fun rho_for_modd_minf x dlcm sg fm1 = |
377 fun rho_for_modd_minf x dlcm sg fm1 = |
859 (* This function should evoluate to the end prove Procedure for one quantifier elimination for Presburger arithmetic*) |
865 (* This function should evoluate to the end prove Procedure for one quantifier elimination for Presburger arithmetic*) |
860 (* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*) |
866 (* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*) |
861 (* ------------------------------------------------------------------------- *) |
867 (* ------------------------------------------------------------------------- *) |
862 |
868 |
863 fun cooper_prv sg (x as Free(xn,xT)) efm = let |
869 fun cooper_prv sg (x as Free(xn,xT)) efm = let |
|
870 (* lfm_thm : efm = linearized form of efm*) |
864 val lfm_thm = proof_of_linform sg [xn] efm |
871 val lfm_thm = proof_of_linform sg [xn] efm |
|
872 (*efm2 is the linearized form of efm *) |
865 val efm2 = snd(qe_get_terms lfm_thm) |
873 val efm2 = snd(qe_get_terms lfm_thm) |
|
874 (* l is the lcm of all coefficients of x *) |
866 val l = formlcm x efm2 |
875 val l = formlcm x efm2 |
867 val ac_thm = [lfm_thm , (thm_of sg (decomp_adjustcoeffeq sg x l) efm2)] MRS trans |
876 (*ac_thm: efm = efm2 with adjusted coefficients of x *) |
|
877 val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans |
|
878 (* fm is efm2 with adjusted coefficients of x *) |
868 val fm = snd (qe_get_terms ac_thm) |
879 val fm = snd (qe_get_terms ac_thm) |
|
880 (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*) |
869 val cfm = unitycoeff x fm |
881 val cfm = unitycoeff x fm |
|
882 (*afm is fm where c*x is replaced by 1*x or -1*x *) |
870 val afm = adjustcoeff x l fm |
883 val afm = adjustcoeff x l fm |
|
884 (* P = %x.afm*) |
871 val P = absfree(xn,xT,afm) |
885 val P = absfree(xn,xT,afm) |
|
886 (* This simpset allows the elimination of the sets in bex {1..d} *) |
872 val ss = presburger_ss addsimps |
887 val ss = presburger_ss addsimps |
873 [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff] |
888 [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff] |
|
889 (* uth : EX x.P(l*x) = EX x. l dvd x & P x*) |
874 val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex) |
890 val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex) |
|
891 (* e_ac_thm : Ex x. efm = EX x. fm*) |
875 val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI) |
892 val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI) |
|
893 (* A and B set of the formula*) |
876 val A = aset x cfm |
894 val A = aset x cfm |
877 val B = bset x cfm |
895 val B = bset x cfm |
|
896 (* the divlcm (delta) of the formula*) |
878 val dlcm = mk_numeral (divlcm x cfm) |
897 val dlcm = mk_numeral (divlcm x cfm) |
|
898 (* Which set is smaller to generate the (hoepfully) shorter proof*) |
879 val cms = if ((length A) < (length B )) then "pi" else "mi" |
899 val cms = if ((length A) < (length B )) then "pi" else "mi" |
|
900 (* synthesize the proof of cooper's theorem*) |
|
901 (* cp_thm: EX x. cfm = Q*) |
880 val cp_thm = cooper_thm sg cms x cfm dlcm A B |
902 val cp_thm = cooper_thm sg cms x cfm dlcm A B |
|
903 (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*) |
|
904 (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*) |
881 val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans))) |
905 val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans))) |
|
906 (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*) |
882 val (lsuth,rsuth) = qe_get_terms (uth) |
907 val (lsuth,rsuth) = qe_get_terms (uth) |
|
908 (* lseacth = EX x. efm; rseacth = EX x. fm*) |
883 val (lseacth,rseacth) = qe_get_terms(e_ac_thm) |
909 val (lseacth,rseacth) = qe_get_terms(e_ac_thm) |
|
910 (* lscth = EX x. cfm; rscth = Q' *) |
884 val (lscth,rscth) = qe_get_terms (exp_cp_thm) |
911 val (lscth,rscth) = qe_get_terms (exp_cp_thm) |
|
912 (* u_c_thm: EX x. P(l*x) = Q'*) |
885 val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans |
913 val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans |
|
914 (* result: EX x. efm = Q'*) |
886 in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans) |
915 in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans) |
887 end |
916 end |
888 |cooper_prv _ _ _ = error "Parameters format"; |
917 |cooper_prv _ _ _ = error "Parameters format"; |
889 |
918 |
890 |
919 |