--- a/NEWS Tue May 31 19:51:01 2016 +0200
+++ b/NEWS Tue May 31 21:54:10 2016 +0200
@@ -344,8 +344,12 @@
nn_integral :: 'a measure => ('a => ennreal) => ennreal
INCOMPATIBILITY.
+
*** ML ***
+* Ad-hoc overloading for standard operations on type Rat.rat: + - * / =
+< <= > >= <>. INCOMPATIBILITY, need to use + instead of +/ etc.
+
* 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 Tue May 31 19:51:01 2016 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue May 31 21:54:10 2016 +0200
@@ -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 < Rat.zero
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 < Rat.zero
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 < Rat.zero
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 < Rat.zero
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/sum_of_squares.ML Tue May 31 19:51:01 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Tue May 31 21:54:10 2016 +0200
@@ -39,7 +39,7 @@
let fun pow r i =
if i = 0 then rat_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 rat_1 else r)
end
in if i < 0 then pow (Rat.inv r) (~ i) else pow r i end;
@@ -47,7 +47,7 @@
let
val (a,b) = Rat.quotient_of_rat (Rat.abs r)
val d = a div b
- val s = if r </ rat_0 then (Rat.neg o Rat.rat_of_int) else Rat.rat_of_int
+ val s = if r < rat_0 then (Rat.neg o Rat.rat_of_int) else Rat.rat_of_int
val x2 = 2 * (a - (b * d))
in s (if x2 >= b then d + 1 else d) end
@@ -78,22 +78,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_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
else 0
in
fun decimalize d x =
- if x =/ rat_0 then "0.0"
+ if x = rat_0 then "0.0"
else
let
val y = Rat.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 = pow10(~ e) * y + rat_1
+ val k = int_of_rat (round_rat(pow10 d * z))
in
- (if x </ rat_0 then "-0." else "0.") ^
+ (if x < rat_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 +117,7 @@
type matrix = (int * int) * Rat.rat FuncUtil.Intpairfunc.table;
-fun iszero (_, r) = r =/ rat_0;
+fun iszero (_, r) = r = rat_0;
(* Vectors. Conventionally indexed 1..n. *)
@@ -128,8 +128,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 = rat_0 then vector_0 n
+ else (n,FuncUtil.Intfunc.map (fn _ => fn x => c * x) (snd v))
end;
fun vector_of_list l =
@@ -151,7 +151,7 @@
(* Monomials. *)
fun monomial_eval assig m =
- FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => a */ rat_pow (FuncUtil.Ctermfunc.apply assig x) k)
+ FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => a * rat_pow (FuncUtil.Ctermfunc.apply assig x) k)
m rat_1;
val monomial_1 = FuncUtil.Ctermfunc.empty;
@@ -169,7 +169,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 rat_0;
val poly_0 = FuncUtil.Monomialfunc.empty;
@@ -180,28 +180,28 @@
fun poly_var x = FuncUtil.Monomialfunc.onefunc (monomial_var x, rat_1);
fun poly_const c =
- if c =/ rat_0 then poly_0 else FuncUtil.Monomialfunc.onefunc (monomial_1, c);
+ if c = rat_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 = rat_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_add p1 p2 =
- FuncUtil.Monomialfunc.combine (curry op +/) (fn x => x =/ rat_0) p1 p2;
+ FuncUtil.Monomialfunc.combine (curry op +) (fn x => x = rat_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 = rat_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;
@@ -323,10 +323,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) / pow10 (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
@@ -337,7 +337,7 @@
val exponent = ($$ "e" || $$ "E") |-- signed decimalint;
val decimal = signed decimalsig -- (emptyin rat_0|| exponent)
- >> (fn (h, x) => h */ pow10 (int_of_rat x));
+ >> (fn (h, x) => h * pow10 (int_of_rat x));
fun mkparser p s =
let val (x,rst) = p (raw_explode s)
@@ -359,7 +359,7 @@
(* 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 =
@@ -374,24 +374,24 @@
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 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 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 = rat_0 then a
else FuncUtil.Intfunc.update (i,y) a
end) v FuncUtil.Intfunc.empty): vector
@@ -400,16 +400,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 = rat_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 = rat_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 rat_0 end;
(* Eliminate all variables, in an essentially arbitrary order. *)
@@ -438,11 +438,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.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)
+ if b = rat_0 then e
+ else tri_equation_add e (tri_equation_cmul (Rat.neg b / a) eq)
end
in
eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map (K elim) dun))
@@ -487,8 +487,8 @@
let
val a11 = FuncUtil.Intpairfunc.tryapplyd (snd m) (i,i) rat_0
in
- if a11 </ rat_0 then raise Failure "diagonalize: not PSD"
- else if a11 =/ rat_0 then
+ if a11 < rat_0 then raise Failure "diagonalize: not PSD"
+ else if a11 = rat_0 then
if FuncUtil.Intfunc.is_empty (snd (row i m))
then diagonalize n (i + 1) m
else raise Failure "diagonalize: not PSD ___ "
@@ -497,7 +497,7 @@
val v = row i m
val v' =
(fst v, FuncUtil.Intfunc.fold (fn (i, c) => fn a =>
- let val y = c // a11
+ let val y = c / a11
in if y = rat_0 then a else FuncUtil.Intfunc.update (i,y) a
end) (snd v) FuncUtil.Intfunc.empty)
fun upt0 x y a =
@@ -508,8 +508,8 @@
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.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.empty)
in (a11, v') :: diagonalize n (i + 1) m' end
@@ -603,10 +603,10 @@
(* 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 = rat_0);
fun bmatrix_cmul c bm =
- if c =/ rat_0 then Inttriplefunc.empty
- else Inttriplefunc.map (fn _ => fn x => c */ x) bm;
+ if c = rat_0 then Inttriplefunc.empty
+ else Inttriplefunc.map (fn _ => fn x => c * x) bm;
val bmatrix_neg = bmatrix_cmul (Rat.rat_of_int ~1);
@@ -803,13 +803,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 <> Rat.zero 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 < Rat.zero 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 <= Rat.zero then nth lts n
else raise Failure "trivial_axiom: Not a trivial axiom"
| _ => error "trivial_axiom: Not a trivial axiom")
in
--- a/src/HOL/Library/positivstellensatz.ML Tue May 31 19:51:01 2016 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Tue May 31 21:54:10 2016 +0200
@@ -585,27 +585,27 @@
(* 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 = Rat.zero)
+ 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
((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 > Rat.zero)) lts of
SOME r => r
| NONE =>
- (case find_first (contradictory (fn x => x >/ Rat.zero)) les of
+ (case find_first (contradictory (fn x => x > Rat.zero)) 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 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)
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 =
@@ -613,7 +613,7 @@
val c1 = FuncUtil.Ctermfunc.tryapplyd e1 v Rat.zero
val c2 = FuncUtil.Ctermfunc.tryapplyd e2 v Rat.zero
in
- if c1 */ c2 >=/ Rat.zero then acc else
+ if c1 * c2 >= Rat.zero then acc else
let
val e1' = linear_cmul (Rat.abs c2) e1
val e2' = linear_cmul (Rat.abs c1) e2
@@ -623,13 +623,13 @@
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 Rat.zero = Rat.zero) 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 Rat.zero = Rat.zero) 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 Rat.zero > Rat.zero) 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 Rat.zero > Rat.zero) 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 = Rat.zero)) eqs of
SOME r => r
| NONE =>
(case eqs of
@@ -651,9 +651,9 @@
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
+ if d = Rat.zero then inp else
let
- val k = (Rat.neg d) */ Rat.abs c // c
+ val k = (Rat.neg d) * Rat.abs c / c
val e' = linear_cmul k e
val t' = linear_cmul (Rat.abs c) t
val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p)
--- a/src/HOL/Multivariate_Analysis/normarith.ML Tue May 31 19:51:01 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Tue May 31 21:54:10 2016 +0200
@@ -28,14 +28,14 @@
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) >= Rat.zero)
(Thm.dest_arg t) acc
| _ => augment_norm true t acc
val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K Rat.neg)
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 = 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
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)
@@ -43,8 +43,8 @@
val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg)
*)
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 = 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
(*
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)
@@ -84,7 +84,7 @@
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) < Rat.zero then arg_conv cv t else Thm.reflexive t
| _ => Thm.reflexive t
(*
fun flip v eq =
@@ -96,7 +96,7 @@
|(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))
+ FuncUtil.Intfunc.fold (fn (x,c) => fn s => s + c * (FuncUtil.Intfunc.apply env x))
lin Rat.zero
fun solve (vs,eqs) = case (vs,eqs) of
@@ -129,11 +129,11 @@
NONE => NONE
| SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) 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 >= Rat.zero)) 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
@@ -297,18 +297,18 @@
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
+ in forall (fn e => evaluate f e = Rat.zero) 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.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 = Rat.zero 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/Tools/groebner.ML Tue May 31 19:51:01 2016 +0200
+++ b/src/HOL/Tools/groebner.ML Tue May 31 21:54:10 2016 +0200
@@ -80,14 +80,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 = rat_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,16 +99,16 @@
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 = rat_0) then error "grob_inv: division by zero"
+ else [(rat_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 = rat_0 then error "grob_div: division by zero"
+ else grob_cmul (rat_1 / c,l) l1
else error "grob_div: non-constant divisor polynomial"
| _ => error "grob_div: non-constant divisor polynomial";
@@ -120,7 +120,7 @@
(* 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. *)
@@ -178,8 +178,8 @@
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((rat_1 / c',map (K 0) m'),hist)) end;
(* The most popular heuristic is to order critical pairs by LCM monomial. *)
@@ -190,14 +190,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);
@@ -318,7 +318,7 @@
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;
+ (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. *)
@@ -608,7 +608,7 @@
[(rat_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 = rat_0 then [] else [(x,map (K 0) vars)]
end)
handle ERROR _ =>
((grob_neg(grobify_term vars (ring_dest_neg tm)))
@@ -712,9 +712,9 @@
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_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
+ (filter (fn (c,_) => c < rat_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 =
--- a/src/Pure/General/rat.ML Tue May 31 19:51:01 2016 +0200
+++ b/src/Pure/General/rat.ML Tue May 31 21:54:10 2016 +0200
@@ -102,17 +102,13 @@
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);
+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 Rat.eq "=";
+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 (not o Rat.eq) "<>";