src/HOL/Library/positivstellensatz.ML
changeset 32829 671eb46eb0a3
parent 32828 ad76967c703d
child 32843 c8f5a7c8353f
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue Sep 22 14:17:54 2009 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Sep 30 13:48:00 2009 +0200
     1.3 @@ -8,41 +8,24 @@
     1.4  
     1.5  signature FUNC = 
     1.6  sig
     1.7 - type 'a T
     1.8 - type key
     1.9 - val apply : 'a T -> key -> 'a
    1.10 - val applyd :'a T -> (key -> 'a) -> key -> 'a
    1.11 - val combine : ('a -> 'a -> 'a) -> ('a -> bool) -> 'a T -> 'a T -> 'a T
    1.12 - val defined : 'a T -> key -> bool
    1.13 - val dom : 'a T -> key list
    1.14 - val fold : (key * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b
    1.15 - val fold_rev : (key * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b
    1.16 - val graph : 'a T -> (key * 'a) list
    1.17 - val is_undefined : 'a T -> bool
    1.18 - val mapf : ('a -> 'b) -> 'a T -> 'b T
    1.19 - val tryapplyd : 'a T -> key -> 'a -> 'a
    1.20 - val undefine :  key -> 'a T -> 'a T
    1.21 - val undefined : 'a T
    1.22 - val update : key * 'a -> 'a T -> 'a T
    1.23 - val updatep : (key * 'a -> bool) -> key * 'a -> 'a T -> 'a T
    1.24 - val choose : 'a T -> key * 'a
    1.25 - val onefunc : key * 'a -> 'a T
    1.26 - val get_first: (key*'a -> 'a option) -> 'a T -> 'a option
    1.27 + include TABLE
    1.28 + val apply : 'a table -> key -> 'a
    1.29 + val applyd :'a table -> (key -> 'a) -> key -> 'a
    1.30 + val combine : ('a -> 'a -> 'a) -> ('a -> bool) -> 'a table -> 'a table -> 'a table
    1.31 + val dom : 'a table -> key list
    1.32 + val tryapplyd : 'a table -> key -> 'a -> 'a
    1.33 + val updatep : (key * 'a -> bool) -> key * 'a -> 'a table -> 'a table
    1.34 + val choose : 'a table -> key * 'a
    1.35 + val onefunc : key * 'a -> 'a table
    1.36  end;
    1.37  
    1.38  functor FuncFun(Key: KEY) : FUNC=
    1.39  struct
    1.40  
    1.41 -type key = Key.key;
    1.42  structure Tab = Table(Key);
    1.43 -type 'a T = 'a Tab.table;
    1.44  
    1.45 -val undefined = Tab.empty;
    1.46 -val is_undefined = Tab.is_empty;
    1.47 -val mapf = Tab.map;
    1.48 -val fold = Tab.fold;
    1.49 -val fold_rev = Tab.fold_rev;
    1.50 -val graph = Tab.dest;
    1.51 +open Tab;
    1.52 +
    1.53  fun dom a = sort Key.ord (Tab.keys a);
    1.54  fun applyd f d x = case Tab.lookup f x of 
    1.55     SOME y => y
    1.56 @@ -50,9 +33,6 @@
    1.57  
    1.58  fun apply f x = applyd f (fn _ => raise Tab.UNDEF x) x;
    1.59  fun tryapplyd f a d = applyd f (K d) a;
    1.60 -val defined = Tab.defined;
    1.61 -fun undefine x t = (Tab.delete x t handle UNDEF => t);
    1.62 -val update = Tab.update;
    1.63  fun updatep p (k,v) t = if p (k, v) then t else update (k,v) t
    1.64  fun combine f z a b = 
    1.65   let
    1.66 @@ -64,16 +44,10 @@
    1.67  
    1.68  fun choose f = case Tab.min_key f of 
    1.69     SOME k => (k,valOf (Tab.lookup f k))
    1.70 - | NONE => error "FuncFun.choose : Completely undefined function"
    1.71 -
    1.72 -fun onefunc kv = update kv undefined
    1.73 + | NONE => error "FuncFun.choose : Completely empty function"
    1.74  
    1.75 -local
    1.76 -fun  find f (k,v) NONE = f (k,v)
    1.77 -   | find f (k,v) r = r
    1.78 -in
    1.79 -fun get_first f t = fold (find f) t NONE
    1.80 -end
    1.81 +fun onefunc kv = update kv empty
    1.82 +
    1.83  end;
    1.84  
    1.85  (* Some standard functors and utility functions for them *)
    1.86 @@ -81,33 +55,31 @@
    1.87  structure FuncUtil =
    1.88  struct
    1.89  
    1.90 -fun increasing f ord (x,y) = ord (f x, f y);
    1.91 -
    1.92  structure Intfunc = FuncFun(type key = int val ord = int_ord);
    1.93  structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord);
    1.94  structure Intpairfunc = FuncFun(type key = int*int val ord = prod_ord int_ord int_ord);
    1.95  structure Symfunc = FuncFun(type key = string val ord = fast_string_ord);
    1.96  structure Termfunc = FuncFun(type key = term val ord = TermOrd.fast_term_ord);
    1.97  
    1.98 -val cterm_ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t))
    1.99 +val cterm_ord = TermOrd.fast_term_ord o pairself term_of
   1.100  
   1.101  structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord);
   1.102  
   1.103 -type monomial = int Ctermfunc.T;
   1.104 +type monomial = int Ctermfunc.table;
   1.105  
   1.106 -fun monomial_ord (m1,m2) = list_ord (prod_ord cterm_ord int_ord) (Ctermfunc.graph m1, Ctermfunc.graph m2)
   1.107 +val monomial_ord = list_ord (prod_ord cterm_ord int_ord) o pairself Ctermfunc.dest
   1.108  
   1.109  structure Monomialfunc = FuncFun(type key = monomial val ord = monomial_ord)
   1.110  
   1.111 -type poly = Rat.rat Monomialfunc.T;
   1.112 +type poly = Rat.rat Monomialfunc.table;
   1.113  
   1.114  (* The ordering so we can create canonical HOL polynomials.                  *)
   1.115  
   1.116 -fun dest_monomial mon = sort (increasing fst cterm_ord) (Ctermfunc.graph mon);
   1.117 +fun dest_monomial mon = sort (cterm_ord o pairself fst) (Ctermfunc.dest mon);
   1.118  
   1.119  fun monomial_order (m1,m2) =
   1.120 - if Ctermfunc.is_undefined m2 then LESS 
   1.121 - else if Ctermfunc.is_undefined m1 then GREATER 
   1.122 + if Ctermfunc.is_empty m2 then LESS 
   1.123 + else if Ctermfunc.is_empty m1 then GREATER 
   1.124   else
   1.125    let val mon1 = dest_monomial m1 
   1.126        val mon2 = dest_monomial m2
   1.127 @@ -357,7 +329,7 @@
   1.128    (Numeral.mk_cnumber @{ctyp nat} k)
   1.129  
   1.130  fun cterm_of_monomial m = 
   1.131 - if FuncUtil.Ctermfunc.is_undefined m then @{cterm "1::real"} 
   1.132 + if FuncUtil.Ctermfunc.is_empty m then @{cterm "1::real"} 
   1.133   else 
   1.134    let 
   1.135     val m' = FuncUtil.dest_monomial m
   1.136 @@ -365,16 +337,16 @@
   1.137    in foldr1 (fn (s, t) => Thm.capply (Thm.capply @{cterm "op * :: real => _"} s) t) vps
   1.138    end
   1.139  
   1.140 -fun cterm_of_cmonomial (m,c) = if FuncUtil.Ctermfunc.is_undefined m then cterm_of_rat c
   1.141 +fun cterm_of_cmonomial (m,c) = if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
   1.142      else if c = Rat.one then cterm_of_monomial m
   1.143      else Thm.capply (Thm.capply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
   1.144  
   1.145  fun cterm_of_poly p = 
   1.146 - if FuncUtil.Monomialfunc.is_undefined p then @{cterm "0::real"} 
   1.147 + if FuncUtil.Monomialfunc.is_empty p then @{cterm "0::real"} 
   1.148   else
   1.149    let 
   1.150     val cms = map cterm_of_cmonomial
   1.151 -     (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.graph p))
   1.152 +     (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p))
   1.153    in foldr1 (fn (t1, t2) => Thm.capply(Thm.capply @{cterm "op + :: real => _"} t1) t2) cms
   1.154    end;
   1.155  
   1.156 @@ -593,10 +565,11 @@
   1.157  (* A linear arithmetic prover *)
   1.158  local
   1.159    val linear_add = FuncUtil.Ctermfunc.combine (curry op +/) (fn z => z =/ Rat.zero)
   1.160 -  fun linear_cmul c = FuncUtil.Ctermfunc.mapf (fn x => c */ x)
   1.161 +  fun linear_cmul c = FuncUtil.Ctermfunc.map (fn x => c */ x)
   1.162    val one_tm = @{cterm "1::real"}
   1.163 -  fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_undefined e) andalso not(p Rat.zero)) orelse
   1.164 -     ((gen_eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso not(p(FuncUtil.Ctermfunc.apply e one_tm)))
   1.165 +  fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
   1.166 +     ((gen_eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
   1.167 +       not(p(FuncUtil.Ctermfunc.apply e one_tm)))
   1.168  
   1.169    fun linear_ineqs vars (les,lts) = 
   1.170     case find_first (contradictory (fn x => x >/ Rat.zero)) lts of
   1.171 @@ -650,9 +623,9 @@
   1.172             (fold_rev (curry (gen_union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
   1.173       in linear_ineqs vars (les,lts) end
   1.174     | (e,p)::es => 
   1.175 -     if FuncUtil.Ctermfunc.is_undefined e then linear_eqs (es,les,lts) else
   1.176 +     if FuncUtil.Ctermfunc.is_empty e then linear_eqs (es,les,lts) else
   1.177       let 
   1.178 -      val (x,c) = FuncUtil.Ctermfunc.choose (FuncUtil.Ctermfunc.undefine one_tm e)
   1.179 +      val (x,c) = FuncUtil.Ctermfunc.choose (FuncUtil.Ctermfunc.delete_safe one_tm e)
   1.180        fun xform (inp as (t,q)) =
   1.181         let val d = FuncUtil.Ctermfunc.tryapplyd t x Rat.zero in
   1.182          if d =/ Rat.zero then inp else
   1.183 @@ -660,7 +633,7 @@
   1.184           val k = (Rat.neg d) */ Rat.abs c // c
   1.185           val e' = linear_cmul k e
   1.186           val t' = linear_cmul (Rat.abs c) t
   1.187 -         val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.undefined, k),p)
   1.188 +         val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p)
   1.189           val q' = Product(Rational_lt(Rat.abs c),q) 
   1.190          in (linear_add e' t',Sum(p',q')) 
   1.191          end 
   1.192 @@ -677,7 +650,7 @@
   1.193     end 
   1.194    
   1.195    fun lin_of_hol ct = 
   1.196 -   if ct aconvc @{cterm "0::real"} then FuncUtil.Ctermfunc.undefined
   1.197 +   if ct aconvc @{cterm "0::real"} then FuncUtil.Ctermfunc.empty
   1.198     else if not (is_comb ct) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   1.199     else if is_ratconst ct then FuncUtil.Ctermfunc.onefunc (one_tm, dest_ratconst ct)
   1.200     else