summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | chaieb |

Fri, 06 Aug 2004 17:29:24 +0200 | |

changeset 15123 | 4c49281dc9a8 |

parent 15122 | 4b52eeb62807 |

child 15124 | 1d9b4fcd222d |

*** empty log message ***

src/HOL/Integ/cooper_proof.ML | file | annotate | diff | comparison | revisions | |

src/HOL/Tools/Presburger/cooper_proof.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Integ/cooper_proof.ML Fri Aug 06 17:19:50 2004 +0200 +++ b/src/HOL/Integ/cooper_proof.ML Fri Aug 06 17:29:24 2004 +0200 @@ -18,7 +18,6 @@ val list_to_set : typ -> term list -> term val qe_get_terms : thm -> term * term val cooper_prv : Sign.sg -> term -> term -> thm - val cooper_prv2 : Sign.sg -> term -> term -> thm val proof_of_evalc : Sign.sg -> term -> thm val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm val proof_of_linform : Sign.sg -> string list -> term -> thm @@ -921,65 +920,6 @@ end |cooper_prv _ _ _ = error "Parameters format"; -(* ********************************** *) -(* cooper_prv2 is just copy and paste *) -(* And only generates proof with *) -(* bset and minusinfity *) -(* ********************************** *) - - - -fun cooper_prv2 sg (x as Free(xn,xT)) efm = let - (* lfm_thm : efm = linearized form of efm*) - val lfm_thm = proof_of_linform sg [xn] efm - (*efm2 is the linearized form of efm *) - val efm2 = snd(qe_get_terms lfm_thm) - (* l is the lcm of all coefficients of x *) - val l = formlcm x efm2 - (*ac_thm: efm = efm2 with adjusted coefficients of x *) - val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans - (* fm is efm2 with adjusted coefficients of x *) - val fm = snd (qe_get_terms ac_thm) - (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*) - val cfm = unitycoeff x fm - (*afm is fm where c*x is replaced by 1*x or -1*x *) - val afm = adjustcoeff x l fm - (* P = %x.afm*) - val P = absfree(xn,xT,afm) - (* This simpset allows the elimination of the sets in bex {1..d} *) - val ss = presburger_ss addsimps - [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff] - (* uth : EX x.P(l*x) = EX x. l dvd x & P x*) - val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex) - (* e_ac_thm : Ex x. efm = EX x. fm*) - val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI) - (* A and B set of the formula*) - val B = bset x cfm - val A = [] - (* the divlcm (delta) of the formula*) - val dlcm = mk_numeral (divlcm x cfm) - (* Which set is smaller to generate the (hoepfully) shorter proof*) - val cms = "mi" - (* synthesize the proof of cooper's theorem*) - (* cp_thm: EX x. cfm = Q*) - val cp_thm = cooper_thm sg cms x cfm dlcm A B - (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*) - (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*) - val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans))) - (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*) - val (lsuth,rsuth) = qe_get_terms (uth) - (* lseacth = EX x. efm; rseacth = EX x. fm*) - val (lseacth,rseacth) = qe_get_terms(e_ac_thm) - (* lscth = EX x. cfm; rscth = Q' *) - val (lscth,rscth) = qe_get_terms (exp_cp_thm) - (* u_c_thm: EX x. P(l*x) = Q'*) - val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans - (* result: EX x. efm = Q'*) - in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans) - end -|cooper_prv2 _ _ _ = error "Parameters format"; - - (* **************************************** *) (* An Other Version of cooper proving *) (* by giving a withness for EX *)

--- a/src/HOL/Tools/Presburger/cooper_proof.ML Fri Aug 06 17:19:50 2004 +0200 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML Fri Aug 06 17:29:24 2004 +0200 @@ -18,7 +18,6 @@ val list_to_set : typ -> term list -> term val qe_get_terms : thm -> term * term val cooper_prv : Sign.sg -> term -> term -> thm - val cooper_prv2 : Sign.sg -> term -> term -> thm val proof_of_evalc : Sign.sg -> term -> thm val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm val proof_of_linform : Sign.sg -> string list -> term -> thm @@ -921,65 +920,6 @@ end |cooper_prv _ _ _ = error "Parameters format"; -(* ********************************** *) -(* cooper_prv2 is just copy and paste *) -(* And only generates proof with *) -(* bset and minusinfity *) -(* ********************************** *) - - - -fun cooper_prv2 sg (x as Free(xn,xT)) efm = let - (* lfm_thm : efm = linearized form of efm*) - val lfm_thm = proof_of_linform sg [xn] efm - (*efm2 is the linearized form of efm *) - val efm2 = snd(qe_get_terms lfm_thm) - (* l is the lcm of all coefficients of x *) - val l = formlcm x efm2 - (*ac_thm: efm = efm2 with adjusted coefficients of x *) - val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans - (* fm is efm2 with adjusted coefficients of x *) - val fm = snd (qe_get_terms ac_thm) - (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*) - val cfm = unitycoeff x fm - (*afm is fm where c*x is replaced by 1*x or -1*x *) - val afm = adjustcoeff x l fm - (* P = %x.afm*) - val P = absfree(xn,xT,afm) - (* This simpset allows the elimination of the sets in bex {1..d} *) - val ss = presburger_ss addsimps - [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff] - (* uth : EX x.P(l*x) = EX x. l dvd x & P x*) - val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex) - (* e_ac_thm : Ex x. efm = EX x. fm*) - val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI) - (* A and B set of the formula*) - val B = bset x cfm - val A = [] - (* the divlcm (delta) of the formula*) - val dlcm = mk_numeral (divlcm x cfm) - (* Which set is smaller to generate the (hoepfully) shorter proof*) - val cms = "mi" - (* synthesize the proof of cooper's theorem*) - (* cp_thm: EX x. cfm = Q*) - val cp_thm = cooper_thm sg cms x cfm dlcm A B - (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*) - (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*) - val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans))) - (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*) - val (lsuth,rsuth) = qe_get_terms (uth) - (* lseacth = EX x. efm; rseacth = EX x. fm*) - val (lseacth,rseacth) = qe_get_terms(e_ac_thm) - (* lscth = EX x. cfm; rscth = Q' *) - val (lscth,rscth) = qe_get_terms (exp_cp_thm) - (* u_c_thm: EX x. P(l*x) = Q'*) - val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans - (* result: EX x. efm = Q'*) - in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans) - end -|cooper_prv2 _ _ _ = error "Parameters format"; - - (* **************************************** *) (* An Other Version of cooper proving *) (* by giving a withness for EX *)