oracle corrected
authorchaieb
Wed Aug 04 17:43:55 2004 +0200 (2004-08-04)
changeset 15107f233706d9fce
parent 15106 e8cef6993701
child 15108 492e5f3a8571
oracle corrected
src/HOL/Integ/cooper_dec.ML
src/HOL/Integ/cooper_proof.ML
src/HOL/Tools/Presburger/cooper_dec.ML
src/HOL/Tools/Presburger/cooper_proof.ML
     1.1 --- a/src/HOL/Integ/cooper_dec.ML	Wed Aug 04 11:25:08 2004 +0200
     1.2 +++ b/src/HOL/Integ/cooper_dec.ML	Wed Aug 04 17:43:55 2004 +0200
     1.3 @@ -42,6 +42,7 @@
     1.4    val plusinf : term -> term -> term
     1.5    val onatoms : (term -> term) -> term -> term
     1.6    val evalc : term -> term
     1.7 +  val cooper_w : string list -> term -> (term option * term)
     1.8    val integer_qelim : Term.term -> Term.term
     1.9    val mk_presburger_oracle : (Sign.sg * exn) -> term
    1.10  end;
    1.11 @@ -197,7 +198,7 @@
    1.12   
    1.13           else (warning "lint: apparent nonlinearity"; raise COOPER)
    1.14           end 
    1.15 -  |_ =>   (error "COOPER:lint: unknown term  ")
    1.16 +  |_ =>  error ("COOPER:lint: unknown term  \n");
    1.17     
    1.18   
    1.19   
    1.20 @@ -414,7 +415,31 @@
    1.21  (* ------------------------------------------------------------------------- *) 
    1.22  (* Evaluation of constant expressions.                                       *) 
    1.23  (* ------------------------------------------------------------------------- *) 
    1.24 - 
    1.25 +
    1.26 +(* An other implementation of divides, that covers more cases*) 
    1.27 +
    1.28 +exception DVD_UNKNOWN
    1.29 +
    1.30 +fun dvd_op (d, t) = 
    1.31 + if not(is_numeral d) then raise DVD_UNKNOWN
    1.32 + else let 
    1.33 +   val dn = dest_numeral d
    1.34 +   fun coeffs_of x = case x of 
    1.35 +     Const(p,_) $ tl $ tr => 
    1.36 +       if p = "op +" then (coeffs_of tl) union (coeffs_of tr)
    1.37 +          else if p = "op *" 
    1.38 +	        then if (is_numeral tr) 
    1.39 +		 then [(dest_numeral tr) * (dest_numeral tl)] 
    1.40 +		 else [dest_numeral tl]
    1.41 +	        else []
    1.42 +    |_ => if (is_numeral t) then [dest_numeral t]  else []
    1.43 +   val ts = coeffs_of t
    1.44 +   in case ts of
    1.45 +     [] => raise DVD_UNKNOWN
    1.46 +    |_  => foldr (fn(k,r) => r andalso (k mod dn = 0)) (ts,true)
    1.47 +   end;
    1.48 +
    1.49 +
    1.50  val operations = 
    1.51    [("op =",op=), ("op <",op<), ("op >",op>), ("op <=",op<=) , ("op >=",op>=), 
    1.52     ("Divides.op dvd",fn (x,y) =>((y mod x) = 0))]; 
    1.53 @@ -423,22 +448,44 @@
    1.54      |applyoperation _ (_, _) = false; 
    1.55   
    1.56  (*Evaluation of constant atomic formulas*) 
    1.57 - 
    1.58 + (*FIXME : This is an optimation but still incorrect !! *)
    1.59 +(*
    1.60  fun evalc_atom at = case at of  
    1.61 -      (Const (p,_) $ s $ t) =>(  
    1.62 -         case assoc (operations,p) of 
    1.63 -             Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
    1.64 -              handle _ => at) 
    1.65 -             | _ =>  at) 
    1.66 -     |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
    1.67 -         case assoc (operations,p) of 
    1.68 -             Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
    1.69 -	     HOLogic.false_const else HOLogic.true_const)  
    1.70 -              handle _ => at) 
    1.71 -             | _ =>  at) 
    1.72 -     | _ =>  at; 
    1.73 - 
    1.74 -(*Function onatoms apllys function f on the atomic formulas involved in a.*) 
    1.75 +  (Const (p,_) $ s $ t) =>
    1.76 +   (if p="Divides.op dvd" then 
    1.77 +     ((if dvd_op(s,t) then HOLogic.true_const
    1.78 +     else HOLogic.false_const)
    1.79 +      handle _ => at)
    1.80 +    else
    1.81 +  case assoc (operations,p) of 
    1.82 +    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
    1.83 +    handle _ => at) 
    1.84 +      | _ =>  at) 
    1.85 +      |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
    1.86 +  case assoc (operations,p) of 
    1.87 +    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
    1.88 +    HOLogic.false_const else HOLogic.true_const)  
    1.89 +    handle _ => at) 
    1.90 +      | _ =>  at) 
    1.91 +      | _ =>  at; 
    1.92 +
    1.93 +*)
    1.94 +
    1.95 +fun evalc_atom at = case at of  
    1.96 +  (Const (p,_) $ s $ t) =>
    1.97 +   ( case assoc (operations,p) of 
    1.98 +    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
    1.99 +    handle _ => at) 
   1.100 +      | _ =>  at) 
   1.101 +      |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
   1.102 +  case assoc (operations,p) of 
   1.103 +    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
   1.104 +    HOLogic.false_const else HOLogic.true_const)  
   1.105 +    handle _ => at) 
   1.106 +      | _ =>  at) 
   1.107 +      | _ =>  at; 
   1.108 +
   1.109 + (*Function onatoms apllys function f on the atomic formulas involved in a.*) 
   1.110   
   1.111  fun onatoms f a = if (is_arith_rel a) then f a else case a of 
   1.112   
   1.113 @@ -653,6 +700,48 @@
   1.114    | _ => error "cooper: not an existential formula";
   1.115    
   1.116  
   1.117 +(* Try to find a withness for the formula *)
   1.118 +
   1.119 +fun inf_w mi d vars x p = 
   1.120 +  let val f = if mi then minusinf else plusinf in
   1.121 +   case (simpl (minusinf x p)) of
   1.122 +   Const("True",_)  => (Some (mk_numeral 1), HOLogic.true_const)
   1.123 +  |Const("False",_) => (None,HOLogic.false_const)
   1.124 +  |F => 
   1.125 +      let 
   1.126 +      fun h n =
   1.127 +       case ((simpl o evalc) (linrep vars x (mk_numeral n) F)) of 
   1.128 +	Const("True",_) => (Some (mk_numeral n),HOLogic.true_const)
   1.129 +       |F' => if n=1 then (None,F')
   1.130 +	     else let val (rw,rf) = h (n-1) in 
   1.131 +	       (rw,HOLogic.mk_disj(F',rf))
   1.132 +	     end
   1.133 +
   1.134 +      in (h d)
   1.135 +      end
   1.136 +  end;
   1.137 +
   1.138 +fun set_w d b st vars x p = let 
   1.139 +    fun h ns = case ns of 
   1.140 +    [] => (None,HOLogic.false_const)
   1.141 +   |n::nl => ( case ((simpl o evalc) (linrep vars x n p)) of
   1.142 +      Const("True",_) => (Some n,HOLogic.true_const)
   1.143 +      |F' => let val (rw,rf) = h nl 
   1.144 +             in (rw,HOLogic.mk_disj(F',rf)) 
   1.145 +	     end)
   1.146 +    val f = if b then linear_add else linear_sub
   1.147 +    val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) (1 upto d,[])
   1.148 +    in h p_elements
   1.149 +    end;
   1.150 +
   1.151 +fun withness d b st vars x p = case (inf_w b d vars x p) of 
   1.152 +   (Some n,_) => (Some n,HOLogic.true_const)
   1.153 +  |(None,Pinf) => (case (set_w d b st vars x p) of 
   1.154 +    (Some n,_) => (Some n,HOLogic.true_const)
   1.155 +    |(_,Pst) => (None,HOLogic.mk_disj(Pinf,Pst)));
   1.156 +
   1.157 +
   1.158 +
   1.159  
   1.160  (*Cooper main procedure*) 
   1.161    
   1.162 @@ -678,6 +767,29 @@
   1.163    | _ => error "cooper: not an existential formula";
   1.164  
   1.165  
   1.166 +(* A Version of cooper that returns a withness *)
   1.167 +fun cooper_w vars1 fm =
   1.168 +  case fm of
   1.169 +   Const ("Ex",_) $ Abs(x0,T,p0) => let 
   1.170 +    val (xn,p1) = variant_abs (x0,T,p0)
   1.171 +    val x = Free (xn,T)
   1.172 +    val vars = (xn::vars1)
   1.173 +(*     val p = unitycoeff x  (posineq (simpl p1)) *)
   1.174 +    val p = unitycoeff x  p1 
   1.175 +    val ast = aset x p
   1.176 +    val bst = bset x p
   1.177 +    val d = divlcm x p
   1.178 +    val (p_inf,S ) = 
   1.179 +    if (length bst) <= (length ast) 
   1.180 +     then (true,bst)
   1.181 +     else (false,ast)
   1.182 +    in withness d p_inf S vars x p 
   1.183 +(*    fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p
   1.184 +    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) S)
   1.185 +   in (list_disj (map stage js))
   1.186 +*)
   1.187 +   end
   1.188 +  | _ => error "cooper: not an existential formula";
   1.189  
   1.190   
   1.191  (*Function itlist applys a double parametred function f : 'a->'b->b iteratively to a List l : 'a 
   1.192 @@ -811,8 +923,8 @@
   1.193  fun mk_presburger_oracle (sg,COOPER_ORACLE t) = 
   1.194      if (!quick_and_dirty) 
   1.195      then HOLogic.mk_Trueprop (HOLogic.mk_eq(t,integer_qelim t))
   1.196 -    else raise COOPER_ORACLE t;
   1.197 -
   1.198 +    else raise COOPER_ORACLE t
   1.199 +    |mk_presburger_oracle (sg,_) = error "Oops";
   1.200  end;
   1.201  
   1.202  
     2.1 --- a/src/HOL/Integ/cooper_proof.ML	Wed Aug 04 11:25:08 2004 +0200
     2.2 +++ b/src/HOL/Integ/cooper_proof.ML	Wed Aug 04 17:43:55 2004 +0200
     2.3 @@ -219,7 +219,8 @@
     2.4          [zdvd_iff_zmod_eq_0,unity_coeff_ex]
     2.5        val ct =  cert_Trueprop sg fm2
     2.6      in 
     2.7 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
     2.8 +      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)] 
     2.9 +
    2.10      end
    2.11  
    2.12    (*"bl" like blast tactic*)
    2.13 @@ -251,7 +252,8 @@
    2.14  
    2.15    | "fa" =>
    2.16      let val ct = cert_Trueprop sg fm2
    2.17 -    in simple_prove_goal_cterm2 ct [simple_arith_tac 1]
    2.18 +    in simple_prove_goal_cterm2 ct [simple_arith_tac 1]  
    2.19 +
    2.20      end
    2.21  
    2.22    | "sa" =>
    2.23 @@ -259,7 +261,8 @@
    2.24        val ss = presburger_ss addsimps zadd_ac
    2.25        val ct = cert_Trueprop sg fm2
    2.26      in 
    2.27 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
    2.28 +      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
    2.29 +
    2.30      end
    2.31    (* like Existance Conjunction *)
    2.32    | "ec" =>
    2.33 @@ -283,7 +286,8 @@
    2.34        val ss = presburger_ss addsimps zadd_ac
    2.35        val ct = cert_Trueprop sg fm2
    2.36      in 
    2.37 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
    2.38 +      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
    2.39 +
    2.40      end;
    2.41  
    2.42  (*=============================================================*)
    2.43 @@ -917,6 +921,71 @@
    2.44  |cooper_prv _ _ _ =  error "Parameters format";
    2.45  
    2.46  
    2.47 +(* **************************************** *)
    2.48 +(*    An Other Version of cooper proving    *)
    2.49 +(*     by giving a withness for EX          *)
    2.50 +(* **************************************** *)
    2.51 +
    2.52 +
    2.53 +
    2.54 +fun cooper_prv_w sg (x as Free(xn,xT)) efm = let 
    2.55 +   (* lfm_thm : efm = linearized form of efm*)
    2.56 +   val lfm_thm = proof_of_linform sg [xn] efm
    2.57 +   (*efm2 is the linearized form of efm *) 
    2.58 +   val efm2 = snd(qe_get_terms lfm_thm)
    2.59 +   (* l is the lcm of all coefficients of x *)
    2.60 +   val l = formlcm x efm2
    2.61 +   (*ac_thm: efm = efm2 with adjusted coefficients of x *)
    2.62 +   val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
    2.63 +   (* fm is efm2 with adjusted coefficients of x *)
    2.64 +   val fm = snd (qe_get_terms ac_thm)
    2.65 +  (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
    2.66 +   val  cfm = unitycoeff x fm
    2.67 +   (*afm is fm where c*x is replaced by 1*x or -1*x *)
    2.68 +   val afm = adjustcoeff x l fm
    2.69 +   (* P = %x.afm*)
    2.70 +   val P = absfree(xn,xT,afm)
    2.71 +   (* This simpset allows the elimination of the sets in bex {1..d} *)
    2.72 +   val ss = presburger_ss addsimps
    2.73 +     [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
    2.74 +   (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
    2.75 +   val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
    2.76 +   (* e_ac_thm : Ex x. efm = EX x. fm*)
    2.77 +   val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
    2.78 +   (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
    2.79 +   val (lsuth,rsuth) = qe_get_terms (uth)
    2.80 +   (* lseacth = EX x. efm; rseacth = EX x. fm*)
    2.81 +   val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
    2.82 +
    2.83 +   val (w,rs) = cooper_w [] cfm
    2.84 +   val exp_cp_thm =  case w of 
    2.85 +     (* FIXME - e_ac_thm just tipped to test syntactical correctness of the program!!!!*)
    2.86 +    Some n =>  e_ac_thm (* Prove cfm (n) and use exI and then Eq_TrueI*)
    2.87 +   |_ => let 
    2.88 +    (* A and B set of the formula*)
    2.89 +    val A = aset x cfm
    2.90 +    val B = bset x cfm
    2.91 +    (* the divlcm (delta) of the formula*)
    2.92 +    val dlcm = mk_numeral (divlcm x cfm)
    2.93 +    (* Which set is smaller to generate the (hoepfully) shorter proof*)
    2.94 +    val cms = if ((length A) < (length B )) then "pi" else "mi"
    2.95 +    (* synthesize the proof of cooper's theorem*)
    2.96 +     (* cp_thm: EX x. cfm = Q*)
    2.97 +    val cp_thm = cooper_thm sg cms x cfm dlcm A B
    2.98 +     (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
    2.99 +    (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
   2.100 +    in refl RS (simplify ss (cp_thm RSN (2,trans)))
   2.101 +    end
   2.102 +   (* lscth = EX x. cfm; rscth = Q' *)
   2.103 +   val (lscth,rscth) = qe_get_terms (exp_cp_thm)
   2.104 +   (* u_c_thm: EX x. P(l*x) = Q'*)
   2.105 +   val  u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
   2.106 +   (* result: EX x. efm = Q'*)
   2.107 + in  ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
   2.108 +   end
   2.109 +|cooper_prv_w _ _ _ =  error "Parameters format";
   2.110 +
   2.111 +
   2.112  
   2.113  fun decomp_cnnf sg lfnp P = case P of 
   2.114       Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI )
     3.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Wed Aug 04 11:25:08 2004 +0200
     3.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Wed Aug 04 17:43:55 2004 +0200
     3.3 @@ -42,6 +42,7 @@
     3.4    val plusinf : term -> term -> term
     3.5    val onatoms : (term -> term) -> term -> term
     3.6    val evalc : term -> term
     3.7 +  val cooper_w : string list -> term -> (term option * term)
     3.8    val integer_qelim : Term.term -> Term.term
     3.9    val mk_presburger_oracle : (Sign.sg * exn) -> term
    3.10  end;
    3.11 @@ -197,7 +198,7 @@
    3.12   
    3.13           else (warning "lint: apparent nonlinearity"; raise COOPER)
    3.14           end 
    3.15 -  |_ =>   (error "COOPER:lint: unknown term  ")
    3.16 +  |_ =>  error ("COOPER:lint: unknown term  \n");
    3.17     
    3.18   
    3.19   
    3.20 @@ -414,7 +415,31 @@
    3.21  (* ------------------------------------------------------------------------- *) 
    3.22  (* Evaluation of constant expressions.                                       *) 
    3.23  (* ------------------------------------------------------------------------- *) 
    3.24 - 
    3.25 +
    3.26 +(* An other implementation of divides, that covers more cases*) 
    3.27 +
    3.28 +exception DVD_UNKNOWN
    3.29 +
    3.30 +fun dvd_op (d, t) = 
    3.31 + if not(is_numeral d) then raise DVD_UNKNOWN
    3.32 + else let 
    3.33 +   val dn = dest_numeral d
    3.34 +   fun coeffs_of x = case x of 
    3.35 +     Const(p,_) $ tl $ tr => 
    3.36 +       if p = "op +" then (coeffs_of tl) union (coeffs_of tr)
    3.37 +          else if p = "op *" 
    3.38 +	        then if (is_numeral tr) 
    3.39 +		 then [(dest_numeral tr) * (dest_numeral tl)] 
    3.40 +		 else [dest_numeral tl]
    3.41 +	        else []
    3.42 +    |_ => if (is_numeral t) then [dest_numeral t]  else []
    3.43 +   val ts = coeffs_of t
    3.44 +   in case ts of
    3.45 +     [] => raise DVD_UNKNOWN
    3.46 +    |_  => foldr (fn(k,r) => r andalso (k mod dn = 0)) (ts,true)
    3.47 +   end;
    3.48 +
    3.49 +
    3.50  val operations = 
    3.51    [("op =",op=), ("op <",op<), ("op >",op>), ("op <=",op<=) , ("op >=",op>=), 
    3.52     ("Divides.op dvd",fn (x,y) =>((y mod x) = 0))]; 
    3.53 @@ -423,22 +448,44 @@
    3.54      |applyoperation _ (_, _) = false; 
    3.55   
    3.56  (*Evaluation of constant atomic formulas*) 
    3.57 - 
    3.58 + (*FIXME : This is an optimation but still incorrect !! *)
    3.59 +(*
    3.60  fun evalc_atom at = case at of  
    3.61 -      (Const (p,_) $ s $ t) =>(  
    3.62 -         case assoc (operations,p) of 
    3.63 -             Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
    3.64 -              handle _ => at) 
    3.65 -             | _ =>  at) 
    3.66 -     |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
    3.67 -         case assoc (operations,p) of 
    3.68 -             Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
    3.69 -	     HOLogic.false_const else HOLogic.true_const)  
    3.70 -              handle _ => at) 
    3.71 -             | _ =>  at) 
    3.72 -     | _ =>  at; 
    3.73 - 
    3.74 -(*Function onatoms apllys function f on the atomic formulas involved in a.*) 
    3.75 +  (Const (p,_) $ s $ t) =>
    3.76 +   (if p="Divides.op dvd" then 
    3.77 +     ((if dvd_op(s,t) then HOLogic.true_const
    3.78 +     else HOLogic.false_const)
    3.79 +      handle _ => at)
    3.80 +    else
    3.81 +  case assoc (operations,p) of 
    3.82 +    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
    3.83 +    handle _ => at) 
    3.84 +      | _ =>  at) 
    3.85 +      |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
    3.86 +  case assoc (operations,p) of 
    3.87 +    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
    3.88 +    HOLogic.false_const else HOLogic.true_const)  
    3.89 +    handle _ => at) 
    3.90 +      | _ =>  at) 
    3.91 +      | _ =>  at; 
    3.92 +
    3.93 +*)
    3.94 +
    3.95 +fun evalc_atom at = case at of  
    3.96 +  (Const (p,_) $ s $ t) =>
    3.97 +   ( case assoc (operations,p) of 
    3.98 +    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
    3.99 +    handle _ => at) 
   3.100 +      | _ =>  at) 
   3.101 +      |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
   3.102 +  case assoc (operations,p) of 
   3.103 +    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
   3.104 +    HOLogic.false_const else HOLogic.true_const)  
   3.105 +    handle _ => at) 
   3.106 +      | _ =>  at) 
   3.107 +      | _ =>  at; 
   3.108 +
   3.109 + (*Function onatoms apllys function f on the atomic formulas involved in a.*) 
   3.110   
   3.111  fun onatoms f a = if (is_arith_rel a) then f a else case a of 
   3.112   
   3.113 @@ -653,6 +700,48 @@
   3.114    | _ => error "cooper: not an existential formula";
   3.115    
   3.116  
   3.117 +(* Try to find a withness for the formula *)
   3.118 +
   3.119 +fun inf_w mi d vars x p = 
   3.120 +  let val f = if mi then minusinf else plusinf in
   3.121 +   case (simpl (minusinf x p)) of
   3.122 +   Const("True",_)  => (Some (mk_numeral 1), HOLogic.true_const)
   3.123 +  |Const("False",_) => (None,HOLogic.false_const)
   3.124 +  |F => 
   3.125 +      let 
   3.126 +      fun h n =
   3.127 +       case ((simpl o evalc) (linrep vars x (mk_numeral n) F)) of 
   3.128 +	Const("True",_) => (Some (mk_numeral n),HOLogic.true_const)
   3.129 +       |F' => if n=1 then (None,F')
   3.130 +	     else let val (rw,rf) = h (n-1) in 
   3.131 +	       (rw,HOLogic.mk_disj(F',rf))
   3.132 +	     end
   3.133 +
   3.134 +      in (h d)
   3.135 +      end
   3.136 +  end;
   3.137 +
   3.138 +fun set_w d b st vars x p = let 
   3.139 +    fun h ns = case ns of 
   3.140 +    [] => (None,HOLogic.false_const)
   3.141 +   |n::nl => ( case ((simpl o evalc) (linrep vars x n p)) of
   3.142 +      Const("True",_) => (Some n,HOLogic.true_const)
   3.143 +      |F' => let val (rw,rf) = h nl 
   3.144 +             in (rw,HOLogic.mk_disj(F',rf)) 
   3.145 +	     end)
   3.146 +    val f = if b then linear_add else linear_sub
   3.147 +    val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) (1 upto d,[])
   3.148 +    in h p_elements
   3.149 +    end;
   3.150 +
   3.151 +fun withness d b st vars x p = case (inf_w b d vars x p) of 
   3.152 +   (Some n,_) => (Some n,HOLogic.true_const)
   3.153 +  |(None,Pinf) => (case (set_w d b st vars x p) of 
   3.154 +    (Some n,_) => (Some n,HOLogic.true_const)
   3.155 +    |(_,Pst) => (None,HOLogic.mk_disj(Pinf,Pst)));
   3.156 +
   3.157 +
   3.158 +
   3.159  
   3.160  (*Cooper main procedure*) 
   3.161    
   3.162 @@ -678,6 +767,29 @@
   3.163    | _ => error "cooper: not an existential formula";
   3.164  
   3.165  
   3.166 +(* A Version of cooper that returns a withness *)
   3.167 +fun cooper_w vars1 fm =
   3.168 +  case fm of
   3.169 +   Const ("Ex",_) $ Abs(x0,T,p0) => let 
   3.170 +    val (xn,p1) = variant_abs (x0,T,p0)
   3.171 +    val x = Free (xn,T)
   3.172 +    val vars = (xn::vars1)
   3.173 +(*     val p = unitycoeff x  (posineq (simpl p1)) *)
   3.174 +    val p = unitycoeff x  p1 
   3.175 +    val ast = aset x p
   3.176 +    val bst = bset x p
   3.177 +    val d = divlcm x p
   3.178 +    val (p_inf,S ) = 
   3.179 +    if (length bst) <= (length ast) 
   3.180 +     then (true,bst)
   3.181 +     else (false,ast)
   3.182 +    in withness d p_inf S vars x p 
   3.183 +(*    fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p
   3.184 +    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) S)
   3.185 +   in (list_disj (map stage js))
   3.186 +*)
   3.187 +   end
   3.188 +  | _ => error "cooper: not an existential formula";
   3.189  
   3.190   
   3.191  (*Function itlist applys a double parametred function f : 'a->'b->b iteratively to a List l : 'a 
   3.192 @@ -811,8 +923,8 @@
   3.193  fun mk_presburger_oracle (sg,COOPER_ORACLE t) = 
   3.194      if (!quick_and_dirty) 
   3.195      then HOLogic.mk_Trueprop (HOLogic.mk_eq(t,integer_qelim t))
   3.196 -    else raise COOPER_ORACLE t;
   3.197 -
   3.198 +    else raise COOPER_ORACLE t
   3.199 +    |mk_presburger_oracle (sg,_) = error "Oops";
   3.200  end;
   3.201  
   3.202  
     4.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Wed Aug 04 11:25:08 2004 +0200
     4.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Wed Aug 04 17:43:55 2004 +0200
     4.3 @@ -219,7 +219,8 @@
     4.4          [zdvd_iff_zmod_eq_0,unity_coeff_ex]
     4.5        val ct =  cert_Trueprop sg fm2
     4.6      in 
     4.7 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
     4.8 +      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)] 
     4.9 +
    4.10      end
    4.11  
    4.12    (*"bl" like blast tactic*)
    4.13 @@ -251,7 +252,8 @@
    4.14  
    4.15    | "fa" =>
    4.16      let val ct = cert_Trueprop sg fm2
    4.17 -    in simple_prove_goal_cterm2 ct [simple_arith_tac 1]
    4.18 +    in simple_prove_goal_cterm2 ct [simple_arith_tac 1]  
    4.19 +
    4.20      end
    4.21  
    4.22    | "sa" =>
    4.23 @@ -259,7 +261,8 @@
    4.24        val ss = presburger_ss addsimps zadd_ac
    4.25        val ct = cert_Trueprop sg fm2
    4.26      in 
    4.27 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
    4.28 +      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
    4.29 +
    4.30      end
    4.31    (* like Existance Conjunction *)
    4.32    | "ec" =>
    4.33 @@ -283,7 +286,8 @@
    4.34        val ss = presburger_ss addsimps zadd_ac
    4.35        val ct = cert_Trueprop sg fm2
    4.36      in 
    4.37 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
    4.38 +      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
    4.39 +
    4.40      end;
    4.41  
    4.42  (*=============================================================*)
    4.43 @@ -917,6 +921,71 @@
    4.44  |cooper_prv _ _ _ =  error "Parameters format";
    4.45  
    4.46  
    4.47 +(* **************************************** *)
    4.48 +(*    An Other Version of cooper proving    *)
    4.49 +(*     by giving a withness for EX          *)
    4.50 +(* **************************************** *)
    4.51 +
    4.52 +
    4.53 +
    4.54 +fun cooper_prv_w sg (x as Free(xn,xT)) efm = let 
    4.55 +   (* lfm_thm : efm = linearized form of efm*)
    4.56 +   val lfm_thm = proof_of_linform sg [xn] efm
    4.57 +   (*efm2 is the linearized form of efm *) 
    4.58 +   val efm2 = snd(qe_get_terms lfm_thm)
    4.59 +   (* l is the lcm of all coefficients of x *)
    4.60 +   val l = formlcm x efm2
    4.61 +   (*ac_thm: efm = efm2 with adjusted coefficients of x *)
    4.62 +   val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
    4.63 +   (* fm is efm2 with adjusted coefficients of x *)
    4.64 +   val fm = snd (qe_get_terms ac_thm)
    4.65 +  (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
    4.66 +   val  cfm = unitycoeff x fm
    4.67 +   (*afm is fm where c*x is replaced by 1*x or -1*x *)
    4.68 +   val afm = adjustcoeff x l fm
    4.69 +   (* P = %x.afm*)
    4.70 +   val P = absfree(xn,xT,afm)
    4.71 +   (* This simpset allows the elimination of the sets in bex {1..d} *)
    4.72 +   val ss = presburger_ss addsimps
    4.73 +     [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
    4.74 +   (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
    4.75 +   val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
    4.76 +   (* e_ac_thm : Ex x. efm = EX x. fm*)
    4.77 +   val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
    4.78 +   (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
    4.79 +   val (lsuth,rsuth) = qe_get_terms (uth)
    4.80 +   (* lseacth = EX x. efm; rseacth = EX x. fm*)
    4.81 +   val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
    4.82 +
    4.83 +   val (w,rs) = cooper_w [] cfm
    4.84 +   val exp_cp_thm =  case w of 
    4.85 +     (* FIXME - e_ac_thm just tipped to test syntactical correctness of the program!!!!*)
    4.86 +    Some n =>  e_ac_thm (* Prove cfm (n) and use exI and then Eq_TrueI*)
    4.87 +   |_ => let 
    4.88 +    (* A and B set of the formula*)
    4.89 +    val A = aset x cfm
    4.90 +    val B = bset x cfm
    4.91 +    (* the divlcm (delta) of the formula*)
    4.92 +    val dlcm = mk_numeral (divlcm x cfm)
    4.93 +    (* Which set is smaller to generate the (hoepfully) shorter proof*)
    4.94 +    val cms = if ((length A) < (length B )) then "pi" else "mi"
    4.95 +    (* synthesize the proof of cooper's theorem*)
    4.96 +     (* cp_thm: EX x. cfm = Q*)
    4.97 +    val cp_thm = cooper_thm sg cms x cfm dlcm A B
    4.98 +     (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
    4.99 +    (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
   4.100 +    in refl RS (simplify ss (cp_thm RSN (2,trans)))
   4.101 +    end
   4.102 +   (* lscth = EX x. cfm; rscth = Q' *)
   4.103 +   val (lscth,rscth) = qe_get_terms (exp_cp_thm)
   4.104 +   (* u_c_thm: EX x. P(l*x) = Q'*)
   4.105 +   val  u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
   4.106 +   (* result: EX x. efm = Q'*)
   4.107 + in  ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
   4.108 +   end
   4.109 +|cooper_prv_w _ _ _ =  error "Parameters format";
   4.110 +
   4.111 +
   4.112  
   4.113  fun decomp_cnnf sg lfnp P = case P of 
   4.114       Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI )