author wenzelm Wed Jun 01 10:45:35 2016 +0200 (2016-06-01) changeset 63201 f151704c08e4 parent 63200 6eccfe9f5ef1 child 63202 e77481be5c97
tuned signature;
```     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.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
```