Table.map replaces Table.map'
authorhaftmann
Thu Sep 02 10:29:48 2010 +0200 (2010-09-02)
changeset 39027e4262f9e6a4e
parent 39026 962d12bc546c
child 39028 0dd6c5a0beef
Table.map replaces Table.map'
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
     1.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Sep 02 10:29:47 2010 +0200
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Sep 02 10:29:48 2010 +0200
     1.3 @@ -124,10 +124,10 @@
     1.4  fun vector_cmul c (v:vector) =
     1.5   let val n = dim v
     1.6   in if c =/ rat_0 then vector_0 n
     1.7 -    else (n,FuncUtil.Intfunc.map (fn x => c */ x) (snd v))
     1.8 +    else (n,FuncUtil.Intfunc.map (fn _ => fn x => c */ x) (snd v))
     1.9   end;
    1.10  
    1.11 -fun vector_neg (v:vector) = (fst v,FuncUtil.Intfunc.map Rat.neg (snd v)) :vector;
    1.12 +fun vector_neg (v:vector) = (fst v,FuncUtil.Intfunc.map (K Rat.neg) (snd v)) :vector;
    1.13  
    1.14  fun vector_add (v1:vector) (v2:vector) =
    1.15   let val m = dim v1
    1.16 @@ -167,11 +167,11 @@
    1.17  fun matrix_cmul c (m:matrix) =
    1.18   let val (i,j) = dimensions m
    1.19   in if c =/ rat_0 then matrix_0 (i,j)
    1.20 -    else ((i,j),FuncUtil.Intpairfunc.map (fn x => c */ x) (snd m))
    1.21 +    else ((i,j),FuncUtil.Intpairfunc.map (fn _ => fn x => c */ x) (snd m))
    1.22   end;
    1.23  
    1.24  fun matrix_neg (m:matrix) =
    1.25 -  (dimensions m, FuncUtil.Intpairfunc.map Rat.neg (snd m)) :matrix;
    1.26 +  (dimensions m, FuncUtil.Intpairfunc.map (K Rat.neg) (snd m)) :matrix;
    1.27  
    1.28  fun matrix_add (m1:matrix) (m2:matrix) =
    1.29   let val d1 = dimensions m1
    1.30 @@ -229,14 +229,14 @@
    1.31  
    1.32  fun monomial_pow m k =
    1.33    if k = 0 then monomial_1
    1.34 -  else FuncUtil.Ctermfunc.map (fn x => k * x) m;
    1.35 +  else FuncUtil.Ctermfunc.map (fn _ => fn x => k * x) m;
    1.36  
    1.37  fun monomial_divides m1 m2 =
    1.38    FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => FuncUtil.Ctermfunc.tryapplyd m2 x 0 >= k andalso a) m1 true;;
    1.39  
    1.40  fun monomial_div m1 m2 =
    1.41   let val m = FuncUtil.Ctermfunc.combine Integer.add
    1.42 -   (fn x => x = 0) m1 (FuncUtil.Ctermfunc.map (fn x => ~ x) m2)
    1.43 +   (fn x => x = 0) m1 (FuncUtil.Ctermfunc.map (fn _ => fn x => ~ x) m2)
    1.44   in if FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k >= 0 andalso a) m true then m
    1.45    else error "monomial_div: non-divisible"
    1.46   end;
    1.47 @@ -270,9 +270,9 @@
    1.48  
    1.49  fun poly_cmul c p =
    1.50    if c =/ rat_0 then poly_0
    1.51 -  else FuncUtil.Monomialfunc.map (fn x => c */ x) p;
    1.52 +  else FuncUtil.Monomialfunc.map (fn _ => fn x => c */ x) p;
    1.53  
    1.54 -fun poly_neg p = FuncUtil.Monomialfunc.map Rat.neg p;;
    1.55 +fun poly_neg p = FuncUtil.Monomialfunc.map (K Rat.neg) p;;
    1.56  
    1.57  fun poly_add p1 p2 =
    1.58    FuncUtil.Monomialfunc.combine (curry op +/) (fn x => x =/ rat_0) p1 p2;
    1.59 @@ -282,7 +282,7 @@
    1.60  fun poly_cmmul (c,m) p =
    1.61   if c =/ rat_0 then poly_0
    1.62   else if FuncUtil.Ctermfunc.is_empty m
    1.63 -      then FuncUtil.Monomialfunc.map (fn d => c */ d) p
    1.64 +      then FuncUtil.Monomialfunc.map (fn _ => fn d => c */ d) p
    1.65        else FuncUtil.Monomialfunc.fold (fn (m', d) => fn a => (FuncUtil.Monomialfunc.update (monomial_mul m m', c */ d) a)) p poly_0;
    1.66  
    1.67  fun poly_mul p1 p2 =
    1.68 @@ -596,13 +596,13 @@
    1.69   let
    1.70    val cd1 = fold_rev (common_denominator FuncUtil.Intpairfunc.fold) mats (rat_1)
    1.71    val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj)  (rat_1)
    1.72 -  val mats' = map (FuncUtil.Intpairfunc.map (fn x => cd1 */ x)) mats
    1.73 +  val mats' = map (FuncUtil.Intpairfunc.map (fn _ => fn x => cd1 */ x)) mats
    1.74    val obj' = vector_cmul cd2 obj
    1.75    val max1 = fold_rev (maximal_element FuncUtil.Intpairfunc.fold) mats' (rat_0)
    1.76    val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') (rat_0)
    1.77    val scal1 = pow2 (20 - trunc(Math.ln (float_of_rat max1) / Math.ln 2.0))
    1.78    val scal2 = pow2 (20 - trunc(Math.ln (float_of_rat max2) / Math.ln 2.0))
    1.79 -  val mats'' = map (FuncUtil.Intpairfunc.map (fn x => x */ scal1)) mats'
    1.80 +  val mats'' = map (FuncUtil.Intpairfunc.map (fn _ => fn x => x */ scal1)) mats'
    1.81    val obj'' = vector_cmul scal2 obj'
    1.82   in solver obj'' mats''
    1.83    end
    1.84 @@ -629,13 +629,13 @@
    1.85   let
    1.86    val cd1 = fold_rev (common_denominator Inttriplefunc.fold) mats (rat_1)
    1.87    val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj)  (rat_1)
    1.88 -  val mats' = map (Inttriplefunc.map (fn x => cd1 */ x)) mats
    1.89 +  val mats' = map (Inttriplefunc.map (fn _ => fn x => cd1 */ x)) mats
    1.90    val obj' = vector_cmul cd2 obj
    1.91    val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' (rat_0)
    1.92    val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') (rat_0)
    1.93    val scal1 = pow2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
    1.94    val scal2 = pow2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0))
    1.95 -  val mats'' = map (Inttriplefunc.map (fn x => x */ scal1)) mats'
    1.96 +  val mats'' = map (Inttriplefunc.map (fn _ => fn x => x */ scal1)) mats'
    1.97    val obj'' = vector_cmul scal2 obj'
    1.98   in solver obj'' mats''
    1.99    end
   1.100 @@ -655,7 +655,7 @@
   1.101  (* Stuff for "equations" ((int*int*int)->num functions).                         *)
   1.102  
   1.103  fun tri_equation_cmul c eq =
   1.104 -  if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (fn d => c */ d) eq;
   1.105 +  if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (fn _ => fn d => c */ d) eq;
   1.106  
   1.107  fun tri_equation_add eq1 eq2 = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0) eq1 eq2;
   1.108  
   1.109 @@ -686,7 +686,7 @@
   1.110       in if b =/ rat_0 then e else
   1.111          tri_equation_add e (tri_equation_cmul (Rat.neg b // a) eq)
   1.112       end
   1.113 -   in eliminate vs (Inttriplefunc.update (v,eq') (Inttriplefunc.map elim dun)) (map elim oeqs)
   1.114 +   in eliminate vs (Inttriplefunc.update (v,eq') (Inttriplefunc.map (K elim) dun)) (map elim oeqs)
   1.115     end)
   1.116    handle Failure _ => eliminate vs dun eqs)
   1.117  in
   1.118 @@ -724,7 +724,7 @@
   1.119           in if b =/ rat_0 then e
   1.120              else tri_equation_add e (tri_equation_cmul (Rat.neg b // a) eq)
   1.121           end
   1.122 -    in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map elim dun))
   1.123 +    in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map (K elim) dun))
   1.124                   (map elim oeqs)
   1.125      end
   1.126  in fn eqs =>
   1.127 @@ -744,7 +744,7 @@
   1.128              (Inttriplefunc.onefunc(one, Rat.rat_of_int ~1))
   1.129    val ass =
   1.130      Inttriplefunc.combine (curry op +/) (K false)
   1.131 -    (Inttriplefunc.map (tri_equation_eval vfn) assigs) vfn
   1.132 +    (Inttriplefunc.map (K (tri_equation_eval vfn)) assigs) vfn
   1.133   in if forall (fn e => tri_equation_eval ass e =/ rat_0) eqs
   1.134      then Inttriplefunc.delete_safe one ass else raise Sanity
   1.135   end;
   1.136 @@ -762,7 +762,7 @@
   1.137  (* Usual operations on equation-parametrized poly.                           *)
   1.138  
   1.139  fun tri_epoly_cmul c l =
   1.140 -  if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (tri_equation_cmul c) l;;
   1.141 +  if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (K (tri_equation_cmul c)) l;;
   1.142  
   1.143  val tri_epoly_neg = tri_epoly_cmul (Rat.rat_of_int ~1);
   1.144  
   1.145 @@ -773,7 +773,7 @@
   1.146  (* Stuff for "equations" ((int*int)->num functions).                         *)
   1.147  
   1.148  fun pi_equation_cmul c eq =
   1.149 -  if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (fn d => c */ d) eq;
   1.150 +  if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (fn _ => fn d => c */ d) eq;
   1.151  
   1.152  fun pi_equation_add eq1 eq2 = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0) eq1 eq2;
   1.153  
   1.154 @@ -804,7 +804,7 @@
   1.155       in if b =/ rat_0 then e else
   1.156          pi_equation_add e (pi_equation_cmul (Rat.neg b // a) eq)
   1.157       end
   1.158 -   in eliminate vs (Inttriplefunc.update (v,eq') (Inttriplefunc.map elim dun)) (map elim oeqs)
   1.159 +   in eliminate vs (Inttriplefunc.update (v,eq') (Inttriplefunc.map (K elim) dun)) (map elim oeqs)
   1.160     end
   1.161    handle Failure _ => eliminate vs dun eqs
   1.162  in
   1.163 @@ -842,7 +842,7 @@
   1.164           in if b =/ rat_0 then e
   1.165              else pi_equation_add e (pi_equation_cmul (Rat.neg b // a) eq)
   1.166           end
   1.167 -    in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map elim dun))
   1.168 +    in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map (K elim) dun))
   1.169                   (map elim oeqs)
   1.170      end
   1.171  in fn eqs =>
   1.172 @@ -862,7 +862,7 @@
   1.173              (Inttriplefunc.onefunc(one, Rat.rat_of_int ~1))
   1.174    val ass =
   1.175      Inttriplefunc.combine (curry op +/) (K false)
   1.176 -    (Inttriplefunc.map (pi_equation_eval vfn) assigs) vfn
   1.177 +    (Inttriplefunc.map (K (pi_equation_eval vfn)) assigs) vfn
   1.178   in if forall (fn e => pi_equation_eval ass e =/ rat_0) eqs
   1.179      then Inttriplefunc.delete_safe one ass else raise Sanity
   1.180   end;
   1.181 @@ -880,7 +880,7 @@
   1.182  (* Usual operations on equation-parametrized poly.                           *)
   1.183  
   1.184  fun pi_epoly_cmul c l =
   1.185 -  if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (pi_equation_cmul c) l;;
   1.186 +  if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (K (pi_equation_cmul c)) l;;
   1.187  
   1.188  val pi_epoly_neg = pi_epoly_cmul (Rat.rat_of_int ~1);
   1.189  
   1.190 @@ -1035,7 +1035,7 @@
   1.191  val bmatrix_add = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0);
   1.192  fun bmatrix_cmul c bm =
   1.193    if c =/ rat_0 then Inttriplefunc.empty
   1.194 -  else Inttriplefunc.map (fn x => c */ x) bm;
   1.195 +  else Inttriplefunc.map (fn _ => fn x => c */ x) bm;
   1.196  
   1.197  val bmatrix_neg = bmatrix_cmul (Rat.rat_of_int ~1);
   1.198  fun bmatrix_sub m1 m2 = bmatrix_add m1 (bmatrix_neg m2);;
     2.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Sep 02 10:29:47 2010 +0200
     2.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Sep 02 10:29:48 2010 +0200
     2.3 @@ -549,7 +549,7 @@
     2.4  (* A linear arithmetic prover *)
     2.5  local
     2.6    val linear_add = FuncUtil.Ctermfunc.combine (curry op +/) (fn z => z =/ Rat.zero)
     2.7 -  fun linear_cmul c = FuncUtil.Ctermfunc.map (fn x => c */ x)
     2.8 +  fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c */ x)
     2.9    val one_tm = @{cterm "1::real"}
    2.10    fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
    2.11       ((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso