# HG changeset patch # User wenzelm # Date 1464803671 -7200 # Node ID 5c8b500347cd3847c85cc268762ebd4434d766ac # Parent 82552b478356e598d6b07669f45973a079694c97# Parent cc9c1f6a6b88cb91bf0cf38ba4897f7f063d085c merged diff -r 82552b478356 -r 5c8b500347cd NEWS --- 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. diff -r 82552b478356 -r 5c8b500347cd src/HOL/Decision_Procs/Dense_Linear_Order.thy --- 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 T --> @{typ bool})) val cz = Thm.dest_arg ct - val neg = cr T --> @{typ bool})) val cz = Thm.dest_arg ct - val neg = cr 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) >> diff -r 82552b478356 -r 5c8b500347cd src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- 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 = 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 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 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 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 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 - 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 diff -r 82552b478356 -r 5c8b500347cd src/HOL/Library/positivstellensatz.ML --- 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 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) diff -r 82552b478356 -r 5c8b500347cd src/HOL/Multivariate_Analysis/normarith.ML --- 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) 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) diff -r 82552b478356 -r 5c8b500347cd src/HOL/Nat.thy --- 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" diff -r 82552b478356 -r 5c8b500347cd src/HOL/Tools/groebner.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 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 (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) diff -r 82552b478356 -r 5c8b500347cd src/HOL/Tools/lin_arith.ML --- 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}); diff -r 82552b478356 -r 5c8b500347cd src/HOL/Tools/semiring_normalizer.ML --- 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) diff -r 82552b478356 -r 5c8b500347cd src/Provers/Arith/fast_lin_arith.ML --- 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 diff -r 82552b478356 -r 5c8b500347cd src/Pure/General/rat.ML --- /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))); diff -r 82552b478356 -r 5c8b500347cd src/Pure/ML/ml_antiquotations.ML --- 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 *) diff -r 82552b478356 -r 5c8b500347cd src/Pure/ML/ml_lex.ML --- 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 = diff -r 82552b478356 -r 5c8b500347cd src/Pure/ML/ml_lex.scala --- 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)) diff -r 82552b478356 -r 5c8b500347cd src/Pure/ROOT.ML --- 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"; diff -r 82552b478356 -r 5c8b500347cd src/Tools/rat.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 = b =/ b = b <=/ a; -fun a <>/ b = not (a =/ b);