*** empty log message ***
authorchaieb
Fri Aug 06 17:29:24 2004 +0200 (2004-08-06)
changeset 151234c49281dc9a8
parent 15122 4b52eeb62807
child 15124 1d9b4fcd222d
*** empty log message ***
src/HOL/Integ/cooper_proof.ML
src/HOL/Tools/Presburger/cooper_proof.ML
     1.1 --- a/src/HOL/Integ/cooper_proof.ML	Fri Aug 06 17:19:50 2004 +0200
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Fri Aug 06 17:29:24 2004 +0200
     1.3 @@ -18,7 +18,6 @@
     1.4    val list_to_set : typ -> term list -> term
     1.5    val qe_get_terms : thm -> term * term
     1.6    val cooper_prv  : Sign.sg -> term -> term -> thm
     1.7 -  val cooper_prv2 : Sign.sg -> term -> term -> thm
     1.8    val proof_of_evalc : Sign.sg -> term -> thm
     1.9    val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
    1.10    val proof_of_linform : Sign.sg -> string list -> term -> thm
    1.11 @@ -921,65 +920,6 @@
    1.12     end
    1.13  |cooper_prv _ _ _ =  error "Parameters format";
    1.14  
    1.15 -(* ********************************** *)
    1.16 -(* cooper_prv2 is just copy and paste *)
    1.17 -(* And only generates proof with      *)
    1.18 -(* bset and minusinfity               *)
    1.19 -(* ********************************** *)
    1.20 -
    1.21 -
    1.22 -
    1.23 -fun cooper_prv2 sg (x as Free(xn,xT)) efm = let 
    1.24 -   (* lfm_thm : efm = linearized form of efm*)
    1.25 -   val lfm_thm = proof_of_linform sg [xn] efm
    1.26 -   (*efm2 is the linearized form of efm *) 
    1.27 -   val efm2 = snd(qe_get_terms lfm_thm)
    1.28 -   (* l is the lcm of all coefficients of x *)
    1.29 -   val l = formlcm x efm2
    1.30 -   (*ac_thm: efm = efm2 with adjusted coefficients of x *)
    1.31 -   val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
    1.32 -   (* fm is efm2 with adjusted coefficients of x *)
    1.33 -   val fm = snd (qe_get_terms ac_thm)
    1.34 -  (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
    1.35 -   val  cfm = unitycoeff x fm
    1.36 -   (*afm is fm where c*x is replaced by 1*x or -1*x *)
    1.37 -   val afm = adjustcoeff x l fm
    1.38 -   (* P = %x.afm*)
    1.39 -   val P = absfree(xn,xT,afm)
    1.40 -   (* This simpset allows the elimination of the sets in bex {1..d} *)
    1.41 -   val ss = presburger_ss addsimps
    1.42 -     [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
    1.43 -   (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
    1.44 -   val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
    1.45 -   (* e_ac_thm : Ex x. efm = EX x. fm*)
    1.46 -   val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
    1.47 -   (* A and B set of the formula*)
    1.48 -   val B = bset x cfm
    1.49 -   val A = []
    1.50 -   (* the divlcm (delta) of the formula*)
    1.51 -   val dlcm = mk_numeral (divlcm x cfm)
    1.52 -   (* Which set is smaller to generate the (hoepfully) shorter proof*)
    1.53 -   val cms = "mi" 
    1.54 -   (* synthesize the proof of cooper's theorem*)
    1.55 -    (* cp_thm: EX x. cfm = Q*)
    1.56 -   val cp_thm = cooper_thm sg cms x cfm dlcm A B
    1.57 -   (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
    1.58 -   (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
    1.59 -   val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
    1.60 -   (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
    1.61 -   val (lsuth,rsuth) = qe_get_terms (uth)
    1.62 -   (* lseacth = EX x. efm; rseacth = EX x. fm*)
    1.63 -   val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
    1.64 -   (* lscth = EX x. cfm; rscth = Q' *)
    1.65 -   val (lscth,rscth) = qe_get_terms (exp_cp_thm)
    1.66 -   (* u_c_thm: EX x. P(l*x) = Q'*)
    1.67 -   val  u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
    1.68 -   (* result: EX x. efm = Q'*)
    1.69 - in  ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
    1.70 -   end
    1.71 -|cooper_prv2 _ _ _ =  error "Parameters format";
    1.72 -
    1.73 -
    1.74  (* **************************************** *)
    1.75  (*    An Other Version of cooper proving    *)
    1.76  (*     by giving a withness for EX          *)
     2.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Fri Aug 06 17:19:50 2004 +0200
     2.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Fri Aug 06 17:29:24 2004 +0200
     2.3 @@ -18,7 +18,6 @@
     2.4    val list_to_set : typ -> term list -> term
     2.5    val qe_get_terms : thm -> term * term
     2.6    val cooper_prv  : Sign.sg -> term -> term -> thm
     2.7 -  val cooper_prv2 : Sign.sg -> term -> term -> thm
     2.8    val proof_of_evalc : Sign.sg -> term -> thm
     2.9    val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
    2.10    val proof_of_linform : Sign.sg -> string list -> term -> thm
    2.11 @@ -921,65 +920,6 @@
    2.12     end
    2.13  |cooper_prv _ _ _ =  error "Parameters format";
    2.14  
    2.15 -(* ********************************** *)
    2.16 -(* cooper_prv2 is just copy and paste *)
    2.17 -(* And only generates proof with      *)
    2.18 -(* bset and minusinfity               *)
    2.19 -(* ********************************** *)
    2.20 -
    2.21 -
    2.22 -
    2.23 -fun cooper_prv2 sg (x as Free(xn,xT)) efm = let 
    2.24 -   (* lfm_thm : efm = linearized form of efm*)
    2.25 -   val lfm_thm = proof_of_linform sg [xn] efm
    2.26 -   (*efm2 is the linearized form of efm *) 
    2.27 -   val efm2 = snd(qe_get_terms lfm_thm)
    2.28 -   (* l is the lcm of all coefficients of x *)
    2.29 -   val l = formlcm x efm2
    2.30 -   (*ac_thm: efm = efm2 with adjusted coefficients of x *)
    2.31 -   val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
    2.32 -   (* fm is efm2 with adjusted coefficients of x *)
    2.33 -   val fm = snd (qe_get_terms ac_thm)
    2.34 -  (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
    2.35 -   val  cfm = unitycoeff x fm
    2.36 -   (*afm is fm where c*x is replaced by 1*x or -1*x *)
    2.37 -   val afm = adjustcoeff x l fm
    2.38 -   (* P = %x.afm*)
    2.39 -   val P = absfree(xn,xT,afm)
    2.40 -   (* This simpset allows the elimination of the sets in bex {1..d} *)
    2.41 -   val ss = presburger_ss addsimps
    2.42 -     [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
    2.43 -   (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
    2.44 -   val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
    2.45 -   (* e_ac_thm : Ex x. efm = EX x. fm*)
    2.46 -   val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
    2.47 -   (* A and B set of the formula*)
    2.48 -   val B = bset x cfm
    2.49 -   val A = []
    2.50 -   (* the divlcm (delta) of the formula*)
    2.51 -   val dlcm = mk_numeral (divlcm x cfm)
    2.52 -   (* Which set is smaller to generate the (hoepfully) shorter proof*)
    2.53 -   val cms = "mi" 
    2.54 -   (* synthesize the proof of cooper's theorem*)
    2.55 -    (* cp_thm: EX x. cfm = Q*)
    2.56 -   val cp_thm = cooper_thm sg cms x cfm dlcm A B
    2.57 -   (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
    2.58 -   (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
    2.59 -   val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
    2.60 -   (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
    2.61 -   val (lsuth,rsuth) = qe_get_terms (uth)
    2.62 -   (* lseacth = EX x. efm; rseacth = EX x. fm*)
    2.63 -   val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
    2.64 -   (* lscth = EX x. cfm; rscth = Q' *)
    2.65 -   val (lscth,rscth) = qe_get_terms (exp_cp_thm)
    2.66 -   (* u_c_thm: EX x. P(l*x) = Q'*)
    2.67 -   val  u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
    2.68 -   (* result: EX x. efm = Q'*)
    2.69 - in  ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
    2.70 -   end
    2.71 -|cooper_prv2 _ _ _ =  error "Parameters format";
    2.72 -
    2.73 -
    2.74  (* **************************************** *)
    2.75  (*    An Other Version of cooper proving    *)
    2.76  (*     by giving a withness for EX          *)