--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Jun 01 15:01:43 2016 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Jun 01 15:10:27 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 < @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:01:43 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML Wed Jun 01 15:10:27 2016 +0200
@@ -50,7 +50,7 @@
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 if c = @1 then string_of_monomial m
else string_of_rat c ^ "*" ^ string_of_monomial m
fun string_of_poly p =
@@ -121,7 +121,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:01:43 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Jun 01 15:10:27 2016 +0200
@@ -19,10 +19,6 @@
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.of_int 10;
val max = Integer.max;
val denominator_rat = Rat.dest #> snd #> Rat.of_int;
@@ -37,9 +33,9 @@
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;
@@ -47,13 +43,13 @@
let
val (a,b) = Rat.dest (Rat.abs r)
val d = a div b
- val s = if r < rat_0 then (Rat.neg o Rat.of_int) else Rat.of_int
+ val s = if r < @0 then (Rat.neg 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 pow2 = rat_pow @2;
+val pow10 = rat_pow @10;
val trace = Attrib.setup_config_bool @{binding sos_trace} (K false);
@@ -78,22 +74,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 < @1/10 then normalize (@10 * y) - 1
+ else if abs_rat 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 e = normalize y
- val z = pow10(~ e) * y + rat_1
+ val z = pow10(~ e) * y + @1
val k = int_of_rat (round_rat(pow10 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 +113,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,7 +124,7 @@
fun vector_cmul c (v: vector) =
let val n = dim v in
- if c = rat_0 then vector_0 n
+ if c = @0 then vector_0 n
else (n,FuncUtil.Intfunc.map (fn _ => fn x => c * x) (snd v))
end;
@@ -152,7 +148,7 @@
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;
+ m @1;
val monomial_1 = FuncUtil.Ctermfunc.empty;
@@ -169,7 +165,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,25 +173,25 @@
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
+ 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_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
@@ -209,7 +205,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 +285,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,7 +298,7 @@
else index_char str chr (pos + 1);
fun rat_of_quotient (a,b) =
- if b = 0 then rat_0 else Rat.make (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
@@ -336,7 +332,7 @@
val exponent = ($$ "e" || $$ "E") |-- signed decimalint;
-val decimal = signed decimalsig -- (emptyin rat_0|| exponent)
+val decimal = signed decimalsig -- (emptyin @0|| exponent)
>> (fn (h, x) => h * pow10 (int_of_rat x));
fun mkparser p s =
@@ -372,12 +368,12 @@
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 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 max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' @0
+ val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') @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'
@@ -391,7 +387,7 @@
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 +396,16 @@
(* Stuff for "equations" ((int*int*int)->num functions). *)
fun tri_equation_cmul c eq =
- if c = rat_0 then Inttriplefunc.empty
+ 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. *)
@@ -440,8 +436,8 @@
val 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
+ let val b = Inttriplefunc.tryapplyd e v @0 in
+ if b = @0 then e
else tri_equation_add e (tri_equation_cmul (Rat.neg b / a) eq)
end
in
@@ -485,10 +481,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 ___ "
@@ -498,19 +494,19 @@
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
+ 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 +541,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
@@ -603,9 +599,9 @@
(* 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
+ if c = @0 then Inttriplefunc.empty
else Inttriplefunc.map (fn _ => fn x => c * x) bm;
val bmatrix_neg = bmatrix_cmul (Rat.of_int ~1);
@@ -641,7 +637,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 +649,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 +666,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 +686,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 +705,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,7 +724,7 @@
val allmats = blocks blocksizes blockmat
in (vec, map diag allmats) end
val (vec, ratdias) =
- if null pvs then find_rounding rat_1
+ if null pvs then find_rounding @1
else tryfind find_rounding (map Rat.of_int (1 upto 31) @ map pow2 (5 upto 66))
val newassigs =
fold_rev (fn k => Inttriplefunc.update (nth pvs (k - 1), int_element vec k))
@@ -803,13 +799,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 +830,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 +848,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 +888,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:01:43 2016 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Wed Jun 01 15:10:27 2016 +0200
@@ -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,35 +585,35 @@
(* A linear arithmetic prover *)
local
- val linear_add = FuncUtil.Ctermfunc.combine (curry op +) (fn z => z = Rat.zero)
+ 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
@@ -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 @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,8 +650,8 @@
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 e' = linear_cmul k e
@@ -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:01:43 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Wed Jun 01 15:10:27 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) >= @0)
(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 = @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)
@@ -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 = @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,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) < @0 then arg_conv cv t else Thm.reflexive t
| _ => Thm.reflexive t
(*
fun flip v eq =
@@ -97,10 +97,10 @@
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
+ 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
@@ -127,9 +127,9 @@
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
+ val unset = filter (forall (fn c => c >= @0)) rawvs
in fold_rev (insert (eq_list op =)) unset []
end
@@ -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
*)
@@ -288,7 +288,7 @@
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,8 +296,8 @@
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
@@ -308,7 +308,7 @@
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/Tools/groebner.ML Wed Jun 01 15:01:43 2016 +0200
+++ b/src/HOL/Tools/groebner.ML Wed Jun 01 15:10:27 2016 +0200
@@ -32,8 +32,6 @@
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.dest #> snd #> Rat.of_int;
fun int_of_rat a =
@@ -81,7 +79,7 @@
| ((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
+ 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);
@@ -99,22 +97,22 @@
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. *)
@@ -125,7 +123,7 @@
(* 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. *)
@@ -179,7 +177,7 @@
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;
+ Mmul((@1 / c',map (K 0) m'),hist)) end;
(* The most popular heuristic is to order critical pairs by LCM monomial. *)
@@ -299,7 +297,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,7 +315,7 @@
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
+ 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 +329,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 +603,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 +660,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 +710,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_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) => (minus_rat c,m))
- (filter (fn (c,_) => c < rat_0) p))) cert
+ (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:01:43 2016 +0200
+++ b/src/HOL/Tools/lin_arith.ML Wed Jun 01 15:10:27 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 Rat.DIVZERO 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'
@@ -172,7 +172,7 @@
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.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.
@@ -227,8 +227,8 @@
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)