merged

--- a/src/HOL/Decision_Procs/approximation_generator.ML	Mon Jan 27 21:31:11 2025 +0100
+++ b/src/HOL/Decision_Procs/approximation_generator.ML	Mon Jan 27 22:27:18 2025 +0100
@@ -38,13 +38,13 @@
       handle TERM _ => raise TERM ("mapprox_float", [t]);
 
 (* TODO: define using compiled terms? *)
-fun mapprox_floatarith \<^Const_>\<open>Add for a b\<close> xs = mapprox_floatarith a xs + mapprox_floatarith b xs
-  | mapprox_floatarith \<^Const_>\<open>Minus for a\<close> xs = ~ (mapprox_floatarith a xs)
-  | mapprox_floatarith \<^Const_>\<open>Mult for a b\<close> xs = mapprox_floatarith a xs * mapprox_floatarith b xs
-  | mapprox_floatarith \<^Const_>\<open>Inverse for a\<close> xs = 1.0 / mapprox_floatarith a xs
+fun mapprox_floatarith \<^Const_>\<open>Add for a b\<close> xs = Real.+ (mapprox_floatarith a xs, mapprox_floatarith b xs)
+  | mapprox_floatarith \<^Const_>\<open>Minus for a\<close> xs = Real.~ (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Mult for a b\<close> xs = Real.* (mapprox_floatarith a xs, mapprox_floatarith b xs)
+  | mapprox_floatarith \<^Const_>\<open>Inverse for a\<close> xs = 1.0 / (mapprox_floatarith a xs : real)
   | mapprox_floatarith \<^Const_>\<open>Cos for a\<close> xs = Math.cos (mapprox_floatarith a xs)
   | mapprox_floatarith \<^Const_>\<open>Arctan for a\<close> xs = Math.atan (mapprox_floatarith a xs)
-  | mapprox_floatarith \<^Const_>\<open>Abs for a\<close> xs = abs (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Abs for a\<close> xs = Real.abs (mapprox_floatarith a xs : real)
   | mapprox_floatarith \<^Const_>\<open>Max for a b\<close> xs =
       Real.max (mapprox_floatarith a xs, mapprox_floatarith b xs)
   | mapprox_floatarith \<^Const_>\<open>Min for a b\<close> xs =
@@ -66,15 +66,15 @@
     let
       val x' = mapprox_floatarith x xs
     in
-      mapprox_floatarith a xs + eps <= x' andalso x' + eps <= mapprox_floatarith b xs
+      Real.<= (Real.+ (mapprox_floatarith a xs, eps), x') andalso Real.<= (Real.+ (x', eps), mapprox_floatarith b xs)
     end
 
 fun mapprox_form eps \<^Const_>\<open>Bound for x a b f\<close> xs =
     (not (mapprox_atLeastAtMost eps x a b xs)) orelse mapprox_form eps f xs
 | mapprox_form eps \<^Const_>\<open>Assign for x a f\<close> xs =
     (Real.!= (mapprox_floatarith x xs, mapprox_floatarith a xs)) orelse mapprox_form eps f xs
-| mapprox_form eps \<^Const_>\<open>Less for a b\<close> xs = mapprox_floatarith a xs + eps < mapprox_floatarith b xs
-| mapprox_form eps \<^Const_>\<open>LessEqual for a b\<close> xs = mapprox_floatarith a xs + eps <= mapprox_floatarith b xs
+| mapprox_form eps \<^Const_>\<open>Less for a b\<close> xs = Real.< (Real.+ (mapprox_floatarith a xs, eps), mapprox_floatarith b xs)
+| mapprox_form eps \<^Const_>\<open>LessEqual for a b\<close> xs = Real.<= (Real.+ (mapprox_floatarith a xs, eps), mapprox_floatarith b xs)
 | mapprox_form eps \<^Const_>\<open>AtLeastAtMost for x a b\<close> xs = mapprox_atLeastAtMost eps x a b xs
 | mapprox_form eps \<^Const_>\<open>Conj for f g\<close> xs = mapprox_form eps f xs andalso mapprox_form eps g xs
 | mapprox_form eps \<^Const_>\<open>Disj for f g\<close> xs = mapprox_form eps f xs orelse mapprox_form eps g xs

--- a/src/HOL/Library/Code_Target_Bit_Shifts.thy	Mon Jan 27 21:31:11 2025 +0100
+++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy	Mon Jan 27 22:27:18 2025 +0100
@@ -44,37 +44,31 @@
   val word_max_index : Word.word (*only for validation*)
 end = struct
 
-type int = IntInf.int;
-
-fun curry f x y = f (x, y);
+open IntInf;
 
 fun fold _ [] y = y
   | fold f (x :: xs) y = fold f xs (f x y);
 
 fun replicate n x = (if n <= 0 then [] else x :: replicate (n - 1) x);
 
-val exp = curry IntInf.pow 2;
-
-val div_mod = curry IntInf.divMod;
+val max_index = pow (2, (Word.wordSize - 3)) - 1; (*experimentally determined*)
 
-val max_index = exp (Word.wordSize - 3) - 1; (*experimentally determined*)
-
-val word_of_int = Word.fromLargeInt o IntInf.toLarge;
+val word_of_int = Word.fromLargeInt o toLarge;
 
 val word_max_index = word_of_int max_index;
 
-fun words_of_int k = case div_mod k max_index
+fun words_of_int k = case divMod (k, max_index)
   of (b, s) => word_of_int s :: (replicate b word_max_index);
 
-fun push' i k = IntInf.<< (k, i);
+fun push' i k = << (k, i);
 
-fun drop' i k = IntInf.~>> (k, i);
+fun drop' i k = ~>> (k, i);
 
 (* The implementations are formally total, though indices >~ max_index will produce heavy computation load *)
 
-fun push i = fold push' (words_of_int (IntInf.abs i));
+fun push i = fold push' (words_of_int (abs i));
 
-fun drop i = fold drop' (words_of_int (IntInf.abs i));
+fun drop i = fold drop' (words_of_int (abs i));
 
 end;\<close> for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit
     and (OCaml) \<open>
@@ -83,8 +77,6 @@
   val drop : Z.t -> Z.t -> Z.t
 end = struct
 
-let curry f x y = f (x, y);;
-
 let rec fold f xs y = match xs with
   [] -> y
   | (x :: xs) -> fold f xs (f x y);;
@@ -109,7 +101,7 @@
 end;;
 \<close> for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit
     and (Haskell) \<open>
-module Bit_Shifts where
+module Bit_Shifts (push, drop, push', drop') where
 
 import Prelude (Int, Integer, toInteger, fromInteger, maxBound, divMod, (-), (<=), abs, flip)
 import GHC.Bits (Bits)
@@ -131,17 +123,17 @@
 
 {- The implementations are formally total, though indices >~ maxIndex will produce heavy computation load -}
 
-push' :: Int -> Int -> Int
-push' i = flip shiftL (abs i)
-
 push :: Integer -> Integer -> Integer
 push i = fold (flip shiftL) (splitIndex (abs i))
 
+drop :: Integer -> Integer -> Integer
+drop i = fold (flip shiftR) (splitIndex (abs i))
+
+push' :: Int -> Int -> Int
+push' i = flip shiftL (abs i)
+
 drop' :: Int -> Int -> Int
 drop' i = flip shiftR (abs i)
-
-drop :: Integer -> Integer -> Integer
-drop i = fold (flip shiftR) (splitIndex (abs i))
 \<close> for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit
     and (Scala) \<open>
 object Bit_Shifts {

--- a/src/HOL/String.thy	Mon Jan 27 21:31:11 2025 +0100
+++ b/src/HOL/String.thy	Mon Jan 27 22:27:18 2025 +0100
@@ -775,9 +775,9 @@
   then k
   else raise Fail "Non-ASCII character in literal";
 
-val char_of_ascii = Char.chr o IntInf.toInt o (fn k => k mod 128);
+val char_of_ascii = Char.chr o toInt o (fn k => k mod 128);
 
-val ascii_of_char = check_ascii o IntInf.fromInt o Char.ord;
+val ascii_of_char = check_ascii o fromInt o Char.ord;
 
 val literal_of_asciis = String.implode o map char_of_ascii;