# HG changeset patch
# User chaieb
# Date 1086453246 -7200
# Node ID 28084696907fcb9f304106da23e73db7284d6141
# Parent  477c414000f890d4804b6318986ead8be4021fe3
More readable code.

diff -r 477c414000f8 -r 28084696907f src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Sat Jun 05 13:08:53 2004 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Sat Jun 05 18:34:06 2004 +0200
@@ -39,6 +39,8 @@
   val has_bound : term -> bool
   val minusinf : term -> term -> term
   val plusinf : term -> term -> term
+  val onatoms : (term -> term) -> term -> term
+  val evalc : term -> term
 end;
 
 structure  CooperDec : COOPER_DEC =
diff -r 477c414000f8 -r 28084696907f src/HOL/Integ/cooper_proof.ML
--- a/src/HOL/Integ/cooper_proof.ML	Sat Jun 05 13:08:53 2004 +0200
+++ b/src/HOL/Integ/cooper_proof.ML	Sat Jun 05 18:34:06 2004 +0200
@@ -15,11 +15,13 @@
   val qe_impI : thm
   val qe_eqI : thm
   val qe_exI : thm
+  val list_to_set : typ -> term list -> term
   val qe_get_terms : thm -> term * term
   val cooper_prv : 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
+  val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
   val prove_elementar : Sign.sg -> string -> term -> thm
   val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
 end;
@@ -365,6 +367,10 @@
 
   |_ => ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl);
 
+fun proof_of_adjustcoeffeq sg x l = thm_of sg (decomp_adjustcoeffeq sg x l);
+
+
+
 (*==================================================*)
 (*   Finding rho for modd_minusinfinity             *)
 (*==================================================*)
@@ -861,28 +867,51 @@
 (* ------------------------------------------------------------------------- *)
 
 fun cooper_prv 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
-   val ac_thm = [lfm_thm , (thm_of sg (decomp_adjustcoeffeq sg x l) efm2)] MRS trans
+   (*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 A = aset x cfm
    val B = bset x cfm
+   (* 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 = if ((length A) < (length B )) then "pi" else "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_prv _ _ _ =  error "Parameters format";
diff -r 477c414000f8 -r 28084696907f src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Sat Jun 05 13:08:53 2004 +0200
+++ b/src/HOL/Integ/presburger.ML	Sat Jun 05 18:34:06 2004 +0200
@@ -282,7 +282,7 @@
       || Args.$$$ "abs" >> K (apsnd (K true));
  in
    Method.simple_args 
-  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
+  (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
     curry (foldl op |>) (true, false))
     (fn (q,a) => fn _ => meth q a 1)
   end;
diff -r 477c414000f8 -r 28084696907f src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Sat Jun 05 13:08:53 2004 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Sat Jun 05 18:34:06 2004 +0200
@@ -39,6 +39,8 @@
   val has_bound : term -> bool
   val minusinf : term -> term -> term
   val plusinf : term -> term -> term
+  val onatoms : (term -> term) -> term -> term
+  val evalc : term -> term
 end;
 
 structure  CooperDec : COOPER_DEC =
diff -r 477c414000f8 -r 28084696907f src/HOL/Tools/Presburger/cooper_proof.ML
--- a/src/HOL/Tools/Presburger/cooper_proof.ML	Sat Jun 05 13:08:53 2004 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Sat Jun 05 18:34:06 2004 +0200
@@ -15,11 +15,13 @@
   val qe_impI : thm
   val qe_eqI : thm
   val qe_exI : thm
+  val list_to_set : typ -> term list -> term
   val qe_get_terms : thm -> term * term
   val cooper_prv : 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
+  val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
   val prove_elementar : Sign.sg -> string -> term -> thm
   val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
 end;
@@ -365,6 +367,10 @@
 
   |_ => ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl);
 
+fun proof_of_adjustcoeffeq sg x l = thm_of sg (decomp_adjustcoeffeq sg x l);
+
+
+
 (*==================================================*)
 (*   Finding rho for modd_minusinfinity             *)
 (*==================================================*)
@@ -861,28 +867,51 @@
 (* ------------------------------------------------------------------------- *)
 
 fun cooper_prv 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
-   val ac_thm = [lfm_thm , (thm_of sg (decomp_adjustcoeffeq sg x l) efm2)] MRS trans
+   (*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 A = aset x cfm
    val B = bset x cfm
+   (* 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 = if ((length A) < (length B )) then "pi" else "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_prv _ _ _ =  error "Parameters format";
diff -r 477c414000f8 -r 28084696907f src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Sat Jun 05 13:08:53 2004 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Sat Jun 05 18:34:06 2004 +0200
@@ -282,7 +282,7 @@
       || Args.$$$ "abs" >> K (apsnd (K true));
  in
    Method.simple_args 
-  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
+  (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
     curry (foldl op |>) (true, false))
     (fn (q,a) => fn _ => meth q a 1)
   end;