src/HOL/Integ/cooper_dec.ML
changeset 15107 f233706d9fce
parent 14981 e73f8140af78
child 15164 5d7c96e0f9dc
     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