tuned signature;
authorwenzelm
Wed Jun 01 10:45:35 2016 +0200 (2016-06-01)
changeset 63201f151704c08e4
parent 63200 6eccfe9f5ef1
child 63202 e77481be5c97
tuned signature;
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Multivariate_Analysis/normarith.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/semiring_normalizer.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/General/rat.ML
     1.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue May 31 23:06:03 2016 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Jun 01 10:45:35 2016 +0200
     1.3 @@ -897,9 +897,9 @@
     1.4  fun dest_frac ct =
     1.5    case Thm.term_of ct of
     1.6      Const (@{const_name Rings.divide},_) $ a $ b=>
     1.7 -      Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
     1.8 -  | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
     1.9 -  | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
    1.10 +      Rat.make (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
    1.11 +  | Const(@{const_name inverse}, _)$a => Rat.make(1, HOLogic.dest_number a |> snd)
    1.12 +  | t => Rat.of_int (snd (HOLogic.dest_number t))
    1.13  
    1.14  fun whatis x ct = case Thm.term_of ct of
    1.15    Const(@{const_name Groups.plus}, _)$(Const(@{const_name Groups.times},_)$_$y)$_ =>
     2.1 --- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Tue May 31 23:06:03 2016 +0200
     2.2 +++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Wed Jun 01 10:45:35 2016 +0200
     2.3 @@ -20,7 +20,7 @@
     2.4  
     2.5  fun string_of_rat r =
     2.6    let
     2.7 -    val (nom, den) = Rat.quotient_of_rat r
     2.8 +    val (nom, den) = Rat.dest r
     2.9    in
    2.10      if den = 1 then string_of_int nom
    2.11      else string_of_int nom ^ "/" ^ string_of_int den
    2.12 @@ -103,8 +103,8 @@
    2.13  
    2.14  val nat = number
    2.15  val int = Scan.optional (str "~" >> K ~1) 1 -- nat >> op *
    2.16 -val rat = int --| str "/" -- int >> Rat.rat_of_quotient
    2.17 -val rat_int = rat || int >> Rat.rat_of_int
    2.18 +val rat = int --| str "/" -- int >> Rat.make
    2.19 +val rat_int = rat || int >> Rat.of_int
    2.20  
    2.21  
    2.22  (* polynomial parsers *)
     3.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue May 31 23:06:03 2016 +0200
     3.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jun 01 10:45:35 2016 +0200
     3.3 @@ -22,18 +22,18 @@
     3.4  val rat_0 = Rat.zero;
     3.5  val rat_1 = Rat.one;
     3.6  val rat_2 = Rat.two;
     3.7 -val rat_10 = Rat.rat_of_int 10;
     3.8 +val rat_10 = Rat.of_int 10;
     3.9  val max = Integer.max;
    3.10  
    3.11 -val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int;
    3.12 +val denominator_rat = Rat.dest #> snd #> Rat.of_int;
    3.13  
    3.14  fun int_of_rat a =
    3.15 -  (case Rat.quotient_of_rat a of
    3.16 +  (case Rat.dest a of
    3.17      (i, 1) => i
    3.18    | _ => error "int_of_rat: not an int");
    3.19  
    3.20  fun lcm_rat x y =
    3.21 -  Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y));
    3.22 +  Rat.of_int (Integer.lcm (int_of_rat x) (int_of_rat y));
    3.23  
    3.24  fun rat_pow r i =
    3.25   let fun pow r i =
    3.26 @@ -45,9 +45,9 @@
    3.27  
    3.28  fun round_rat r =
    3.29    let
    3.30 -    val (a,b) = Rat.quotient_of_rat (Rat.abs r)
    3.31 +    val (a,b) = Rat.dest (Rat.abs r)
    3.32      val d = a div b
    3.33 -    val s = if r < rat_0 then (Rat.neg o Rat.rat_of_int) else Rat.rat_of_int
    3.34 +    val s = if r < rat_0 then (Rat.neg o Rat.of_int) else Rat.of_int
    3.35      val x2 = 2 * (a - (b * d))
    3.36    in s (if x2 >= b then d + 1 else d) end
    3.37  
    3.38 @@ -302,11 +302,11 @@
    3.39    else index_char str chr (pos + 1);
    3.40  
    3.41  fun rat_of_quotient (a,b) =
    3.42 -  if b = 0 then rat_0 else Rat.rat_of_quotient (a, b);
    3.43 +  if b = 0 then rat_0 else Rat.make (a, b);
    3.44  
    3.45  fun rat_of_string s =
    3.46    let val n = index_char s #"/" 0 in
    3.47 -    if n = ~1 then s |> Int.fromString |> the |> Rat.rat_of_int
    3.48 +    if n = ~1 then s |> Int.fromString |> the |> Rat.of_int
    3.49      else
    3.50        let
    3.51          val SOME numer = Int.fromString(String.substring(s,0,n))
    3.52 @@ -365,7 +365,7 @@
    3.53    fun maximal_element fld amat acc =
    3.54      fld (fn (_,c) => fn maxa => max_rat maxa (abs_rat c)) amat acc
    3.55    fun float_of_rat x =
    3.56 -    let val (a,b) = Rat.quotient_of_rat x
    3.57 +    let val (a,b) = Rat.dest x
    3.58      in Real.fromInt a / Real.fromInt b end;
    3.59    fun int_of_float x = (trunc x handle Overflow => 0 | Domain => 0)
    3.60  in
    3.61 @@ -438,7 +438,7 @@
    3.62                val v = choose_variable eq
    3.63                val a = Inttriplefunc.apply eq v
    3.64                val eq' =
    3.65 -                tri_equation_cmul ((Rat.rat_of_int ~1) / a) (Inttriplefunc.delete_safe v eq)
    3.66 +                tri_equation_cmul ((Rat.of_int ~1) / a) (Inttriplefunc.delete_safe v eq)
    3.67                fun elim e =
    3.68                  let val b = Inttriplefunc.tryapplyd e v rat_0 in
    3.69                    if b = rat_0 then e
    3.70 @@ -608,7 +608,7 @@
    3.71    if c = rat_0 then Inttriplefunc.empty
    3.72    else Inttriplefunc.map (fn _ => fn x => c * x) bm;
    3.73  
    3.74 -val bmatrix_neg = bmatrix_cmul (Rat.rat_of_int ~1);
    3.75 +val bmatrix_neg = bmatrix_cmul (Rat.of_int ~1);
    3.76  
    3.77  (* Smash a block matrix into components.                                     *)
    3.78  
    3.79 @@ -729,10 +729,10 @@
    3.80        in (vec, map diag allmats) end
    3.81      val (vec, ratdias) =
    3.82        if null pvs then find_rounding rat_1
    3.83 -      else tryfind find_rounding (map Rat.rat_of_int (1 upto 31) @ map pow2 (5 upto 66))
    3.84 +      else tryfind find_rounding (map Rat.of_int (1 upto 31) @ map pow2 (5 upto 66))
    3.85      val newassigs =
    3.86        fold_rev (fn k => Inttriplefunc.update (nth pvs (k - 1), int_element vec k))
    3.87 -        (1 upto dim vec) (Inttriplefunc.onefunc ((0, 0, 0), Rat.rat_of_int ~1))
    3.88 +        (1 upto dim vec) (Inttriplefunc.onefunc ((0, 0, 0), Rat.of_int ~1))
    3.89      val finalassigs =
    3.90        Inttriplefunc.fold (fn (v, e) => fn a =>
    3.91          Inttriplefunc.update (v, tri_equation_eval newassigs e) a) allassig newassigs
     4.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue May 31 23:06:03 2016 +0200
     4.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 10:45:35 2016 +0200
     4.3 @@ -287,7 +287,7 @@
     4.4  
     4.5  fun cterm_of_rat x =
     4.6    let
     4.7 -    val (a, b) = Rat.quotient_of_rat x
     4.8 +    val (a, b) = Rat.dest x
     4.9    in
    4.10      if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
    4.11      else Thm.apply (Thm.apply @{cterm "op / :: real => _"}
    4.12 @@ -297,8 +297,8 @@
    4.13  
    4.14  fun dest_ratconst t =
    4.15    case Thm.term_of t of
    4.16 -    Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    4.17 -  | _ => Rat.rat_of_int (HOLogic.dest_number (Thm.term_of t) |> snd)
    4.18 +    Const(@{const_name divide}, _)$a$b => Rat.make(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    4.19 +  | _ => Rat.of_int (HOLogic.dest_number (Thm.term_of t) |> snd)
    4.20  fun is_ratconst t = can dest_ratconst t
    4.21  
    4.22  (*
     5.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Tue May 31 23:06:03 2016 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Wed Jun 01 10:45:35 2016 +0200
     5.3 @@ -16,9 +16,9 @@
     5.4   open Conv;
     5.5   val bool_eq = op = : bool *bool -> bool
     5.6    fun dest_ratconst t = case Thm.term_of t of
     5.7 -   Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
     5.8 - | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
     5.9 - | _ => Rat.rat_of_int (HOLogic.dest_number (Thm.term_of t) |> snd)
    5.10 +   Const(@{const_name divide}, _)$a$b => Rat.make(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    5.11 + | Const(@{const_name inverse}, _)$a => Rat.make(1, HOLogic.dest_number a |> snd)
    5.12 + | _ => Rat.of_int (HOLogic.dest_number (Thm.term_of t) |> snd)
    5.13   fun is_ratconst t = can dest_ratconst t
    5.14   fun augment_norm b t acc = case Thm.term_of t of
    5.15       Const(@{const_name norm}, _) $ _ => insert (eq_pair bool_eq (op aconvc)) (b,Thm.dest_arg t) acc
    5.16 @@ -146,7 +146,7 @@
    5.17  fun match_mp PQ P = P RS PQ;
    5.18  
    5.19  fun cterm_of_rat x =
    5.20 -let val (a, b) = Rat.quotient_of_rat x
    5.21 +let val (a, b) = Rat.dest x
    5.22  in
    5.23   if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
    5.24    else Thm.apply (Thm.apply @{cterm "op / :: real => _"}
    5.25 @@ -301,7 +301,7 @@
    5.26          end
    5.27         val goodverts = filter check_solution rawverts
    5.28         val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs
    5.29 -      in map (map2 (fn s => fn c => Rat.rat_of_int s * c) signfixups) goodverts
    5.30 +      in map (map2 (fn s => fn c => Rat.of_int s * c) signfixups) goodverts
    5.31        end
    5.32       val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) []
    5.33      in subsume allverts []
     6.1 --- a/src/HOL/Tools/groebner.ML	Tue May 31 23:06:03 2016 +0200
     6.2 +++ b/src/HOL/Tools/groebner.ML	Wed Jun 01 10:45:35 2016 +0200
     6.3 @@ -35,10 +35,10 @@
     6.4  val rat_0 = Rat.zero;
     6.5  val rat_1 = Rat.one;
     6.6  val minus_rat = Rat.neg;
     6.7 -val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int;
     6.8 +val denominator_rat = Rat.dest #> snd #> Rat.of_int;
     6.9  fun int_of_rat a =
    6.10 -    case Rat.quotient_of_rat a of (i,1) => i | _ => error "int_of_rat: not an int";
    6.11 -val lcm_rat = fn x => fn y => Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y));
    6.12 +    case Rat.dest a of (i,1) => i | _ => error "int_of_rat: not an int";
    6.13 +val lcm_rat = fn x => fn y => Rat.of_int (Integer.lcm (int_of_rat x) (int_of_rat y));
    6.14  
    6.15  val (eqF_intr, eqF_elim) =
    6.16    let val [th1,th2] = @{thms PFalse}
     7.1 --- a/src/HOL/Tools/lin_arith.ML	Tue May 31 23:06:03 2016 +0200
     7.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Jun 01 10:45:35 2016 +0200
     7.3 @@ -179,10 +179,10 @@
     7.4        Same for Suc-terms that turn out not to be numerals -
     7.5        although the simplifier should eliminate those anyway ...*)
     7.6      | demult (t as Const ("Num.numeral_class.numeral", _) $ n, m) =
     7.7 -      ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_numeral n)))
     7.8 +      ((NONE, Rat.mult m (Rat.of_int (HOLogic.dest_numeral n)))
     7.9          handle TERM _ => (SOME t, m))
    7.10      | demult (t as Const (@{const_name Suc}, _) $ _, m) =
    7.11 -      ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_nat t)))
    7.12 +      ((NONE, Rat.mult m (Rat.of_int (HOLogic.dest_nat t)))
    7.13          handle TERM _ => (SOME t, m))
    7.14      (* injection constants are ignored *)
    7.15      | demult (t as Const f $ x, m) =
    7.16 @@ -209,7 +209,7 @@
    7.17          (p, Rat.add i m)
    7.18      | poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) =
    7.19          (let val k = HOLogic.dest_numeral t
    7.20 -        in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k))) end
    7.21 +        in (p, Rat.add i (Rat.mult m (Rat.of_int k))) end
    7.22          handle TERM _ => add_atom all m pi)
    7.23      | poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =
    7.24          poly (t, m, (p, Rat.add i m))
     8.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Tue May 31 23:06:03 2016 +0200
     8.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Wed Jun 01 10:45:35 2016 +0200
     8.3 @@ -115,11 +115,11 @@
     8.4  val semiring_funs =
     8.5     {is_const = can HOLogic.dest_number o Thm.term_of,
     8.6      dest_const = (fn ct =>
     8.7 -      Rat.rat_of_int (snd
     8.8 +      Rat.of_int (snd
     8.9          (HOLogic.dest_number (Thm.term_of ct)
    8.10            handle TERM _ => error "ring_dest_const"))),
    8.11      mk_const = (fn cT => fn x => Numeral.mk_cnumber cT
    8.12 -      (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int")),
    8.13 +      (case Rat.dest x of (i, 1) => i | _ => error "int_of_rat: bad int")),
    8.14      conv = (fn ctxt =>
    8.15        Simplifier.rewrite (put_simpset semiring_norm_ss ctxt)
    8.16        then_conv Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_One}))};
    8.17 @@ -137,13 +137,13 @@
    8.18       | t => can HOLogic.dest_number t
    8.19      fun dest_const ct = ((case Thm.term_of ct of
    8.20         Const (@{const_name Rings.divide},_) $ a $ b=>
    8.21 -        Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
    8.22 +        Rat.make (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
    8.23       | Const (@{const_name Fields.inverse},_)$t =>
    8.24 -                   Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
    8.25 -     | t => Rat.rat_of_int (snd (HOLogic.dest_number t)))
    8.26 +                   Rat.inv (Rat.of_int (snd (HOLogic.dest_number t)))
    8.27 +     | t => Rat.of_int (snd (HOLogic.dest_number t)))
    8.28         handle TERM _ => error "ring_dest_const")
    8.29      fun mk_const cT x =
    8.30 -      let val (a, b) = Rat.quotient_of_rat x
    8.31 +      let val (a, b) = Rat.dest x
    8.32        in if b = 1 then Numeral.mk_cnumber cT a
    8.33          else Thm.apply
    8.34               (Thm.apply (Thm.instantiate_cterm ([(divide_tvar, cT)], []) divide_const)
     9.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue May 31 23:06:03 2016 +0200
     9.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Jun 01 10:45:35 2016 +0200
     9.3 @@ -482,10 +482,10 @@
     9.4    AList.lookup Envir.aeconv poly atom |> the_default 0;
     9.5  
     9.6  fun integ(rlhs,r,rel,rrhs,s,d) =
     9.7 -let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
     9.8 -    val m = Integer.lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs))
     9.9 +let val (rn,rd) = Rat.dest r and (sn,sd) = Rat.dest s
    9.10 +    val m = Integer.lcms(map (abs o snd o Rat.dest) (r :: s :: map snd rlhs @ map snd rrhs))
    9.11      fun mult(t,r) =
    9.12 -        let val (i,j) = Rat.quotient_of_rat r
    9.13 +        let val (i,j) = Rat.dest r
    9.14          in (t,i * (m div j)) end
    9.15  in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end
    9.16  
    10.1 --- a/src/Pure/General/rat.ML	Tue May 31 23:06:03 2016 +0200
    10.2 +++ b/src/Pure/General/rat.ML	Wed Jun 01 10:45:35 2016 +0200
    10.3 @@ -11,9 +11,9 @@
    10.4    val zero: rat
    10.5    val one: rat
    10.6    val two: rat
    10.7 -  val rat_of_int: int -> rat
    10.8 -  val rat_of_quotient: int * int -> rat
    10.9 -  val quotient_of_rat: rat -> int * int
   10.10 +  val of_int: int -> rat
   10.11 +  val make: int * int -> rat
   10.12 +  val dest: rat -> int * int
   10.13    val string_of_rat: rat -> string
   10.14    val eq: rat * rat -> bool
   10.15    val ord: rat * rat -> order
   10.16 @@ -40,19 +40,19 @@
   10.17  
   10.18  exception DIVZERO;
   10.19  
   10.20 -fun rat_of_quotient (p, q) =
   10.21 +fun make (p, q) =
   10.22    let
   10.23      val m = PolyML.IntInf.gcd (p, q);
   10.24      val (p', q') = (p div m, q div m) handle Div => raise DIVZERO;
   10.25    in Rat (if q' < 0 then (~ p', ~ q') else (p', q')) end
   10.26  
   10.27 -fun quotient_of_rat (Rat r) = r;
   10.28 +fun dest (Rat r) = r;
   10.29  
   10.30 -fun rat_of_int i = Rat (i, 1);
   10.31 +fun of_int i = Rat (i, 1);
   10.32  
   10.33 -val zero = rat_of_int 0;
   10.34 -val one = rat_of_int 1;
   10.35 -val two = rat_of_int 2;
   10.36 +val zero = of_int 0;
   10.37 +val one = of_int 1;
   10.38 +val two = of_int 2;
   10.39  
   10.40  fun string_of_rat (Rat (p, q)) =
   10.41    string_of_int p ^ "/" ^ string_of_int q;
   10.42 @@ -80,10 +80,10 @@
   10.43  fun add (Rat (p1, q1)) (Rat (p2, q2)) =
   10.44    let
   10.45      val ((m1, m2), n) = common (p1, q1) (p2, q2);
   10.46 -  in rat_of_quotient (m1 + m2, n) end;
   10.47 +  in make (m1 + m2, n) end;
   10.48  
   10.49  fun mult (Rat (p1, q1)) (Rat (p2, q2)) =
   10.50 -  rat_of_quotient (p1 * p2, q1 * q2);
   10.51 +  make (p1 * p2, q1 * q2);
   10.52  
   10.53  fun neg (Rat (p, q)) = Rat (~ p, q);
   10.54