More readable code.
authorchaieb
Sat Jun 05 18:34:06 2004 +0200 (2004-06-05)
changeset 1487728084696907f
parent 14876 477c414000f8
child 14878 b884a7ba7238
More readable code.
src/HOL/Integ/cooper_dec.ML
src/HOL/Integ/cooper_proof.ML
src/HOL/Integ/presburger.ML
src/HOL/Tools/Presburger/cooper_dec.ML
src/HOL/Tools/Presburger/cooper_proof.ML
src/HOL/Tools/Presburger/presburger.ML
     1.1 --- a/src/HOL/Integ/cooper_dec.ML	Sat Jun 05 13:08:53 2004 +0200
     1.2 +++ b/src/HOL/Integ/cooper_dec.ML	Sat Jun 05 18:34:06 2004 +0200
     1.3 @@ -39,6 +39,8 @@
     1.4    val has_bound : term -> bool
     1.5    val minusinf : term -> term -> term
     1.6    val plusinf : term -> term -> term
     1.7 +  val onatoms : (term -> term) -> term -> term
     1.8 +  val evalc : term -> term
     1.9  end;
    1.10  
    1.11  structure  CooperDec : COOPER_DEC =
     2.1 --- a/src/HOL/Integ/cooper_proof.ML	Sat Jun 05 13:08:53 2004 +0200
     2.2 +++ b/src/HOL/Integ/cooper_proof.ML	Sat Jun 05 18:34:06 2004 +0200
     2.3 @@ -15,11 +15,13 @@
     2.4    val qe_impI : thm
     2.5    val qe_eqI : thm
     2.6    val qe_exI : thm
     2.7 +  val list_to_set : typ -> term list -> term
     2.8    val qe_get_terms : thm -> term * term
     2.9    val cooper_prv : Sign.sg -> term -> term -> thm
    2.10    val proof_of_evalc : Sign.sg -> term -> thm
    2.11    val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
    2.12    val proof_of_linform : Sign.sg -> string list -> term -> thm
    2.13 +  val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
    2.14    val prove_elementar : Sign.sg -> string -> term -> thm
    2.15    val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
    2.16  end;
    2.17 @@ -365,6 +367,10 @@
    2.18  
    2.19    |_ => ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl);
    2.20  
    2.21 +fun proof_of_adjustcoeffeq sg x l = thm_of sg (decomp_adjustcoeffeq sg x l);
    2.22 +
    2.23 +
    2.24 +
    2.25  (*==================================================*)
    2.26  (*   Finding rho for modd_minusinfinity             *)
    2.27  (*==================================================*)
    2.28 @@ -861,28 +867,51 @@
    2.29  (* ------------------------------------------------------------------------- *)
    2.30  
    2.31  fun cooper_prv sg (x as Free(xn,xT)) efm = let 
    2.32 +   (* lfm_thm : efm = linearized form of efm*)
    2.33     val lfm_thm = proof_of_linform sg [xn] efm
    2.34 +   (*efm2 is the linearized form of efm *) 
    2.35     val efm2 = snd(qe_get_terms lfm_thm)
    2.36 +   (* l is the lcm of all coefficients of x *)
    2.37     val l = formlcm x efm2
    2.38 -   val ac_thm = [lfm_thm , (thm_of sg (decomp_adjustcoeffeq sg x l) efm2)] MRS trans
    2.39 +   (*ac_thm: efm = efm2 with adjusted coefficients of x *)
    2.40 +   val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
    2.41 +   (* fm is efm2 with adjusted coefficients of x *)
    2.42     val fm = snd (qe_get_terms ac_thm)
    2.43 +  (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
    2.44     val  cfm = unitycoeff x fm
    2.45 +   (*afm is fm where c*x is replaced by 1*x or -1*x *)
    2.46     val afm = adjustcoeff x l fm
    2.47 +   (* P = %x.afm*)
    2.48     val P = absfree(xn,xT,afm)
    2.49 +   (* This simpset allows the elimination of the sets in bex {1..d} *)
    2.50     val ss = presburger_ss addsimps
    2.51       [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
    2.52 +   (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
    2.53     val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
    2.54 +   (* e_ac_thm : Ex x. efm = EX x. fm*)
    2.55     val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
    2.56 +   (* A and B set of the formula*)
    2.57     val A = aset x cfm
    2.58     val B = bset x cfm
    2.59 +   (* the divlcm (delta) of the formula*)
    2.60     val dlcm = mk_numeral (divlcm x cfm)
    2.61 +   (* Which set is smaller to generate the (hoepfully) shorter proof*)
    2.62     val cms = if ((length A) < (length B )) then "pi" else "mi"
    2.63 +   (* synthesize the proof of cooper's theorem*)
    2.64 +    (* cp_thm: EX x. cfm = Q*)
    2.65     val cp_thm = cooper_thm sg cms x cfm dlcm A B
    2.66 +   (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
    2.67 +   (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
    2.68     val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
    2.69 +   (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
    2.70     val (lsuth,rsuth) = qe_get_terms (uth)
    2.71 +   (* lseacth = EX x. efm; rseacth = EX x. fm*)
    2.72     val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
    2.73 +   (* lscth = EX x. cfm; rscth = Q' *)
    2.74     val (lscth,rscth) = qe_get_terms (exp_cp_thm)
    2.75 +   (* u_c_thm: EX x. P(l*x) = Q'*)
    2.76     val  u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
    2.77 +   (* result: EX x. efm = Q'*)
    2.78   in  ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
    2.79     end
    2.80  |cooper_prv _ _ _ =  error "Parameters format";
     3.1 --- a/src/HOL/Integ/presburger.ML	Sat Jun 05 13:08:53 2004 +0200
     3.2 +++ b/src/HOL/Integ/presburger.ML	Sat Jun 05 18:34:06 2004 +0200
     3.3 @@ -282,7 +282,7 @@
     3.4        || Args.$$$ "abs" >> K (apsnd (K true));
     3.5   in
     3.6     Method.simple_args 
     3.7 -  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
     3.8 +  (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
     3.9      curry (foldl op |>) (true, false))
    3.10      (fn (q,a) => fn _ => meth q a 1)
    3.11    end;
     4.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Sat Jun 05 13:08:53 2004 +0200
     4.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Sat Jun 05 18:34:06 2004 +0200
     4.3 @@ -39,6 +39,8 @@
     4.4    val has_bound : term -> bool
     4.5    val minusinf : term -> term -> term
     4.6    val plusinf : term -> term -> term
     4.7 +  val onatoms : (term -> term) -> term -> term
     4.8 +  val evalc : term -> term
     4.9  end;
    4.10  
    4.11  structure  CooperDec : COOPER_DEC =
     5.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Sat Jun 05 13:08:53 2004 +0200
     5.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Sat Jun 05 18:34:06 2004 +0200
     5.3 @@ -15,11 +15,13 @@
     5.4    val qe_impI : thm
     5.5    val qe_eqI : thm
     5.6    val qe_exI : thm
     5.7 +  val list_to_set : typ -> term list -> term
     5.8    val qe_get_terms : thm -> term * term
     5.9    val cooper_prv : Sign.sg -> term -> term -> thm
    5.10    val proof_of_evalc : Sign.sg -> term -> thm
    5.11    val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
    5.12    val proof_of_linform : Sign.sg -> string list -> term -> thm
    5.13 +  val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
    5.14    val prove_elementar : Sign.sg -> string -> term -> thm
    5.15    val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
    5.16  end;
    5.17 @@ -365,6 +367,10 @@
    5.18  
    5.19    |_ => ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl);
    5.20  
    5.21 +fun proof_of_adjustcoeffeq sg x l = thm_of sg (decomp_adjustcoeffeq sg x l);
    5.22 +
    5.23 +
    5.24 +
    5.25  (*==================================================*)
    5.26  (*   Finding rho for modd_minusinfinity             *)
    5.27  (*==================================================*)
    5.28 @@ -861,28 +867,51 @@
    5.29  (* ------------------------------------------------------------------------- *)
    5.30  
    5.31  fun cooper_prv sg (x as Free(xn,xT)) efm = let 
    5.32 +   (* lfm_thm : efm = linearized form of efm*)
    5.33     val lfm_thm = proof_of_linform sg [xn] efm
    5.34 +   (*efm2 is the linearized form of efm *) 
    5.35     val efm2 = snd(qe_get_terms lfm_thm)
    5.36 +   (* l is the lcm of all coefficients of x *)
    5.37     val l = formlcm x efm2
    5.38 -   val ac_thm = [lfm_thm , (thm_of sg (decomp_adjustcoeffeq sg x l) efm2)] MRS trans
    5.39 +   (*ac_thm: efm = efm2 with adjusted coefficients of x *)
    5.40 +   val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
    5.41 +   (* fm is efm2 with adjusted coefficients of x *)
    5.42     val fm = snd (qe_get_terms ac_thm)
    5.43 +  (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
    5.44     val  cfm = unitycoeff x fm
    5.45 +   (*afm is fm where c*x is replaced by 1*x or -1*x *)
    5.46     val afm = adjustcoeff x l fm
    5.47 +   (* P = %x.afm*)
    5.48     val P = absfree(xn,xT,afm)
    5.49 +   (* This simpset allows the elimination of the sets in bex {1..d} *)
    5.50     val ss = presburger_ss addsimps
    5.51       [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
    5.52 +   (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
    5.53     val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
    5.54 +   (* e_ac_thm : Ex x. efm = EX x. fm*)
    5.55     val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
    5.56 +   (* A and B set of the formula*)
    5.57     val A = aset x cfm
    5.58     val B = bset x cfm
    5.59 +   (* the divlcm (delta) of the formula*)
    5.60     val dlcm = mk_numeral (divlcm x cfm)
    5.61 +   (* Which set is smaller to generate the (hoepfully) shorter proof*)
    5.62     val cms = if ((length A) < (length B )) then "pi" else "mi"
    5.63 +   (* synthesize the proof of cooper's theorem*)
    5.64 +    (* cp_thm: EX x. cfm = Q*)
    5.65     val cp_thm = cooper_thm sg cms x cfm dlcm A B
    5.66 +   (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
    5.67 +   (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
    5.68     val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
    5.69 +   (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
    5.70     val (lsuth,rsuth) = qe_get_terms (uth)
    5.71 +   (* lseacth = EX x. efm; rseacth = EX x. fm*)
    5.72     val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
    5.73 +   (* lscth = EX x. cfm; rscth = Q' *)
    5.74     val (lscth,rscth) = qe_get_terms (exp_cp_thm)
    5.75 +   (* u_c_thm: EX x. P(l*x) = Q'*)
    5.76     val  u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
    5.77 +   (* result: EX x. efm = Q'*)
    5.78   in  ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
    5.79     end
    5.80  |cooper_prv _ _ _ =  error "Parameters format";
     6.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Sat Jun 05 13:08:53 2004 +0200
     6.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Sat Jun 05 18:34:06 2004 +0200
     6.3 @@ -282,7 +282,7 @@
     6.4        || Args.$$$ "abs" >> K (apsnd (K true));
     6.5   in
     6.6     Method.simple_args 
     6.7 -  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
     6.8 +  (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
     6.9      curry (foldl op |>) (true, false))
    6.10      (fn (q,a) => fn _ => meth q a 1)
    6.11    end;