tuned FuncFun and FuncUtil structure in positivstellensatz.ML
authorPhilipp Meyer
Wed Sep 30 13:48:00 2009 +0200 (2009-09-30)
changeset 32829671eb46eb0a3
parent 32828 ad76967c703d
child 32830 47c1b15c03fe
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
     1.1 --- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Tue Sep 22 14:17:54 2009 +0200
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Wed Sep 30 13:48:00 2009 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4    end
     1.5  
     1.6  fun string_of_monomial m = 
     1.7 - if FuncUtil.Ctermfunc.is_undefined m then "1" 
     1.8 + if FuncUtil.Ctermfunc.is_empty m then "1" 
     1.9   else 
    1.10    let 
    1.11     val m' = FuncUtil.dest_monomial m
    1.12 @@ -48,16 +48,16 @@
    1.13    end
    1.14  
    1.15  fun string_of_cmonomial (m,c) =
    1.16 -  if FuncUtil.Ctermfunc.is_undefined m then string_of_rat c
    1.17 +  if FuncUtil.Ctermfunc.is_empty m then string_of_rat c
    1.18    else if c = Rat.one then string_of_monomial m
    1.19    else (string_of_rat c) ^ "*" ^ (string_of_monomial m);
    1.20  
    1.21  fun string_of_poly p = 
    1.22 - if FuncUtil.Monomialfunc.is_undefined p then "0" 
    1.23 + if FuncUtil.Monomialfunc.is_empty p then "0" 
    1.24   else
    1.25    let 
    1.26     val cms = map string_of_cmonomial
    1.27 -     (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.graph p))
    1.28 +     (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p))
    1.29    in foldr1 (fn (t1, t2) => t1 ^ " + " ^ t2) cms
    1.30    end;
    1.31  
    1.32 @@ -101,15 +101,15 @@
    1.33    (fn (x, k) => (cterm_of (Context.theory_of_proof ctxt) (Free (x, @{typ real})), k)) 
    1.34  
    1.35  fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
    1.36 -  foldl (uncurry FuncUtil.Ctermfunc.update) FuncUtil.Ctermfunc.undefined
    1.37 +  foldl (uncurry FuncUtil.Ctermfunc.update) FuncUtil.Ctermfunc.empty
    1.38  
    1.39  fun parse_cmonomial ctxt =
    1.40    rat_int --| str "*" -- (parse_monomial ctxt) >> swap ||
    1.41    (parse_monomial ctxt) >> (fn m => (m, Rat.one)) ||
    1.42 -  rat_int >> (fn r => (FuncUtil.Ctermfunc.undefined, r))
    1.43 +  rat_int >> (fn r => (FuncUtil.Ctermfunc.empty, r))
    1.44  
    1.45  fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >>
    1.46 -  foldl (uncurry FuncUtil.Monomialfunc.update) FuncUtil.Monomialfunc.undefined
    1.47 +  foldl (uncurry FuncUtil.Monomialfunc.update) FuncUtil.Monomialfunc.empty
    1.48  
    1.49  (* positivstellensatz parser *)
    1.50  
     2.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Tue Sep 22 14:17:54 2009 +0200
     2.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Wed Sep 30 13:48:00 2009 +0200
     2.3 @@ -102,9 +102,9 @@
     2.4  
     2.5  (* The main types.                                                           *)
     2.6  
     2.7 -type vector = int* Rat.rat FuncUtil.Intfunc.T;
     2.8 +type vector = int* Rat.rat FuncUtil.Intfunc.table;
     2.9  
    2.10 -type matrix = (int*int)*(Rat.rat FuncUtil.Intpairfunc.T);
    2.11 +type matrix = (int*int)*(Rat.rat FuncUtil.Intpairfunc.table);
    2.12  
    2.13  fun iszero (k,r) = r =/ rat_0;
    2.14  
    2.15 @@ -116,23 +116,23 @@
    2.16   
    2.17  (* Vectors. Conventionally indexed 1..n.                                     *)
    2.18  
    2.19 -fun vector_0 n = (n,FuncUtil.Intfunc.undefined):vector;
    2.20 +fun vector_0 n = (n,FuncUtil.Intfunc.empty):vector;
    2.21  
    2.22  fun dim (v:vector) = fst v;
    2.23  
    2.24  fun vector_const c n =
    2.25    if c =/ rat_0 then vector_0 n
    2.26 -  else (n,fold_rev (fn k => FuncUtil.Intfunc.update (k,c)) (1 upto n) FuncUtil.Intfunc.undefined) :vector;
    2.27 +  else (n,fold_rev (fn k => FuncUtil.Intfunc.update (k,c)) (1 upto n) FuncUtil.Intfunc.empty) :vector;
    2.28  
    2.29  val vector_1 = vector_const rat_1;
    2.30  
    2.31  fun vector_cmul c (v:vector) =
    2.32   let val n = dim v 
    2.33   in if c =/ rat_0 then vector_0 n
    2.34 -    else (n,FuncUtil.Intfunc.mapf (fn x => c */ x) (snd v))
    2.35 +    else (n,FuncUtil.Intfunc.map (fn x => c */ x) (snd v))
    2.36   end;
    2.37  
    2.38 -fun vector_neg (v:vector) = (fst v,FuncUtil.Intfunc.mapf Rat.neg (snd v)) :vector;
    2.39 +fun vector_neg (v:vector) = (fst v,FuncUtil.Intfunc.map Rat.neg (snd v)) :vector;
    2.40  
    2.41  fun vector_add (v1:vector) (v2:vector) =
    2.42   let val m = dim v1  
    2.43 @@ -153,30 +153,30 @@
    2.44  
    2.45  fun vector_of_list l =
    2.46   let val n = length l 
    2.47 - in (n,fold_rev2 (curry FuncUtil.Intfunc.update) (1 upto n) l FuncUtil.Intfunc.undefined) :vector
    2.48 + in (n,fold_rev2 (curry FuncUtil.Intfunc.update) (1 upto n) l FuncUtil.Intfunc.empty) :vector
    2.49   end;
    2.50  
    2.51  (* Matrices; again rows and columns indexed from 1.                          *)
    2.52  
    2.53 -fun matrix_0 (m,n) = ((m,n),FuncUtil.Intpairfunc.undefined):matrix;
    2.54 +fun matrix_0 (m,n) = ((m,n),FuncUtil.Intpairfunc.empty):matrix;
    2.55  
    2.56  fun dimensions (m:matrix) = fst m;
    2.57  
    2.58  fun matrix_const c (mn as (m,n)) =
    2.59    if m <> n then error "matrix_const: needs to be square"
    2.60    else if c =/ rat_0 then matrix_0 mn
    2.61 -  else (mn,fold_rev (fn k => FuncUtil.Intpairfunc.update ((k,k), c)) (1 upto n) FuncUtil.Intpairfunc.undefined) :matrix;;
    2.62 +  else (mn,fold_rev (fn k => FuncUtil.Intpairfunc.update ((k,k), c)) (1 upto n) FuncUtil.Intpairfunc.empty) :matrix;;
    2.63  
    2.64  val matrix_1 = matrix_const rat_1;
    2.65  
    2.66  fun matrix_cmul c (m:matrix) =
    2.67   let val (i,j) = dimensions m 
    2.68   in if c =/ rat_0 then matrix_0 (i,j)
    2.69 -    else ((i,j),FuncUtil.Intpairfunc.mapf (fn x => c */ x) (snd m))
    2.70 +    else ((i,j),FuncUtil.Intpairfunc.map (fn x => c */ x) (snd m))
    2.71   end;
    2.72  
    2.73  fun matrix_neg (m:matrix) = 
    2.74 -  (dimensions m, FuncUtil.Intpairfunc.mapf Rat.neg (snd m)) :matrix;
    2.75 +  (dimensions m, FuncUtil.Intpairfunc.map Rat.neg (snd m)) :matrix;
    2.76  
    2.77  fun matrix_add (m1:matrix) (m2:matrix) =
    2.78   let val d1 = dimensions m1 
    2.79 @@ -191,32 +191,32 @@
    2.80  fun row k (m:matrix) =
    2.81   let val (i,j) = dimensions m 
    2.82   in (j,
    2.83 -   FuncUtil.Intpairfunc.fold (fn ((i,j), c) => fn a => if i = k then FuncUtil.Intfunc.update (j,c) a else a) (snd m) FuncUtil.Intfunc.undefined ) : vector
    2.84 +   FuncUtil.Intpairfunc.fold (fn ((i,j), c) => fn a => if i = k then FuncUtil.Intfunc.update (j,c) a else a) (snd m) FuncUtil.Intfunc.empty ) : vector
    2.85   end;
    2.86  
    2.87  fun column k (m:matrix) =
    2.88    let val (i,j) = dimensions m 
    2.89    in (i,
    2.90 -   FuncUtil.Intpairfunc.fold (fn ((i,j), c) => fn a => if j = k then FuncUtil.Intfunc.update (i,c) a else a) (snd m)  FuncUtil.Intfunc.undefined)
    2.91 +   FuncUtil.Intpairfunc.fold (fn ((i,j), c) => fn a => if j = k then FuncUtil.Intfunc.update (i,c) a else a) (snd m)  FuncUtil.Intfunc.empty)
    2.92     : vector
    2.93   end;
    2.94  
    2.95  fun transp (m:matrix) =
    2.96    let val (i,j) = dimensions m 
    2.97    in
    2.98 -  ((j,i),FuncUtil.Intpairfunc.fold (fn ((i,j), c) => fn a => FuncUtil.Intpairfunc.update ((j,i), c) a) (snd m) FuncUtil.Intpairfunc.undefined) :matrix
    2.99 +  ((j,i),FuncUtil.Intpairfunc.fold (fn ((i,j), c) => fn a => FuncUtil.Intpairfunc.update ((j,i), c) a) (snd m) FuncUtil.Intpairfunc.empty) :matrix
   2.100   end;
   2.101  
   2.102  fun diagonal (v:vector) =
   2.103   let val n = dim v 
   2.104 - in ((n,n),FuncUtil.Intfunc.fold (fn (i, c) => fn a => FuncUtil.Intpairfunc.update ((i,i), c) a) (snd v) FuncUtil.Intpairfunc.undefined) : matrix
   2.105 + in ((n,n),FuncUtil.Intfunc.fold (fn (i, c) => fn a => FuncUtil.Intpairfunc.update ((i,i), c) a) (snd v) FuncUtil.Intpairfunc.empty) : matrix
   2.106   end;
   2.107  
   2.108  fun matrix_of_list l =
   2.109   let val m = length l 
   2.110   in if m = 0 then matrix_0 (0,0) else
   2.111     let val n = length (hd l) 
   2.112 -   in ((m,n),itern 1 l (fn v => fn i => itern 1 v (fn c => fn j => FuncUtil.Intpairfunc.update ((i,j), c))) FuncUtil.Intpairfunc.undefined)
   2.113 +   in ((m,n),itern 1 l (fn v => fn i => itern 1 v (fn c => fn j => FuncUtil.Intpairfunc.update ((i,j), c))) FuncUtil.Intpairfunc.empty)
   2.114     end
   2.115   end;
   2.116  
   2.117 @@ -225,7 +225,7 @@
   2.118  fun monomial_eval assig m =
   2.119    FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => a */ rat_pow (FuncUtil.Ctermfunc.apply assig x) k)
   2.120          m rat_1;
   2.121 -val monomial_1 = FuncUtil.Ctermfunc.undefined;
   2.122 +val monomial_1 = FuncUtil.Ctermfunc.empty;
   2.123  
   2.124  fun monomial_var x = FuncUtil.Ctermfunc.onefunc (x, 1);
   2.125  
   2.126 @@ -234,14 +234,14 @@
   2.127  
   2.128  fun monomial_pow m k =
   2.129    if k = 0 then monomial_1
   2.130 -  else FuncUtil.Ctermfunc.mapf (fn x => k * x) m;
   2.131 +  else FuncUtil.Ctermfunc.map (fn x => k * x) m;
   2.132  
   2.133  fun monomial_divides m1 m2 =
   2.134    FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => FuncUtil.Ctermfunc.tryapplyd m2 x 0 >= k andalso a) m1 true;;
   2.135  
   2.136  fun monomial_div m1 m2 =
   2.137   let val m = FuncUtil.Ctermfunc.combine (curry op +) 
   2.138 -   (fn x => x = 0) m1 (FuncUtil.Ctermfunc.mapf (fn x => ~ x) m2) 
   2.139 +   (fn x => x = 0) m1 (FuncUtil.Ctermfunc.map (fn x => ~ x) m2) 
   2.140   in if FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k >= 0 andalso a) m true then m
   2.141    else error "monomial_div: non-divisible"
   2.142   end;
   2.143 @@ -251,7 +251,7 @@
   2.144  
   2.145  fun monomial_lcm m1 m2 =
   2.146    fold_rev (fn x => FuncUtil.Ctermfunc.update (x, max (monomial_degree x m1) (monomial_degree x m2)))
   2.147 -          (gen_union (is_equal o  FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1, FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.undefined);
   2.148 +          (gen_union (is_equal o  FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1, FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.empty);
   2.149  
   2.150  fun monomial_multidegree m = 
   2.151   FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k + a) m 0;;
   2.152 @@ -263,10 +263,10 @@
   2.153  fun eval assig p =
   2.154    FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => a +/ c */ monomial_eval assig m) p rat_0;
   2.155  
   2.156 -val poly_0 = FuncUtil.Monomialfunc.undefined;
   2.157 +val poly_0 = FuncUtil.Monomialfunc.empty;
   2.158  
   2.159  fun poly_isconst p = 
   2.160 -  FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => FuncUtil.Ctermfunc.is_undefined m andalso a) p true;
   2.161 +  FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => FuncUtil.Ctermfunc.is_empty m andalso a) p true;
   2.162  
   2.163  fun poly_var x = FuncUtil.Monomialfunc.onefunc (monomial_var x,rat_1);
   2.164  
   2.165 @@ -275,9 +275,9 @@
   2.166  
   2.167  fun poly_cmul c p =
   2.168    if c =/ rat_0 then poly_0
   2.169 -  else FuncUtil.Monomialfunc.mapf (fn x => c */ x) p;
   2.170 +  else FuncUtil.Monomialfunc.map (fn x => c */ x) p;
   2.171  
   2.172 -fun poly_neg p = FuncUtil.Monomialfunc.mapf Rat.neg p;;
   2.173 +fun poly_neg p = FuncUtil.Monomialfunc.map Rat.neg p;;
   2.174  
   2.175  fun poly_add p1 p2 =
   2.176    FuncUtil.Monomialfunc.combine (curry op +/) (fn x => x =/ rat_0) p1 p2;
   2.177 @@ -286,8 +286,8 @@
   2.178  
   2.179  fun poly_cmmul (c,m) p =
   2.180   if c =/ rat_0 then poly_0
   2.181 - else if FuncUtil.Ctermfunc.is_undefined m 
   2.182 -      then FuncUtil.Monomialfunc.mapf (fn d => c */ d) p
   2.183 + else if FuncUtil.Ctermfunc.is_empty m 
   2.184 +      then FuncUtil.Monomialfunc.map (fn d => c */ d) p
   2.185        else FuncUtil.Monomialfunc.fold (fn (m', d) => fn a => (FuncUtil.Monomialfunc.update (monomial_mul m m', c */ d) a)) p poly_0;
   2.186  
   2.187  fun poly_mul p1 p2 =
   2.188 @@ -296,7 +296,7 @@
   2.189  fun poly_div p1 p2 =
   2.190   if not(poly_isconst p2) 
   2.191   then error "poly_div: non-constant" else
   2.192 - let val c = eval FuncUtil.Ctermfunc.undefined p2 
   2.193 + let val c = eval FuncUtil.Ctermfunc.empty p2 
   2.194   in if c =/ rat_0 then error "poly_div: division by zero"
   2.195      else poly_cmul (Rat.inv c) p1
   2.196   end;
   2.197 @@ -312,7 +312,7 @@
   2.198  fun poly_exp p1 p2 =
   2.199    if not(poly_isconst p2) 
   2.200    then error "poly_exp: not a constant" 
   2.201 -  else poly_pow p1 (int_of_rat (eval FuncUtil.Ctermfunc.undefined p2));
   2.202 +  else poly_pow p1 (int_of_rat (eval FuncUtil.Ctermfunc.empty p2));
   2.203  
   2.204  fun degree x p = 
   2.205   FuncUtil.Monomialfunc.fold (fn (m,c) => fn a => max (monomial_degree x m) a) p 0;
   2.206 @@ -321,7 +321,7 @@
   2.207    FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => max (monomial_multidegree m) a) p 0;
   2.208  
   2.209  fun poly_variables p =
   2.210 -  sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => curry (gen_union (is_equal o  FuncUtil.cterm_ord)) (monomial_variables m)) p []);;
   2.211 +  sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => curry (gen_union (is_equal o FuncUtil.cterm_ord)) (monomial_variables m)) p []);;
   2.212  
   2.213  (* Order monomials for human presentation.                                   *)
   2.214  
   2.215 @@ -337,8 +337,8 @@
   2.216     | EQUAL => ord (t1,t2)
   2.217     | GREATER => GREATER)
   2.218  in fun humanorder_monomial m1 m2 = 
   2.219 - ord (sort humanorder_varpow (FuncUtil.Ctermfunc.graph m1),
   2.220 -  sort humanorder_varpow (FuncUtil.Ctermfunc.graph m2))
   2.221 + ord (sort humanorder_varpow (FuncUtil.Ctermfunc.dest m1),
   2.222 +  sort humanorder_varpow (FuncUtil.Ctermfunc.dest m2))
   2.223  end;
   2.224  
   2.225  (* Conversions to strings.                                                   *)
   2.226 @@ -383,21 +383,21 @@
   2.227    else string_of_cterm x^"^"^string_of_int k;
   2.228  
   2.229  fun string_of_monomial m =
   2.230 - if FuncUtil.Ctermfunc.is_undefined m then "1" else
   2.231 + if FuncUtil.Ctermfunc.is_empty m then "1" else
   2.232   let val vps = fold_rev (fn (x,k) => fn a => string_of_varpow x k :: a)
   2.233 -  (sort humanorder_varpow (FuncUtil.Ctermfunc.graph m)) [] 
   2.234 +  (sort humanorder_varpow (FuncUtil.Ctermfunc.dest m)) [] 
   2.235   in foldr1 (fn (s, t) => s^"*"^t) vps
   2.236   end;
   2.237  
   2.238  fun string_of_cmonomial (c,m) =
   2.239 - if FuncUtil.Ctermfunc.is_undefined m then Rat.string_of_rat c
   2.240 + if FuncUtil.Ctermfunc.is_empty m then Rat.string_of_rat c
   2.241   else if c =/ rat_1 then string_of_monomial m
   2.242   else Rat.string_of_rat c ^ "*" ^ string_of_monomial m;;
   2.243  
   2.244  fun string_of_poly p =
   2.245 - if FuncUtil.Monomialfunc.is_undefined p then "<<0>>" else
   2.246 + if FuncUtil.Monomialfunc.is_empty p then "<<0>>" else
   2.247   let 
   2.248 -  val cms = sort (fn ((m1,_),(m2,_)) => humanorder_monomial m1  m2) (FuncUtil.Monomialfunc.graph p)
   2.249 +  val cms = sort (fn ((m1,_),(m2,_)) => humanorder_monomial m1  m2) (FuncUtil.Monomialfunc.dest p)
   2.250    val s = fold (fn (m,c) => fn a =>
   2.251               if c </ rat_0 then a ^ " - " ^ string_of_cmonomial(Rat.neg c,m)
   2.252               else a ^ " + " ^ string_of_cmonomial(c,m))
   2.253 @@ -430,7 +430,7 @@
   2.254        else if lop aconvc inv_tm then
   2.255         let val p = poly_of_term r 
   2.256         in if poly_isconst p 
   2.257 -          then poly_const(Rat.inv (eval FuncUtil.Ctermfunc.undefined p))
   2.258 +          then poly_const(Rat.inv (eval FuncUtil.Ctermfunc.empty p))
   2.259            else error "poly_of_term: inverse of non-constant polyomial"
   2.260         end
   2.261     else (let val (opr,l) = Thm.dest_comb lop
   2.262 @@ -447,7 +447,7 @@
   2.263             then let 
   2.264                    val p = poly_of_term l 
   2.265                    val q = poly_of_term r 
   2.266 -                in if poly_isconst q then poly_cmul (Rat.inv (eval FuncUtil.Ctermfunc.undefined q)) p
   2.267 +                in if poly_isconst q then poly_cmul (Rat.inv (eval FuncUtil.Ctermfunc.empty q)) p
   2.268                     else error "poly_of_term: division by non-constant polynomial"
   2.269                  end
   2.270            else poly_var tm
   2.271 @@ -483,7 +483,7 @@
   2.272    val pfx = string_of_int k ^" "
   2.273    val ents =
   2.274      Inttriplefunc.fold (fn ((b,i,j), c) => fn a => if i > j then a else ((b,i,j),c)::a) m []
   2.275 -  val entss = sort (FuncUtil.increasing fst triple_int_ord ) ents
   2.276 +  val entss = sort (triple_int_ord o pairself fst) ents
   2.277   in  fold_rev (fn ((b,i,j),c) => fn a =>
   2.278       pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^
   2.279       " " ^ decimalize 20 c ^ "\n" ^ a) entss ""
   2.280 @@ -495,7 +495,7 @@
   2.281   let 
   2.282    val pfx = string_of_int k ^ " 1 "
   2.283    val ms = FuncUtil.Intpairfunc.fold (fn ((i,j), c) => fn  a => if i > j then a else ((i,j),c)::a) (snd m) [] 
   2.284 -  val mss = sort (FuncUtil.increasing fst (prod_ord int_ord int_ord)) ms 
   2.285 +  val mss = sort ((prod_ord int_ord int_ord) o pairself fst) ms 
   2.286   in fold_rev (fn ((i,j),c) => fn a =>
   2.287       pfx ^ string_of_int i ^ " " ^ string_of_int j ^
   2.288       " " ^ decimalize 20 c ^ "\n" ^ a) mss ""
   2.289 @@ -599,13 +599,13 @@
   2.290   let 
   2.291    val cd1 = fold_rev (common_denominator FuncUtil.Intpairfunc.fold) mats (rat_1)
   2.292    val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj)  (rat_1) 
   2.293 -  val mats' = map (FuncUtil.Intpairfunc.mapf (fn x => cd1 */ x)) mats
   2.294 +  val mats' = map (FuncUtil.Intpairfunc.map (fn x => cd1 */ x)) mats
   2.295    val obj' = vector_cmul cd2 obj
   2.296    val max1 = fold_rev (maximal_element FuncUtil.Intpairfunc.fold) mats' (rat_0)
   2.297    val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') (rat_0) 
   2.298    val scal1 = pow2 (20 - trunc(Math.ln (float_of_rat max1) / Math.ln 2.0))
   2.299    val scal2 = pow2 (20 - trunc(Math.ln (float_of_rat max2) / Math.ln 2.0)) 
   2.300 -  val mats'' = map (FuncUtil.Intpairfunc.mapf (fn x => x */ scal1)) mats'
   2.301 +  val mats'' = map (FuncUtil.Intpairfunc.map (fn x => x */ scal1)) mats'
   2.302    val obj'' = vector_cmul scal2 obj' 
   2.303   in solver obj'' mats''
   2.304    end
   2.305 @@ -632,13 +632,13 @@
   2.306   let 
   2.307    val cd1 = fold_rev (common_denominator Inttriplefunc.fold) mats (rat_1)
   2.308    val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj)  (rat_1) 
   2.309 -  val mats' = map (Inttriplefunc.mapf (fn x => cd1 */ x)) mats
   2.310 +  val mats' = map (Inttriplefunc.map (fn x => cd1 */ x)) mats
   2.311    val obj' = vector_cmul cd2 obj
   2.312    val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' (rat_0)
   2.313    val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') (rat_0) 
   2.314    val scal1 = pow2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
   2.315    val scal2 = pow2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0)) 
   2.316 -  val mats'' = map (Inttriplefunc.mapf (fn x => x */ scal1)) mats'
   2.317 +  val mats'' = map (Inttriplefunc.map (fn x => x */ scal1)) mats'
   2.318    val obj'' = vector_cmul scal2 obj' 
   2.319   in solver obj'' mats''
   2.320    end
   2.321 @@ -651,14 +651,14 @@
   2.322   (d, FuncUtil.Intfunc.fold (fn (i,c) => fn a => 
   2.323     let val y = nice_rational n c 
   2.324     in if c =/ rat_0 then a 
   2.325 -      else FuncUtil.Intfunc.update (i,y) a end) v FuncUtil.Intfunc.undefined):vector
   2.326 +      else FuncUtil.Intfunc.update (i,y) a end) v FuncUtil.Intfunc.empty):vector
   2.327  
   2.328  fun dest_ord f x = is_equal (f x);
   2.329  
   2.330  (* Stuff for "equations" ((int*int*int)->num functions).                         *)
   2.331  
   2.332  fun tri_equation_cmul c eq =
   2.333 -  if c =/ rat_0 then Inttriplefunc.undefined else Inttriplefunc.mapf (fn d => c */ d) eq;
   2.334 +  if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (fn d => c */ d) eq;
   2.335  
   2.336  fun tri_equation_add eq1 eq2 = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0) eq1 eq2;
   2.337  
   2.338 @@ -677,25 +677,25 @@
   2.339   | h::t => if p h then (h,t) else
   2.340            let val (k,s) = extract_first p t in (k,h::s) end
   2.341  fun eliminate vars dun eqs = case vars of 
   2.342 -  [] => if forall Inttriplefunc.is_undefined eqs then dun
   2.343 +  [] => if forall Inttriplefunc.is_empty eqs then dun
   2.344          else raise Unsolvable
   2.345   | v::vs =>
   2.346    ((let 
   2.347      val (eq,oeqs) = extract_first (fn e => Inttriplefunc.defined e v) eqs 
   2.348      val a = Inttriplefunc.apply eq v
   2.349 -    val eq' = tri_equation_cmul ((Rat.neg rat_1) // a) (Inttriplefunc.undefine v eq)
   2.350 +    val eq' = tri_equation_cmul ((Rat.neg rat_1) // a) (Inttriplefunc.delete_safe v eq)
   2.351      fun elim e =
   2.352       let val b = Inttriplefunc.tryapplyd e v rat_0 
   2.353       in if b =/ rat_0 then e else
   2.354          tri_equation_add e (tri_equation_cmul (Rat.neg b // a) eq)
   2.355       end
   2.356 -   in eliminate vs (Inttriplefunc.update (v,eq') (Inttriplefunc.mapf elim dun)) (map elim oeqs)
   2.357 +   in eliminate vs (Inttriplefunc.update (v,eq') (Inttriplefunc.map elim dun)) (map elim oeqs)
   2.358     end)
   2.359    handle Failure _ => eliminate vs dun eqs)
   2.360  in
   2.361  fun tri_eliminate_equations one vars eqs =
   2.362   let 
   2.363 -  val assig = eliminate vars Inttriplefunc.undefined eqs
   2.364 +  val assig = eliminate vars Inttriplefunc.empty eqs
   2.365    val vs = Inttriplefunc.fold (fn (x, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
   2.366    in (distinct (dest_ord triple_int_ord) vs, assig)
   2.367    end
   2.368 @@ -708,8 +708,8 @@
   2.369    fun choose_variable eq =
   2.370     let val (v,_) = Inttriplefunc.choose eq 
   2.371     in if is_equal (triple_int_ord(v,one)) then
   2.372 -      let val eq' = Inttriplefunc.undefine v eq 
   2.373 -      in if Inttriplefunc.is_undefined eq' then error "choose_variable" 
   2.374 +      let val eq' = Inttriplefunc.delete_safe v eq 
   2.375 +      in if Inttriplefunc.is_empty eq' then error "choose_variable" 
   2.376           else fst (Inttriplefunc.choose eq')
   2.377        end
   2.378      else v 
   2.379 @@ -717,22 +717,22 @@
   2.380    fun eliminate dun eqs = case eqs of 
   2.381      [] => dun
   2.382    | eq::oeqs =>
   2.383 -    if Inttriplefunc.is_undefined eq then eliminate dun oeqs else
   2.384 +    if Inttriplefunc.is_empty eq then eliminate dun oeqs else
   2.385      let val v = choose_variable eq
   2.386          val a = Inttriplefunc.apply eq v
   2.387          val eq' = tri_equation_cmul ((Rat.rat_of_int ~1) // a) 
   2.388 -                   (Inttriplefunc.undefine v eq)
   2.389 +                   (Inttriplefunc.delete_safe v eq)
   2.390          fun elim e =
   2.391           let val b = Inttriplefunc.tryapplyd e v rat_0 
   2.392           in if b =/ rat_0 then e 
   2.393              else tri_equation_add e (tri_equation_cmul (Rat.neg b // a) eq)
   2.394           end
   2.395 -    in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.mapf elim dun)) 
   2.396 +    in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map elim dun)) 
   2.397                   (map elim oeqs) 
   2.398      end
   2.399  in fn eqs =>
   2.400   let 
   2.401 -  val assig = eliminate Inttriplefunc.undefined eqs
   2.402 +  val assig = eliminate Inttriplefunc.empty eqs
   2.403    val vs = Inttriplefunc.fold (fn (x, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
   2.404   in (distinct (dest_ord triple_int_ord) vs,assig)
   2.405   end
   2.406 @@ -747,9 +747,9 @@
   2.407              (Inttriplefunc.onefunc(one, Rat.rat_of_int ~1))
   2.408    val ass =
   2.409      Inttriplefunc.combine (curry op +/) (K false) 
   2.410 -    (Inttriplefunc.mapf (tri_equation_eval vfn) assigs) vfn 
   2.411 +    (Inttriplefunc.map (tri_equation_eval vfn) assigs) vfn 
   2.412   in if forall (fn e => tri_equation_eval ass e =/ rat_0) eqs
   2.413 -    then Inttriplefunc.undefine one ass else raise Sanity
   2.414 +    then Inttriplefunc.delete_safe one ass else raise Sanity
   2.415   end;
   2.416  
   2.417  (* Multiply equation-parametrized poly by regular poly and add accumulator.  *)
   2.418 @@ -758,25 +758,25 @@
   2.419   FuncUtil.Monomialfunc.fold (fn (m1, c) => fn a =>
   2.420    FuncUtil.Monomialfunc.fold (fn (m2,e) => fn b =>
   2.421     let val m =  monomial_mul m1 m2
   2.422 -       val es = FuncUtil.Monomialfunc.tryapplyd b m Inttriplefunc.undefined 
   2.423 +       val es = FuncUtil.Monomialfunc.tryapplyd b m Inttriplefunc.empty 
   2.424     in FuncUtil.Monomialfunc.update (m,tri_equation_add (tri_equation_cmul c e) es) b 
   2.425     end) q a) p acc ;
   2.426  
   2.427  (* Usual operations on equation-parametrized poly.                           *)
   2.428  
   2.429  fun tri_epoly_cmul c l =
   2.430 -  if c =/ rat_0 then Inttriplefunc.undefined else Inttriplefunc.mapf (tri_equation_cmul c) l;;
   2.431 +  if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (tri_equation_cmul c) l;;
   2.432  
   2.433  val tri_epoly_neg = tri_epoly_cmul (Rat.rat_of_int ~1);
   2.434  
   2.435 -val tri_epoly_add = Inttriplefunc.combine tri_equation_add Inttriplefunc.is_undefined;
   2.436 +val tri_epoly_add = Inttriplefunc.combine tri_equation_add Inttriplefunc.is_empty;
   2.437  
   2.438  fun tri_epoly_sub p q = tri_epoly_add p (tri_epoly_neg q);;
   2.439  
   2.440  (* Stuff for "equations" ((int*int)->num functions).                         *)
   2.441  
   2.442  fun pi_equation_cmul c eq =
   2.443 -  if c =/ rat_0 then Inttriplefunc.undefined else Inttriplefunc.mapf (fn d => c */ d) eq;
   2.444 +  if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (fn d => c */ d) eq;
   2.445  
   2.446  fun pi_equation_add eq1 eq2 = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0) eq1 eq2;
   2.447  
   2.448 @@ -795,25 +795,25 @@
   2.449   | h::t => if p h then (h,t) else
   2.450            let val (k,s) = extract_first p t in (k,h::s) end
   2.451  fun eliminate vars dun eqs = case vars of 
   2.452 -  [] => if forall Inttriplefunc.is_undefined eqs then dun
   2.453 +  [] => if forall Inttriplefunc.is_empty eqs then dun
   2.454          else raise Unsolvable
   2.455   | v::vs =>
   2.456     let 
   2.457      val (eq,oeqs) = extract_first (fn e => Inttriplefunc.defined e v) eqs 
   2.458      val a = Inttriplefunc.apply eq v
   2.459 -    val eq' = pi_equation_cmul ((Rat.neg rat_1) // a) (Inttriplefunc.undefine v eq)
   2.460 +    val eq' = pi_equation_cmul ((Rat.neg rat_1) // a) (Inttriplefunc.delete_safe v eq)
   2.461      fun elim e =
   2.462       let val b = Inttriplefunc.tryapplyd e v rat_0 
   2.463       in if b =/ rat_0 then e else
   2.464          pi_equation_add e (pi_equation_cmul (Rat.neg b // a) eq)
   2.465       end
   2.466 -   in eliminate vs (Inttriplefunc.update (v,eq') (Inttriplefunc.mapf elim dun)) (map elim oeqs)
   2.467 +   in eliminate vs (Inttriplefunc.update (v,eq') (Inttriplefunc.map elim dun)) (map elim oeqs)
   2.468     end
   2.469    handle Failure _ => eliminate vs dun eqs
   2.470  in
   2.471  fun pi_eliminate_equations one vars eqs =
   2.472   let 
   2.473 -  val assig = eliminate vars Inttriplefunc.undefined eqs
   2.474 +  val assig = eliminate vars Inttriplefunc.empty eqs
   2.475    val vs = Inttriplefunc.fold (fn (x, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
   2.476    in (distinct (dest_ord triple_int_ord) vs, assig)
   2.477    end
   2.478 @@ -826,8 +826,8 @@
   2.479    fun choose_variable eq =
   2.480     let val (v,_) = Inttriplefunc.choose eq 
   2.481     in if is_equal (triple_int_ord(v,one)) then
   2.482 -      let val eq' = Inttriplefunc.undefine v eq 
   2.483 -      in if Inttriplefunc.is_undefined eq' then error "choose_variable" 
   2.484 +      let val eq' = Inttriplefunc.delete_safe v eq 
   2.485 +      in if Inttriplefunc.is_empty eq' then error "choose_variable" 
   2.486           else fst (Inttriplefunc.choose eq')
   2.487        end
   2.488      else v 
   2.489 @@ -835,22 +835,22 @@
   2.490    fun eliminate dun eqs = case eqs of 
   2.491      [] => dun
   2.492    | eq::oeqs =>
   2.493 -    if Inttriplefunc.is_undefined eq then eliminate dun oeqs else
   2.494 +    if Inttriplefunc.is_empty eq then eliminate dun oeqs else
   2.495      let val v = choose_variable eq
   2.496          val a = Inttriplefunc.apply eq v
   2.497          val eq' = pi_equation_cmul ((Rat.rat_of_int ~1) // a) 
   2.498 -                   (Inttriplefunc.undefine v eq)
   2.499 +                   (Inttriplefunc.delete_safe v eq)
   2.500          fun elim e =
   2.501           let val b = Inttriplefunc.tryapplyd e v rat_0 
   2.502           in if b =/ rat_0 then e 
   2.503              else pi_equation_add e (pi_equation_cmul (Rat.neg b // a) eq)
   2.504           end
   2.505 -    in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.mapf elim dun)) 
   2.506 +    in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map elim dun)) 
   2.507                   (map elim oeqs) 
   2.508      end
   2.509  in fn eqs =>
   2.510   let 
   2.511 -  val assig = eliminate Inttriplefunc.undefined eqs
   2.512 +  val assig = eliminate Inttriplefunc.empty eqs
   2.513    val vs = Inttriplefunc.fold (fn (x, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
   2.514   in (distinct (dest_ord triple_int_ord) vs,assig)
   2.515   end
   2.516 @@ -865,9 +865,9 @@
   2.517              (Inttriplefunc.onefunc(one, Rat.rat_of_int ~1))
   2.518    val ass =
   2.519      Inttriplefunc.combine (curry op +/) (K false) 
   2.520 -    (Inttriplefunc.mapf (pi_equation_eval vfn) assigs) vfn 
   2.521 +    (Inttriplefunc.map (pi_equation_eval vfn) assigs) vfn 
   2.522   in if forall (fn e => pi_equation_eval ass e =/ rat_0) eqs
   2.523 -    then Inttriplefunc.undefine one ass else raise Sanity
   2.524 +    then Inttriplefunc.delete_safe one ass else raise Sanity
   2.525   end;
   2.526  
   2.527  (* Multiply equation-parametrized poly by regular poly and add accumulator.  *)
   2.528 @@ -876,18 +876,18 @@
   2.529   FuncUtil.Monomialfunc.fold (fn (m1, c) => fn a =>
   2.530    FuncUtil.Monomialfunc.fold (fn (m2,e) => fn b =>
   2.531     let val m =  monomial_mul m1 m2
   2.532 -       val es = FuncUtil.Monomialfunc.tryapplyd b m Inttriplefunc.undefined 
   2.533 +       val es = FuncUtil.Monomialfunc.tryapplyd b m Inttriplefunc.empty 
   2.534     in FuncUtil.Monomialfunc.update (m,pi_equation_add (pi_equation_cmul c e) es) b 
   2.535     end) q a) p acc ;
   2.536  
   2.537  (* Usual operations on equation-parametrized poly.                           *)
   2.538  
   2.539  fun pi_epoly_cmul c l =
   2.540 -  if c =/ rat_0 then Inttriplefunc.undefined else Inttriplefunc.mapf (pi_equation_cmul c) l;;
   2.541 +  if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (pi_equation_cmul c) l;;
   2.542  
   2.543  val pi_epoly_neg = pi_epoly_cmul (Rat.rat_of_int ~1);
   2.544  
   2.545 -val pi_epoly_add = Inttriplefunc.combine pi_equation_add Inttriplefunc.is_undefined;
   2.546 +val pi_epoly_add = Inttriplefunc.combine pi_equation_add Inttriplefunc.is_empty;
   2.547  
   2.548  fun pi_epoly_sub p q = pi_epoly_add p (pi_epoly_neg q);;
   2.549  
   2.550 @@ -906,12 +906,12 @@
   2.551  
   2.552  local
   2.553  fun diagonalize n i m =
   2.554 - if FuncUtil.Intpairfunc.is_undefined (snd m) then [] 
   2.555 + if FuncUtil.Intpairfunc.is_empty (snd m) then [] 
   2.556   else
   2.557    let val a11 = FuncUtil.Intpairfunc.tryapplyd (snd m) (i,i) rat_0 
   2.558    in if a11 </ rat_0 then raise Failure "diagonalize: not PSD"
   2.559      else if a11 =/ rat_0 then
   2.560 -          if FuncUtil.Intfunc.is_undefined (snd (row i m)) then diagonalize n (i + 1) m
   2.561 +          if FuncUtil.Intfunc.is_empty (snd (row i m)) then diagonalize n (i + 1) m
   2.562            else raise Failure "diagonalize: not PSD ___ "
   2.563      else
   2.564       let 
   2.565 @@ -919,14 +919,14 @@
   2.566        val v' = (fst v, FuncUtil.Intfunc.fold (fn (i, c) => fn a => 
   2.567         let val y = c // a11 
   2.568         in if y = rat_0 then a else FuncUtil.Intfunc.update (i,y) a 
   2.569 -       end)  (snd v) FuncUtil.Intfunc.undefined)
   2.570 +       end)  (snd v) FuncUtil.Intfunc.empty)
   2.571        fun upt0 x y a = if y = rat_0 then a else FuncUtil.Intpairfunc.update (x,y) a
   2.572        val m' =
   2.573        ((n,n),
   2.574        iter (i+1,n) (fn j =>
   2.575            iter (i+1,n) (fn k =>
   2.576                (upt0 (j,k) (FuncUtil.Intpairfunc.tryapplyd (snd m) (j,k) rat_0 -/ FuncUtil.Intfunc.tryapplyd (snd v) j rat_0 */ FuncUtil.Intfunc.tryapplyd (snd v') k rat_0))))
   2.577 -          FuncUtil.Intpairfunc.undefined)
   2.578 +          FuncUtil.Intpairfunc.empty)
   2.579       in (a11,v')::diagonalize n (i + 1) m' 
   2.580       end
   2.581    end
   2.582 @@ -947,7 +947,7 @@
   2.583  local
   2.584   fun upd0 x y a = if y =/ rat_0 then a else FuncUtil.Intfunc.update(x,y) a;
   2.585   fun mapa f (d,v) = 
   2.586 -  (d, FuncUtil.Intfunc.fold (fn (i,c) => fn a => upd0 i (f c) a) v FuncUtil.Intfunc.undefined)
   2.587 +  (d, FuncUtil.Intfunc.fold (fn (i,c) => fn a => upd0 i (f c) a) v FuncUtil.Intfunc.empty)
   2.588   fun adj (c,l) =
   2.589   let val a = 
   2.590    FuncUtil.Intfunc.fold (fn (i,c) => fn a => lcm_rat a (denominator_rat c)) 
   2.591 @@ -969,7 +969,7 @@
   2.592  
   2.593  fun enumerate_monomials d vars = 
   2.594   if d < 0 then []
   2.595 - else if d = 0 then [FuncUtil.Ctermfunc.undefined]
   2.596 + else if d = 0 then [FuncUtil.Ctermfunc.empty]
   2.597   else if null vars then [monomial_1] else
   2.598   let val alts =
   2.599    map (fn k => let val oths = enumerate_monomials (d - k) (tl vars) 
   2.600 @@ -997,7 +997,7 @@
   2.601  (* Convert regular polynomial. Note that we treat (0,0,0) as -1.             *)
   2.602  
   2.603  fun epoly_of_poly p =
   2.604 -  FuncUtil.Monomialfunc.fold (fn (m,c) => fn a => FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((0,0,0), Rat.neg c)) a) p FuncUtil.Monomialfunc.undefined;
   2.605 +  FuncUtil.Monomialfunc.fold (fn (m,c) => fn a => FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((0,0,0), Rat.neg c)) a) p FuncUtil.Monomialfunc.empty;
   2.606  
   2.607  (* String for block diagonal matrix numbered k.                              *)
   2.608  
   2.609 @@ -1008,7 +1008,7 @@
   2.610      Inttriplefunc.fold 
   2.611        (fn ((b,i,j),c) => fn a => if i > j then a else ((b,i,j),c)::a) 
   2.612        m [] 
   2.613 -  val entss = sort (FuncUtil.increasing fst triple_int_ord) ents 
   2.614 +  val entss = sort (triple_int_ord o pairself fst) ents 
   2.615   in fold_rev (fn ((b,i,j),c) => fn a =>
   2.616       pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^
   2.617       " " ^ decimalize 20 c ^ "\n" ^ a) entss ""
   2.618 @@ -1037,8 +1037,8 @@
   2.619  
   2.620  val bmatrix_add = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0);
   2.621  fun bmatrix_cmul c bm =
   2.622 -  if c =/ rat_0 then Inttriplefunc.undefined
   2.623 -  else Inttriplefunc.mapf (fn x => c */ x) bm;
   2.624 +  if c =/ rat_0 then Inttriplefunc.empty
   2.625 +  else Inttriplefunc.map (fn x => c */ x) bm;
   2.626  
   2.627  val bmatrix_neg = bmatrix_cmul (Rat.rat_of_int ~1);
   2.628  fun bmatrix_sub m1 m2 = bmatrix_add m1 (bmatrix_neg m2);;
   2.629 @@ -1048,7 +1048,7 @@
   2.630  fun blocks blocksizes bm =
   2.631   map (fn (bs,b0) =>
   2.632        let val m = Inttriplefunc.fold
   2.633 -          (fn ((b,i,j),c) => fn a => if b = b0 then FuncUtil.Intpairfunc.update ((i,j),c) a else a) bm FuncUtil.Intpairfunc.undefined
   2.634 +          (fn ((b,i,j),c) => fn a => if b = b0 then FuncUtil.Intpairfunc.update ((i,j),c) a else a) bm FuncUtil.Intpairfunc.empty
   2.635            val d = FuncUtil.Intpairfunc.fold (fn ((i,j),c) => fn a => max a (max i j)) m 0 
   2.636        in (((bs,bs),m):matrix) end)
   2.637   (blocksizes ~~ (1 upto length blocksizes));;
   2.638 @@ -1079,7 +1079,7 @@
   2.639     val mons = enumerate_monomials e vars
   2.640     val nons = mons ~~ (1 upto length mons) 
   2.641    in (mons,
   2.642 -      fold_rev (fn (m,n) => FuncUtil.Monomialfunc.update(m,Inttriplefunc.onefunc((~k,~n,n),rat_1))) nons FuncUtil.Monomialfunc.undefined)
   2.643 +      fold_rev (fn (m,n) => FuncUtil.Monomialfunc.update(m,Inttriplefunc.onefunc((~k,~n,n),rat_1))) nons FuncUtil.Monomialfunc.empty)
   2.644    end
   2.645  
   2.646   fun mk_sqmultiplier k (p,c) =
   2.647 @@ -1093,11 +1093,11 @@
   2.648          let val m = monomial_mul m1 m2 
   2.649          in if n1 > n2 then a else
   2.650            let val c = if n1 = n2 then rat_1 else rat_2
   2.651 -              val e = FuncUtil.Monomialfunc.tryapplyd a m Inttriplefunc.undefined 
   2.652 +              val e = FuncUtil.Monomialfunc.tryapplyd a m Inttriplefunc.empty 
   2.653            in FuncUtil.Monomialfunc.update(m, tri_equation_add (Inttriplefunc.onefunc((k,n1,n2), c)) e) a
   2.654            end
   2.655          end)  nons)
   2.656 -       nons FuncUtil.Monomialfunc.undefined)
   2.657 +       nons FuncUtil.Monomialfunc.empty)
   2.658    end
   2.659  
   2.660    val (sqmonlist,sqs) = split_list (map2 mk_sqmultiplier (1 upto length monoid) monoid)
   2.661 @@ -1118,15 +1118,15 @@
   2.662           in if c = rat_0 then m else
   2.663              Inttriplefunc.update ((b,j,i), c) (Inttriplefunc.update ((b,i,j), c) m)
   2.664           end)
   2.665 -          allassig Inttriplefunc.undefined
   2.666 +          allassig Inttriplefunc.empty
   2.667    val diagents = Inttriplefunc.fold
   2.668      (fn ((b,i,j), e) => fn a => if b > 0 andalso i = j then tri_equation_add e a else a)
   2.669 -    allassig Inttriplefunc.undefined
   2.670 +    allassig Inttriplefunc.empty
   2.671  
   2.672    val mats = map mk_matrix qvars
   2.673    val obj = (length pvs,
   2.674              itern 1 pvs (fn v => fn i => FuncUtil.Intfunc.updatep iszero (i,Inttriplefunc.tryapplyd diagents v rat_0))
   2.675 -                        FuncUtil.Intfunc.undefined)
   2.676 +                        FuncUtil.Intfunc.empty)
   2.677    val raw_vec = if null pvs then vector_0 0
   2.678                  else tri_scale_then (run_blockproblem prover nblocks blocksizes) obj mats
   2.679    fun int_element (d,v) i = FuncUtil.Intfunc.tryapplyd v i rat_0
   2.680 @@ -1155,11 +1155,11 @@
   2.681      Inttriplefunc.fold (fn (v,e) => fn a => Inttriplefunc.update(v, tri_equation_eval newassigs e) a) allassig newassigs
   2.682    fun poly_of_epoly p =
   2.683      FuncUtil.Monomialfunc.fold (fn (v,e) => fn a => FuncUtil.Monomialfunc.updatep iszero (v,tri_equation_eval finalassigs e) a)
   2.684 -          p FuncUtil.Monomialfunc.undefined
   2.685 +          p FuncUtil.Monomialfunc.empty
   2.686    fun  mk_sos mons =
   2.687     let fun mk_sq (c,m) =
   2.688      (c,fold_rev (fn k=> fn a => FuncUtil.Monomialfunc.updatep iszero (nth mons (k - 1), int_element m k) a)
   2.689 -                 (1 upto length mons) FuncUtil.Monomialfunc.undefined)
   2.690 +                 (1 upto length mons) FuncUtil.Monomialfunc.empty)
   2.691     in map mk_sq
   2.692     end
   2.693    val sqs = map2 mk_sos sqmonlist ratdias
   2.694 @@ -1171,7 +1171,7 @@
   2.695             (fold_rev2 (fn p => fn q => poly_add (poly_mul p q)) cfs eqs
   2.696                      (poly_neg pol))
   2.697  
   2.698 -in if not(FuncUtil.Monomialfunc.is_undefined sanity) then raise Sanity else
   2.699 +in if not(FuncUtil.Monomialfunc.is_empty sanity) then raise Sanity else
   2.700    (cfs,map (fn (a,b) => (snd a,b)) msq)
   2.701   end
   2.702  
   2.703 @@ -1216,11 +1216,11 @@
   2.704     val (kltp,ltp) = List.partition (fn (p,_) => multidegree p = 0) ltp0
   2.705     fun trivial_axiom (p,ax) =
   2.706      case ax of
   2.707 -       RealArith.Axiom_eq n => if eval FuncUtil.Ctermfunc.undefined p <>/ Rat.zero then nth eqs n 
   2.708 +       RealArith.Axiom_eq n => if eval FuncUtil.Ctermfunc.empty p <>/ Rat.zero then nth eqs n 
   2.709                       else raise Failure "trivial_axiom: Not a trivial axiom"
   2.710 -     | RealArith.Axiom_le n => if eval FuncUtil.Ctermfunc.undefined p </ Rat.zero then nth les n 
   2.711 +     | RealArith.Axiom_le n => if eval FuncUtil.Ctermfunc.empty p </ Rat.zero then nth les n 
   2.712                       else raise Failure "trivial_axiom: Not a trivial axiom"
   2.713 -     | RealArith.Axiom_lt n => if eval FuncUtil.Ctermfunc.undefined p <=/ Rat.zero then nth lts n 
   2.714 +     | RealArith.Axiom_lt n => if eval FuncUtil.Ctermfunc.empty p <=/ Rat.zero then nth lts n 
   2.715                       else raise Failure "trivial_axiom: Not a trivial axiom"
   2.716       | _ => error "trivial_axiom: Not a trivial axiom"
   2.717     in 
     3.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue Sep 22 14:17:54 2009 +0200
     3.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Sep 30 13:48:00 2009 +0200
     3.3 @@ -8,41 +8,24 @@
     3.4  
     3.5  signature FUNC = 
     3.6  sig
     3.7 - type 'a T
     3.8 - type key
     3.9 - val apply : 'a T -> key -> 'a
    3.10 - val applyd :'a T -> (key -> 'a) -> key -> 'a
    3.11 - val combine : ('a -> 'a -> 'a) -> ('a -> bool) -> 'a T -> 'a T -> 'a T
    3.12 - val defined : 'a T -> key -> bool
    3.13 - val dom : 'a T -> key list
    3.14 - val fold : (key * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b
    3.15 - val fold_rev : (key * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b
    3.16 - val graph : 'a T -> (key * 'a) list
    3.17 - val is_undefined : 'a T -> bool
    3.18 - val mapf : ('a -> 'b) -> 'a T -> 'b T
    3.19 - val tryapplyd : 'a T -> key -> 'a -> 'a
    3.20 - val undefine :  key -> 'a T -> 'a T
    3.21 - val undefined : 'a T
    3.22 - val update : key * 'a -> 'a T -> 'a T
    3.23 - val updatep : (key * 'a -> bool) -> key * 'a -> 'a T -> 'a T
    3.24 - val choose : 'a T -> key * 'a
    3.25 - val onefunc : key * 'a -> 'a T
    3.26 - val get_first: (key*'a -> 'a option) -> 'a T -> 'a option
    3.27 + include TABLE
    3.28 + val apply : 'a table -> key -> 'a
    3.29 + val applyd :'a table -> (key -> 'a) -> key -> 'a
    3.30 + val combine : ('a -> 'a -> 'a) -> ('a -> bool) -> 'a table -> 'a table -> 'a table
    3.31 + val dom : 'a table -> key list
    3.32 + val tryapplyd : 'a table -> key -> 'a -> 'a
    3.33 + val updatep : (key * 'a -> bool) -> key * 'a -> 'a table -> 'a table
    3.34 + val choose : 'a table -> key * 'a
    3.35 + val onefunc : key * 'a -> 'a table
    3.36  end;
    3.37  
    3.38  functor FuncFun(Key: KEY) : FUNC=
    3.39  struct
    3.40  
    3.41 -type key = Key.key;
    3.42  structure Tab = Table(Key);
    3.43 -type 'a T = 'a Tab.table;
    3.44  
    3.45 -val undefined = Tab.empty;
    3.46 -val is_undefined = Tab.is_empty;
    3.47 -val mapf = Tab.map;
    3.48 -val fold = Tab.fold;
    3.49 -val fold_rev = Tab.fold_rev;
    3.50 -val graph = Tab.dest;
    3.51 +open Tab;
    3.52 +
    3.53  fun dom a = sort Key.ord (Tab.keys a);
    3.54  fun applyd f d x = case Tab.lookup f x of 
    3.55     SOME y => y
    3.56 @@ -50,9 +33,6 @@
    3.57  
    3.58  fun apply f x = applyd f (fn _ => raise Tab.UNDEF x) x;
    3.59  fun tryapplyd f a d = applyd f (K d) a;
    3.60 -val defined = Tab.defined;
    3.61 -fun undefine x t = (Tab.delete x t handle UNDEF => t);
    3.62 -val update = Tab.update;
    3.63  fun updatep p (k,v) t = if p (k, v) then t else update (k,v) t
    3.64  fun combine f z a b = 
    3.65   let
    3.66 @@ -64,16 +44,10 @@
    3.67  
    3.68  fun choose f = case Tab.min_key f of 
    3.69     SOME k => (k,valOf (Tab.lookup f k))
    3.70 - | NONE => error "FuncFun.choose : Completely undefined function"
    3.71 -
    3.72 -fun onefunc kv = update kv undefined
    3.73 + | NONE => error "FuncFun.choose : Completely empty function"
    3.74  
    3.75 -local
    3.76 -fun  find f (k,v) NONE = f (k,v)
    3.77 -   | find f (k,v) r = r
    3.78 -in
    3.79 -fun get_first f t = fold (find f) t NONE
    3.80 -end
    3.81 +fun onefunc kv = update kv empty
    3.82 +
    3.83  end;
    3.84  
    3.85  (* Some standard functors and utility functions for them *)
    3.86 @@ -81,33 +55,31 @@
    3.87  structure FuncUtil =
    3.88  struct
    3.89  
    3.90 -fun increasing f ord (x,y) = ord (f x, f y);
    3.91 -
    3.92  structure Intfunc = FuncFun(type key = int val ord = int_ord);
    3.93  structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord);
    3.94  structure Intpairfunc = FuncFun(type key = int*int val ord = prod_ord int_ord int_ord);
    3.95  structure Symfunc = FuncFun(type key = string val ord = fast_string_ord);
    3.96  structure Termfunc = FuncFun(type key = term val ord = TermOrd.fast_term_ord);
    3.97  
    3.98 -val cterm_ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t))
    3.99 +val cterm_ord = TermOrd.fast_term_ord o pairself term_of
   3.100  
   3.101  structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord);
   3.102  
   3.103 -type monomial = int Ctermfunc.T;
   3.104 +type monomial = int Ctermfunc.table;
   3.105  
   3.106 -fun monomial_ord (m1,m2) = list_ord (prod_ord cterm_ord int_ord) (Ctermfunc.graph m1, Ctermfunc.graph m2)
   3.107 +val monomial_ord = list_ord (prod_ord cterm_ord int_ord) o pairself Ctermfunc.dest
   3.108  
   3.109  structure Monomialfunc = FuncFun(type key = monomial val ord = monomial_ord)
   3.110  
   3.111 -type poly = Rat.rat Monomialfunc.T;
   3.112 +type poly = Rat.rat Monomialfunc.table;
   3.113  
   3.114  (* The ordering so we can create canonical HOL polynomials.                  *)
   3.115  
   3.116 -fun dest_monomial mon = sort (increasing fst cterm_ord) (Ctermfunc.graph mon);
   3.117 +fun dest_monomial mon = sort (cterm_ord o pairself fst) (Ctermfunc.dest mon);
   3.118  
   3.119  fun monomial_order (m1,m2) =
   3.120 - if Ctermfunc.is_undefined m2 then LESS 
   3.121 - else if Ctermfunc.is_undefined m1 then GREATER 
   3.122 + if Ctermfunc.is_empty m2 then LESS 
   3.123 + else if Ctermfunc.is_empty m1 then GREATER 
   3.124   else
   3.125    let val mon1 = dest_monomial m1 
   3.126        val mon2 = dest_monomial m2
   3.127 @@ -357,7 +329,7 @@
   3.128    (Numeral.mk_cnumber @{ctyp nat} k)
   3.129  
   3.130  fun cterm_of_monomial m = 
   3.131 - if FuncUtil.Ctermfunc.is_undefined m then @{cterm "1::real"} 
   3.132 + if FuncUtil.Ctermfunc.is_empty m then @{cterm "1::real"} 
   3.133   else 
   3.134    let 
   3.135     val m' = FuncUtil.dest_monomial m
   3.136 @@ -365,16 +337,16 @@
   3.137    in foldr1 (fn (s, t) => Thm.capply (Thm.capply @{cterm "op * :: real => _"} s) t) vps
   3.138    end
   3.139  
   3.140 -fun cterm_of_cmonomial (m,c) = if FuncUtil.Ctermfunc.is_undefined m then cterm_of_rat c
   3.141 +fun cterm_of_cmonomial (m,c) = if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
   3.142      else if c = Rat.one then cterm_of_monomial m
   3.143      else Thm.capply (Thm.capply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
   3.144  
   3.145  fun cterm_of_poly p = 
   3.146 - if FuncUtil.Monomialfunc.is_undefined p then @{cterm "0::real"} 
   3.147 + if FuncUtil.Monomialfunc.is_empty p then @{cterm "0::real"} 
   3.148   else
   3.149    let 
   3.150     val cms = map cterm_of_cmonomial
   3.151 -     (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.graph p))
   3.152 +     (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p))
   3.153    in foldr1 (fn (t1, t2) => Thm.capply(Thm.capply @{cterm "op + :: real => _"} t1) t2) cms
   3.154    end;
   3.155  
   3.156 @@ -593,10 +565,11 @@
   3.157  (* A linear arithmetic prover *)
   3.158  local
   3.159    val linear_add = FuncUtil.Ctermfunc.combine (curry op +/) (fn z => z =/ Rat.zero)
   3.160 -  fun linear_cmul c = FuncUtil.Ctermfunc.mapf (fn x => c */ x)
   3.161 +  fun linear_cmul c = FuncUtil.Ctermfunc.map (fn x => c */ x)
   3.162    val one_tm = @{cterm "1::real"}
   3.163 -  fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_undefined e) andalso not(p Rat.zero)) orelse
   3.164 -     ((gen_eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso not(p(FuncUtil.Ctermfunc.apply e one_tm)))
   3.165 +  fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
   3.166 +     ((gen_eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
   3.167 +       not(p(FuncUtil.Ctermfunc.apply e one_tm)))
   3.168  
   3.169    fun linear_ineqs vars (les,lts) = 
   3.170     case find_first (contradictory (fn x => x >/ Rat.zero)) lts of
   3.171 @@ -650,9 +623,9 @@
   3.172             (fold_rev (curry (gen_union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
   3.173       in linear_ineqs vars (les,lts) end
   3.174     | (e,p)::es => 
   3.175 -     if FuncUtil.Ctermfunc.is_undefined e then linear_eqs (es,les,lts) else
   3.176 +     if FuncUtil.Ctermfunc.is_empty e then linear_eqs (es,les,lts) else
   3.177       let 
   3.178 -      val (x,c) = FuncUtil.Ctermfunc.choose (FuncUtil.Ctermfunc.undefine one_tm e)
   3.179 +      val (x,c) = FuncUtil.Ctermfunc.choose (FuncUtil.Ctermfunc.delete_safe one_tm e)
   3.180        fun xform (inp as (t,q)) =
   3.181         let val d = FuncUtil.Ctermfunc.tryapplyd t x Rat.zero in
   3.182          if d =/ Rat.zero then inp else
   3.183 @@ -660,7 +633,7 @@
   3.184           val k = (Rat.neg d) */ Rat.abs c // c
   3.185           val e' = linear_cmul k e
   3.186           val t' = linear_cmul (Rat.abs c) t
   3.187 -         val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.undefined, k),p)
   3.188 +         val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p)
   3.189           val q' = Product(Rational_lt(Rat.abs c),q) 
   3.190          in (linear_add e' t',Sum(p',q')) 
   3.191          end 
   3.192 @@ -677,7 +650,7 @@
   3.193     end 
   3.194    
   3.195    fun lin_of_hol ct = 
   3.196 -   if ct aconvc @{cterm "0::real"} then FuncUtil.Ctermfunc.undefined
   3.197 +   if ct aconvc @{cterm "0::real"} then FuncUtil.Ctermfunc.empty
   3.198     else if not (is_comb ct) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   3.199     else if is_ratconst ct then FuncUtil.Ctermfunc.onefunc (one_tm, dest_ratconst ct)
   3.200     else