tuned signature;

--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue May 31 23:06:03 2016 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Jun 01 10:45:35 2016 +0200
@@ -897,9 +897,9 @@
 fun dest_frac ct =
   case Thm.term_of ct of
     Const (@{const_name Rings.divide},_) $ a $ b=>
-      Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
-  | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
-  | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
+      Rat.make (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
+  | Const(@{const_name inverse}, _)$a => Rat.make(1, HOLogic.dest_number a |> snd)
+  | t => Rat.of_int (snd (HOLogic.dest_number t))
 
 fun whatis x ct = case Thm.term_of ct of
   Const(@{const_name Groups.plus}, _)$(Const(@{const_name Groups.times},_)$_$y)$_ =>

--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Tue May 31 23:06:03 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Wed Jun 01 10:45:35 2016 +0200
@@ -20,7 +20,7 @@
 
 fun string_of_rat r =
   let
-    val (nom, den) = Rat.quotient_of_rat r
+    val (nom, den) = Rat.dest r
   in
     if den = 1 then string_of_int nom
     else string_of_int nom ^ "/" ^ string_of_int den
@@ -103,8 +103,8 @@
 
 val nat = number
 val int = Scan.optional (str "~" >> K ~1) 1 -- nat >> op *
-val rat = int --| str "/" -- int >> Rat.rat_of_quotient
-val rat_int = rat || int >> Rat.rat_of_int
+val rat = int --| str "/" -- int >> Rat.make
+val rat_int = rat || int >> Rat.of_int
 
 
 (* polynomial parsers *)

--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue May 31 23:06:03 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jun 01 10:45:35 2016 +0200
@@ -22,18 +22,18 @@
 val rat_0 = Rat.zero;
 val rat_1 = Rat.one;
 val rat_2 = Rat.two;
-val rat_10 = Rat.rat_of_int 10;
+val rat_10 = Rat.of_int 10;
 val max = Integer.max;
 
-val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int;
+val denominator_rat = Rat.dest #> snd #> Rat.of_int;
 
 fun int_of_rat a =
-  (case Rat.quotient_of_rat a of
+  (case Rat.dest a of
     (i, 1) => i
   | _ => error "int_of_rat: not an int");
 
 fun lcm_rat x y =
-  Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y));
+  Rat.of_int (Integer.lcm (int_of_rat x) (int_of_rat y));
 
 fun rat_pow r i =
  let fun pow r i =
@@ -45,9 +45,9 @@
 
 fun round_rat r =
   let
-    val (a,b) = Rat.quotient_of_rat (Rat.abs r)
+    val (a,b) = Rat.dest (Rat.abs r)
     val d = a div b
-    val s = if r < rat_0 then (Rat.neg o Rat.rat_of_int) else Rat.rat_of_int
+    val s = if r < rat_0 then (Rat.neg o Rat.of_int) else Rat.of_int
     val x2 = 2 * (a - (b * d))
   in s (if x2 >= b then d + 1 else d) end
 
@@ -302,11 +302,11 @@
   else index_char str chr (pos + 1);
 
 fun rat_of_quotient (a,b) =
-  if b = 0 then rat_0 else Rat.rat_of_quotient (a, b);
+  if b = 0 then rat_0 else Rat.make (a, b);
 
 fun rat_of_string s =
   let val n = index_char s #"/" 0 in
-    if n = ~1 then s |> Int.fromString |> the |> Rat.rat_of_int
+    if n = ~1 then s |> Int.fromString |> the |> Rat.of_int
     else
       let
         val SOME numer = Int.fromString(String.substring(s,0,n))
@@ -365,7 +365,7 @@
   fun maximal_element fld amat acc =
     fld (fn (_,c) => fn maxa => max_rat maxa (abs_rat c)) amat acc
   fun float_of_rat x =
-    let val (a,b) = Rat.quotient_of_rat x
+    let val (a,b) = Rat.dest x
     in Real.fromInt a / Real.fromInt b end;
   fun int_of_float x = (trunc x handle Overflow => 0 | Domain => 0)
 in
@@ -438,7 +438,7 @@
               val v = choose_variable eq
               val a = Inttriplefunc.apply eq v
               val eq' =
-                tri_equation_cmul ((Rat.rat_of_int ~1) / a) (Inttriplefunc.delete_safe v eq)
+                tri_equation_cmul ((Rat.of_int ~1) / a) (Inttriplefunc.delete_safe v eq)
               fun elim e =
                 let val b = Inttriplefunc.tryapplyd e v rat_0 in
                   if b = rat_0 then e
@@ -608,7 +608,7 @@
   if c = rat_0 then Inttriplefunc.empty
   else Inttriplefunc.map (fn _ => fn x => c * x) bm;
 
-val bmatrix_neg = bmatrix_cmul (Rat.rat_of_int ~1);
+val bmatrix_neg = bmatrix_cmul (Rat.of_int ~1);
 
 (* Smash a block matrix into components.                                     *)
 
@@ -729,10 +729,10 @@
       in (vec, map diag allmats) end
     val (vec, ratdias) =
       if null pvs then find_rounding rat_1
-      else tryfind find_rounding (map Rat.rat_of_int (1 upto 31) @ map pow2 (5 upto 66))
+      else tryfind find_rounding (map Rat.of_int (1 upto 31) @ map pow2 (5 upto 66))
     val newassigs =
       fold_rev (fn k => Inttriplefunc.update (nth pvs (k - 1), int_element vec k))
-        (1 upto dim vec) (Inttriplefunc.onefunc ((0, 0, 0), Rat.rat_of_int ~1))
+        (1 upto dim vec) (Inttriplefunc.onefunc ((0, 0, 0), Rat.of_int ~1))
     val finalassigs =
       Inttriplefunc.fold (fn (v, e) => fn a =>
         Inttriplefunc.update (v, tri_equation_eval newassigs e) a) allassig newassigs

--- a/src/HOL/Library/positivstellensatz.ML	Tue May 31 23:06:03 2016 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 10:45:35 2016 +0200
@@ -287,7 +287,7 @@
 
 fun cterm_of_rat x =
   let
-    val (a, b) = Rat.quotient_of_rat x
+    val (a, b) = Rat.dest x
   in
     if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
     else Thm.apply (Thm.apply @{cterm "op / :: real => _"}
@@ -297,8 +297,8 @@
 
 fun dest_ratconst t =
   case Thm.term_of t of
-    Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
-  | _ => Rat.rat_of_int (HOLogic.dest_number (Thm.term_of t) |> snd)
+    Const(@{const_name divide}, _)$a$b => Rat.make(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
+  | _ => Rat.of_int (HOLogic.dest_number (Thm.term_of t) |> snd)
 fun is_ratconst t = can dest_ratconst t
 
 (*

--- a/src/HOL/Multivariate_Analysis/normarith.ML	Tue May 31 23:06:03 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Wed Jun 01 10:45:35 2016 +0200
@@ -16,9 +16,9 @@
  open Conv;
  val bool_eq = op = : bool *bool -> bool
   fun dest_ratconst t = case Thm.term_of t of
-   Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
- | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
- | _ => Rat.rat_of_int (HOLogic.dest_number (Thm.term_of t) |> snd)
+   Const(@{const_name divide}, _)$a$b => Rat.make(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
+ | Const(@{const_name inverse}, _)$a => Rat.make(1, HOLogic.dest_number a |> snd)
+ | _ => Rat.of_int (HOLogic.dest_number (Thm.term_of t) |> snd)
  fun is_ratconst t = can dest_ratconst t
  fun augment_norm b t acc = case Thm.term_of t of
      Const(@{const_name norm}, _) $ _ => insert (eq_pair bool_eq (op aconvc)) (b,Thm.dest_arg t) acc
@@ -146,7 +146,7 @@
 fun match_mp PQ P = P RS PQ;
 
 fun cterm_of_rat x =
-let val (a, b) = Rat.quotient_of_rat x
+let val (a, b) = Rat.dest x
 in
  if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
   else Thm.apply (Thm.apply @{cterm "op / :: real => _"}
@@ -301,7 +301,7 @@
         end
        val goodverts = filter check_solution rawverts
        val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs
-      in map (map2 (fn s => fn c => Rat.rat_of_int s * c) signfixups) goodverts
+      in map (map2 (fn s => fn c => Rat.of_int s * c) signfixups) goodverts
       end
      val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) []
     in subsume allverts []

--- a/src/HOL/Tools/groebner.ML	Tue May 31 23:06:03 2016 +0200
+++ b/src/HOL/Tools/groebner.ML	Wed Jun 01 10:45:35 2016 +0200
@@ -35,10 +35,10 @@
 val rat_0 = Rat.zero;
 val rat_1 = Rat.one;
 val minus_rat = Rat.neg;
-val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int;
+val denominator_rat = Rat.dest #> snd #> Rat.of_int;
 fun int_of_rat a =
-    case Rat.quotient_of_rat a of (i,1) => i | _ => error "int_of_rat: not an int";
-val lcm_rat = fn x => fn y => Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y));
+    case Rat.dest a of (i,1) => i | _ => error "int_of_rat: not an int";
+val lcm_rat = fn x => fn y => Rat.of_int (Integer.lcm (int_of_rat x) (int_of_rat y));
 
 val (eqF_intr, eqF_elim) =
   let val [th1,th2] = @{thms PFalse}

--- a/src/HOL/Tools/lin_arith.ML	Tue May 31 23:06:03 2016 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Wed Jun 01 10:45:35 2016 +0200
@@ -179,10 +179,10 @@
       Same for Suc-terms that turn out not to be numerals -
       although the simplifier should eliminate those anyway ...*)
     | demult (t as Const ("Num.numeral_class.numeral", _) $ n, m) =
-      ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_numeral n)))
+      ((NONE, Rat.mult m (Rat.of_int (HOLogic.dest_numeral n)))
         handle TERM _ => (SOME t, m))
     | demult (t as Const (@{const_name Suc}, _) $ _, m) =
-      ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_nat t)))
+      ((NONE, Rat.mult m (Rat.of_int (HOLogic.dest_nat t)))
         handle TERM _ => (SOME t, m))
     (* injection constants are ignored *)
     | demult (t as Const f $ x, m) =
@@ -209,7 +209,7 @@
         (p, Rat.add i m)
     | poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) =
         (let val k = HOLogic.dest_numeral t
-        in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k))) end
+        in (p, Rat.add i (Rat.mult m (Rat.of_int k))) end
         handle TERM _ => add_atom all m pi)
     | poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =
         poly (t, m, (p, Rat.add i m))

--- a/src/HOL/Tools/semiring_normalizer.ML	Tue May 31 23:06:03 2016 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML	Wed Jun 01 10:45:35 2016 +0200
@@ -115,11 +115,11 @@
 val semiring_funs =
    {is_const = can HOLogic.dest_number o Thm.term_of,
     dest_const = (fn ct =>
-      Rat.rat_of_int (snd
+      Rat.of_int (snd
         (HOLogic.dest_number (Thm.term_of ct)
           handle TERM _ => error "ring_dest_const"))),
     mk_const = (fn cT => fn x => Numeral.mk_cnumber cT
-      (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int")),
+      (case Rat.dest x of (i, 1) => i | _ => error "int_of_rat: bad int")),
     conv = (fn ctxt =>
       Simplifier.rewrite (put_simpset semiring_norm_ss ctxt)
       then_conv Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_One}))};
@@ -137,13 +137,13 @@
      | t => can HOLogic.dest_number t
     fun dest_const ct = ((case Thm.term_of ct of
        Const (@{const_name Rings.divide},_) $ a $ b=>
-        Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
+        Rat.make (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
      | Const (@{const_name Fields.inverse},_)$t =>
-                   Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
-     | t => Rat.rat_of_int (snd (HOLogic.dest_number t)))
+                   Rat.inv (Rat.of_int (snd (HOLogic.dest_number t)))
+     | t => Rat.of_int (snd (HOLogic.dest_number t)))
        handle TERM _ => error "ring_dest_const")
     fun mk_const cT x =
-      let val (a, b) = Rat.quotient_of_rat x
+      let val (a, b) = Rat.dest x
       in if b = 1 then Numeral.mk_cnumber cT a
         else Thm.apply
              (Thm.apply (Thm.instantiate_cterm ([(divide_tvar, cT)], []) divide_const)

--- a/src/Provers/Arith/fast_lin_arith.ML	Tue May 31 23:06:03 2016 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Jun 01 10:45:35 2016 +0200
@@ -482,10 +482,10 @@
   AList.lookup Envir.aeconv poly atom |> the_default 0;
 
 fun integ(rlhs,r,rel,rrhs,s,d) =
-let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
-    val m = Integer.lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs))
+let val (rn,rd) = Rat.dest r and (sn,sd) = Rat.dest s
+    val m = Integer.lcms(map (abs o snd o Rat.dest) (r :: s :: map snd rlhs @ map snd rrhs))
     fun mult(t,r) =
-        let val (i,j) = Rat.quotient_of_rat r
+        let val (i,j) = Rat.dest r
         in (t,i * (m div j)) end
 in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end
 

--- a/src/Pure/General/rat.ML	Tue May 31 23:06:03 2016 +0200
+++ b/src/Pure/General/rat.ML	Wed Jun 01 10:45:35 2016 +0200
@@ -11,9 +11,9 @@
   val zero: rat
   val one: rat
   val two: rat
-  val rat_of_int: int -> rat
-  val rat_of_quotient: int * int -> rat
-  val quotient_of_rat: rat -> int * int
+  val of_int: int -> rat
+  val make: int * int -> rat
+  val dest: rat -> int * int
   val string_of_rat: rat -> string
   val eq: rat * rat -> bool
   val ord: rat * rat -> order
@@ -40,19 +40,19 @@
 
 exception DIVZERO;
 
-fun rat_of_quotient (p, q) =
+fun make (p, q) =
   let
     val m = PolyML.IntInf.gcd (p, q);
     val (p', q') = (p div m, q div m) handle Div => raise DIVZERO;
   in Rat (if q' < 0 then (~ p', ~ q') else (p', q')) end
 
-fun quotient_of_rat (Rat r) = r;
+fun dest (Rat r) = r;
 
-fun rat_of_int i = Rat (i, 1);
+fun of_int i = Rat (i, 1);
 
-val zero = rat_of_int 0;
-val one = rat_of_int 1;
-val two = rat_of_int 2;
+val zero = of_int 0;
+val one = of_int 1;
+val two = of_int 2;
 
 fun string_of_rat (Rat (p, q)) =
   string_of_int p ^ "/" ^ string_of_int q;
@@ -80,10 +80,10 @@
 fun add (Rat (p1, q1)) (Rat (p2, q2)) =
   let
     val ((m1, m2), n) = common (p1, q1) (p2, q2);
-  in rat_of_quotient (m1 + m2, n) end;
+  in make (m1 + m2, n) end;
 
 fun mult (Rat (p1, q1)) (Rat (p2, q2)) =
-  rat_of_quotient (p1 * p2, q1 * q2);
+  make (p1 * p2, q1 * q2);
 
 fun neg (Rat (p, q)) = Rat (~ p, q);