--- a/NEWS Wed Jun 01 15:43:15 2016 +0200
+++ b/NEWS Wed Jun 01 19:54:31 2016 +0200
@@ -344,8 +344,17 @@
nn_integral :: 'a measure => ('a => ennreal) => ennreal
INCOMPATIBILITY.
+
*** ML ***
+* Structure Rat for rational numbers is now an integral part of
+Isabelle/ML, with special notation @int/nat for numerals (an
+abbreviation for antiquotation @{Pure.rat int/nat}) and ML pretty
+printing. Standard operations on type Rat.rat are provided via ad-hoc
+overloading of + - * / = < <= > >= <> ~ abs. INCOMPATIBILITY, need to
+use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been
+superseded by General.Div.
+
* The ML function "ML" provides easy access to run-time compilation.
This is particularly useful for conditional compilation, without
requiring separate files.
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Jun 01 15:43:15 2016 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Jun 01 19:54:31 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)$_ =>
@@ -923,7 +923,7 @@
val cr = dest_frac c
val clt = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
- val neg = cr </ Rat.zero
+ val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
(Thm.apply @{cterm "Trueprop"}
(if neg then Thm.apply (Thm.apply clt c) cz
@@ -946,7 +946,7 @@
val cr = dest_frac c
val clt = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
- val neg = cr </ Rat.zero
+ val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
(Thm.apply @{cterm "Trueprop"}
(if neg then Thm.apply (Thm.apply clt c) cz
@@ -968,7 +968,7 @@
val cr = dest_frac c
val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool}))
val cz = Thm.dest_arg ct
- val neg = cr </ Rat.zero
+ val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
(Thm.apply @{cterm "Trueprop"}
(if neg then Thm.apply (Thm.apply clt c) cz
@@ -993,7 +993,7 @@
val cr = dest_frac c
val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool}))
val cz = Thm.dest_arg ct
- val neg = cr </ Rat.zero
+ val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
(Thm.apply @{cterm "Trueprop"}
(if neg then Thm.apply (Thm.apply clt c) cz
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML Wed Jun 01 15:43:15 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML Wed Jun 01 19:54:31 2016 +0200
@@ -18,15 +18,6 @@
local
-fun string_of_rat r =
- let
- val (nom, den) = Rat.quotient_of_rat r
- in
- if den = 1 then string_of_int nom
- else string_of_int nom ^ "/" ^ string_of_int den
- end
-
-
(* map polynomials to strings *)
fun string_of_varpow x k =
@@ -49,9 +40,9 @@
in foldr1 (fn (s, t) => s ^ "*" ^ t) vps end
fun string_of_cmonomial (m,c) =
- if FuncUtil.Ctermfunc.is_empty m then string_of_rat c
- else if c = Rat.one then string_of_monomial m
- else string_of_rat c ^ "*" ^ string_of_monomial m
+ if FuncUtil.Ctermfunc.is_empty m then Rat.string_of_rat c
+ else if c = @1 then string_of_monomial m
+ else Rat.string_of_rat c ^ "*" ^ string_of_monomial m
fun string_of_poly p =
if FuncUtil.Monomialfunc.is_empty p then "0"
@@ -67,9 +58,9 @@
fun pss_to_cert (RealArith.Axiom_eq i) = "A=" ^ string_of_int i
| pss_to_cert (RealArith.Axiom_le i) = "A<=" ^ string_of_int i
| pss_to_cert (RealArith.Axiom_lt i) = "A<" ^ string_of_int i
- | pss_to_cert (RealArith.Rational_eq r) = "R=" ^ string_of_rat r
- | pss_to_cert (RealArith.Rational_le r) = "R<=" ^ string_of_rat r
- | pss_to_cert (RealArith.Rational_lt r) = "R<" ^ string_of_rat r
+ | pss_to_cert (RealArith.Rational_eq r) = "R=" ^ Rat.string_of_rat r
+ | pss_to_cert (RealArith.Rational_le r) = "R<=" ^ Rat.string_of_rat r
+ | pss_to_cert (RealArith.Rational_lt r) = "R<" ^ Rat.string_of_rat r
| pss_to_cert (RealArith.Square p) = "[" ^ string_of_poly p ^ "]^2"
| pss_to_cert (RealArith.Eqmul (p, pss)) =
"([" ^ string_of_poly p ^ "] * " ^ pss_to_cert pss ^ ")"
@@ -103,8 +94,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 *)
@@ -121,7 +112,7 @@
fun parse_cmonomial ctxt =
rat_int --| str "*" -- (parse_monomial ctxt) >> swap ||
- (parse_monomial ctxt) >> (fn m => (m, Rat.one)) ||
+ (parse_monomial ctxt) >> (fn m => (m, @1)) ||
rat_int >> (fn r => (FuncUtil.Ctermfunc.empty, r))
fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >>
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Jun 01 15:43:15 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Jun 01 19:54:31 2016 +0200
@@ -19,42 +19,34 @@
structure Sum_of_Squares: SUM_OF_SQUARES =
struct
-val rat_0 = Rat.zero;
-val rat_1 = Rat.one;
-val rat_2 = Rat.two;
-val rat_10 = Rat.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 =
- if i = 0 then rat_1 else
+ if i = 0 then @1 else
let val d = pow r (i div 2)
- in d */ d */ (if i mod 2 = 0 then rat_1 else r)
+ in d * d * (if i mod 2 = 0 then @1 else r)
end
in if i < 0 then pow (Rat.inv r) (~ i) else pow r i end;
fun round_rat r =
let
- val (a,b) = Rat.quotient_of_rat (Rat.abs r)
+ val (a,b) = Rat.dest (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 < @0 then ~ 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
-val abs_rat = Rat.abs;
-val pow2 = rat_pow rat_2;
-val pow10 = rat_pow rat_10;
-
val trace = Attrib.setup_config_bool @{binding sos_trace} (K false);
val debug = Attrib.setup_config_bool @{binding sos_debug} (K false);
@@ -78,22 +70,22 @@
local
fun normalize y =
- if abs_rat y </ (rat_1 // rat_10) then normalize (rat_10 */ y) - 1
- else if abs_rat y >=/ rat_1 then normalize (y // rat_10) + 1
+ if abs y < @1/10 then normalize (@10 * y) - 1
+ else if abs y >= @1 then normalize (y / @10) + 1
else 0
in
fun decimalize d x =
- if x =/ rat_0 then "0.0"
+ if x = @0 then "0.0"
else
let
- val y = Rat.abs x
+ val y = abs x
val e = normalize y
- val z = pow10(~ e) */ y +/ rat_1
- val k = int_of_rat (round_rat(pow10 d */ z))
+ val z = rat_pow @10 (~ e) * y + @1
+ val k = int_of_rat (round_rat (rat_pow @10 d * z))
in
- (if x </ rat_0 then "-0." else "0.") ^
+ (if x < @0 then "-0." else "0.") ^
implode (tl (raw_explode(string_of_int k))) ^
(if e = 0 then "" else "e" ^ string_of_int e)
end
@@ -117,7 +109,7 @@
type matrix = (int * int) * Rat.rat FuncUtil.Intpairfunc.table;
-fun iszero (_, r) = r =/ rat_0;
+fun iszero (_, r) = r = @0;
(* Vectors. Conventionally indexed 1..n. *)
@@ -128,8 +120,8 @@
fun vector_cmul c (v: vector) =
let val n = dim v in
- if c =/ rat_0 then vector_0 n
- else (n,FuncUtil.Intfunc.map (fn _ => fn x => c */ x) (snd v))
+ if c = @0 then vector_0 n
+ else (n,FuncUtil.Intfunc.map (fn _ => fn x => c * x) (snd v))
end;
fun vector_of_list l =
@@ -151,8 +143,8 @@
(* Monomials. *)
fun monomial_eval assig m =
- FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => a */ rat_pow (FuncUtil.Ctermfunc.apply assig x) k)
- m rat_1;
+ FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => a * rat_pow (FuncUtil.Ctermfunc.apply assig x) k)
+ m @1;
val monomial_1 = FuncUtil.Ctermfunc.empty;
@@ -169,7 +161,7 @@
(* Polynomials. *)
fun eval assig p =
- FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => a +/ c */ monomial_eval assig m) p rat_0;
+ FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => a + c * monomial_eval assig m) p @0;
val poly_0 = FuncUtil.Monomialfunc.empty;
@@ -177,31 +169,31 @@
FuncUtil.Monomialfunc.fold (fn (m, _) => fn a => FuncUtil.Ctermfunc.is_empty m andalso a)
p true;
-fun poly_var x = FuncUtil.Monomialfunc.onefunc (monomial_var x, rat_1);
+fun poly_var x = FuncUtil.Monomialfunc.onefunc (monomial_var x, @1);
fun poly_const c =
- if c =/ rat_0 then poly_0 else FuncUtil.Monomialfunc.onefunc (monomial_1, c);
+ if c = @0 then poly_0 else FuncUtil.Monomialfunc.onefunc (monomial_1, c);
fun poly_cmul c p =
- if c =/ rat_0 then poly_0
- else FuncUtil.Monomialfunc.map (fn _ => fn x => c */ x) p;
+ if c = @0 then poly_0
+ else FuncUtil.Monomialfunc.map (fn _ => fn x => c * x) p;
-fun poly_neg p = FuncUtil.Monomialfunc.map (K Rat.neg) p;
+fun poly_neg p = FuncUtil.Monomialfunc.map (K ~) p;
fun poly_add p1 p2 =
- FuncUtil.Monomialfunc.combine (curry op +/) (fn x => x =/ rat_0) p1 p2;
+ FuncUtil.Monomialfunc.combine (curry op +) (fn x => x = @0) p1 p2;
fun poly_sub p1 p2 = poly_add p1 (poly_neg p2);
fun poly_cmmul (c,m) p =
- if c =/ rat_0 then poly_0
+ if c = @0 then poly_0
else
if FuncUtil.Ctermfunc.is_empty m
- then FuncUtil.Monomialfunc.map (fn _ => fn d => c */ d) p
+ then FuncUtil.Monomialfunc.map (fn _ => fn d => c * d) p
else
FuncUtil.Monomialfunc.fold (fn (m', d) => fn a =>
- (FuncUtil.Monomialfunc.update (monomial_mul m m', c */ d) a)) p poly_0;
+ (FuncUtil.Monomialfunc.update (monomial_mul m m', c * d) a)) p poly_0;
fun poly_mul p1 p2 =
FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => poly_add (poly_cmmul (c,m) p2) a) p1 poly_0;
@@ -209,7 +201,7 @@
fun poly_square p = poly_mul p p;
fun poly_pow p k =
- if k = 0 then poly_const rat_1
+ if k = 0 then poly_const @1
else if k = 1 then p
else
let val q = poly_square(poly_pow p (k div 2))
@@ -289,7 +281,7 @@
let
val n = dim v
val strs =
- map (decimalize 20 o (fn i => FuncUtil.Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n)
+ map (decimalize 20 o (fn i => FuncUtil.Intfunc.tryapplyd (snd v) i @0)) (1 upto n)
in space_implode " " strs ^ "\n" end;
fun triple_int_ord ((a, b, c), (a', b', c')) =
@@ -302,11 +294,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 @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))
@@ -323,10 +315,10 @@
val numeral = Scan.one isnum
val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
val decimalfrac = Scan.repeat1 numeral
- >> (fn s => rat_of_string(implode s) // pow10 (length s))
+ >> (fn s => rat_of_string(implode s) / rat_pow @10 (length s))
val decimalsig =
decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac)
- >> (fn (h,NONE) => h | (h,SOME x) => h +/ x)
+ >> (fn (h,NONE) => h | (h,SOME x) => h + x)
fun signed prs =
$$ "-" |-- prs >> Rat.neg
|| $$ "+" |-- prs
@@ -336,8 +328,8 @@
val exponent = ($$ "e" || $$ "E") |-- signed decimalint;
-val decimal = signed decimalsig -- (emptyin rat_0|| exponent)
- >> (fn (h, x) => h */ pow10 (int_of_rat x));
+val decimal = signed decimalsig -- (emptyin @0|| exponent)
+ >> (fn (h, x) => h * rat_pow @10 (int_of_rat x));
fun mkparser p s =
let val (x,rst) = p (raw_explode s)
@@ -359,39 +351,39 @@
(* Version for (int*int*int) keys *)
local
- fun max_rat x y = if x </ y then y else x
+ fun max_rat x y = if x < y then y else x
fun common_denominator fld amat acc =
fld (fn (_,c) => fn a => lcm_rat (denominator_rat c) a) amat acc
fun maximal_element fld amat acc =
- fld (fn (_,c) => fn maxa => max_rat maxa (abs_rat c)) amat acc
+ fld (fn (_,c) => fn maxa => max_rat maxa (abs 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
fun tri_scale_then solver (obj:vector) mats =
let
- val cd1 = fold_rev (common_denominator Inttriplefunc.fold) mats (rat_1)
- val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj) (rat_1)
- val mats' = map (Inttriplefunc.map (fn _ => fn x => cd1 */ x)) mats
+ val cd1 = fold_rev (common_denominator Inttriplefunc.fold) mats @1
+ val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj) @1
+ val mats' = map (Inttriplefunc.map (fn _ => fn x => cd1 * x)) mats
val obj' = vector_cmul cd2 obj
- val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' (rat_0)
- val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') (rat_0)
- val scal1 = pow2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
- val scal2 = pow2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0))
- val mats'' = map (Inttriplefunc.map (fn _ => fn x => x */ scal1)) mats'
+ val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' @0
+ val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') @0
+ val scal1 = rat_pow @2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
+ val scal2 = rat_pow @2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0))
+ val mats'' = map (Inttriplefunc.map (fn _ => fn x => x * scal1)) mats'
val obj'' = vector_cmul scal2 obj'
in solver obj'' mats'' end
end;
(* Round a vector to "nice" rationals. *)
-fun nice_rational n x = round_rat (n */ x) // n;
+fun nice_rational n x = round_rat (n * x) / n;
fun nice_vector n ((d,v) : vector) =
(d, FuncUtil.Intfunc.fold (fn (i,c) => fn a =>
let val y = nice_rational n c in
- if c =/ rat_0 then a
+ if c = @0 then a
else FuncUtil.Intfunc.update (i,y) a
end) v FuncUtil.Intfunc.empty): vector
@@ -400,16 +392,16 @@
(* Stuff for "equations" ((int*int*int)->num functions). *)
fun tri_equation_cmul c eq =
- if c =/ rat_0 then Inttriplefunc.empty
- else Inttriplefunc.map (fn _ => fn d => c */ d) eq;
+ if c = @0 then Inttriplefunc.empty
+ else Inttriplefunc.map (fn _ => fn d => c * d) eq;
fun tri_equation_add eq1 eq2 =
- Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0) eq1 eq2;
+ Inttriplefunc.combine (curry op +) (fn x => x = @0) eq1 eq2;
fun tri_equation_eval assig eq =
let
fun value v = Inttriplefunc.apply assig v
- in Inttriplefunc.fold (fn (v, c) => fn a => a +/ value v */ c) eq rat_0 end;
+ in Inttriplefunc.fold (fn (v, c) => fn a => a + value v * c) eq @0 end;
(* Eliminate all variables, in an essentially arbitrary order. *)
@@ -438,11 +430,11 @@
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
- else tri_equation_add e (tri_equation_cmul (Rat.neg b // a) eq)
+ let val b = Inttriplefunc.tryapplyd e v @0 in
+ if b = @0 then e
+ else tri_equation_add e (tri_equation_cmul (~ b / a) eq)
end
in
eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map (K elim) dun))
@@ -485,10 +477,10 @@
if FuncUtil.Intpairfunc.is_empty (snd m) then []
else
let
- val a11 = FuncUtil.Intpairfunc.tryapplyd (snd m) (i,i) rat_0
+ val a11 = FuncUtil.Intpairfunc.tryapplyd (snd m) (i,i) @0
in
- if a11 </ rat_0 then raise Failure "diagonalize: not PSD"
- else if a11 =/ rat_0 then
+ if a11 < @0 then raise Failure "diagonalize: not PSD"
+ else if a11 = @0 then
if FuncUtil.Intfunc.is_empty (snd (row i m))
then diagonalize n (i + 1) m
else raise Failure "diagonalize: not PSD ___ "
@@ -497,20 +489,20 @@
val v = row i m
val v' =
(fst v, FuncUtil.Intfunc.fold (fn (i, c) => fn a =>
- let val y = c // a11
- in if y = rat_0 then a else FuncUtil.Intfunc.update (i,y) a
+ let val y = c / a11
+ in if y = @0 then a else FuncUtil.Intfunc.update (i,y) a
end) (snd v) FuncUtil.Intfunc.empty)
fun upt0 x y a =
- if y = rat_0 then a
+ if y = @0 then a
else FuncUtil.Intpairfunc.update (x,y) a
val m' =
((n, n),
iter (i + 1, n) (fn j =>
iter (i + 1, n) (fn k =>
(upt0 (j, k)
- (FuncUtil.Intpairfunc.tryapplyd (snd m) (j, k) rat_0 -/
- FuncUtil.Intfunc.tryapplyd (snd v) j rat_0 */
- FuncUtil.Intfunc.tryapplyd (snd v') k rat_0))))
+ (FuncUtil.Intpairfunc.tryapplyd (snd m) (j, k) @0 -
+ FuncUtil.Intfunc.tryapplyd (snd v) j @0 *
+ FuncUtil.Intfunc.tryapplyd (snd v') k @0))))
FuncUtil.Intpairfunc.empty)
in (a11, v') :: diagonalize n (i + 1) m' end
end
@@ -545,11 +537,11 @@
(* Give the output polynomial and a record of how it was derived. *)
fun enumerate_products d pols =
- if d = 0 then [(poly_const rat_1,RealArith.Rational_lt rat_1)]
+ if d = 0 then [(poly_const @1, RealArith.Rational_lt @1)]
else if d < 0 then []
else
(case pols of
- [] => [(poly_const rat_1, RealArith.Rational_lt rat_1)]
+ [] => [(poly_const @1, RealArith.Rational_lt @1)]
| (p, b) :: ps =>
let val e = multidegree p in
if e = 0 then enumerate_products d ps
@@ -563,7 +555,7 @@
fun epoly_of_poly p =
FuncUtil.Monomialfunc.fold (fn (m, c) => fn a =>
- FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((0, 0, 0), Rat.neg c)) a)
+ FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((0, 0, 0), ~ c)) a)
p FuncUtil.Monomialfunc.empty;
(* String for block diagonal matrix numbered k. *)
@@ -603,12 +595,12 @@
(* 3D versions of matrix operations to consider blocks separately. *)
-val bmatrix_add = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0);
+val bmatrix_add = Inttriplefunc.combine (curry op +) (fn x => x = @0);
fun bmatrix_cmul c bm =
- if c =/ rat_0 then Inttriplefunc.empty
- else Inttriplefunc.map (fn _ => fn x => c */ x) bm;
+ if c = @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. *)
@@ -641,7 +633,7 @@
(pol :: eqs @ map fst leqs) []
val monoid =
if linf then
- (poly_const rat_1,RealArith.Rational_lt rat_1)::
+ (poly_const @1, RealArith.Rational_lt @1)::
(filter (fn (p,_) => multidegree p <= d) leqs)
else enumerate_products d leqs
val nblocks = length monoid
@@ -653,7 +645,7 @@
in
(mons,
fold_rev (fn (m, n) =>
- FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((~k, ~n, n), rat_1)))
+ FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((~k, ~n, n), @1)))
nons FuncUtil.Monomialfunc.empty)
end
@@ -670,7 +662,7 @@
if n1 > n2 then a
else
let
- val c = if n1 = n2 then rat_1 else rat_2
+ val c = if n1 = n2 then @1 else @2
val e = FuncUtil.Monomialfunc.tryapplyd a m Inttriplefunc.empty
in
FuncUtil.Monomialfunc.update
@@ -690,13 +682,13 @@
val (pvs, assig) = tri_eliminate_all_equations (0, 0, 0) eqns
val qvars = (0, 0, 0) :: pvs
val allassig =
- fold_rev (fn v => Inttriplefunc.update (v, (Inttriplefunc.onefunc (v, rat_1)))) pvs assig
+ fold_rev (fn v => Inttriplefunc.update (v, (Inttriplefunc.onefunc (v, @1)))) pvs assig
fun mk_matrix v =
Inttriplefunc.fold (fn ((b, i, j), ass) => fn m =>
if b < 0 then m
else
- let val c = Inttriplefunc.tryapplyd ass v rat_0 in
- if c = rat_0 then m
+ let val c = Inttriplefunc.tryapplyd ass v @0 in
+ if c = @0 then m
else Inttriplefunc.update ((b, j, i), c) (Inttriplefunc.update ((b, i, j), c) m)
end)
allassig Inttriplefunc.empty
@@ -709,12 +701,12 @@
val obj =
(length pvs,
itern 1 pvs (fn v => fn i =>
- FuncUtil.Intfunc.updatep iszero (i,Inttriplefunc.tryapplyd diagents v rat_0))
+ FuncUtil.Intfunc.updatep iszero (i,Inttriplefunc.tryapplyd diagents v @0))
FuncUtil.Intfunc.empty)
val raw_vec =
if null pvs then vector_0 0
else tri_scale_then (run_blockproblem prover nblocks blocksizes) obj mats
- fun int_element (_, v) i = FuncUtil.Intfunc.tryapplyd v i rat_0
+ fun int_element (_, v) i = FuncUtil.Intfunc.tryapplyd v i @0
fun find_rounding d =
let
@@ -728,11 +720,11 @@
val allmats = blocks blocksizes blockmat
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))
+ if null pvs then find_rounding @1
+ else tryfind find_rounding (map Rat.of_int (1 upto 31) @ map (rat_pow @2) (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
@@ -803,13 +795,13 @@
fun trivial_axiom (p, ax) =
(case ax of
RealArith.Axiom_eq n =>
- if eval FuncUtil.Ctermfunc.empty p <>/ Rat.zero then nth eqs n
+ if eval FuncUtil.Ctermfunc.empty p <> @0 then nth eqs n
else raise Failure "trivial_axiom: Not a trivial axiom"
| RealArith.Axiom_le n =>
- if eval FuncUtil.Ctermfunc.empty p </ Rat.zero then nth les n
+ if eval FuncUtil.Ctermfunc.empty p < @0 then nth les n
else raise Failure "trivial_axiom: Not a trivial axiom"
| RealArith.Axiom_lt n =>
- if eval FuncUtil.Ctermfunc.empty p <=/ Rat.zero then nth lts n
+ if eval FuncUtil.Ctermfunc.empty p <= @0 then nth lts n
else raise Failure "trivial_axiom: Not a trivial axiom"
| _ => error "trivial_axiom: Not a trivial axiom")
in
@@ -834,7 +826,7 @@
| Prover prover =>
(* call prover *)
let
- val pol = fold_rev poly_mul (map fst ltp) (poly_const Rat.one)
+ val pol = fold_rev poly_mul (map fst ltp) (poly_const @1)
val leq = lep @ ltp
fun tryall d =
let
@@ -852,11 +844,11 @@
map2 (fn q => fn (_,ax) => RealArith.Eqmul(q,ax)) cert_ideal eq
val proofs_cone = map cterm_of_sos cert_cone
val proof_ne =
- if null ltp then RealArith.Rational_lt Rat.one
+ if null ltp then RealArith.Rational_lt @1
else
let val p = foldr1 RealArith.Product (map snd ltp) in
funpow i (fn q => RealArith.Product (p, q))
- (RealArith.Rational_lt Rat.one)
+ (RealArith.Rational_lt @1)
end
in
foldr1 RealArith.Sum (proof_ne :: proofs_ideal @ proofs_cone)
@@ -892,7 +884,7 @@
fun substitutable_monomial fvs tm =
(case Thm.term_of tm of
Free (_, @{typ real}) =>
- if not (member (op aconvc) fvs tm) then (Rat.one, tm)
+ if not (member (op aconvc) fvs tm) then (@1, tm)
else raise Failure "substitutable_monomial"
| @{term "op * :: real => _"} $ _ $ (Free _) =>
if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso
--- a/src/HOL/Library/positivstellensatz.ML Wed Jun 01 15:43:15 2016 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Wed Jun 01 19:54:31 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
(*
@@ -338,7 +338,7 @@
fun cterm_of_cmonomial (m,c) =
if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
- else if c = Rat.one then cterm_of_monomial m
+ else if c = @1 then cterm_of_monomial m
else Thm.apply (Thm.apply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
fun cterm_of_poly p =
@@ -585,51 +585,51 @@
(* A linear arithmetic prover *)
local
- val linear_add = FuncUtil.Ctermfunc.combine (curry op +/) (fn z => z =/ Rat.zero)
- fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c */ x)
+ val linear_add = FuncUtil.Ctermfunc.combine (curry op +) (fn z => z = @0)
+ fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c * x)
val one_tm = @{cterm "1::real"}
- fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
+ fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p @0)) orelse
((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
not(p(FuncUtil.Ctermfunc.apply e one_tm)))
fun linear_ineqs vars (les,lts) =
- case find_first (contradictory (fn x => x >/ Rat.zero)) lts of
+ case find_first (contradictory (fn x => x > @0)) lts of
SOME r => r
| NONE =>
- (case find_first (contradictory (fn x => x >/ Rat.zero)) les of
+ (case find_first (contradictory (fn x => x > @0)) les of
SOME r => r
| NONE =>
if null vars then error "linear_ineqs: no contradiction" else
let
val ineqs = les @ lts
fun blowup v =
- length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) ineqs) +
- length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) ineqs) *
- length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero </ Rat.zero) ineqs)
+ length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 = @0) ineqs) +
+ length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 > @0) ineqs) *
+ length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 < @0) ineqs)
val v = fst(hd(sort (fn ((_,i),(_,j)) => int_ord (i,j))
(map (fn v => (v,blowup v)) vars)))
fun addup (e1,p1) (e2,p2) acc =
let
- val c1 = FuncUtil.Ctermfunc.tryapplyd e1 v Rat.zero
- val c2 = FuncUtil.Ctermfunc.tryapplyd e2 v Rat.zero
+ val c1 = FuncUtil.Ctermfunc.tryapplyd e1 v @0
+ val c2 = FuncUtil.Ctermfunc.tryapplyd e2 v @0
in
- if c1 */ c2 >=/ Rat.zero then acc else
+ if c1 * c2 >= @0 then acc else
let
- val e1' = linear_cmul (Rat.abs c2) e1
- val e2' = linear_cmul (Rat.abs c1) e2
- val p1' = Product(Rational_lt(Rat.abs c2),p1)
- val p2' = Product(Rational_lt(Rat.abs c1),p2)
+ val e1' = linear_cmul (abs c2) e1
+ val e2' = linear_cmul (abs c1) e2
+ val p1' = Product(Rational_lt (abs c2), p1)
+ val p2' = Product(Rational_lt (abs c1), p2)
in (linear_add e1' e2',Sum(p1',p2'))::acc
end
end
val (les0,les1) =
- List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) les
+ List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 = @0) les
val (lts0,lts1) =
- List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) lts
+ List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 = @0) lts
val (lesp,lesn) =
- List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) les1
+ List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 > @0) les1
val (ltsp,ltsn) =
- List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) lts1
+ List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 > @0) lts1
val les' = fold_rev (fn ep1 => fold_rev (addup ep1) lesp) lesn les0
val lts' = fold_rev (fn ep1 => fold_rev (addup ep1) (lesp@ltsp)) ltsn
(fold_rev (fn ep1 => fold_rev (addup ep1) (lesn@ltsn)) ltsp lts0)
@@ -637,7 +637,7 @@
end)
fun linear_eqs(eqs,les,lts) =
- case find_first (contradictory (fn x => x =/ Rat.zero)) eqs of
+ case find_first (contradictory (fn x => x = @0)) eqs of
SOME r => r
| NONE =>
(case eqs of
@@ -650,14 +650,14 @@
let
val (x,c) = FuncUtil.Ctermfunc.choose (FuncUtil.Ctermfunc.delete_safe one_tm e)
fun xform (inp as (t,q)) =
- let val d = FuncUtil.Ctermfunc.tryapplyd t x Rat.zero in
- if d =/ Rat.zero then inp else
+ let val d = FuncUtil.Ctermfunc.tryapplyd t x @0 in
+ if d = @0 then inp else
let
- val k = (Rat.neg d) */ Rat.abs c // c
+ val k = ~ d * abs c / c
val e' = linear_cmul k e
- val t' = linear_cmul (Rat.abs c) t
+ val t' = linear_cmul (abs c) t
val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p)
- val q' = Product(Rational_lt(Rat.abs c),q)
+ val q' = Product(Rational_lt (abs c), q)
in (linear_add e' t',Sum(p',q'))
end
end
@@ -674,12 +674,12 @@
fun lin_of_hol ct =
if ct aconvc @{cterm "0::real"} then FuncUtil.Ctermfunc.empty
- else if not (is_comb ct) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
+ else if not (is_comb ct) then FuncUtil.Ctermfunc.onefunc (ct, @1)
else if is_ratconst ct then FuncUtil.Ctermfunc.onefunc (one_tm, dest_ratconst ct)
else
let val (lop,r) = Thm.dest_comb ct
in
- if not (is_comb lop) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
+ if not (is_comb lop) then FuncUtil.Ctermfunc.onefunc (ct, @1)
else
let val (opr,l) = Thm.dest_comb lop
in
@@ -687,7 +687,7 @@
then linear_add (lin_of_hol l) (lin_of_hol r)
else if opr aconvc @{cterm "op * :: real =>_"}
andalso is_ratconst l then FuncUtil.Ctermfunc.onefunc (r, dest_ratconst l)
- else FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
+ else FuncUtil.Ctermfunc.onefunc (ct, @1)
end
end
@@ -707,7 +707,7 @@
val aliens = filter is_alien
(fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom)
(eq_pols @ le_pols @ lt_pols) [])
- val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
+ val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,@1)) aliens
val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
val le' = le @ map (fn a => Thm.instantiate' [] [SOME (Thm.dest_arg a)] @{thm of_nat_0_le_iff}) aliens
in ((translator (eq,le',lt) proof), Trivial)
--- a/src/HOL/Multivariate_Analysis/normarith.ML Wed Jun 01 15:43:15 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Wed Jun 01 19:54:31 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
@@ -28,23 +28,23 @@
find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc)
| @{term "op * :: real => _"}$_$_ =>
if not (is_ratconst (Thm.dest_arg1 t)) then acc else
- augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero)
+ augment_norm (dest_ratconst (Thm.dest_arg1 t) >= @0)
(Thm.dest_arg t) acc
| _ => augment_norm true t acc
- val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K Rat.neg)
+ val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K ~)
fun cterm_lincomb_cmul c t =
- if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x */ c) t
- fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
+ if c = @0 then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x * c) t
+ fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +) (fn x => x = @0) l r
fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r)
fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
(*
- val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg)
+ val int_lincomb_neg = FuncUtil.Intfunc.map (K ~)
*)
fun int_lincomb_cmul c t =
- if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x */ c) t
- fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
+ if c = @0 then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x * c) t
+ fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +) (fn x => x = @0) l r
(*
fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r)
fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)
@@ -64,11 +64,11 @@
let
val b = ((snd o HOLogic.dest_number o term_of o Thm.dest_arg) t = 0
handle TERM _=> false)
- in if b then FuncUtil.Ctermfunc.onefunc (t,Rat.one)
+ in if b then FuncUtil.Ctermfunc.onefunc (t,@1)
else FuncUtil.Ctermfunc.empty
end
*)
- | _ => FuncUtil.Ctermfunc.onefunc (t,Rat.one)
+ | _ => FuncUtil.Ctermfunc.onefunc (t,@1)
fun vector_lincombs ts =
fold_rev
@@ -84,23 +84,23 @@
fun replacenegnorms cv t = case Thm.term_of t of
@{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
| @{term "op * :: real => _"}$_$_ =>
- if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else Thm.reflexive t
+ if dest_ratconst (Thm.dest_arg1 t) < @0 then arg_conv cv t else Thm.reflexive t
| _ => Thm.reflexive t
(*
fun flip v eq =
if FuncUtil.Ctermfunc.defined eq v
- then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq
+ then FuncUtil.Ctermfunc.update (v, ~ (FuncUtil.Ctermfunc.apply eq v)) eq else eq
*)
fun allsubsets s = case s of
[] => [[]]
|(a::t) => let val res = allsubsets t in
map (cons a) res @ res end
fun evaluate env lin =
- FuncUtil.Intfunc.fold (fn (x,c) => fn s => s +/ c */ (FuncUtil.Intfunc.apply env x))
- lin Rat.zero
+ FuncUtil.Intfunc.fold (fn (x,c) => fn s => s + c * (FuncUtil.Intfunc.apply env x))
+ lin @0
fun solve (vs,eqs) = case (vs,eqs) of
- ([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,Rat.one))
+ ([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,@1))
|(_,eq::oeqs) =>
(case filter (member (op =) vs) (FuncUtil.Intfunc.dom eq) of (*FIXME use find_first here*)
[] => NONE
@@ -109,7 +109,7 @@
then
let
val c = FuncUtil.Intfunc.apply eq v
- val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq
+ val vdef = int_lincomb_cmul (~ (Rat.inv c)) eq
fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn
else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn
in (case solve (remove (op =) v vs, map eliminate oeqs) of
@@ -127,13 +127,13 @@
let
fun vertex cmb = case solve(vs,cmb) of
NONE => NONE
- | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs)
+ | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v @0) vs)
val rawvs = map_filter vertex (combinations (length vs) eqs)
- val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs
- in fold_rev (insert (eq_list op =/)) unset []
+ val unset = filter (forall (fn c => c >= @0)) rawvs
+ in fold_rev (insert (eq_list op =)) unset []
end
-val subsumes = eq_list (fn (x, y) => Rat.abs x <=/ Rat.abs y)
+val subsumes = eq_list (fn (x, y) => Rat.abs x <= Rat.abs y)
fun subsume todo dun = case todo of
[] => dun
@@ -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 => _"}
@@ -242,7 +242,7 @@
(* FIXME
| Const(@{const_name vec},_)$n =>
let val n = Thm.dest_arg ct
- in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero)
+ in if is_ratconst n andalso not (dest_ratconst n =/ @0)
then Thm.reflexive ct else apply_pth1 ct
end
*)
@@ -254,7 +254,7 @@
fun int_flip v eq =
if FuncUtil.Intfunc.defined eq v
- then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq;
+ then FuncUtil.Intfunc.update (v, ~ (FuncUtil.Intfunc.apply eq v)) eq else eq;
local
val pth_zero = @{thm norm_zero}
@@ -283,12 +283,14 @@
let
fun coefficients x =
let
- val inp = if FuncUtil.Ctermfunc.defined d x then FuncUtil.Intfunc.onefunc (0, Rat.neg(FuncUtil.Ctermfunc.apply d x))
- else FuncUtil.Intfunc.empty
+ val inp =
+ if FuncUtil.Ctermfunc.defined d x
+ then FuncUtil.Intfunc.onefunc (0, ~ (FuncUtil.Ctermfunc.apply d x))
+ else FuncUtil.Intfunc.empty
in fold_rev (fn (f,v) => fn g => if FuncUtil.Ctermfunc.defined f x then FuncUtil.Intfunc.update (v, FuncUtil.Ctermfunc.apply f x) g else g) srccombs inp
end
val equations = map coefficients vvs
- val inequalities = map (fn n => FuncUtil.Intfunc.onefunc (n,Rat.one)) nvs
+ val inequalities = map (fn n => FuncUtil.Intfunc.onefunc (n,@1)) nvs
fun plausiblevertices f =
let
val flippedequations = map (fold_rev int_flip f) equations
@@ -296,19 +298,19 @@
val rawverts = vertices nvs constraints
fun check_solution v =
let
- val f = fold_rev FuncUtil.Intfunc.update (nvs ~~ v) (FuncUtil.Intfunc.onefunc (0, Rat.one))
- in forall (fn e => evaluate f e =/ Rat.zero) flippedequations
+ val f = fold_rev FuncUtil.Intfunc.update (nvs ~~ v) (FuncUtil.Intfunc.onefunc (0, @1))
+ in forall (fn e => evaluate f e = @0) flippedequations
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 []
end
fun compute_ineq v =
let
- val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE
+ val ths = map_filter (fn (v,t) => if v = @0 then NONE
else SOME(norm_cmul_rule v t))
(v ~~ nubs)
fun end_itlist f xs = split_last xs |> uncurry (fold_rev f)
--- a/src/HOL/Nat.thy Wed Jun 01 15:43:15 2016 +0200
+++ b/src/HOL/Nat.thy Wed Jun 01 19:54:31 2016 +0200
@@ -11,8 +11,6 @@
imports Inductive Typedef Fun Rings
begin
-ML_file "~~/src/Tools/rat.ML"
-
named_theorems arith "arith facts -- only ground formulas"
ML_file "Tools/arith_data.ML"
--- a/src/HOL/Tools/groebner.ML Wed Jun 01 15:43:15 2016 +0200
+++ b/src/HOL/Tools/groebner.ML Wed Jun 01 19:54:31 2016 +0200
@@ -32,13 +32,10 @@
if is_binop ct ct' then Thm.dest_binop ct'
else raise CTERM ("dest_binary: bad binop", [ct, ct'])
-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}
@@ -72,7 +69,7 @@
(* Arithmetic on canonical polynomials. *)
-fun grob_neg l = map (fn (c,m) => (minus_rat c,m)) l;
+fun grob_neg l = map (fn (c,m) => (Rat.neg c,m)) l;
fun grob_add l1 l2 =
case (l1,l2) of
@@ -80,14 +77,14 @@
| (l1,[]) => l1
| ((c1,m1)::o1,(c2,m2)::o2) =>
if m1 = m2 then
- let val c = c1+/c2 val rest = grob_add o1 o2 in
- if c =/ rat_0 then rest else (c,m1)::rest end
+ let val c = c1 + c2 val rest = grob_add o1 o2 in
+ if c = @0 then rest else (c,m1)::rest end
else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2)
else (c2,m2)::(grob_add l1 o2);
fun grob_sub l1 l2 = grob_add l1 (grob_neg l2);
-fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2, ListPair.map (op +) (m1, m2));
+fun grob_mmul (c1,m1) (c2,m2) = (c1 * c2, ListPair.map (op +) (m1, m2));
fun grob_cmul cm pol = map (grob_mmul cm) pol;
@@ -99,33 +96,33 @@
fun grob_inv l =
case l of
[(c,vs)] => if (forall (fn x => x = 0) vs) then
- if (c =/ rat_0) then error "grob_inv: division by zero"
- else [(rat_1 // c,vs)]
+ if c = @0 then error "grob_inv: division by zero"
+ else [(@1 / c,vs)]
else error "grob_inv: non-constant divisor polynomial"
| _ => error "grob_inv: non-constant divisor polynomial";
fun grob_div l1 l2 =
case l2 of
[(c,l)] => if (forall (fn x => x = 0) l) then
- if c =/ rat_0 then error "grob_div: division by zero"
- else grob_cmul (rat_1 // c,l) l1
+ if c = @0 then error "grob_div: division by zero"
+ else grob_cmul (@1 / c,l) l1
else error "grob_div: non-constant divisor polynomial"
| _ => error "grob_div: non-constant divisor polynomial";
fun grob_pow vars l n =
if n < 0 then error "grob_pow: negative power"
- else if n = 0 then [(rat_1,map (K 0) vars)]
+ else if n = 0 then [(@1,map (K 0) vars)]
else grob_mul l (grob_pow vars l (n - 1));
(* Monomial division operation. *)
fun mdiv (c1,m1) (c2,m2) =
- (c1//c2,
+ (c1 / c2,
map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 - n2) m1 m2);
(* Lowest common multiple of two monomials. *)
-fun mlcm (_,m1) (_,m2) = (rat_1, ListPair.map Int.max (m1, m2));
+fun mlcm (_,m1) (_,m2) = (@1, ListPair.map Int.max (m1, m2));
(* Reduce monomial cm by polynomial pol, returning replacement for cm. *)
@@ -133,8 +130,8 @@
case pol of
[] => error "reduce1"
| cm1::cms => ((let val (c,m) = mdiv cm cm1 in
- (grob_cmul (minus_rat c,m) cms,
- Mmul((minus_rat c,m),hpol)) end)
+ (grob_cmul (~ c, m) cms,
+ Mmul ((~ c,m),hpol)) end)
handle ERROR _ => error "reduce1");
(* Try this for all polynomials in a basis. *)
@@ -171,15 +168,15 @@
(grob_sub (grob_cmul (mdiv cm cm1) ptl1)
(grob_cmul (mdiv cm cm2) ptl2),
Add(Mmul(mdiv cm cm1,his1),
- Mmul(mdiv (minus_rat(fst cm),snd cm) cm2,his2)));
+ Mmul(mdiv (~ (fst cm),snd cm) cm2,his2)));
(* Make a polynomial monic. *)
fun monic (pol,hist) =
if null pol then (pol,hist) else
let val (c',m') = hd pol in
- (map (fn (c,m) => (c//c',m)) pol,
- Mmul((rat_1 // c',map (K 0) m'),hist)) end;
+ (map (fn (c,m) => (c / c',m)) pol,
+ Mmul((@1 / c',map (K 0) m'),hist)) end;
(* The most popular heuristic is to order critical pairs by LCM monomial. *)
@@ -190,14 +187,14 @@
(_,[]) => false
| ([],_) => true
| ((c1,m1)::o1,(c2,m2)::o2) =>
- c1 </ c2 orelse
- c1 =/ c2 andalso ((morder_lt m1 m2) orelse m1 = m2 andalso poly_lt o1 o2);
+ c1 < c2 orelse
+ c1 = c2 andalso ((morder_lt m1 m2) orelse m1 = m2 andalso poly_lt o1 o2);
fun align ((p,hp),(q,hq)) =
if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp));
fun poly_eq p1 p2 =
- eq_list (fn ((c1, m1), (c2, m2)) => c1 =/ c2 andalso (m1: int list) = m2) (p1, p2);
+ eq_list (fn ((c1, m1), (c2, m2)) => c1 = c2 andalso (m1: int list) = m2) (p1, p2);
fun memx ((p1,_),(p2,_)) ppairs =
not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
@@ -299,7 +296,7 @@
fun resolve_proof vars prf =
case prf of
Start(~1) => []
- | Start m => [(m,[(rat_1,map (K 0) vars)])]
+ | Start m => [(m,[(@1,map (K 0) vars)])]
| Mmul(pol,lin) =>
let val lis = resolve_proof vars lin in
map (fn (n,p) => (n,grob_cmul pol p)) lis end
@@ -317,8 +314,8 @@
fun grobner_weak vars pols =
let val cert = resolve_proof vars (grobner_refute pols)
val l =
- fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert (rat_1) in
- (l,map (fn (i,p) => (i,map (fn (d,m) => (l*/d,m)) p)) cert) end;
+ fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert @1 in
+ (l,map (fn (i,p) => (i,map (fn (d,m) => (l * d,m)) p)) cert) end;
(* Prove a polynomial is in ideal generated by others, using Grobner basis. *)
@@ -331,8 +328,8 @@
fun grobner_strong vars pols pol =
let val vars' = @{cterm "True"}::vars
- val grob_z = [(rat_1,1::(map (K 0) vars))]
- val grob_1 = [(rat_1,(map (K 0) vars'))]
+ val grob_z = [(@1, 1::(map (K 0) vars))]
+ val grob_1 = [(@1, (map (K 0) vars'))]
fun augment p= map (fn (c,m) => (c,0::m)) p
val pols' = map augment pols
val pol' = augment pol
@@ -605,10 +602,10 @@
fun grobify_term vars tm =
((if not (member (op aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else
- [(rat_1,map (fn i => if i aconvc tm then 1 else 0) vars)])
+ [(@1, map (fn i => if i aconvc tm then 1 else 0) vars)])
handle CTERM _ =>
((let val x = dest_const tm
- in if x =/ rat_0 then [] else [(x,map (K 0) vars)]
+ in if x = @0 then [] else [(x,map (K 0) vars)]
end)
handle ERROR _ =>
((grob_neg(grobify_term vars (ring_dest_neg tm)))
@@ -662,15 +659,15 @@
in end_itlist ring_mk_mul (mk_const c :: xps)
end
fun holify_polynomial vars p =
- if null p then mk_const (rat_0)
+ if null p then mk_const @0
else end_itlist ring_mk_add (map (holify_monomial vars) p)
in holify_polynomial
end ;
fun idom_rule ctxt = simplify (put_simpset HOL_basic_ss ctxt addsimps [idom_thm]);
fun prove_nz n = eqF_elim
- (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const(rat_0))));
-val neq_01 = prove_nz (rat_1);
+ (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const @0)));
+val neq_01 = prove_nz @1;
fun neq_rule n th = [prove_nz n, th] MRS neq_thm;
fun mk_add th1 = Thm.combination (Drule.arg_cong_rule ring_add_tm th1);
@@ -712,13 +709,13 @@
val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr ctxt th1) neq_01
in (vars,l,cert,th2)
end)
- val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c >/ rat_0) p)) cert
- val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
- (filter (fn (c,_) => c </ rat_0) p))) cert
+ val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > @0) p)) cert
+ val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (~ c,m))
+ (filter (fn (c,_) => c < @0) p))) cert
val herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
val herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg
fun thm_fn pols =
- if null pols then Thm.reflexive(mk_const rat_0) else
+ if null pols then Thm.reflexive(mk_const @0) else
end_itlist mk_add
(map (fn (i,p) => Drule.arg_cong_rule (Thm.apply ring_mul_tm p)
(nth eths i |> mk_meta_eq)) pols)
--- a/src/HOL/Tools/lin_arith.ML Wed Jun 01 15:43:15 2016 +0200
+++ b/src/HOL/Tools/lin_arith.ML Wed Jun 01 19:54:31 2016 +0200
@@ -156,11 +156,11 @@
if we choose to do so here, the simpset used by arith must be able to
perform the same simplifications. *)
(* quotient 's / t', where the denominator t can be NONE *)
- (* Note: will raise Rat.DIVZERO iff m' is Rat.zero *)
+ (* Note: will raise Div iff m' is @0 *)
if of_field_sort thy (domain_type T) then
let
val (os',m') = demult (s, m);
- val (ot',p) = demult (t, Rat.one)
+ val (ot',p) = demult (t, @1)
in (case (os',ot') of
(SOME s', SOME t') => SOME (mC $ s' $ t')
| (SOME s', NONE) => SOME s'
@@ -171,18 +171,18 @@
end
else (SOME atom, m)
(* terms that evaluate to numeric constants *)
- | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m)
- | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, Rat.zero)
+ | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, ~ m)
+ | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, @0)
| demult (Const (@{const_name Groups.one}, _), m) = (NONE, m)
(*Warning: in rare cases (neg_)numeral encloses a non-numeral,
in which case dest_numeral raises TERM; hence all the handles below.
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) =
@@ -200,16 +200,16 @@
fun poly (Const (@{const_name Groups.plus}, _) $ s $ t,
m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi))
| poly (all as Const (@{const_name Groups.minus}, T) $ s $ t, m, pi) =
- if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi))
+ if nT T then add_atom all m pi else poly (s, m, poly (t, ~ m, pi))
| poly (all as Const (@{const_name Groups.uminus}, T) $ t, m, pi) =
- if nT T then add_atom all m pi else poly (t, Rat.neg m, pi)
+ if nT T then add_atom all m pi else poly (t, ~ m, pi)
| poly (Const (@{const_name Groups.zero}, _), _, pi) =
pi
| poly (Const (@{const_name Groups.one}, _), m, (p, i)) =
(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))
@@ -227,15 +227,15 @@
if member (op =) inj_consts f then poly (x, m, pi) else add_atom all m pi
| poly (all, m, pi) =
add_atom all m pi
- val (p, i) = poly (lhs, Rat.one, ([], Rat.zero))
- val (q, j) = poly (rhs, Rat.one, ([], Rat.zero))
+ val (p, i) = poly (lhs, @1, ([], @0))
+ val (q, j) = poly (rhs, @1, ([], @0))
in
case rel of
@{const_name Orderings.less} => SOME (p, i, "<", q, j)
| @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
| @{const_name HOL.eq} => SOME (p, i, "=", q, j)
| _ => NONE
-end handle Rat.DIVZERO => NONE;
+end handle General.Div => NONE;
fun of_lin_arith_sort thy U =
Sign.of_sort thy (U, @{sort Rings.linordered_idom});
--- a/src/HOL/Tools/semiring_normalizer.ML Wed Jun 01 15:43:15 2016 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Wed Jun 01 19:54:31 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 Wed Jun 01 15:43:15 2016 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Jun 01 19:54:31 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/rat.ML Wed Jun 01 19:54:31 2016 +0200
@@ -0,0 +1,107 @@
+(* Title: Pure/General/rat.ML
+ Author: Tobias Nipkow, Florian Haftmann, TU Muenchen
+ Author: Makarius
+
+Canonical implementation of exact rational numbers.
+*)
+
+signature RAT =
+sig
+ eqtype rat
+ val of_int: int -> rat
+ val make: int * int -> rat
+ val dest: rat -> int * int
+ val string_of_rat: rat -> string
+ val signed_string_of_rat: rat -> string
+ val ord: rat * rat -> order
+ val le: rat -> rat -> bool
+ val lt: rat -> rat -> bool
+ val sign: rat -> order
+ val abs: rat -> rat
+ val add: rat -> rat -> rat
+ val mult: rat -> rat -> rat
+ val neg: rat -> rat
+ val inv: rat -> rat
+ val floor: rat -> int
+ val ceil: rat -> int
+end;
+
+structure Rat : RAT =
+struct
+
+datatype rat = Rat of int * int; (*numerator, positive (!) denominator*)
+
+fun common (p1, q1) (p2, q2) =
+ let val m = PolyML.IntInf.lcm (q1, q2)
+ in ((p1 * (m div q1), p2 * (m div q2)), m) end;
+
+fun make (_, 0) = raise Div
+ | make (p, q) =
+ let
+ val m = PolyML.IntInf.gcd (p, q);
+ val (p', q') = (p div m, q div m);
+ in Rat (if q' < 0 then (~ p', ~ q') else (p', q')) end
+
+fun dest (Rat r) = r;
+
+fun of_int i = Rat (i, 1);
+
+fun string_of_rat (Rat (p, 1)) = string_of_int p
+ | string_of_rat (Rat (p, q)) = string_of_int p ^ "/" ^ string_of_int q;
+
+fun signed_string_of_rat (Rat (p, 1)) = signed_string_of_int p
+ | signed_string_of_rat (Rat (p, q)) = signed_string_of_int p ^ "/" ^ string_of_int q;
+
+fun ord (Rat (p1, q1), Rat (p2, q2)) =
+ (case (Integer.sign p1, Integer.sign p2) of
+ (LESS, EQUAL) => LESS
+ | (LESS, GREATER) => LESS
+ | (EQUAL, LESS) => GREATER
+ | (EQUAL, EQUAL) => EQUAL
+ | (EQUAL, GREATER) => LESS
+ | (GREATER, LESS) => GREATER
+ | (GREATER, EQUAL) => GREATER
+ | _ => int_ord (fst (common (p1, q1) (p2, q2))));
+
+fun le a b = ord (a, b) <> GREATER;
+fun lt a b = ord (a, b) = LESS;
+
+fun sign (Rat (p, _)) = Integer.sign p;
+
+fun abs (r as Rat (p, q)) = if p < 0 then Rat (~ p, q) else r;
+
+fun add (Rat (p1, q1)) (Rat (p2, q2)) =
+ let val ((m1, m2), n) = common (p1, q1) (p2, q2)
+ in make (m1 + m2, n) end;
+
+fun mult (Rat (p1, q1)) (Rat (p2, q2)) = make (p1 * p2, q1 * q2);
+
+fun neg (Rat (p, q)) = Rat (~ p, q);
+
+fun inv (Rat (p, q)) =
+ (case Integer.sign p of
+ LESS => Rat (~ q, ~ p)
+ | EQUAL => raise Div
+ | GREATER => Rat (q, p));
+
+fun floor (Rat (p, q)) = p div q;
+
+fun ceil (Rat (p, q)) =
+ (case Integer.div_mod p q of
+ (m, 0) => m
+ | (m, _) => m);
+
+end;
+
+ML_system_overload (uncurry Rat.add) "+";
+ML_system_overload (fn (a, b) => Rat.add a (Rat.neg b)) "-";
+ML_system_overload (uncurry Rat.mult) "*";
+ML_system_overload (fn (a, b) => Rat.mult a (Rat.inv b)) "/";
+ML_system_overload (uncurry Rat.lt) "<";
+ML_system_overload (uncurry Rat.le) "<=";
+ML_system_overload (fn (a, b) => Rat.lt b a) ">";
+ML_system_overload (fn (a, b) => Rat.le b a) ">=";
+ML_system_overload Rat.neg "~";
+ML_system_overload Rat.abs "abs";
+
+ML_system_pp (fn _ => fn _ => fn x => Pretty.to_polyml (Pretty.str ("@" ^ Rat.string_of_rat x)));
--- a/src/Pure/ML/ml_antiquotations.ML Wed Jun 01 15:43:15 2016 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Wed Jun 01 19:54:31 2016 +0200
@@ -29,7 +29,12 @@
ML_Syntax.print_position pos ^ "));\n";
val body =
"(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))";
- in (K (env, body), ctxt') end));
+ in (K (env, body), ctxt') end) #>
+
+ ML_Antiquotation.value @{binding rat}
+ (Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat --
+ Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) =>
+ "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b))))
(* formal entities *)
--- a/src/Pure/ML/ml_lex.ML Wed Jun 01 15:43:15 2016 +0200
+++ b/src/Pure/ML/ml_lex.ML Wed Jun 01 19:54:31 2016 +0200
@@ -218,6 +218,8 @@
val scan_int = scan_sign @@@ ($$$ "0" @@@ $$$ "x" @@@ scan_hex || scan_dec);
+val scan_rat = scan_decint @@@ Scan.optional ($$$ "/" @@@ scan_dec) [];
+
val scan_real =
scan_decint @@@ $$$ "." @@@ scan_dec @@@ Scan.optional scan_exp [] ||
scan_decint @@@ scan_exp;
@@ -265,6 +267,19 @@
end;
+(* rat antiquotation *)
+
+val rat_name = Symbol_Pos.explode ("Pure.rat ", Position.none);
+
+val scan_rat_antiq =
+ Symbol_Pos.scan_pos -- ($$ "@" |-- Symbol_Pos.scan_pos -- scan_rat) -- Symbol_Pos.scan_pos
+ >> (fn ((pos1, (pos2, body)), pos3) =>
+ {start = Position.range_position (pos1, pos2),
+ stop = Position.none,
+ range = Position.range (pos1, pos3),
+ body = rat_name @ body});
+
+
(* scan tokens *)
local
@@ -290,6 +305,7 @@
val scan_ml_antiq =
Antiquote.scan_control >> Antiquote.Control ||
Antiquote.scan_antiq >> Antiquote.Antiq ||
+ scan_rat_antiq >> Antiquote.Antiq ||
scan_ml >> Antiquote.Text;
fun recover msg =
--- a/src/Pure/ML/ml_lex.scala Wed Jun 01 15:43:15 2016 +0200
+++ b/src/Pure/ML/ml_lex.scala Wed Jun 01 19:54:31 2016 +0200
@@ -190,6 +190,9 @@
sign ~ ("0x" ~ hex ^^ { case x ~ y => x + y } | dec) ^^
{ case x ~ y => Token(Kind.INT, x + y) }
+ val rat =
+ decint ~ opt("/" ~ dec) ^^ { case x ~ None => x case x ~ Some(y ~ z) => x + y + z }
+
val real =
(decint ~ "." ~ dec ~ (opt(exp) ^^ { case Some(x) => x case None => "" }) ^^
{ case x ~ y ~ z ~ w => x + y + z + w } |
@@ -203,7 +206,9 @@
val keyword = literal(lexicon) ^^ (x => Token(Kind.KEYWORD, x))
val ml_control = control ^^ (x => Token(Kind.CONTROL, x))
- val ml_antiq = antiq ^^ (x => Token(Kind.ANTIQ, x))
+ val ml_antiq =
+ "@" ~ rat ^^ { case x ~ y => Token(Kind.ANTIQ, x + y) } |
+ antiq ^^ (x => Token(Kind.ANTIQ, x))
val bad = one(_ => true) ^^ (x => Token(Kind.ERROR, x))
--- a/src/Pure/ROOT.ML Wed Jun 01 15:43:15 2016 +0200
+++ b/src/Pure/ROOT.ML Wed Jun 01 19:54:31 2016 +0200
@@ -61,6 +61,7 @@
ML_file "General/linear_set.ML";
ML_file "General/buffer.ML";
ML_file "General/pretty.ML";
+ML_file "General/rat.ML";
ML_file "PIDE/xml.ML";
ML_file "General/path.ML";
ML_file "General/url.ML";
--- a/src/Tools/rat.ML Wed Jun 01 15:43:15 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,118 +0,0 @@
-(* Title: Tools/rat.ML
- Author: Tobias Nipkow, Florian Haftmann, TU Muenchen
-
-Canonical implementation of exact rational numbers.
-*)
-
-signature RAT =
-sig
- eqtype rat
- exception DIVZERO
- 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 string_of_rat: rat -> string
- val eq: rat * rat -> bool
- val ord: rat * rat -> order
- val le: rat -> rat -> bool
- val lt: rat -> rat -> bool
- val sign: rat -> order
- val abs: rat -> rat
- val add: rat -> rat -> rat
- val mult: rat -> rat -> rat
- val neg: rat -> rat
- val inv: rat -> rat
- val rounddown: rat -> rat
- val roundup: rat -> rat
-end;
-
-structure Rat : RAT =
-struct
-
-fun common (p1, q1) (p2, q2) =
- let
- val m = Integer.lcm q1 q2;
- in ((p1 * (m div q1), p2 * (m div q2)), m) end;
-
-datatype rat = Rat of int * int; (*nominator, denominator (positive!)*)
-
-exception DIVZERO;
-
-fun rat_of_quotient (p, q) =
- let
- val m = Integer.gcd (Int.abs p) q
- in Rat (p div m, q div m) end handle Div => raise DIVZERO;
-
-fun quotient_of_rat (Rat r) = r;
-
-fun rat_of_int i = Rat (i, 1);
-
-val zero = rat_of_int 0;
-val one = rat_of_int 1;
-val two = rat_of_int 2;
-
-fun string_of_rat (Rat (p, q)) =
- string_of_int p ^ "/" ^ string_of_int q;
-
-fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2);
-
-fun ord (Rat (p1, q1), Rat (p2, q2)) =
- case (Integer.sign p1, Integer.sign p2)
- of (LESS, EQUAL) => LESS
- | (LESS, GREATER) => LESS
- | (EQUAL, LESS) => GREATER
- | (EQUAL, EQUAL) => EQUAL
- | (EQUAL, GREATER) => LESS
- | (GREATER, LESS) => GREATER
- | (GREATER, EQUAL) => GREATER
- | _ => int_ord (fst (common (p1, q1) (p2, q2)));
-
-fun le a b = not (ord (a, b) = GREATER);
-fun lt a b = (ord (a, b) = LESS);
-
-fun sign (Rat (p, _)) = Integer.sign p;
-
-fun abs (Rat (p, q)) = Rat (Int.abs p, q);
-
-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;
-
-fun mult (Rat (p1, q1)) (Rat (p2, q2)) =
- rat_of_quotient (p1 * p2, q1 * q2);
-
-fun neg (Rat (p, q)) = Rat (~ p, q);
-
-fun inv (Rat (p, q)) =
- case Integer.sign p
- of LESS => Rat (~ q, ~ p)
- | EQUAL => raise DIVZERO
- | GREATER => Rat (q, p);
-
-fun rounddown (Rat (p, q)) = Rat (p div q, 1);
-
-fun roundup (Rat (p, q)) =
- case Integer.div_mod p q
- of (m, 0) => Rat (m, 1)
- | (m, _) => Rat (m + 1, 1);
-
-end;
-
-infix 7 */ //;
-infix 6 +/ -/;
-infix 4 =/ </ <=/ >/ >=/ <>/;
-
-fun a +/ b = Rat.add a b;
-fun a -/ b = a +/ Rat.neg b;
-fun a */ b = Rat.mult a b;
-fun a // b = a */ Rat.inv b;
-fun a =/ b = Rat.eq (a, b);
-fun a </ b = Rat.lt a b;
-fun a <=/ b = Rat.le a b;
-fun a >/ b = b </ a;
-fun a >=/ b = b <=/ a;
-fun a <>/ b = not (a =/ b);