--- a/src/HOL/Algebra/IntRing.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Algebra/IntRing.thy Mon Dec 28 01:28:28 2015 +0100
@@ -13,7 +13,7 @@
lemma dvds_eq_abseq:
fixes k :: int
- shows "l dvd k \<and> k dvd l \<longleftrightarrow> abs l = abs k"
+ shows "l dvd k \<and> k dvd l \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>"
apply rule
apply (simp add: zdvd_antisym_abs)
apply (simp add: dvd_if_abs_eq)
@@ -281,7 +281,7 @@
finally show ?thesis .
qed
-lemma Idl_eq_abs: "Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> abs l = abs k"
+lemma Idl_eq_abs: "Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>"
apply (subst dvds_eq_abseq[symmetric])
apply (rule dvds_eq_Idl[symmetric])
done
--- a/src/HOL/Decision_Procs/Approximation.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon Dec 28 01:28:28 2015 +0100
@@ -170,10 +170,10 @@
"float_power_bnds prec n l u =
(if 0 < l then (power_down_fl prec l n, power_up_fl prec u n)
else if odd n then
- (- power_up_fl prec (abs l) n,
- if u < 0 then - power_down_fl prec (abs u) n else power_up_fl prec u n)
- else if u < 0 then (power_down_fl prec (abs u) n, power_up_fl prec (abs l) n)
- else (0, power_up_fl prec (max (abs l) (abs u)) n))"
+ (- power_up_fl prec \<bar>l\<bar> n,
+ if u < 0 then - power_down_fl prec \<bar>u\<bar> n else power_up_fl prec u n)
+ else if u < 0 then (power_down_fl prec \<bar>u\<bar> n, power_up_fl prec \<bar>l\<bar> n)
+ else (0, power_up_fl prec (max \<bar>l\<bar> \<bar>u\<bar>) n))"
lemma le_minus_power_downI: "0 \<le> x \<Longrightarrow> x ^ n \<le> - a \<Longrightarrow> a \<le> - power_down prec x n"
by (subst le_minus_iff) (auto intro: power_down_le power_mono_odd)
@@ -2679,7 +2679,7 @@
"interpret_floatarith (Arctan a) vs = arctan (interpret_floatarith a vs)" |
"interpret_floatarith (Min a b) vs = min (interpret_floatarith a vs) (interpret_floatarith b vs)" |
"interpret_floatarith (Max a b) vs = max (interpret_floatarith a vs) (interpret_floatarith b vs)" |
-"interpret_floatarith (Abs a) vs = abs (interpret_floatarith a vs)" |
+"interpret_floatarith (Abs a) vs = \<bar>interpret_floatarith a vs\<bar>" |
"interpret_floatarith Pi vs = pi" |
"interpret_floatarith (Sqrt a) vs = sqrt (interpret_floatarith a vs)" |
"interpret_floatarith (Exp a) vs = exp (interpret_floatarith a vs)" |
--- a/src/HOL/Decision_Procs/Cooper.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Mon Dec 28 01:28:28 2015 +0100
@@ -618,11 +618,11 @@
| "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v \<noteq> 0 then T else F | _ \<Rightarrow> NEq a')"
| "simpfm (Dvd i a) =
(if i = 0 then simpfm (Eq a)
- else if abs i = 1 then T
+ else if \<bar>i\<bar> = 1 then T
else let a' = simpnum a in case a' of C v \<Rightarrow> if i dvd v then T else F | _ \<Rightarrow> Dvd i a')"
| "simpfm (NDvd i a) =
(if i = 0 then simpfm (NEq a)
- else if abs i = 1 then F
+ else if \<bar>i\<bar> = 1 then F
else let a' = simpnum a in case a' of C v \<Rightarrow> if \<not>( i dvd v) then T else F | _ \<Rightarrow> NDvd i a')"
| "simpfm p = p"
by pat_completeness auto
@@ -718,7 +718,7 @@
let ?sa = "simpnum a"
from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
by simp
- consider "i = 0" | "abs i = 1" | "i \<noteq> 0" "abs i \<noteq> 1" by blast
+ consider "i = 0" | "\<bar>i\<bar> = 1" | "i \<noteq> 0" "\<bar>i\<bar> \<noteq> 1" by blast
then show ?case
proof cases
case 1
@@ -740,7 +740,7 @@
proof cases
case 1
with sa[symmetric] i show ?thesis
- by (cases "abs i = 1") auto
+ by (cases "\<bar>i\<bar> = 1") auto
next
case 2
then have "simpfm (Dvd i a) = Dvd i ?sa"
@@ -753,7 +753,7 @@
let ?sa = "simpnum a"
from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
by simp
- consider "i = 0" | "abs i = 1" | "i \<noteq> 0" "abs i \<noteq> 1" by blast
+ consider "i = 0" | "\<bar>i\<bar> = 1" | "i \<noteq> 0" "\<bar>i\<bar> \<noteq> 1" by blast
then show ?case
proof cases
case 1
@@ -775,7 +775,7 @@
proof cases
case 1
with sa[symmetric] i show ?thesis
- by (cases "abs i = 1") auto
+ by (cases "\<bar>i\<bar> = 1") auto
next
case 2
then have "simpfm (NDvd i a) = NDvd i ?sa"
@@ -1046,16 +1046,16 @@
(if i = 0 then zlfm (Eq a)
else
let (c, r) = zsplit0 a in
- if c = 0 then Dvd (abs i) r
- else if c > 0 then Dvd (abs i) (CN 0 c r)
- else Dvd (abs i) (CN 0 (- c) (Neg r)))"
+ if c = 0 then Dvd \<bar>i\<bar> r
+ else if c > 0 then Dvd \<bar>i\<bar> (CN 0 c r)
+ else Dvd \<bar>i\<bar> (CN 0 (- c) (Neg r)))"
"zlfm (NDvd i a) =
(if i = 0 then zlfm (NEq a)
else
let (c, r) = zsplit0 a in
- if c = 0 then NDvd (abs i) r
- else if c > 0 then NDvd (abs i) (CN 0 c r)
- else NDvd (abs i) (CN 0 (- c) (Neg r)))"
+ if c = 0 then NDvd \<bar>i\<bar> r
+ else if c > 0 then NDvd \<bar>i\<bar> (CN 0 c r)
+ else NDvd \<bar>i\<bar> (CN 0 (- c) (Neg r)))"
"zlfm (NOT (And p q)) = Or (zlfm (NOT p)) (zlfm (NOT q))"
"zlfm (NOT (Or p q)) = And (zlfm (NOT p)) (zlfm (NOT q))"
"zlfm (NOT (Imp p q)) = And (zlfm p) (zlfm (NOT q))"
@@ -1213,7 +1213,7 @@
case 4
then have l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
- with Ia 4 dvd_minus_iff[of "abs j" "?c*i + ?N ?r"] show ?thesis
+ with Ia 4 dvd_minus_iff[of "\<bar>j\<bar>" "?c*i + ?N ?r"] show ?thesis
by (simp add: Let_def split_def)
qed
next
@@ -1253,7 +1253,7 @@
case 4
then have l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
- with Ia 4 dvd_minus_iff[of "abs j" "?c*i + ?N ?r"] show ?thesis
+ with Ia 4 dvd_minus_iff[of "\<bar>j\<bar>" "?c*i + ?N ?r"] show ?thesis
by (simp add: Let_def split_def)
qed
qed auto
--- a/src/HOL/Decision_Procs/Ferrack.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Mon Dec 28 01:28:28 2015 +0100
@@ -455,8 +455,8 @@
fun maxcoeff:: "num \<Rightarrow> int"
where
- "maxcoeff (C i) = abs i"
-| "maxcoeff (CN n c t) = max (abs c) (maxcoeff t)"
+ "maxcoeff (C i) = \<bar>i\<bar>"
+| "maxcoeff (CN n c t) = max \<bar>c\<bar> (maxcoeff t)"
| "maxcoeff t = 1"
lemma maxcoeff_pos: "maxcoeff t \<ge> 0"
@@ -498,7 +498,7 @@
declare dvd_trans [trans add]
-lemma natabs0: "nat (abs x) = 0 \<longleftrightarrow> x = 0"
+lemma natabs0: "nat \<bar>x\<bar> = 0 \<longleftrightarrow> x = 0"
by arith
lemma numgcd0:
@@ -536,8 +536,8 @@
fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
where
- "ismaxcoeff (C i) = (\<lambda>x. abs i \<le> x)"
-| "ismaxcoeff (CN n c t) = (\<lambda>x. abs c \<le> x \<and> ismaxcoeff t x)"
+ "ismaxcoeff (C i) = (\<lambda>x. \<bar>i\<bar> \<le> x)"
+| "ismaxcoeff (CN n c t) = (\<lambda>x. \<bar>c\<bar> \<le> x \<and> ismaxcoeff t x)"
| "ismaxcoeff t = (\<lambda>x. True)"
lemma ismaxcoeff_mono: "ismaxcoeff t c \<Longrightarrow> c \<le> c' \<Longrightarrow> ismaxcoeff t c'"
@@ -547,18 +547,18 @@
proof (induct t rule: maxcoeff.induct)
case (2 n c t)
then have H:"ismaxcoeff t (maxcoeff t)" .
- have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)"
+ have thh: "maxcoeff t \<le> max \<bar>c\<bar> (maxcoeff t)"
by simp
from ismaxcoeff_mono[OF H thh] show ?case
by simp
qed simp_all
lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow>
- abs i > 1 \<and> abs j > 1 \<or> abs i = 0 \<and> abs j > 1 \<or> abs i > 1 \<and> abs j = 0"
- apply (cases "abs i = 0", simp_all add: gcd_int_def)
- apply (cases "abs j = 0", simp_all)
- apply (cases "abs i = 1", simp_all)
- apply (cases "abs j = 1", simp_all)
+ \<bar>i\<bar> > 1 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> = 0 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> > 1 \<and> \<bar>j\<bar> = 0"
+ apply (cases "\<bar>i\<bar> = 0", simp_all add: gcd_int_def)
+ apply (cases "\<bar>j\<bar> = 0", simp_all)
+ apply (cases "\<bar>i\<bar> = 1", simp_all)
+ apply (cases "\<bar>j\<bar> = 1", simp_all)
apply auto
done
@@ -577,7 +577,7 @@
from 2 have th: "gcd c ?g > 1"
by simp
from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
- consider "abs c > 1" "?g > 1" | "abs c = 0" "?g > 1" | "?g = 0"
+ consider "\<bar>c\<bar> > 1" "?g > 1" | "\<bar>c\<bar> = 0" "?g > 1" | "?g = 0"
by auto
then show ?case
proof cases
@@ -744,11 +744,11 @@
lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0"
proof (induct t rule: maxcoeff.induct)
case (2 n c t)
- then have cnz: "c \<noteq> 0" and mx: "max (abs c) (maxcoeff t) = 0"
+ then have cnz: "c \<noteq> 0" and mx: "max \<bar>c\<bar> (maxcoeff t) = 0"
by simp_all
- have "max (abs c) (maxcoeff t) \<ge> abs c"
+ have "max \<bar>c\<bar> (maxcoeff t) \<ge> \<bar>c\<bar>"
by simp
- with cnz have "max (abs c) (maxcoeff t) > 0"
+ with cnz have "max \<bar>c\<bar> (maxcoeff t) > 0"
by arith
with 2 show ?case
by simp
--- a/src/HOL/Decision_Procs/MIR.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Mon Dec 28 01:28:28 2015 +0100
@@ -48,19 +48,19 @@
by (auto simp add: rdvd_def dvd_def) (rule_tac x="k" in exI, simp only: of_int_mult[symmetric])
-lemma rdvd_abs1: "(abs (real_of_int d) rdvd t) = (real_of_int (d ::int) rdvd t)"
+lemma rdvd_abs1: "(\<bar>real_of_int d\<bar> rdvd t) = (real_of_int (d ::int) rdvd t)"
proof
assume d: "real_of_int d rdvd t"
from d int_rdvd_real have d2: "d dvd \<lfloor>t\<rfloor>" and ti: "real_of_int \<lfloor>t\<rfloor> = t"
by auto
- from iffD2[OF abs_dvd_iff] d2 have "(abs d) dvd \<lfloor>t\<rfloor>" by blast
- with ti int_rdvd_real[symmetric] have "real_of_int (abs d) rdvd t" by blast
- thus "abs (real_of_int d) rdvd t" by simp
+ from iffD2[OF abs_dvd_iff] d2 have "\<bar>d\<bar> dvd \<lfloor>t\<rfloor>" by blast
+ with ti int_rdvd_real[symmetric] have "real_of_int \<bar>d\<bar> rdvd t" by blast
+ thus "\<bar>real_of_int d\<bar> rdvd t" by simp
next
- assume "abs (real_of_int d) rdvd t" hence "real_of_int (abs d) rdvd t" by simp
- with int_rdvd_real[where i="abs d" and x="t"]
- have d2: "abs d dvd \<lfloor>t\<rfloor>" and ti: "real_of_int \<lfloor>t\<rfloor> = t"
+ assume "\<bar>real_of_int d\<bar> rdvd t" hence "real_of_int \<bar>d\<bar> rdvd t" by simp
+ with int_rdvd_real[where i="\<bar>d\<bar>" and x="t"]
+ have d2: "\<bar>d\<bar> dvd \<lfloor>t\<rfloor>" and ti: "real_of_int \<lfloor>t\<rfloor> = t"
by auto
from iffD1[OF abs_dvd_iff] d2 have "d dvd \<lfloor>t\<rfloor>" by blast
with ti int_rdvd_real[symmetric] show "real_of_int d rdvd t" by blast
@@ -528,9 +528,9 @@
"lex_bnd t s \<equiv> lex_ns (bnds t) (bnds s)"
fun maxcoeff:: "num \<Rightarrow> int" where
- "maxcoeff (C i) = abs i"
-| "maxcoeff (CN n c t) = max (abs c) (maxcoeff t)"
-| "maxcoeff (CF c t s) = max (abs c) (maxcoeff s)"
+ "maxcoeff (C i) = \<bar>i\<bar>"
+| "maxcoeff (CN n c t) = max \<bar>c\<bar> (maxcoeff t)"
+| "maxcoeff (CF c t s) = max \<bar>c\<bar> (maxcoeff s)"
| "maxcoeff t = 1"
lemma maxcoeff_pos: "maxcoeff t \<ge> 0"
@@ -602,9 +602,9 @@
qed (auto simp add: numgcd_def gp)
fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
- "ismaxcoeff (C i) = (\<lambda> x. abs i \<le> x)"
-| "ismaxcoeff (CN n c t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))"
-| "ismaxcoeff (CF c s t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))"
+ "ismaxcoeff (C i) = (\<lambda> x. \<bar>i\<bar> \<le> x)"
+| "ismaxcoeff (CN n c t) = (\<lambda>x. \<bar>c\<bar> \<le> x \<and> (ismaxcoeff t x))"
+| "ismaxcoeff (CF c s t) = (\<lambda>x. \<bar>c\<bar> \<le> x \<and> (ismaxcoeff t x))"
| "ismaxcoeff t = (\<lambda>x. True)"
lemma ismaxcoeff_mono: "ismaxcoeff t c \<Longrightarrow> c \<le> c' \<Longrightarrow> ismaxcoeff t c'"
@@ -614,7 +614,7 @@
proof (induct t rule: maxcoeff.induct)
case (2 n c t)
hence H:"ismaxcoeff t (maxcoeff t)" .
- have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by simp
+ have thh: "maxcoeff t \<le> max \<bar>c\<bar> (maxcoeff t)" by simp
from ismaxcoeff_mono[OF H thh] show ?case by simp
next
case (3 c t s)
@@ -623,12 +623,12 @@
from ismaxcoeff_mono[OF H1 thh1] show ?case by simp
qed simp_all
-lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))"
+lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow> ((\<bar>i\<bar> > 1 \<and> \<bar>j\<bar> > 1) \<or> (\<bar>i\<bar> = 0 \<and> \<bar>j\<bar> > 1) \<or> (\<bar>i\<bar> > 1 \<and> \<bar>j\<bar> = 0))"
apply (unfold gcd_int_def)
apply (cases "i = 0", simp_all)
apply (cases "j = 0", simp_all)
- apply (cases "abs i = 1", simp_all)
- apply (cases "abs j = 1", simp_all)
+ apply (cases "\<bar>i\<bar> = 1", simp_all)
+ apply (cases "\<bar>j\<bar> = 1", simp_all)
apply auto
done
@@ -644,17 +644,17 @@
let ?g = "numgcdh t m"
from 2 have th:"gcd c ?g > 1" by simp
from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
- have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
- moreover {assume "abs c > 1" and gp: "?g > 1" with 2
+ have "(\<bar>c\<bar> > 1 \<and> ?g > 1) \<or> (\<bar>c\<bar> = 0 \<and> ?g > 1) \<or> (\<bar>c\<bar> > 1 \<and> ?g = 0)" by simp
+ moreover {assume "\<bar>c\<bar> > 1" and gp: "?g > 1" with 2
have th: "dvdnumcoeff t ?g" by simp
have th': "gcd c ?g dvd ?g" by simp
from dvdnumcoeff_trans[OF th' th] have ?case by simp }
- moreover {assume "abs c = 0 \<and> ?g > 1"
+ moreover {assume "\<bar>c\<bar> = 0 \<and> ?g > 1"
with 2 have th: "dvdnumcoeff t ?g" by simp
have th': "gcd c ?g dvd ?g" by simp
from dvdnumcoeff_trans[OF th' th] have ?case by simp
hence ?case by simp }
- moreover {assume "abs c > 1" and g0:"?g = 0"
+ moreover {assume "\<bar>c\<bar> > 1" and g0:"?g = 0"
from numgcdh0[OF g0] have "m=0". with 2 g0 have ?case by simp }
ultimately show ?case by blast
next
@@ -662,17 +662,17 @@
let ?g = "numgcdh t m"
from 3 have th:"gcd c ?g > 1" by simp
from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
- have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
- moreover {assume "abs c > 1" and gp: "?g > 1" with 3
+ have "(\<bar>c\<bar> > 1 \<and> ?g > 1) \<or> (\<bar>c\<bar> = 0 \<and> ?g > 1) \<or> (\<bar>c\<bar> > 1 \<and> ?g = 0)" by simp
+ moreover {assume "\<bar>c\<bar> > 1" and gp: "?g > 1" with 3
have th: "dvdnumcoeff t ?g" by simp
have th': "gcd c ?g dvd ?g" by simp
from dvdnumcoeff_trans[OF th' th] have ?case by simp }
- moreover {assume "abs c = 0 \<and> ?g > 1"
+ moreover {assume "\<bar>c\<bar> = 0 \<and> ?g > 1"
with 3 have th: "dvdnumcoeff t ?g" by simp
have th': "gcd c ?g dvd ?g" by simp
from dvdnumcoeff_trans[OF th' th] have ?case by simp
hence ?case by simp }
- moreover {assume "abs c > 1" and g0:"?g = 0"
+ moreover {assume "\<bar>c\<bar> > 1" and g0:"?g = 0"
from numgcdh0[OF g0] have "m=0". with 3 g0 have ?case by simp }
ultimately show ?case by blast
qed auto
@@ -904,15 +904,15 @@
lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0"
proof (induct t rule: maxcoeff.induct)
case (2 n c t)
- hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+
- have "max (abs c) (maxcoeff t) \<ge> abs c" by simp
- with cnz have "max (abs c) (maxcoeff t) > 0" by arith
+ hence cnz: "c \<noteq>0" and mx: "max \<bar>c\<bar> (maxcoeff t) = 0" by simp+
+ have "max \<bar>c\<bar> (maxcoeff t) \<ge> \<bar>c\<bar>" by simp
+ with cnz have "max \<bar>c\<bar> (maxcoeff t) > 0" by arith
with 2 show ?case by simp
next
case (3 c s t)
- hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+
- have "max (abs c) (maxcoeff t) \<ge> abs c" by simp
- with cnz have "max (abs c) (maxcoeff t) > 0" by arith
+ hence cnz: "c \<noteq>0" and mx: "max \<bar>c\<bar> (maxcoeff t) = 0" by simp+
+ have "max \<bar>c\<bar> (maxcoeff t) \<ge> \<bar>c\<bar>" by simp
+ with cnz have "max \<bar>c\<bar> (maxcoeff t) > 0" by arith
with 3 show ?case by simp
qed auto
@@ -1152,10 +1152,10 @@
| "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0) then T else F | _ \<Rightarrow> Eq (reducecoeff a'))"
| "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0) then T else F | _ \<Rightarrow> NEq (reducecoeff a'))"
| "simpfm (Dvd i a) = (if i=0 then simpfm (Eq a)
- else if (abs i = 1) \<and> check_int a then T
+ else if (\<bar>i\<bar> = 1) \<and> check_int a then T
else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v) then T else F | _ \<Rightarrow> (let (d,t) = simpdvd i a' in Dvd d t))"
| "simpfm (NDvd i a) = (if i=0 then simpfm (NEq a)
- else if (abs i = 1) \<and> check_int a then F
+ else if (\<bar>i\<bar> = 1) \<and> check_int a then F
else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F | _ \<Rightarrow> (let (d,t) = simpdvd i a' in NDvd d t))"
| "simpfm p = p"
by pat_completeness auto
@@ -1266,10 +1266,10 @@
ultimately show ?case by blast
next
case (12 i a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp
- have "i=0 \<or> (abs i = 1 \<and> check_int a) \<or> (i\<noteq>0 \<and> ((abs i \<noteq> 1) \<or> (\<not> check_int a)))" by auto
+ have "i=0 \<or> (\<bar>i\<bar> = 1 \<and> check_int a) \<or> (i\<noteq>0 \<and> ((\<bar>i\<bar> \<noteq> 1) \<or> (\<not> check_int a)))" by auto
{assume "i=0" hence ?case using "12.hyps" by (simp add: rdvd_left_0_eq Let_def)}
moreover
- {assume ai1: "abs i = 1" and ai: "check_int a"
+ {assume ai1: "\<bar>i\<bar> = 1" and ai: "check_int a"
hence "i=1 \<or> i= - 1" by arith
moreover {assume i1: "i = 1"
from rdvd_left1_int[OF check_int[OF ai, simplified isint_iff]]
@@ -1280,9 +1280,9 @@
have ?case using i1 ai by simp }
ultimately have ?case by blast}
moreover
- {assume inz: "i\<noteq>0" and cond: "(abs i \<noteq> 1) \<or> (\<not> check_int a)"
+ {assume inz: "i\<noteq>0" and cond: "(\<bar>i\<bar> \<noteq> 1) \<or> (\<not> check_int a)"
{fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
- by (cases "abs i = 1", auto simp add: int_rdvd_iff) }
+ by (cases "\<bar>i\<bar> = 1", auto simp add: int_rdvd_iff) }
moreover {assume H:"\<not> (\<exists> v. ?sa = C v)"
hence th: "simpfm (Dvd i a) = Dvd (fst (simpdvd i ?sa)) (snd (simpdvd i ?sa))" using inz cond by (cases ?sa, auto simp add: Let_def split_def)
from simpnum_nz have nz:"nozerocoeff ?sa" by simp
@@ -1291,10 +1291,10 @@
ultimately show ?case by blast
next
case (13 i a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp
- have "i=0 \<or> (abs i = 1 \<and> check_int a) \<or> (i\<noteq>0 \<and> ((abs i \<noteq> 1) \<or> (\<not> check_int a)))" by auto
+ have "i=0 \<or> (\<bar>i\<bar> = 1 \<and> check_int a) \<or> (i\<noteq>0 \<and> ((\<bar>i\<bar> \<noteq> 1) \<or> (\<not> check_int a)))" by auto
{assume "i=0" hence ?case using "13.hyps" by (simp add: rdvd_left_0_eq Let_def)}
moreover
- {assume ai1: "abs i = 1" and ai: "check_int a"
+ {assume ai1: "\<bar>i\<bar> = 1" and ai: "check_int a"
hence "i=1 \<or> i= - 1" by arith
moreover {assume i1: "i = 1"
from rdvd_left1_int[OF check_int[OF ai, simplified isint_iff]]
@@ -1305,9 +1305,9 @@
have ?case using i1 ai by simp }
ultimately have ?case by blast}
moreover
- {assume inz: "i\<noteq>0" and cond: "(abs i \<noteq> 1) \<or> (\<not> check_int a)"
+ {assume inz: "i\<noteq>0" and cond: "(\<bar>i\<bar> \<noteq> 1) \<or> (\<not> check_int a)"
{fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
- by (cases "abs i = 1", auto simp add: int_rdvd_iff) }
+ by (cases "\<bar>i\<bar> = 1", auto simp add: int_rdvd_iff) }
moreover {assume H:"\<not> (\<exists> v. ?sa = C v)"
hence th: "simpfm (NDvd i a) = NDvd (fst (simpdvd i ?sa)) (snd (simpdvd i ?sa))" using inz cond
by (cases ?sa, auto simp add: Let_def split_def)
@@ -1599,14 +1599,14 @@
else (Or (NEq (CN 0 (-c) (Floor (Neg r)))) (NEq (Add (Floor (Neg r)) r))))"
"zlfm (Dvd i a) = (if i=0 then zlfm (Eq a)
else (let (c,r) = zsplit0 a in
- if c=0 then Dvd (abs i) r else
- if c>0 then And (Eq (Sub (Floor r) r)) (Dvd (abs i) (CN 0 c (Floor r)))
- else And (Eq (Sub (Floor r) r)) (Dvd (abs i) (CN 0 (-c) (Neg (Floor r))))))"
+ if c=0 then Dvd \<bar>i\<bar> r else
+ if c>0 then And (Eq (Sub (Floor r) r)) (Dvd \<bar>i\<bar> (CN 0 c (Floor r)))
+ else And (Eq (Sub (Floor r) r)) (Dvd \<bar>i\<bar> (CN 0 (-c) (Neg (Floor r))))))"
"zlfm (NDvd i a) = (if i=0 then zlfm (NEq a)
else (let (c,r) = zsplit0 a in
- if c=0 then NDvd (abs i) r else
- if c>0 then Or (NEq (Sub (Floor r) r)) (NDvd (abs i) (CN 0 c (Floor r)))
- else Or (NEq (Sub (Floor r) r)) (NDvd (abs i) (CN 0 (-c) (Neg (Floor r))))))"
+ if c=0 then NDvd \<bar>i\<bar> r else
+ if c>0 then Or (NEq (Sub (Floor r) r)) (NDvd \<bar>i\<bar> (CN 0 c (Floor r)))
+ else Or (NEq (Sub (Floor r) r)) (NDvd \<bar>i\<bar> (CN 0 (-c) (Neg (Floor r))))))"
"zlfm (NOT (And p q)) = disj (zlfm (NOT p)) (zlfm (NOT q))"
"zlfm (NOT (Or p q)) = conj (zlfm (NOT p)) (zlfm (NOT q))"
"zlfm (NOT (Imp p q)) = conj (zlfm p) (zlfm (NOT q))"
@@ -1865,11 +1865,11 @@
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (Dvd j a) = (real_of_int j rdvd (real_of_int (?c * i) + (?N ?r)))"
using Ia by (simp add: Let_def split_def)
- also have "\<dots> = (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r))"
+ also have "\<dots> = (real_of_int \<bar>j\<bar> rdvd real_of_int (?c*i) + (?N ?r))"
by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
- also have "\<dots> = ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
+ also have "\<dots> = (\<bar>j\<bar> dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
(real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r))))"
- by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
+ by(simp only: int_rdvd_real[where i="\<bar>j\<bar>" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
also have "\<dots> = (?I (?l (Dvd j a)))" using cp cnz jnz
by (simp add: Let_def split_def int_rdvd_iff[symmetric]
del: of_int_mult) (auto simp add: ac_simps)
@@ -1879,13 +1879,13 @@
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (Dvd j a) = (real_of_int j rdvd (real_of_int (?c * i) + (?N ?r)))"
using Ia by (simp add: Let_def split_def)
- also have "\<dots> = (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r))"
+ also have "\<dots> = (real_of_int \<bar>j\<bar> rdvd real_of_int (?c*i) + (?N ?r))"
by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
- also have "\<dots> = ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
+ also have "\<dots> = (\<bar>j\<bar> dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
(real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r))))"
- by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
+ by(simp only: int_rdvd_real[where i="\<bar>j\<bar>" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
also have "\<dots> = (?I (?l (Dvd j a)))" using cn cnz jnz
- using rdvd_minus [where d="abs j" and t="real_of_int (?c*i + \<lfloor>?N ?r\<rfloor>)", simplified, symmetric]
+ using rdvd_minus [where d="\<bar>j\<bar>" and t="real_of_int (?c*i + \<lfloor>?N ?r\<rfloor>)", simplified, symmetric]
by (simp add: Let_def split_def int_rdvd_iff[symmetric]
del: of_int_mult) (auto simp add: ac_simps)
finally have ?case using l jnz by blast }
@@ -1911,11 +1911,11 @@
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (NDvd j a) = (\<not> (real_of_int j rdvd (real_of_int (?c * i) + (?N ?r))))"
using Ia by (simp add: Let_def split_def)
- also have "\<dots> = (\<not> (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r)))"
+ also have "\<dots> = (\<not> (real_of_int \<bar>j\<bar> rdvd real_of_int (?c*i) + (?N ?r)))"
by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
- also have "\<dots> = (\<not> ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
+ also have "\<dots> = (\<not> (\<bar>j\<bar> dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
(real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r)))))"
- by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
+ by(simp only: int_rdvd_real[where i="\<bar>j\<bar>" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
also have "\<dots> = (?I (?l (NDvd j a)))" using cp cnz jnz
by (simp add: Let_def split_def int_rdvd_iff[symmetric]
del: of_int_mult) (auto simp add: ac_simps)
@@ -1925,13 +1925,13 @@
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (NDvd j a) = (\<not> (real_of_int j rdvd (real_of_int (?c * i) + (?N ?r))))"
using Ia by (simp add: Let_def split_def)
- also have "\<dots> = (\<not> (real_of_int (abs j) rdvd real_of_int (?c*i) + (?N ?r)))"
+ also have "\<dots> = (\<not> (real_of_int \<bar>j\<bar> rdvd real_of_int (?c*i) + (?N ?r)))"
by (simp only: rdvd_abs1[where d="j" and t="real_of_int (?c*i) + ?N ?r", symmetric]) simp
- also have "\<dots> = (\<not> ((abs j) dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
+ also have "\<dots> = (\<not> (\<bar>j\<bar> dvd \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> \<and>
(real_of_int \<lfloor>(?N ?r) + real_of_int (?c*i)\<rfloor> = (real_of_int (?c*i) + (?N ?r)))))"
- by(simp only: int_rdvd_real[where i="abs j" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
+ by(simp only: int_rdvd_real[where i="\<bar>j\<bar>" and x="real_of_int (?c*i) + (?N ?r)"]) (simp only: ac_simps)
also have "\<dots> = (?I (?l (NDvd j a)))" using cn cnz jnz
- using rdvd_minus [where d="abs j" and t="real_of_int (?c*i + \<lfloor>?N ?r\<rfloor>)", simplified, symmetric]
+ using rdvd_minus [where d="\<bar>j\<bar>" and t="real_of_int (?c*i + \<lfloor>?N ?r\<rfloor>)", simplified, symmetric]
by (simp add: Let_def split_def int_rdvd_iff[symmetric]
del: of_int_mult) (auto simp add: ac_simps)
finally have ?case using l jnz by blast }
@@ -3261,7 +3261,7 @@
from iszlfm_gen [OF lp,rule_format, where y="a"] have lp':"iszlfm p (a#bs)" .
from \<rho>'[OF lp' d dp, rule_format, OF nob] have th:"\<forall> x. ?P x \<longrightarrow> ?P (x - ?d)" by blast
from minusinf_inf[OF lp] obtain z where z:"\<forall> x<z. ?MP x = ?P x" by blast
- have zp: "abs (x - z) + 1 \<ge> 0" by arith
+ have zp: "\<bar>x - z\<bar> + 1 \<ge> 0" by arith
from decr_lemma[OF dp,where x="x" and z="z"]
decr_mult_lemma[OF dp th zp, rule_format, OF px] z have th:"\<exists> x. ?MP x" by auto
with minusinf_bex[OF lp] px nob have ?thesis by blast}
@@ -3860,12 +3860,12 @@
definition DVD :: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" where
DVD_def: "DVD i c t =
(if i=0 then eq c t else
- if c = 0 then (Dvd i t) else if c >0 then DVDJ (abs i) c t else DVDJ (abs i) (-c) (Neg t))"
+ if c = 0 then (Dvd i t) else if c >0 then DVDJ \<bar>i\<bar> c t else DVDJ \<bar>i\<bar> (-c) (Neg t))"
definition NDVD :: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" where
"NDVD i c t =
(if i=0 then neq c t else
- if c = 0 then (NDvd i t) else if c >0 then NDVDJ (abs i) c t else NDVDJ (abs i) (-c) (Neg t))"
+ if c = 0 then (NDvd i t) else if c >0 then NDVDJ \<bar>i\<bar> c t else NDVDJ \<bar>i\<bar> (-c) (Neg t))"
lemma DVD_mono:
assumes xp: "0\<le> x" and x1: "x < 1"
@@ -5671,7 +5671,7 @@
lemma "\<forall>x::real. \<exists>y \<le> x. (\<lfloor>x\<rfloor> = \<lceil>y\<rceil>)"
by mir
-lemma "\<forall>(x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
+lemma "\<forall>(x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> \<bar>y - x\<bar> \<and> \<bar>y - x\<bar> \<le> 1"
by mir
end
--- a/src/HOL/Decision_Procs/Polynomial_List.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Mon Dec 28 01:28:28 2015 +0100
@@ -1118,7 +1118,7 @@
text \<open>Bound for polynomial.\<close>
lemma poly_mono:
fixes x :: "'a::linordered_idom"
- shows "abs x \<le> k \<Longrightarrow> abs (poly p x) \<le> poly (map abs p) k"
+ shows "\<bar>x\<bar> \<le> k \<Longrightarrow> \<bar>poly p x\<bar> \<le> poly (map abs p) k"
proof (induct p)
case Nil
then show ?case by simp
@@ -1126,7 +1126,7 @@
case (Cons a p)
then show ?case
apply auto
- apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans)
+ apply (rule_tac y = "\<bar>a\<bar> + \<bar>x * poly p x\<bar>" in order_trans)
apply (rule abs_triangle_ineq)
apply (auto intro!: mult_mono simp add: abs_mult)
done
--- a/src/HOL/Library/BigO.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Library/BigO.thy Mon Dec 28 01:28:28 2015 +0100
@@ -35,19 +35,19 @@
subsection \<open>Definitions\<close>
definition bigo :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(1O'(_'))")
- where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. abs (h x) \<le> c * abs (f x)}"
+ where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>}"
lemma bigo_pos_const:
- "(\<exists>c::'a::linordered_idom. \<forall>x. abs (h x) \<le> c * abs (f x)) \<longleftrightarrow>
- (\<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x)))"
+ "(\<exists>c::'a::linordered_idom. \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>) \<longleftrightarrow>
+ (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
apply auto
apply (case_tac "c = 0")
apply simp
apply (rule_tac x = "1" in exI)
apply simp
- apply (rule_tac x = "abs c" in exI)
+ apply (rule_tac x = "\<bar>c\<bar>" in exI)
apply auto
- apply (subgoal_tac "c * abs (f x) \<le> abs c * abs (f x)")
+ apply (subgoal_tac "c * \<bar>f x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>")
apply (erule_tac x = x in allE)
apply force
apply (rule mult_right_mono)
@@ -55,7 +55,7 @@
apply (rule abs_ge_zero)
done
-lemma bigo_alt_def: "O(f) = {h. \<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x))}"
+lemma bigo_alt_def: "O(f) = {h. \<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)}"
by (auto simp add: bigo_def bigo_pos_const)
lemma bigo_elt_subset [intro]: "f \<in> O(g) \<Longrightarrow> O(f) \<le> O(g)"
@@ -65,7 +65,7 @@
apply simp
apply (rule allI)
apply (drule_tac x = "xa" in spec)+
- apply (subgoal_tac "ca * abs (f xa) \<le> ca * (c * abs (g xa))")
+ apply (subgoal_tac "ca * \<bar>f xa\<bar> \<le> ca * (c * \<bar>g xa\<bar>)")
apply (erule order_trans)
apply (simp add: ac_simps)
apply (rule mult_left_mono, assumption)
@@ -110,29 +110,29 @@
apply (rule subsetI)
apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
apply (subst bigo_pos_const [symmetric])+
- apply (rule_tac x = "\<lambda>n. if abs (g n) \<le> (abs (f n)) then x n else 0" in exI)
+ apply (rule_tac x = "\<lambda>n. if \<bar>g n\<bar> \<le> \<bar>f n\<bar> then x n else 0" in exI)
apply (rule conjI)
apply (rule_tac x = "c + c" in exI)
apply (clarsimp)
- apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (f xa)")
+ apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> (c + c) * \<bar>f xa\<bar>")
apply (erule_tac x = xa in allE)
apply (erule order_trans)
apply (simp)
- apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))")
+ apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
apply (erule order_trans)
apply (simp add: ring_distribs)
apply (rule mult_left_mono)
apply (simp add: abs_triangle_ineq)
apply (simp add: order_less_le)
- apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI)
+ apply (rule_tac x = "\<lambda>n. if \<bar>f n\<bar> < \<bar>g n\<bar> then x n else 0" in exI)
apply (rule conjI)
apply (rule_tac x = "c + c" in exI)
apply auto
- apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (g xa)")
+ apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> (c + c) * \<bar>g xa\<bar>")
apply (erule_tac x = xa in allE)
apply (erule order_trans)
apply simp
- apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))")
+ apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
apply (erule order_trans)
apply (simp add: ring_distribs)
apply (rule mult_left_mono)
@@ -162,8 +162,8 @@
apply (drule_tac x = "xa" in spec)+
apply (subgoal_tac "0 \<le> f xa + g xa")
apply (simp add: ring_distribs)
- apply (subgoal_tac "abs (a xa + b xa) \<le> abs (a xa) + abs (b xa)")
- apply (subgoal_tac "abs (a xa) + abs (b xa) \<le> max c ca * f xa + max c ca * g xa")
+ apply (subgoal_tac "\<bar>a xa + b xa\<bar> \<le> \<bar>a xa\<bar> + \<bar>b xa\<bar>")
+ apply (subgoal_tac "\<bar>a xa\<bar> + \<bar>b xa\<bar> \<le> max c ca * f xa + max c ca * g xa")
apply force
apply (rule add_mono)
apply (subgoal_tac "c * f xa \<le> max c ca * f xa")
@@ -183,7 +183,7 @@
lemma bigo_bounded_alt: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> c * g x \<Longrightarrow> f \<in> O(g)"
apply (auto simp add: bigo_def)
- apply (rule_tac x = "abs c" in exI)
+ apply (rule_tac x = "\<bar>c\<bar>" in exI)
apply auto
apply (drule_tac x = x in spec)+
apply (simp add: abs_mult [symmetric])
@@ -202,21 +202,21 @@
apply force
done
-lemma bigo_abs: "(\<lambda>x. abs (f x)) =o O(f)"
+lemma bigo_abs: "(\<lambda>x. \<bar>f x\<bar>) =o O(f)"
apply (unfold bigo_def)
apply auto
apply (rule_tac x = 1 in exI)
apply auto
done
-lemma bigo_abs2: "f =o O(\<lambda>x. abs (f x))"
+lemma bigo_abs2: "f =o O(\<lambda>x. \<bar>f x\<bar>)"
apply (unfold bigo_def)
apply auto
apply (rule_tac x = 1 in exI)
apply auto
done
-lemma bigo_abs3: "O(f) = O(\<lambda>x. abs (f x))"
+lemma bigo_abs3: "O(f) = O(\<lambda>x. \<bar>f x\<bar>)"
apply (rule equalityI)
apply (rule bigo_elt_subset)
apply (rule bigo_abs2)
@@ -224,15 +224,15 @@
apply (rule bigo_abs)
done
-lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. abs (f x)) =o (\<lambda>x. abs (g x)) +o O(h)"
+lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o (\<lambda>x. \<bar>g x\<bar>) +o O(h)"
apply (drule set_plus_imp_minus)
apply (rule set_minus_imp_plus)
apply (subst fun_diff_def)
proof -
assume a: "f - g \<in> O(h)"
- have "(\<lambda>x. abs (f x) - abs (g x)) =o O(\<lambda>x. abs (abs (f x) - abs (g x)))"
+ have "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) =o O(\<lambda>x. \<bar>\<bar>f x\<bar> - \<bar>g x\<bar>\<bar>)"
by (rule bigo_abs2)
- also have "\<dots> \<subseteq> O(\<lambda>x. abs (f x - g x))"
+ also have "\<dots> \<subseteq> O(\<lambda>x. \<bar>f x - g x\<bar>)"
apply (rule bigo_elt_subset)
apply (rule bigo_bounded)
apply force
@@ -246,10 +246,10 @@
done
also from a have "\<dots> \<subseteq> O(h)"
by (rule bigo_elt_subset)
- finally show "(\<lambda>x. abs (f x) - abs (g x)) \<in> O(h)".
+ finally show "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) \<in> O(h)".
qed
-lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. abs (f x)) =o O(g)"
+lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o O(g)"
by (unfold bigo_def, auto)
lemma bigo_elt_subset2 [intro]: "f \<in> g +o O(h) \<Longrightarrow> O(f) \<subseteq> O(g) + O(h)"
@@ -257,16 +257,16 @@
assume "f \<in> g +o O(h)"
also have "\<dots> \<subseteq> O(g) + O(h)"
by (auto del: subsetI)
- also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))"
+ also have "\<dots> = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
apply (subst bigo_abs3 [symmetric])+
apply (rule refl)
done
- also have "\<dots> = O((\<lambda>x. abs (g x)) + (\<lambda>x. abs (h x)))"
+ also have "\<dots> = O((\<lambda>x. \<bar>g x\<bar>) + (\<lambda>x. \<bar>h x\<bar>))"
by (rule bigo_plus_eq [symmetric]) auto
finally have "f \<in> \<dots>" .
then have "O(f) \<subseteq> \<dots>"
by (elim bigo_elt_subset)
- also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))"
+ also have "\<dots> = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
by (rule bigo_plus_eq, auto)
finally show ?thesis
by (simp add: bigo_abs3 [symmetric])
@@ -279,7 +279,7 @@
apply (rule_tac x = "c * ca" in exI)
apply (rule allI)
apply (erule_tac x = x in allE)+
- apply (subgoal_tac "c * ca * abs (f x * g x) = (c * abs (f x)) * (ca * abs (g x))")
+ apply (subgoal_tac "c * ca * \<bar>f x * g x\<bar> = (c * \<bar>f x\<bar>) * (ca * \<bar>g x\<bar>)")
apply (erule ssubst)
apply (subst abs_mult)
apply (rule mult_mono)
@@ -293,7 +293,7 @@
apply (rule_tac x = c in exI)
apply auto
apply (drule_tac x = x in spec)
- apply (subgoal_tac "abs (f x) * abs (b x) \<le> abs (f x) * (c * abs (g x))")
+ apply (subgoal_tac "\<bar>f x\<bar> * \<bar>b x\<bar> \<le> \<bar>f x\<bar> * (c * \<bar>g x\<bar>)")
apply (force simp add: ac_simps)
apply (rule mult_left_mono, assumption)
apply (rule abs_ge_zero)
@@ -450,7 +450,7 @@
fixes c :: "'a::linordered_field"
shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. 1) \<in> O(\<lambda>x. c)"
apply (simp add: bigo_def)
- apply (rule_tac x = "abs (inverse c)" in exI)
+ apply (rule_tac x = "\<bar>inverse c\<bar>" in exI)
apply (simp add: abs_mult [symmetric])
done
@@ -473,7 +473,7 @@
lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)"
apply (simp add: bigo_def)
- apply (rule_tac x = "abs c" in exI)
+ apply (rule_tac x = "\<bar>c\<bar>" in exI)
apply (auto simp add: abs_mult [symmetric])
done
@@ -486,7 +486,7 @@
fixes c :: "'a::linordered_field"
shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)"
apply (simp add: bigo_def)
- apply (rule_tac x = "abs (inverse c)" in exI)
+ apply (rule_tac x = "\<bar>inverse c\<bar>" in exI)
apply (simp add: abs_mult mult.assoc [symmetric])
done
@@ -516,15 +516,15 @@
apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI)
apply (simp add: mult.assoc [symmetric] abs_mult)
- apply (rule_tac x = "abs (inverse c) * ca" in exI)
+ apply (rule_tac x = "\<bar>inverse c\<bar> * ca" in exI)
apply auto
done
lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) \<subseteq> O(f)"
apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
- apply (rule_tac x = "ca * abs c" in exI)
+ apply (rule_tac x = "ca * \<bar>c\<bar>" in exI)
apply (rule allI)
- apply (subgoal_tac "ca * abs c * abs (f x) = abs c * (ca * abs (f x))")
+ apply (subgoal_tac "ca * \<bar>c\<bar> * \<bar>f x\<bar> = \<bar>c\<bar> * (ca * \<bar>f x\<bar>)")
apply (erule ssubst)
apply (subst abs_mult)
apply (rule mult_left_mono)
@@ -559,10 +559,10 @@
subsection \<open>Setsum\<close>
lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 \<le> h x y \<Longrightarrow>
- \<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) \<le> c * (h x y) \<Longrightarrow>
+ \<exists>c. \<forall>x. \<forall>y \<in> A x. \<bar>f x y\<bar> \<le> c * h x y \<Longrightarrow>
(\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
apply (auto simp add: bigo_def)
- apply (rule_tac x = "abs c" in exI)
+ apply (rule_tac x = "\<bar>c\<bar>" in exI)
apply (subst abs_of_nonneg) back back
apply (rule setsum_nonneg)
apply force
@@ -583,7 +583,7 @@
done
lemma bigo_setsum1: "\<forall>x y. 0 \<le> h x y \<Longrightarrow>
- \<exists>c. \<forall>x y. abs (f x y) \<le> c * h x y \<Longrightarrow>
+ \<exists>c. \<forall>x y. \<bar>f x y\<bar> \<le> c * h x y \<Longrightarrow>
(\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
apply (rule bigo_setsum_main)
apply force
@@ -593,12 +593,12 @@
done
lemma bigo_setsum2: "\<forall>y. 0 \<le> h y \<Longrightarrow>
- \<exists>c. \<forall>y. abs (f y) \<le> c * (h y) \<Longrightarrow>
+ \<exists>c. \<forall>y. \<bar>f y\<bar> \<le> c * (h y) \<Longrightarrow>
(\<lambda>x. \<Sum>y \<in> A x. f y) =o O(\<lambda>x. \<Sum>y \<in> A x. h y)"
by (rule bigo_setsum1) auto
lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
- (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o O(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))"
+ (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h (k x y)\<bar>)"
apply (rule bigo_setsum1)
apply (rule allI)+
apply (rule abs_ge_zero)
@@ -616,7 +616,7 @@
lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
(\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
(\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o
- O(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))"
+ O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h (k x y)\<bar>)"
apply (rule set_minus_imp_plus)
apply (subst fun_diff_def)
apply (subst setsum_subtractf [symmetric])
@@ -631,7 +631,7 @@
(\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))"
apply (subgoal_tac "(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y)) =
- (\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))")
+ (\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h (k x y)\<bar>)")
apply (erule ssubst)
apply (erule bigo_setsum3)
apply (rule ext)
@@ -715,7 +715,7 @@
definition lesso :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" (infixl "<o" 70)
where "f <o g = (\<lambda>x. max (f x - g x) 0)"
-lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> abs (f x) \<Longrightarrow> g =o O(h)"
+lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> \<le> \<bar>f x\<bar> \<Longrightarrow> g =o O(h)"
apply (unfold bigo_def)
apply clarsimp
apply (rule_tac x = c in exI)
@@ -724,7 +724,7 @@
apply (erule spec)+
done
-lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> f x \<Longrightarrow> g =o O(h)"
+lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> \<le> f x \<Longrightarrow> g =o O(h)"
apply (erule bigo_lesseq1)
apply (rule allI)
apply (drule_tac x = x in spec)
@@ -741,7 +741,7 @@
done
lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow>
- \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> abs (f x) \<Longrightarrow> g =o O(h)"
+ \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> \<bar>f x\<bar> \<Longrightarrow> g =o O(h)"
apply (erule bigo_lesseq1)
apply (rule allI)
apply (subst abs_of_nonneg)
@@ -819,13 +819,13 @@
apply (auto simp add: func_plus fun_diff_def algebra_simps split: split_max abs_split)
done
-lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x \<le> g x + C * abs (h x)"
+lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x \<le> g x + C * \<bar>h x\<bar>"
apply (simp only: lesso_def bigo_alt_def)
apply clarsimp
apply (rule_tac x = c in exI)
apply (rule allI)
apply (drule_tac x = x in spec)
- apply (subgoal_tac "abs (max (f x - g x) 0) = max (f x - g x) 0")
+ apply (subgoal_tac "\<bar>max (f x - g x) 0\<bar> = max (f x - g x) 0")
apply (clarsimp simp add: algebra_simps)
apply (rule abs_of_nonneg)
apply (rule max.cobounded2)
@@ -856,7 +856,7 @@
apply (rule order_le_less_trans)
apply assumption
apply (rule order_less_le_trans)
- apply (subgoal_tac "c * abs (g n) < c * (r / c)")
+ apply (subgoal_tac "c * \<bar>g n\<bar> < c * (r / c)")
apply assumption
apply (erule mult_strict_left_mono)
apply assumption
--- a/src/HOL/Library/Extended_Real.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy Mon Dec 28 01:28:28 2015 +0100
@@ -3484,7 +3484,7 @@
fixes a :: real
assumes "a \<le> x"
and "x \<le> b"
- shows "abs x \<le> max (abs a) (abs b)"
+ shows "\<bar>x\<bar> \<le> max \<bar>a\<bar> \<bar>b\<bar>"
by (metis abs_less_iff assms leI le_max_iff_disj
less_eq_real_def less_le_not_le less_minus_iff minus_minus)
--- a/src/HOL/Library/Float.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Library/Float.thy Mon Dec 28 01:28:28 2015 +0100
@@ -110,7 +110,7 @@
lemma minus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x - y \<in> float"
using plus_float [of x "- y"] by simp
-lemma abs_float[simp]: "x \<in> float \<Longrightarrow> abs x \<in> float"
+lemma abs_float[simp]: "x \<in> float \<Longrightarrow> \<bar>x\<bar> \<in> float"
by (cases x rule: linorder_cases[of 0]) auto
lemma sgn_of_float[simp]: "x \<in> float \<Longrightarrow> sgn x \<in> float"
@@ -594,7 +594,7 @@
qualified lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m"
by transfer (auto simp add: is_float_zero_def)
-qualified lemma compute_float_abs[code]: "abs (Float m e) = Float (abs m) e"
+qualified lemma compute_float_abs[code]: "\<bar>Float m e\<bar> = Float \<bar>m\<bar> e"
by transfer (simp add: abs_mult)
qualified lemma compute_float_eq[code]: "equal_class.equal f g = is_float_zero (f - g)"
@@ -1186,7 +1186,7 @@
begin
qualified lemma compute_float_round_down[code]:
- "float_round_down prec (Float m e) = (let d = bitlen (abs m) - int prec in
+ "float_round_down prec (Float m e) = (let d = bitlen \<bar>m\<bar> - int prec in
if 0 < d then Float (div_twopow m (nat d)) (e + d)
else Float m e)"
using Float.compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
@@ -1543,8 +1543,8 @@
lemma sum_neq_zeroI:
fixes a k :: real
- shows "abs a \<ge> k \<Longrightarrow> abs b < k \<Longrightarrow> a + b \<noteq> 0"
- and "abs a > k \<Longrightarrow> abs b \<le> k \<Longrightarrow> a + b \<noteq> 0"
+ shows "\<bar>a\<bar> \<ge> k \<Longrightarrow> \<bar>b\<bar> < k \<Longrightarrow> a + b \<noteq> 0"
+ and "\<bar>a\<bar> > k \<Longrightarrow> \<bar>b\<bar> \<le> k \<Longrightarrow> a + b \<noteq> 0"
by auto
lemma abs_real_le_2_powr_bitlen[simp]: "\<bar>real_of_int m2\<bar> < 2 powr real_of_int (bitlen \<bar>m2\<bar>)"
@@ -1564,7 +1564,7 @@
fixes ai p q :: int
and a b :: real
assumes "a * 2 powr p = ai"
- and b_le_1: "abs (b * 2 powr (p + 1)) \<le> 1"
+ and b_le_1: "\<bar>b * 2 powr (p + 1)\<bar> \<le> 1"
and leqp: "q \<le> p"
shows "\<lfloor>(a + b) * 2 powr q\<rfloor> = \<lfloor>(2 * ai + sgn b) * 2 powr (q - p - 1)\<rfloor>"
proof -
@@ -1576,7 +1576,7 @@
by (simp add: assms(1)[symmetric] powr_add[symmetric] algebra_simps powr_mult_base)
next
case 2
- then have "b * 2 powr p < abs (b * 2 powr (p + 1))"
+ then have "b * 2 powr p < \<bar>b * 2 powr (p + 1)\<bar>"
by simp
also note b_le_1
finally have b_less_1: "b * 2 powr real_of_int p < 1" .
@@ -1635,7 +1635,7 @@
lemma log2_abs_int_add_less_half_sgn_eq:
fixes ai :: int
and b :: real
- assumes "abs b \<le> 1/2"
+ assumes "\<bar>b\<bar> \<le> 1/2"
and "ai \<noteq> 0"
shows "\<lfloor>log 2 \<bar>real_of_int ai + b\<bar>\<rfloor> = \<lfloor>log 2 \<bar>ai + sgn b / 2\<bar>\<rfloor>"
proof (cases "b = 0")
@@ -1664,21 +1664,21 @@
have "\<bar>ai\<bar> = 2 powr k + r"
using \<open>k \<ge> 0\<close> by (auto simp: k_def r_def powr_realpow[symmetric])
- have pos: "abs b < 1 \<Longrightarrow> 0 < 2 powr k + (r + b)" for b :: real
+ have pos: "\<bar>b\<bar> < 1 \<Longrightarrow> 0 < 2 powr k + (r + b)" for b :: real
using \<open>0 \<le> k\<close> \<open>ai \<noteq> 0\<close>
by (auto simp add: r_def powr_realpow[symmetric] abs_if sgn_if algebra_simps
split: split_if_asm)
have less: "\<bar>sgn ai * b\<bar> < 1"
and less': "\<bar>sgn (sgn ai * b) / 2\<bar> < 1"
- using \<open>abs b \<le> _\<close> by (auto simp: abs_if sgn_if split: split_if_asm)
+ using \<open>\<bar>b\<bar> \<le> _\<close> by (auto simp: abs_if sgn_if split: split_if_asm)
- have floor_eq: "\<And>b::real. abs b \<le> 1 / 2 \<Longrightarrow>
+ have floor_eq: "\<And>b::real. \<bar>b\<bar> \<le> 1 / 2 \<Longrightarrow>
\<lfloor>log 2 (1 + (r + b) / 2 powr k)\<rfloor> = (if r = 0 \<and> b < 0 then -1 else 0)"
using \<open>k \<ge> 0\<close> r r_le
by (auto simp: floor_log_eq_powr_iff powr_minus_divide field_simps sgn_if)
from \<open>real_of_int \<bar>ai\<bar> = _\<close> have "\<bar>ai + b\<bar> = 2 powr k + (r + sgn ai * b)"
- using \<open>abs b <= _\<close> \<open>0 \<le> k\<close> r
+ using \<open>\<bar>b\<bar> <= _\<close> \<open>0 \<le> k\<close> r
by (auto simp add: sgn_if abs_if)
also have "\<lfloor>log 2 \<dots>\<rfloor> = \<lfloor>log 2 (2 powr k + r + sgn (sgn ai * b) / 2)\<rfloor>"
proof -
@@ -1690,14 +1690,14 @@
also
let ?if = "if r = 0 \<and> sgn ai * b < 0 then -1 else 0"
have "\<lfloor>log 2 (1 + (r + sgn ai * b) / 2 powr k)\<rfloor> = ?if"
- using \<open>abs b <= _\<close>
+ using \<open>\<bar>b\<bar> <= _\<close>
by (intro floor_eq) (auto simp: abs_mult sgn_if)
also
have "\<dots> = \<lfloor>log 2 (1 + (r + sgn (sgn ai * b) / 2) / 2 powr k)\<rfloor>"
by (subst floor_eq) (auto simp: sgn_if)
also have "k + \<dots> = \<lfloor>log 2 (2 powr k * (1 + (r + sgn (sgn ai * b) / 2) / 2 powr k))\<rfloor>"
unfolding floor_add2[symmetric]
- using pos[OF less'] \<open>abs b \<le> _\<close>
+ using pos[OF less'] \<open>\<bar>b\<bar> \<le> _\<close>
by (simp add: field_simps add_log_eq_powr)
also have "2 powr k * (1 + (r + sgn (sgn ai * b) / 2) / 2 powr k) =
2 powr k + r + sgn (sgn ai * b) / 2"
@@ -1885,7 +1885,7 @@
lemma float_zero[simp]: "real_of_float (Float 0 e) = 0"
by simp
-lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
+lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> \<bar>(a::int) div 2\<bar> < \<bar>a\<bar>"
by arith
lemma lapprox_rat: "real_of_float (lapprox_rat prec x y) \<le> real_of_int x / real_of_int y"
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Mon Dec 28 01:28:28 2015 +0100
@@ -136,9 +136,9 @@
proof -
from that z xy have "2 * x \<le> 1" "2 * x \<ge> -1" "2 * y \<le> 1" "2 * y \<ge> -1"
by (simp_all add: cmod_def power2_eq_square algebra_simps)
- then have "abs (2 * x) \<le> 1" "abs (2 * y) \<le> 1"
+ then have "\<bar>2 * x\<bar> \<le> 1" "\<bar>2 * y\<bar> \<le> 1"
by simp_all
- then have "(abs (2 * x))\<^sup>2 \<le> 1\<^sup>2" "(abs (2 * y))\<^sup>2 \<le> 1\<^sup>2"
+ then have "\<bar>2 * x\<bar>\<^sup>2 \<le> 1\<^sup>2" "\<bar>2 * y\<bar>\<^sup>2 \<le> 1\<^sup>2"
by - (rule power_mono, simp, simp)+
then have th0: "4 * x\<^sup>2 \<le> 1" "4 * y\<^sup>2 \<le> 1"
by (simp_all add: power_mult_distrib)
--- a/src/HOL/Library/Infinite_Set.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Mon Dec 28 01:28:28 2015 +0100
@@ -56,12 +56,12 @@
lemma infinite_int_iff_infinite_nat_abs: "infinite (S::int set) \<longleftrightarrow> infinite ((nat o abs) ` S)"
by (auto simp: transfer_nat_int_set_relations o_def image_comp dest: finite_image_absD)
-proposition infinite_int_iff_unbounded_le: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. abs n \<ge> m \<and> n \<in> S)"
+proposition infinite_int_iff_unbounded_le: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)"
apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded_le o_def image_def)
apply (metis abs_ge_zero nat_le_eq_zle le_nat_iff)
done
-proposition infinite_int_iff_unbounded: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. abs n > m \<and> n \<in> S)"
+proposition infinite_int_iff_unbounded: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> > m \<and> n \<in> S)"
apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded o_def image_def)
apply (metis (full_types) nat_le_iff nat_mono not_le)
done
--- a/src/HOL/Library/Polynomial.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Library/Polynomial.thy Mon Dec 28 01:28:28 2015 +0100
@@ -1062,7 +1062,7 @@
"x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y - x)"
definition
- "abs (x::'a poly) = (if x < 0 then - x else x)"
+ "\<bar>x::'a poly\<bar> = (if x < 0 then - x else x)"
definition
"sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
--- a/src/HOL/Library/positivstellensatz.ML Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Library/positivstellensatz.ML Mon Dec 28 01:28:28 2015 +0100
@@ -221,12 +221,12 @@
@{thms "HOL.all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
val real_abs_thms1 = @{lemma
- "((-1 * abs(x::real) >= r) = (-1 * x >= r & 1 * x >= r))" and
- "((-1 * abs(x) + a >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
- "((a + -1 * abs(x) >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
- "((a + -1 * abs(x) + b >= r) = (a + -1 * x + b >= r & a + 1 * x + b >= r))" and
- "((a + b + -1 * abs(x) >= r) = (a + b + -1 * x >= r & a + b + 1 * x >= r))" and
- "((a + b + -1 * abs(x) + c >= r) = (a + b + -1 * x + c >= r & a + b + 1 * x + c >= r))" and
+ "((-1 * \<bar>x::real\<bar> >= r) = (-1 * x >= r & 1 * x >= r))" and
+ "((-1 * \<bar>x\<bar> + a >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
+ "((a + -1 * \<bar>x\<bar> >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
+ "((a + -1 * \<bar>x\<bar> + b >= r) = (a + -1 * x + b >= r & a + 1 * x + b >= r))" and
+ "((a + b + -1 * \<bar>x\<bar> >= r) = (a + b + -1 * x >= r & a + b + 1 * x >= r))" and
+ "((a + b + -1 * \<bar>x\<bar> + c >= r) = (a + b + -1 * x + c >= r & a + b + 1 * x + c >= r))" and
"((-1 * max x y >= r) = (-1 * x >= r & -1 * y >= r))" and
"((-1 * max x y + a >= r) = (a + -1 * x >= r & a + -1 * y >= r))" and
"((a + -1 * max x y >= r) = (a + -1 * x >= r & a + -1 * y >= r))" and
@@ -245,12 +245,12 @@
"((a + min x y + b >= r) = (a + x + b >= r & a + y + b >= r))" and
"((a + b + min x y >= r) = (a + b + x >= r & a + b + y >= r))" and
"((a + b + min x y + c >= r) = (a + b + x + c >= r & a + b + y + c >= r))" and
- "((-1 * abs(x) > r) = (-1 * x > r & 1 * x > r))" and
- "((-1 * abs(x) + a > r) = (a + -1 * x > r & a + 1 * x > r))" and
- "((a + -1 * abs(x) > r) = (a + -1 * x > r & a + 1 * x > r))" and
- "((a + -1 * abs(x) + b > r) = (a + -1 * x + b > r & a + 1 * x + b > r))" and
- "((a + b + -1 * abs(x) > r) = (a + b + -1 * x > r & a + b + 1 * x > r))" and
- "((a + b + -1 * abs(x) + c > r) = (a + b + -1 * x + c > r & a + b + 1 * x + c > r))" and
+ "((-1 * \<bar>x\<bar> > r) = (-1 * x > r & 1 * x > r))" and
+ "((-1 * \<bar>x\<bar> + a > r) = (a + -1 * x > r & a + 1 * x > r))" and
+ "((a + -1 * \<bar>x\<bar> > r) = (a + -1 * x > r & a + 1 * x > r))" and
+ "((a + -1 * \<bar>x\<bar> + b > r) = (a + -1 * x + b > r & a + 1 * x + b > r))" and
+ "((a + b + -1 * \<bar>x\<bar> > r) = (a + b + -1 * x > r & a + b + 1 * x > r))" and
+ "((a + b + -1 * \<bar>x\<bar> + c > r) = (a + b + -1 * x + c > r & a + b + 1 * x + c > r))" and
"((-1 * max x y > r) = ((-1 * x > r) & -1 * y > r))" and
"((-1 * max x y + a > r) = (a + -1 * x > r & a + -1 * y > r))" and
"((a + -1 * max x y > r) = (a + -1 * x > r & a + -1 * y > r))" and
@@ -265,7 +265,7 @@
"((a + b + min x y + c > r) = (a + b + x + c > r & a + b + y + c > r))"
by auto};
-val abs_split' = @{lemma "P (abs (x::'a::linordered_idom)) == (x >= 0 & P x | x < 0 & P (-x))"
+val abs_split' = @{lemma "P \<bar>x::'a::linordered_idom\<bar> == (x >= 0 & P x | x < 0 & P (-x))"
by (atomize (full)) (auto split add: abs_split)};
val max_split = @{lemma "P (max x y) == ((x::'a::linorder) <= y & P y | x > y & P x)"
--- a/src/HOL/Matrix_LP/ComputeFloat.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy Mon Dec 28 01:28:28 2015 +0100
@@ -106,7 +106,7 @@
lemma int_mod_zmod: "int (a mod b) = (int a) mod (int b)"
by (rule zmod_int)
-lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
+lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> \<bar>(a::int) div 2\<bar> < \<bar>a\<bar>"
by arith
lemma norm_0_1: "(1::_::numeral) = Numeral1"
@@ -195,7 +195,7 @@
by (simp add: float_def mult_le_0_iff) (simp add: not_less [symmetric])
lemma float_abs:
- "abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
+ "\<bar>float (a,b)\<bar> = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
by (simp add: float_def abs_if mult_less_0_iff not_less)
lemma float_zero:
--- a/src/HOL/Matrix_LP/LP.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Matrix_LP/LP.thy Mon Dec 28 01:28:28 2015 +0100
@@ -19,47 +19,47 @@
assumes
"A * x \<le> (b::'a::lattice_ring)"
"0 \<le> y"
- "abs (A - A') \<le> \<delta>_A"
+ "\<bar>A - A'\<bar> \<le> \<delta>_A"
"b \<le> b'"
- "abs (c - c') \<le> \<delta>_c"
- "abs x \<le> r"
+ "\<bar>c - c'\<bar> \<le> \<delta>_c"
+ "\<bar>x\<bar> \<le> r"
shows
- "c * x \<le> y * b' + (y * \<delta>_A + abs (y * A' - c') + \<delta>_c) * r"
+ "c * x \<le> y * b' + (y * \<delta>_A + \<bar>y * A' - c'\<bar> + \<delta>_c) * r"
proof -
from assms have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
from assms have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono)
have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: algebra_simps)
from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp
- have 5: "c * x <= y * b' + abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"
+ have 5: "c * x <= y * b' + \<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar>"
by (simp only: 4 estimate_by_abs)
- have 6: "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <= abs (y * (A - A') + (y * A' - c') + (c'-c)) * abs x"
+ have 6: "\<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar> <= \<bar>y * (A - A') + (y * A' - c') + (c'-c)\<bar> * \<bar>x\<bar>"
by (simp add: abs_le_mult)
- have 7: "(abs (y * (A - A') + (y * A' - c') + (c'-c))) * abs x <= (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x"
+ have 7: "(\<bar>y * (A - A') + (y * A' - c') + (c'-c)\<bar>) * \<bar>x\<bar> <= (\<bar>y * (A-A') + (y*A'-c')\<bar> + \<bar>c' - c\<bar>) * \<bar>x\<bar>"
by(rule abs_triangle_ineq [THEN mult_right_mono]) simp
- have 8: " (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x <= (abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x"
+ have 8: "(\<bar>y * (A-A') + (y*A'-c')\<bar> + \<bar>c' - c\<bar>) * \<bar>x\<bar> <= (\<bar>y * (A-A')\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c' - c\<bar>) * \<bar>x\<bar>"
by (simp add: abs_triangle_ineq mult_right_mono)
- have 9: "(abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x"
+ have 9: "(\<bar>y * (A-A')\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c'-c\<bar>) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c'-c\<bar>) * \<bar>x\<bar>"
by (simp add: abs_le_mult mult_right_mono)
have 10: "c'-c = -(c-c')" by (simp add: algebra_simps)
- have 11: "abs (c'-c) = abs (c-c')"
+ have 11: "\<bar>c'-c\<bar> = \<bar>c-c'\<bar>"
by (subst 10, subst abs_minus_cancel, simp)
- have 12: "(abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + \<delta>_c) * abs x"
+ have 12: "(\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c'-c\<bar>) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar>"
by (simp add: 11 assms mult_right_mono)
- have 13: "(abs y * abs (A-A') + abs (y*A'-c') + \<delta>_c) * abs x <= (abs y * \<delta>_A + abs (y*A'-c') + \<delta>_c) * abs x"
+ have 13: "(\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar>"
by (simp add: assms mult_right_mono mult_left_mono)
- have r: "(abs y * \<delta>_A + abs (y*A'-c') + \<delta>_c) * abs x <= (abs y * \<delta>_A + abs (y*A'-c') + \<delta>_c) * r"
+ have r: "(\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * r"
apply (rule mult_left_mono)
apply (simp add: assms)
apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+
apply (rule mult_left_mono[of "0" "\<delta>_A", simplified])
apply (simp_all)
- apply (rule order_trans[where y="abs (A-A')"], simp_all add: assms)
- apply (rule order_trans[where y="abs (c-c')"], simp_all add: assms)
+ apply (rule order_trans[where y="\<bar>A-A'\<bar>"], simp_all add: assms)
+ apply (rule order_trans[where y="\<bar>c-c'\<bar>"], simp_all add: assms)
done
- from 6 7 8 9 12 13 r have 14:" abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <=(abs y * \<delta>_A + abs (y*A'-c') + \<delta>_c) * r"
+ from 6 7 8 9 12 13 r have 14: "\<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar> <= (\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * r"
by (simp)
show ?thesis
- apply (rule le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
+ apply (rule le_add_right_mono[of _ _ "\<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar>"])
apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified assms]])
done
qed
@@ -68,14 +68,14 @@
assumes
"A1 <= (A::'a::lattice_ring)"
"A <= A2"
- shows "abs (A-A1) <= A2-A1"
+ shows "\<bar>A-A1\<bar> <= A2-A1"
proof -
have "0 <= A - A1"
proof -
from assms add_right_mono [of A1 A "- A1"] show ?thesis by simp
qed
- then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg)
- with assms show "abs (A-A1) <= (A2-A1)" by simp
+ then have "\<bar>A-A1\<bar> = A-A1" by (rule abs_of_nonneg)
+ with assms show "\<bar>A-A1\<bar> <= (A2-A1)" by simp
qed
lemma mult_le_prts:
--- a/src/HOL/Matrix_LP/Matrix.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Matrix_LP/Matrix.thy Mon Dec 28 01:28:28 2015 +0100
@@ -918,8 +918,8 @@
apply (simp add: move_matrix_def)
apply (auto)
by (subst RepAbs_matrix,
- rule exI[of _ "(nrows A)+(nat (abs y))"], auto, rule nrows, arith,
- rule exI[of _ "(ncols A)+(nat (abs x))"], auto, rule ncols, arith)+
+ rule exI[of _ "(nrows A)+(nat \<bar>y\<bar>)"], auto, rule nrows, arith,
+ rule exI[of _ "(ncols A)+(nat \<bar>x\<bar>)"], auto, rule ncols, arith)+
lemma move_matrix_0_0[simp]: "move_matrix A 0 0 = A"
by (simp add: move_matrix_def)
@@ -1496,7 +1496,7 @@
begin
definition
- abs_matrix_def: "abs (A :: 'a matrix) = sup A (- A)"
+ abs_matrix_def: "\<bar>A :: 'a matrix\<bar> = sup A (- A)"
instance ..
@@ -1613,7 +1613,7 @@
instance matrix :: (lattice_ring) lattice_ring
proof
fix A B C :: "('a :: lattice_ring) matrix"
- show "abs A = sup A (-A)"
+ show "\<bar>A\<bar> = sup A (-A)"
by (simp add: abs_matrix_def)
qed
@@ -1814,7 +1814,7 @@
lemma Rep_minus[simp]: "Rep_matrix (-(A::_::group_add)) x y = - (Rep_matrix A x y)"
by (simp add: minus_matrix_def)
-lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lattice_ab_group_add)) x y = abs (Rep_matrix A x y)"
+lemma Rep_abs[simp]: "Rep_matrix \<bar>A::_::lattice_ab_group_add\<bar> x y = \<bar>Rep_matrix A x y\<bar>"
by (simp add: abs_lattice sup_matrix_def)
end
--- a/src/HOL/Matrix_LP/SparseMatrix.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Matrix_LP/SparseMatrix.thy Mon Dec 28 01:28:28 2015 +0100
@@ -108,7 +108,7 @@
primrec abs_spvec :: "('a::lattice_ab_group_add_abs) spvec \<Rightarrow> 'a spvec"
where
"abs_spvec [] = []"
-| "abs_spvec (a#as) = (fst a, abs (snd a))#(abs_spvec as)"
+| "abs_spvec (a#as) = (fst a, \<bar>snd a\<bar>)#(abs_spvec as)"
lemma sparse_row_vector_minus:
"sparse_row_vector (minus_spvec v) = - (sparse_row_vector v)"
@@ -127,7 +127,7 @@
(*FIXME move*)
lemma sparse_row_vector_abs:
- "sorted_spvec (v :: 'a::lattice_ring spvec) \<Longrightarrow> sparse_row_vector (abs_spvec v) = abs (sparse_row_vector v)"
+ "sorted_spvec (v :: 'a::lattice_ring spvec) \<Longrightarrow> sparse_row_vector (abs_spvec v) = \<bar>sparse_row_vector v\<bar>"
apply (induct v)
apply simp_all
apply (frule_tac sorted_spvec_cons1, simp)
@@ -770,7 +770,7 @@
qed
lemma sparse_row_matrix_abs:
- "sorted_spvec A \<Longrightarrow> sorted_spmat A \<Longrightarrow> sparse_row_matrix (abs_spmat A) = abs (sparse_row_matrix A)"
+ "sorted_spvec A \<Longrightarrow> sorted_spmat A \<Longrightarrow> sparse_row_matrix (abs_spmat A) = \<bar>sparse_row_matrix A\<bar>"
apply (induct A)
apply (simp_all add: sparse_row_vector_abs sparse_row_matrix_cons)
apply (frule_tac sorted_spvec_cons1, simp)
@@ -1060,7 +1060,7 @@
"A <= sparse_row_matrix A2"
"sparse_row_matrix c1 <= c"
"c <= sparse_row_matrix c2"
- "abs x \<le> sparse_row_matrix r"
+ "\<bar>x\<bar> \<le> sparse_row_matrix r"
shows
"c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b, mult_spmat (add_spmat (add_spmat (mult_spmat y (diff_spmat A2 A1),
abs_spmat (diff_spmat (mult_spmat y A1) c1)), diff_spmat c2 c1)) r))"
--- a/src/HOL/Metis_Examples/Big_O.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy Mon Dec 28 01:28:28 2015 +0100
@@ -17,12 +17,12 @@
subsection {* Definitions *}
definition bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set" ("(1O'(_'))") where
- "O(f::('a => 'b)) == {h. \<exists>c. \<forall>x. abs (h x) <= c * abs (f x)}"
+ "O(f::('a => 'b)) == {h. \<exists>c. \<forall>x. \<bar>h x\<bar> <= c * \<bar>f x\<bar>}"
lemma bigo_pos_const:
"(\<exists>c::'a::linordered_idom.
- \<forall>x. abs (h x) \<le> c * abs (f x))
- \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+ \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)
+ \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
by (metis (no_types) abs_ge_zero
algebra_simps mult.comm_neutral
mult_nonpos_nonneg not_le_imp_less order_trans zero_less_one)
@@ -33,12 +33,12 @@
lemma
"(\<exists>c::'a::linordered_idom.
- \<forall>x. abs (h x) \<le> c * abs (f x))
- \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+ \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)
+ \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
- apply (rule_tac x = "abs c" in exI, auto)
+ apply (rule_tac x = "\<bar>c\<bar>" in exI, auto)
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
@@ -64,12 +64,12 @@
lemma
"(\<exists>c::'a::linordered_idom.
- \<forall>x. abs (h x) \<le> c * abs (f x))
- \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+ \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)
+ \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
- apply (rule_tac x = "abs c" in exI, auto)
+ apply (rule_tac x = "\<bar>c\<bar>" in exI, auto)
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
@@ -87,12 +87,12 @@
lemma
"(\<exists>c::'a::linordered_idom.
- \<forall>x. abs (h x) \<le> c * abs (f x))
- \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+ \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)
+ \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
- apply (rule_tac x = "abs c" in exI, auto)
+ apply (rule_tac x = "\<bar>c\<bar>" in exI, auto)
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
@@ -107,12 +107,12 @@
lemma
"(\<exists>c::'a::linordered_idom.
- \<forall>x. abs (h x) \<le> c * abs (f x))
- \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+ \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)
+ \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
- apply (rule_tac x = "abs c" in exI, auto)
+ apply (rule_tac x = "\<bar>c\<bar>" in exI, auto)
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
@@ -125,7 +125,7 @@
sledgehammer_params [isar_proofs, compress = 1]
-lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
+lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. \<bar>h x\<bar> <= c * \<bar>f x\<bar>))}"
by (auto simp add: bigo_def bigo_pos_const)
lemma bigo_elt_subset [intro]: "f : O(g) \<Longrightarrow> O(f) \<le> O(g)"
@@ -160,25 +160,25 @@
apply (rule subsetI)
apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
apply (subst bigo_pos_const [symmetric])+
-apply (rule_tac x = "\<lambda>n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
+apply (rule_tac x = "\<lambda>n. if \<bar>g n\<bar> <= \<bar>f n\<bar> then x n else 0" in exI)
apply (rule conjI)
apply (rule_tac x = "c + c" in exI)
apply clarsimp
- apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
+ apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> <= (c + c) * \<bar>f xa\<bar>")
apply (metis mult_2 order_trans)
- apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
+ apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> <= c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
apply (erule order_trans)
apply (simp add: ring_distribs)
apply (rule mult_left_mono)
apply (simp add: abs_triangle_ineq)
apply (simp add: order_less_le)
-apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI)
+apply (rule_tac x = "\<lambda>n. if \<bar>f n\<bar> < \<bar>g n\<bar> then x n else 0" in exI)
apply (rule conjI)
apply (rule_tac x = "c + c" in exI)
apply auto
-apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
+apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> <= (c + c) * \<bar>g xa\<bar>")
apply (metis order_trans mult_2)
-apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
+apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> <= c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
apply (erule order_trans)
apply (simp add: ring_distribs)
by (metis abs_triangle_ineq mult_le_cancel_left_pos)
@@ -200,9 +200,8 @@
apply (drule_tac x = "xa" in spec)+
apply (subgoal_tac "0 <= f xa + g xa")
apply (simp add: ring_distribs)
- apply (subgoal_tac "abs (a xa + b xa) <= abs (a xa) + abs (b xa)")
- apply (subgoal_tac "abs (a xa) + abs (b xa) <=
- max c ca * f xa + max c ca * g xa")
+ apply (subgoal_tac "\<bar>a xa + b xa\<bar> <= \<bar>a xa\<bar> + \<bar>b xa\<bar>")
+ apply (subgoal_tac "\<bar>a xa\<bar> + \<bar>b xa\<bar> <= max c ca * f xa + max c ca * g xa")
apply (metis order_trans)
defer 1
apply (metis abs_triangle_ineq)
@@ -236,17 +235,17 @@
by (metis add_le_cancel_left diff_add_cancel func_plus le_fun_def
algebra_simps)
-lemma bigo_abs: "(\<lambda>x. abs(f x)) =o O(f)"
+lemma bigo_abs: "(\<lambda>x. \<bar>f x\<bar>) =o O(f)"
apply (unfold bigo_def)
apply auto
by (metis mult_1 order_refl)
-lemma bigo_abs2: "f =o O(\<lambda>x. abs(f x))"
+lemma bigo_abs2: "f =o O(\<lambda>x. \<bar>f x\<bar>)"
apply (unfold bigo_def)
apply auto
by (metis mult_1 order_refl)
-lemma bigo_abs3: "O(f) = O(\<lambda>x. abs(f x))"
+lemma bigo_abs3: "O(f) = O(\<lambda>x. \<bar>f x\<bar>)"
proof -
have F1: "\<forall>v u. u \<in> O(v) \<longrightarrow> O(u) \<subseteq> O(v)" by (metis bigo_elt_subset)
have F2: "\<forall>u. (\<lambda>R. \<bar>u R\<bar>) \<in> O(u)" by (metis bigo_abs)
@@ -254,15 +253,15 @@
thus "O(f) = O(\<lambda>x. \<bar>f x\<bar>)" using F1 F2 by auto
qed
-lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. abs (f x)) =o (\<lambda>x. abs (g x)) +o O(h)"
+lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o (\<lambda>x. \<bar>g x\<bar>) +o O(h)"
apply (drule set_plus_imp_minus)
apply (rule set_minus_imp_plus)
apply (subst fun_diff_def)
proof -
assume a: "f - g : O(h)"
- have "(\<lambda>x. abs (f x) - abs (g x)) =o O(\<lambda>x. abs(abs (f x) - abs (g x)))"
+ have "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) =o O(\<lambda>x. \<bar>\<bar>f x\<bar> - \<bar>g x\<bar>\<bar>)"
by (rule bigo_abs2)
- also have "... <= O(\<lambda>x. abs (f x - g x))"
+ also have "... <= O(\<lambda>x. \<bar>f x - g x\<bar>)"
apply (rule bigo_elt_subset)
apply (rule bigo_bounded)
apply (metis abs_ge_zero)
@@ -274,10 +273,10 @@
done
also have "... <= O(h)"
using a by (rule bigo_elt_subset)
- finally show "(\<lambda>x. abs (f x) - abs (g x)) : O(h)".
+ finally show "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) : O(h)" .
qed
-lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. abs(f x)) =o O(g)"
+lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o O(g)"
by (unfold bigo_def, auto)
lemma bigo_elt_subset2 [intro]: "f : g +o O(h) \<Longrightarrow> O(f) <= O(g) + O(h)"
@@ -285,14 +284,14 @@
assume "f : g +o O(h)"
also have "... <= O(g) + O(h)"
by (auto del: subsetI)
- also have "... = O(\<lambda>x. abs(g x)) + O(\<lambda>x. abs(h x))"
+ also have "... = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
by (metis bigo_abs3)
- also have "... = O((\<lambda>x. abs(g x)) + (\<lambda>x. abs(h x)))"
+ also have "... = O((\<lambda>x. \<bar>g x\<bar>) + (\<lambda>x. \<bar>h x\<bar>))"
by (rule bigo_plus_eq [symmetric], auto)
finally have "f : ...".
then have "O(f) <= ..."
by (elim bigo_elt_subset)
- also have "... = O(\<lambda>x. abs(g x)) + O(\<lambda>x. abs(h x))"
+ also have "... = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
by (rule bigo_plus_eq, auto)
finally show ?thesis
by (simp add: bigo_abs3 [symmetric])
@@ -307,7 +306,7 @@
apply (rule_tac x = "c * ca" in exI)
apply (rule allI)
apply (erule_tac x = x in allE)+
-apply (subgoal_tac "c * ca * abs (f x * g x) = (c * abs(f x)) * (ca * abs (g x))")
+apply (subgoal_tac "c * ca * \<bar>f x * g x\<bar> = (c * \<bar>f x\<bar>) * (ca * \<bar>g x\<bar>)")
apply (metis (no_types) abs_ge_zero abs_mult mult_mono')
by (metis mult.assoc mult.left_commute abs_of_pos mult.left_commute abs_mult)
@@ -466,9 +465,9 @@
simp add: bigo_def elt_set_times_def func_times
simp del: abs_mult ac_simps)
(* sledgehammer *)
- apply (rule_tac x = "ca * (abs c)" in exI)
+ apply (rule_tac x = "ca * \<bar>c\<bar>" in exI)
apply (rule allI)
- apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))")
+ apply (subgoal_tac "ca * \<bar>c\<bar> * \<bar>f x\<bar> = \<bar>c\<bar> * (ca * \<bar>f x\<bar>)")
apply (erule ssubst)
apply (subst abs_mult)
apply (rule mult_left_mono)
@@ -493,10 +492,10 @@
subsection {* Setsum *}
lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 <= h x y \<Longrightarrow>
- \<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) <= c * (h x y) \<Longrightarrow>
+ \<exists>c. \<forall>x. \<forall>y \<in> A x. \<bar>f x y\<bar> <= c * (h x y) \<Longrightarrow>
(\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
apply (auto simp add: bigo_def)
-apply (rule_tac x = "abs c" in exI)
+apply (rule_tac x = "\<bar>c\<bar>" in exI)
apply (subst abs_of_nonneg) back back
apply (rule setsum_nonneg)
apply force
@@ -508,19 +507,19 @@
by (metis abs_ge_self abs_mult_pos order_trans)
lemma bigo_setsum1: "\<forall>x y. 0 <= h x y \<Longrightarrow>
- \<exists>c. \<forall>x y. abs (f x y) <= c * (h x y) \<Longrightarrow>
+ \<exists>c. \<forall>x y. \<bar>f x y\<bar> <= c * (h x y) \<Longrightarrow>
(\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
by (metis (no_types) bigo_setsum_main)
lemma bigo_setsum2: "\<forall>y. 0 <= h y \<Longrightarrow>
- \<exists>c. \<forall>y. abs (f y) <= c * (h y) \<Longrightarrow>
+ \<exists>c. \<forall>y. \<bar>f y\<bar> <= c * (h y) \<Longrightarrow>
(\<lambda>x. SUM y : A x. f y) =o O(\<lambda>x. SUM y : A x. h y)"
apply (rule bigo_setsum1)
by metis+
lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
(\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
- O(\<lambda>x. SUM y : A x. abs(l x y * h(k x y)))"
+ O(\<lambda>x. SUM y : A x. \<bar>l x y * h(k x y)\<bar>)"
apply (rule bigo_setsum1)
apply (rule allI)+
apply (rule abs_ge_zero)
@@ -531,7 +530,7 @@
lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
(\<lambda>x. SUM y : A x. l x y * f(k x y)) =o
(\<lambda>x. SUM y : A x. l x y * g(k x y)) +o
- O(\<lambda>x. SUM y : A x. abs(l x y * h(k x y)))"
+ O(\<lambda>x. SUM y : A x. \<bar>l x y * h(k x y)\<bar>)"
apply (rule set_minus_imp_plus)
apply (subst fun_diff_def)
apply (subst setsum_subtractf [symmetric])
@@ -544,7 +543,7 @@
(\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
O(\<lambda>x. SUM y : A x. (l x y) * h(k x y))"
apply (subgoal_tac "(\<lambda>x. SUM y : A x. (l x y) * h(k x y)) =
- (\<lambda>x. SUM y : A x. abs((l x y) * h(k x y)))")
+ (\<lambda>x. SUM y : A x. \<bar>(l x y) * h(k x y)\<bar>)")
apply (erule ssubst)
apply (erule bigo_setsum3)
apply (rule ext)
@@ -616,14 +615,14 @@
definition lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)" (infixl "<o" 70) where
"f <o g == (\<lambda>x. max (f x - g x) 0)"
-lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) <= abs (f x) \<Longrightarrow>
+lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> <= \<bar>f x\<bar> \<Longrightarrow>
g =o O(h)"
apply (unfold bigo_def)
apply clarsimp
apply (blast intro: order_trans)
done
-lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) <= f x \<Longrightarrow>
+lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> <= f x \<Longrightarrow>
g =o O(h)"
apply (erule bigo_lesseq1)
apply (blast intro: abs_ge_self order_trans)
@@ -638,7 +637,7 @@
done
lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow>
- \<forall>x. 0 <= g x \<Longrightarrow> \<forall>x. g x <= abs (f x) \<Longrightarrow>
+ \<forall>x. 0 <= g x \<Longrightarrow> \<forall>x. g x <= \<bar>f x\<bar> \<Longrightarrow>
g =o O(h)"
apply (erule bigo_lesseq1)
apply (rule allI)
@@ -703,7 +702,7 @@
by (auto simp add: func_plus fun_diff_def algebra_simps
split: split_max abs_split)
-lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x <= g x + C * abs (h x)"
+lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x <= g x + C * \<bar>h x\<bar>"
apply (simp only: lesso_def bigo_alt_def)
apply clarsimp
by (metis add.commute diff_le_eq)
--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Mon Dec 28 01:28:28 2015 +0100
@@ -307,7 +307,7 @@
proof (intro bcontfunI)
fix x
assume "\<And>x. dist (f x) 0 \<le> y"
- then show "dist (a *\<^sub>R f x) 0 \<le> abs a * y"
+ then show "dist (a *\<^sub>R f x) 0 \<le> \<bar>a\<bar> * y"
by (metis norm_cmul_rule_thm norm_conv_dist)
qed (simp add: continuous_intros)
qed
--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Mon Dec 28 01:28:28 2015 +0100
@@ -398,7 +398,7 @@
by transfer (auto simp: algebra_simps setsum_subtractf)
lemma norm_blinfun_of_matrix:
- "norm (blinfun_of_matrix a) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. abs (a i j))"
+ "norm (blinfun_of_matrix a) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>a i j\<bar>)"
apply (rule norm_blinfun_bound)
apply (simp add: setsum_nonneg)
apply (simp only: blinfun_of_matrix_apply setsum_left_distrib)
@@ -413,7 +413,7 @@
proof -
have "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> Zfun (\<lambda>x. norm (b x i j - a i j)) F"
using assms unfolding tendsto_Zfun_iff Zfun_norm_iff .
- hence "Zfun (\<lambda>x. (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. abs (b x i j - a i j))) F"
+ hence "Zfun (\<lambda>x. (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. \<bar>b x i j - a i j\<bar>)) F"
by (auto intro!: Zfun_setsum)
thus ?thesis
unfolding tendsto_Zfun_iff blinfun_of_matrix_minus
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Dec 28 01:28:28 2015 +0100
@@ -1473,7 +1473,7 @@
using kuhn_labelling_lemma[OF *] by blast
note label = this [rule_format]
have lem1: "\<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>i\<in>Basis. label x i \<noteq> label y i \<longrightarrow>
- abs (f x \<bullet> i - x \<bullet> i) \<le> norm (f y - f x) + norm (y - x)"
+ \<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
proof safe
fix x y :: 'a
assume x: "x \<in> unit_cube"
@@ -1481,8 +1481,8 @@
fix i
assume i: "label x i \<noteq> label y i" "i \<in> Basis"
have *: "\<And>x y fx fy :: real. x \<le> fx \<and> fy \<le> y \<or> fx \<le> x \<and> y \<le> fy \<Longrightarrow>
- abs (fx - x) \<le> abs (fy - fx) + abs (y - x)" by auto
- have "\<bar>(f x - x) \<bullet> i\<bar> \<le> abs ((f y - f x)\<bullet>i) + abs ((y - x)\<bullet>i)"
+ \<bar>fx - x\<bar> \<le> \<bar>fy - fx\<bar> + \<bar>y - x\<bar>" by auto
+ have "\<bar>(f x - x) \<bullet> i\<bar> \<le> \<bar>(f y - f x)\<bullet>i\<bar> + \<bar>(y - x)\<bullet>i\<bar>"
unfolding inner_simps
apply (rule *)
apply (cases "label x i = 0")
@@ -1531,7 +1531,7 @@
qed
have "\<exists>e>0. \<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>z\<in>unit_cube. \<forall>i\<in>Basis.
norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<longrightarrow>
- abs ((f(z) - z)\<bullet>i) < d / (real n)"
+ \<bar>(f(z) - z)\<bullet>i\<bar> < d / (real n)"
proof -
have d': "d / real n / 8 > 0"
using d(1) by (simp add: n_def DIM_positive)
@@ -1559,10 +1559,10 @@
"norm (y - z) < min (e / 2) (d / real n / 8)"
"label x i \<noteq> label y i"
assume i: "i \<in> Basis"
- have *: "\<And>z fz x fx n1 n2 n3 n4 d4 d :: real. abs(fx - x) \<le> n1 + n2 \<Longrightarrow>
- abs (fx - fz) \<le> n3 \<Longrightarrow> abs (x - z) \<le> n4 \<Longrightarrow>
+ have *: "\<And>z fz x fx n1 n2 n3 n4 d4 d :: real. \<bar>fx - x\<bar> \<le> n1 + n2 \<Longrightarrow>
+ \<bar>fx - fz\<bar> \<le> n3 \<Longrightarrow> \<bar>x - z\<bar> \<le> n4 \<Longrightarrow>
n1 < d4 \<Longrightarrow> n2 < 2 * d4 \<Longrightarrow> n3 < d4 \<Longrightarrow> n4 < d4 \<Longrightarrow>
- (8 * d4 = d) \<Longrightarrow> abs(fz - z) < d"
+ (8 * d4 = d) \<Longrightarrow> \<bar>fz - z\<bar> < d"
by auto
show "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
unfolding inner_simps
@@ -1669,7 +1669,7 @@
(label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) i"
by (rule kuhn_lemma[OF q1 q2 q3])
def z \<equiv> "(\<Sum>i\<in>Basis. (real (q (b' i)) / real p) *\<^sub>R i)::'a"
- have "\<exists>i\<in>Basis. d / real n \<le> abs ((f z - z)\<bullet>i)"
+ have "\<exists>i\<in>Basis. d / real n \<le> \<bar>(f z - z)\<bullet>i\<bar>"
proof (rule ccontr)
have "\<forall>i\<in>Basis. q (b' i) \<in> {0..p}"
using q(1) b'
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Dec 28 01:28:28 2015 +0100
@@ -792,7 +792,7 @@
dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
-lemma infnorm_cart:"infnorm (x::real^'n) = Sup {abs(x$i) |i. i\<in>UNIV}"
+lemma infnorm_cart:"infnorm (x::real^'n) = Sup {\<bar>x$i\<bar> |i. i\<in>UNIV}"
by (simp add: infnorm_def inner_axis Basis_vec_def) (metis (lifting) inner_axis real_inner_1_right)
lemma component_le_infnorm_cart: "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)"
@@ -1243,10 +1243,10 @@
lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
by (simp add: norm_vec_def)
-lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"
+lemma norm_real: "norm(x::real ^ 1) = \<bar>x$1\<bar>"
by (simp add: norm_vector_1)
-lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))"
+lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x$1) - (y$1)\<bar>"
by (auto simp add: norm_real dist_norm)
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Dec 28 01:28:28 2015 +0100
@@ -3862,7 +3862,7 @@
lemma winding_number_big_meets:
fixes z::complex
- assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>" and "abs (Re (winding_number \<gamma> z)) \<ge> 1"
+ assumes \<gamma>: "valid_path \<gamma>" and z: "z \<notin> path_image \<gamma>" and "\<bar>Re (winding_number \<gamma> z)\<bar> \<ge> 1"
and w: "w \<noteq> z"
shows "\<exists>a::real. 0 < a \<and> z + a*(w - z) \<in> path_image \<gamma>"
proof -
@@ -3888,7 +3888,7 @@
shows
"\<lbrakk>valid_path \<gamma>; z \<notin> path_image \<gamma>; w \<noteq> z;
\<And>a::real. 0 < a \<Longrightarrow> z + a*(w - z) \<notin> path_image \<gamma>\<rbrakk>
- \<Longrightarrow> abs (Re(winding_number \<gamma> z)) < 1"
+ \<Longrightarrow> \<bar>Re(winding_number \<gamma> z)\<bar> < 1"
by (auto simp: not_less dest: winding_number_big_meets)
text\<open>One way of proving that WN=1 for a loop.\<close>
@@ -4319,7 +4319,7 @@
{ assume wnz_12: "\<bar>Re (winding_number \<gamma> z)\<bar> > 1/2"
have "isCont (winding_number \<gamma>) z"
by (metis continuous_at_winding_number valid_path_imp_path \<gamma> z)
- then obtain d where "d>0" and d: "\<And>x'. dist x' z < d \<Longrightarrow> dist (winding_number \<gamma> x') (winding_number \<gamma> z) < abs(Re(winding_number \<gamma> z)) - 1/2"
+ then obtain d where "d>0" and d: "\<And>x'. dist x' z < d \<Longrightarrow> dist (winding_number \<gamma> x') (winding_number \<gamma> z) < \<bar>Re(winding_number \<gamma> z)\<bar> - 1/2"
using continuous_at_eps_delta wnz_12 diff_gt_0_iff_gt by blast
def z' \<equiv> "z - (d / (2 * cmod a)) *\<^sub>R a"
have *: "a \<bullet> z' \<le> b - d / 3 * cmod a"
@@ -4479,7 +4479,7 @@
done
}
then have "\<exists>e. 0 < e \<and>
- (\<forall>t1 t2. t1 \<in> {0..1} \<and> t2 \<in> {0..1} \<and> abs(t1 - t) < e \<and> abs(t2 - t) < e
+ (\<forall>t1 t2. t1 \<in> {0..1} \<and> t2 \<in> {0..1} \<and> \<bar>t1 - t\<bar> < e \<and> \<bar>t2 - t\<bar> < e
\<longrightarrow> (\<exists>d. 0 < d \<and>
(\<forall>g1 g2. valid_path g1 \<and> valid_path g2 \<and>
(\<forall>u \<in> {0..1}.
@@ -4490,7 +4490,7 @@
}
then obtain ee where ee:
"\<And>t. t \<in> {0..1} \<Longrightarrow> ee t > 0 \<and>
- (\<forall>t1 t2. t1 \<in> {0..1} \<longrightarrow> t2 \<in> {0..1} \<longrightarrow> abs(t1 - t) < ee t \<longrightarrow> abs(t2 - t) < ee t
+ (\<forall>t1 t2. t1 \<in> {0..1} \<longrightarrow> t2 \<in> {0..1} \<longrightarrow> \<bar>t1 - t\<bar> < ee t \<longrightarrow> \<bar>t2 - t\<bar> < ee t
\<longrightarrow> (\<exists>d. 0 < d \<and>
(\<forall>g1 g2. valid_path g1 \<and> valid_path g2 \<and>
(\<forall>u \<in> {0..1}.
@@ -4867,7 +4867,7 @@
with assms show ?thesis by simp
next
case 2
- have [simp]: "abs r = r" using \<open>r > 0\<close> by linarith
+ have [simp]: "\<bar>r\<bar> = r" using \<open>r > 0\<close> by linarith
have [simp]: "cmod (complex_of_real t - complex_of_real s) = t-s"
by (metis "2" abs_of_pos diff_gt_0_iff_gt norm_of_real of_real_diff)
have "finite (part_circlepath z r s t -` {y} \<inter> {0..1})" if "y \<in> k" for y
@@ -4940,7 +4940,7 @@
qed
proposition simple_path_part_circlepath:
- "simple_path(part_circlepath z r s t) \<longleftrightarrow> (r \<noteq> 0 \<and> s \<noteq> t \<and> abs(s - t) \<le> 2*pi)"
+ "simple_path(part_circlepath z r s t) \<longleftrightarrow> (r \<noteq> 0 \<and> s \<noteq> t \<and> \<bar>s - t\<bar> \<le> 2*pi)"
proof (cases "r = 0 \<or> s = t")
case True
then show ?thesis
@@ -4952,17 +4952,17 @@
have *: "\<And>x y z s t. ii*((1 - x) * s + x * t) = ii*(((1 - y) * s + y * t)) + z \<longleftrightarrow> ii*(x - y) * (t - s) = z"
by (simp add: algebra_simps)
have abs01: "\<And>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1
- \<Longrightarrow> (x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0 \<longleftrightarrow> abs(x - y) \<in> {0,1})"
+ \<Longrightarrow> (x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0 \<longleftrightarrow> \<bar>x - y\<bar> \<in> {0,1})"
by auto
- have abs_away: "\<And>P. (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. P(abs(x - y))) \<longleftrightarrow> (\<forall>x::real. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> P x)"
+ have abs_away: "\<And>P. (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. P \<bar>x - y\<bar>) \<longleftrightarrow> (\<forall>x::real. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> P x)"
by force
have **: "\<And>x y. (\<exists>n. (complex_of_real x - of_real y) * (of_real t - of_real s) = 2 * (of_int n * of_real pi)) \<longleftrightarrow>
- (\<exists>n. abs(x - y) * (t - s) = 2 * (of_int n * pi))"
+ (\<exists>n. \<bar>x - y\<bar> * (t - s) = 2 * (of_int n * pi))"
by (force simp: algebra_simps abs_if dest: arg_cong [where f=Re] arg_cong [where f=complex_of_real]
intro: exI [where x = "-n" for n])
have 1: "\<forall>x. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> (\<exists>n. x * (t - s) = 2 * (real_of_int n * pi)) \<longrightarrow> x = 0 \<or> x = 1 \<Longrightarrow> \<bar>s - t\<bar> \<le> 2 * pi"
apply (rule ccontr)
- apply (drule_tac x="2*pi / abs(t-s)" in spec)
+ apply (drule_tac x="2*pi / \<bar>t - s\<bar>" in spec)
using False
apply (simp add: abs_minus_commute divide_simps)
apply (frule_tac x=1 in spec)
@@ -4986,7 +4986,7 @@
qed
proposition arc_part_circlepath:
- assumes "r \<noteq> 0" "s \<noteq> t" "abs(s - t) < 2*pi"
+ assumes "r \<noteq> 0" "s \<noteq> t" "\<bar>s - t\<bar> < 2*pi"
shows "arc (part_circlepath z r s t)"
proof -
have *: "x = y" if eq: "\<i> * (linepath s t x) = \<i> * (linepath s t y) + 2 * of_int n * complex_of_real pi * \<i>"
@@ -5111,7 +5111,7 @@
qed
proposition path_image_circlepath [simp]:
- "path_image (circlepath z r) = sphere z (abs r)"
+ "path_image (circlepath z r) = sphere z \<bar>r\<bar>"
using path_image_circlepath_minus
by (force simp add: path_image_circlepath_nonneg abs_if)
@@ -6163,7 +6163,7 @@
with inf [unfolded Lim_at_infinity, rule_format, of "norm(f z)/2"]
obtain B where B: "\<And>x. B \<le> cmod x \<Longrightarrow> norm (f x) * 2 < cmod (f z)"
by (auto simp: dist_norm)
- def R \<equiv> "1 + abs B + norm z"
+ def R \<equiv> "1 + \<bar>B\<bar> + norm z"
have "R > 0" unfolding R_def by (meson abs_add_one_gt_zero le_less_trans less_add_same_cancel2 norm_ge_zero)
have *: "((\<lambda>u. f u / (u - z)) has_contour_integral 2 * complex_of_real pi * \<i> * f z) (circlepath z R)"
apply (rule Cauchy_integral_circlepath)
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Dec 28 01:28:28 2015 +0100
@@ -8,7 +8,7 @@
lemma cmod_add_real_less:
assumes "Im z \<noteq> 0" "r\<noteq>0"
- shows "cmod (z + r) < cmod z + abs r"
+ shows "cmod (z + r) < cmod z + \<bar>r\<bar>"
proof (cases z)
case (Complex x y)
have "r * x / \<bar>r\<bar> < sqrt (x*x + y*y)"
@@ -23,7 +23,7 @@
done
qed
-lemma cmod_diff_real_less: "Im z \<noteq> 0 \<Longrightarrow> x\<noteq>0 \<Longrightarrow> cmod (z - x) < cmod z + abs x"
+lemma cmod_diff_real_less: "Im z \<noteq> 0 \<Longrightarrow> x\<noteq>0 \<Longrightarrow> cmod (z - x) < cmod z + \<bar>x\<bar>"
using cmod_add_real_less [of z "-x"]
by simp
@@ -205,7 +205,7 @@
finally show ?thesis .
qed
-lemma exp_complex_eqI: "abs(Im w - Im z) < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
+lemma exp_complex_eqI: "\<bar>Im w - Im z\<bar> < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
by (auto simp: exp_eq abs_mult)
lemma exp_integer_2pi:
@@ -361,7 +361,7 @@
finally show ?thesis .
qed
-lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * abs(sin(t / 2))"
+lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * \<bar>sin(t / 2)\<bar>"
apply (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps)
using cos_double_sin [of "t/2"]
apply (simp add: real_sqrt_mult)
@@ -579,7 +579,7 @@
declare power_Suc [simp]
text\<open>32-bit Approximation to e\<close>
-lemma e_approx_32: "abs(exp(1) - 5837465777 / 2147483648) \<le> (inverse(2 ^ 32)::real)"
+lemma e_approx_32: "\<bar>exp(1) - 5837465777 / 2147483648\<bar> \<le> (inverse(2 ^ 32)::real)"
using Taylor_exp [of 1 14] exp_le
apply (simp add: setsum_left_distrib in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
apply (simp only: pos_le_divide_eq [symmetric], linarith)
@@ -1055,14 +1055,14 @@
lemma Re_Ln_pos_lt:
assumes "z \<noteq> 0"
- shows "abs(Im(Ln z)) < pi/2 \<longleftrightarrow> 0 < Re(z)"
+ shows "\<bar>Im(Ln z)\<bar> < pi/2 \<longleftrightarrow> 0 < Re(z)"
proof -
{ fix w
assume "w = Ln z"
then have w: "Im w \<le> pi" "- pi < Im w"
using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
by auto
- then have "abs(Im w) < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
+ then have "\<bar>Im w\<bar> < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
apply (auto simp: Re_exp zero_less_mult_iff cos_gt_zero_pi)
using cos_lt_zero_pi [of "-(Im w)"] cos_lt_zero_pi [of "(Im w)"]
apply (simp add: abs_if split: split_if_asm)
@@ -1077,14 +1077,14 @@
lemma Re_Ln_pos_le:
assumes "z \<noteq> 0"
- shows "abs(Im(Ln z)) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)"
+ shows "\<bar>Im(Ln z)\<bar> \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)"
proof -
{ fix w
assume "w = Ln z"
then have w: "Im w \<le> pi" "- pi < Im w"
using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
by auto
- then have "abs(Im w) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(exp w)"
+ then have "\<bar>Im w\<bar> \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(exp w)"
apply (auto simp: Re_exp zero_le_mult_iff cos_ge_zero)
using cos_lt_zero_pi [of "- (Im w)"] cos_lt_zero_pi [of "(Im w)"] not_le
apply (auto simp: abs_if split: split_if_asm)
@@ -1132,7 +1132,7 @@
by auto
qed
-lemma Re_Ln_pos_lt_imp: "0 < Re(z) \<Longrightarrow> abs(Im(Ln z)) < pi/2"
+lemma Re_Ln_pos_lt_imp: "0 < Re(z) \<Longrightarrow> \<bar>Im(Ln z)\<bar> < pi/2"
by (metis Re_Ln_pos_lt less_irrefl zero_complex.simps(1))
lemma Im_Ln_pos_lt_imp: "0 < Im(z) \<Longrightarrow> 0 < Im(Ln z) \<and> Im(Ln z) < pi"
@@ -1834,7 +1834,7 @@
assumes "\<bar>Re z\<bar> < pi/2"
shows "Arctan(tan z) = z"
proof -
- have ge_pi2: "\<And>n::int. abs (of_int (2*n + 1) * pi/2) \<ge> pi/2"
+ have ge_pi2: "\<And>n::int. \<bar>of_int (2*n + 1) * pi/2\<bar> \<ge> pi/2"
by (case_tac n rule: int_cases) (auto simp: abs_mult)
have "exp (\<i>*z)*exp (\<i>*z) = -1 \<longleftrightarrow> exp (2*\<i>*z) = -1"
by (metis distrib_right exp_add mult_2)
@@ -1863,8 +1863,8 @@
qed
lemma
- assumes "Re z = 0 \<Longrightarrow> abs(Im z) < 1"
- shows Re_Arctan_bounds: "abs(Re(Arctan z)) < pi/2"
+ assumes "Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1"
+ shows Re_Arctan_bounds: "\<bar>Re(Arctan z)\<bar> < pi/2"
and has_field_derivative_Arctan: "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)"
proof -
have nz0: "1 + \<i>*z \<noteq> 0"
@@ -1889,7 +1889,7 @@
using assms
apply (auto simp: algebra_simps abs_square_less_1 [unfolded power2_eq_square])
done
- show "abs(Re(Arctan z)) < pi/2"
+ show "\<bar>Re(Arctan z)\<bar> < pi/2"
unfolding Arctan_def divide_complex_def
using mpi_less_Im_Ln [OF nzi]
by (auto simp: abs_if intro: Im_Ln_less_pi * [unfolded divide_complex_def])
@@ -1903,31 +1903,31 @@
done
qed
-lemma complex_differentiable_at_Arctan: "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> Arctan complex_differentiable at z"
+lemma complex_differentiable_at_Arctan: "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan complex_differentiable at z"
using has_field_derivative_Arctan
by (auto simp: complex_differentiable_def)
lemma complex_differentiable_within_Arctan:
- "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> Arctan complex_differentiable (at z within s)"
+ "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan complex_differentiable (at z within s)"
using complex_differentiable_at_Arctan complex_differentiable_at_within by blast
declare has_field_derivative_Arctan [derivative_intros]
declare has_field_derivative_Arctan [THEN DERIV_chain2, derivative_intros]
lemma continuous_at_Arctan:
- "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> continuous (at z) Arctan"
+ "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous (at z) Arctan"
by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Arctan)
lemma continuous_within_Arctan:
- "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> continuous (at z within s) Arctan"
+ "(Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arctan"
using continuous_at_Arctan continuous_at_imp_continuous_within by blast
lemma continuous_on_Arctan [continuous_intros]:
- "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> abs \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous_on s Arctan"
+ "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous_on s Arctan"
by (auto simp: continuous_at_imp_continuous_on continuous_within_Arctan)
lemma holomorphic_on_Arctan:
- "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> abs \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan holomorphic_on s"
+ "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan holomorphic_on s"
by (simp add: complex_differentiable_within_Arctan holomorphic_on_def)
@@ -1988,17 +1988,17 @@
lemma arctan_less_pi4_neg: "-1 < x \<Longrightarrow> -(pi/4) < arctan x"
by (metis arctan_less_iff arctan_minus arctan_one)
-lemma arctan_less_pi4: "abs x < 1 \<Longrightarrow> abs(arctan x) < pi/4"
+lemma arctan_less_pi4: "\<bar>x\<bar> < 1 \<Longrightarrow> \<bar>arctan x\<bar> < pi/4"
by (metis abs_less_iff arctan_less_pi4_pos arctan_minus)
-lemma arctan_le_pi4: "abs x \<le> 1 \<Longrightarrow> abs(arctan x) \<le> pi/4"
+lemma arctan_le_pi4: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>arctan x\<bar> \<le> pi/4"
by (metis abs_le_iff arctan_le_iff arctan_minus arctan_one)
-lemma abs_arctan: "abs(arctan x) = arctan(abs x)"
+lemma abs_arctan: "\<bar>arctan x\<bar> = arctan \<bar>x\<bar>"
by (simp add: abs_if arctan_minus)
lemma arctan_add_raw:
- assumes "abs(arctan x + arctan y) < pi/2"
+ assumes "\<bar>arctan x + arctan y\<bar> < pi/2"
shows "arctan x + arctan y = arctan((x + y) / (1 - x * y))"
proof (rule arctan_unique [symmetric])
show 12: "- (pi / 2) < arctan x + arctan y" "arctan x + arctan y < pi / 2"
@@ -2027,7 +2027,7 @@
qed
lemma arctan_add_small:
- assumes "abs(x * y) < 1"
+ assumes "\<bar>x * y\<bar> < 1"
shows "(arctan x + arctan y = arctan((x + y) / (1 - x * y)))"
proof (cases "x = 0 \<or> y = 0")
case True then show ?thesis
@@ -2044,7 +2044,7 @@
qed
lemma abs_arctan_le:
- fixes x::real shows "abs(arctan x) \<le> abs x"
+ fixes x::real shows "\<bar>arctan x\<bar> \<le> \<bar>x\<bar>"
proof -
{ fix w::complex and z::complex
assume *: "w \<in> \<real>" "z \<in> \<real>"
@@ -2064,7 +2064,7 @@
lemma arctan_le_self: "0 \<le> x \<Longrightarrow> arctan x \<le> x"
by (metis abs_arctan_le abs_of_nonneg zero_le_arctan_iff)
-lemma abs_tan_ge: "abs x < pi/2 \<Longrightarrow> abs x \<le> abs(tan x)"
+lemma abs_tan_ge: "\<bar>x\<bar> < pi/2 \<Longrightarrow> \<bar>x\<bar> \<le> \<bar>tan x\<bar>"
by (metis abs_arctan_le abs_less_iff arctan_tan minus_less_iff)
@@ -2078,7 +2078,7 @@
apply auto
by (metis complex_i_mult_minus diff_add_cancel diff_minus_eq_add diff_self mult.assoc mult.left_commute numeral_One power2_csqrt power2_eq_square zero_neq_numeral)
-lemma Arcsin_range_lemma: "abs (Re z) < 1 \<Longrightarrow> 0 < Re(\<i> * z + csqrt(1 - z\<^sup>2))"
+lemma Arcsin_range_lemma: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Re(\<i> * z + csqrt(1 - z\<^sup>2))"
using Complex.cmod_power2 [of z, symmetric]
by (simp add: real_less_rsqrt algebra_simps Re_power2 cmod_square_less_1_plus)
@@ -2393,7 +2393,7 @@
subsection\<open>Upper and Lower Bounds for Inverse Sine and Cosine\<close>
-lemma Arcsin_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> abs(Re(Arcsin z)) < pi/2"
+lemma Arcsin_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> \<bar>Re(Arcsin z)\<bar> < pi/2"
unfolding Re_Arcsin
by (blast intro: Re_Ln_pos_lt_imp Arcsin_range_lemma)
@@ -2405,14 +2405,14 @@
unfolding Re_Arccos
by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arccos_body_lemma)
-lemma Re_Arccos_bound: "abs(Re(Arccos z)) \<le> pi"
+lemma Re_Arccos_bound: "\<bar>Re(Arccos z)\<bar> \<le> pi"
by (meson Re_Arccos_bounds abs_le_iff less_eq_real_def minus_less_iff)
lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \<le> pi"
unfolding Re_Arcsin
by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma)
-lemma Re_Arcsin_bound: "abs(Re(Arcsin z)) \<le> pi"
+lemma Re_Arcsin_bound: "\<bar>Re(Arcsin z)\<bar> \<le> pi"
by (meson Re_Arcsin_bounds abs_le_iff less_eq_real_def minus_less_iff)
@@ -2521,7 +2521,7 @@
subsection\<open>Relationship with Arcsin on the Real Numbers\<close>
lemma Im_Arcsin_of_real:
- assumes "abs x \<le> 1"
+ assumes "\<bar>x\<bar> \<le> 1"
shows "Im (Arcsin (of_real x)) = 0"
proof -
have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
@@ -2539,7 +2539,7 @@
by (metis Im_Arcsin_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
lemma arcsin_eq_Re_Arcsin:
- assumes "abs x \<le> 1"
+ assumes "\<bar>x\<bar> \<le> 1"
shows "arcsin x = Re (Arcsin (of_real x))"
unfolding arcsin_def
proof (rule the_equality, safe)
@@ -2564,14 +2564,14 @@
done
qed
-lemma of_real_arcsin: "abs x \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)"
+lemma of_real_arcsin: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)"
by (metis Im_Arcsin_of_real add.right_neutral arcsin_eq_Re_Arcsin complex_eq mult_zero_right of_real_0)
subsection\<open>Relationship with Arccos on the Real Numbers\<close>
lemma Im_Arccos_of_real:
- assumes "abs x \<le> 1"
+ assumes "\<bar>x\<bar> \<le> 1"
shows "Im (Arccos (of_real x)) = 0"
proof -
have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
@@ -2589,7 +2589,7 @@
by (metis Im_Arccos_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
lemma arccos_eq_Re_Arccos:
- assumes "abs x \<le> 1"
+ assumes "\<bar>x\<bar> \<le> 1"
shows "arccos x = Re (Arccos (of_real x))"
unfolding arccos_def
proof (rule the_equality, safe)
@@ -2614,7 +2614,7 @@
done
qed
-lemma of_real_arccos: "abs x \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
+lemma of_real_arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
subsection\<open>Some interrelationships among the real inverse trig functions.\<close>
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Dec 28 01:28:28 2015 +0100
@@ -3328,13 +3328,13 @@
ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x \<in> affine hull S"
using as affine_affine_hull[of S] mem_affine[of "affine hull S" y x "(1 / e)" "-((1 - e) / e)"]
by (simp add: algebra_simps)
- have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
+ have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = \<bar>1/e\<bar> * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
unfolding dist_norm norm_scaleR[symmetric]
apply (rule arg_cong[where f=norm])
using \<open>e > 0\<close>
apply (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
done
- also have "\<dots> = abs (1/e) * norm (x - e *\<^sub>R (x - c) - y)"
+ also have "\<dots> = \<bar>1/e\<bar> * norm (x - e *\<^sub>R (x - c) - y)"
by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
also have "\<dots> < d"
using as[unfolded dist_norm] and \<open>e > 0\<close>
@@ -6076,15 +6076,15 @@
fixes s :: "('a::real_normed_vector) set"
assumes "open s"
and "convex_on s f"
- and "\<forall>x\<in>s. abs(f x) \<le> b"
+ and "\<forall>x\<in>s. \<bar>f x\<bar> \<le> b"
shows "continuous_on s f"
apply (rule continuous_at_imp_continuous_on)
unfolding continuous_at_real_range
proof (rule,rule,rule)
fix x and e :: real
assume "x \<in> s" "e > 0"
- def B \<equiv> "abs b + 1"
- have B: "0 < B" "\<And>x. x\<in>s \<Longrightarrow> abs (f x) \<le> B"
+ def B \<equiv> "\<bar>b\<bar> + 1"
+ have B: "0 < B" "\<And>x. x\<in>s \<Longrightarrow> \<bar>f x\<bar> \<le> B"
unfolding B_def
defer
apply (drule assms(3)[rule_format])
@@ -6193,7 +6193,7 @@
fixes x :: "'a::real_normed_vector"
assumes "convex_on (cball x e) f"
and "\<forall>y \<in> cball x e. f y \<le> b"
- shows "\<forall>y \<in> cball x e. abs (f y) \<le> b + 2 * abs (f x)"
+ shows "\<forall>y \<in> cball x e. \<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>"
apply rule
proof (cases "0 \<le> e")
case True
@@ -6310,7 +6310,7 @@
apply (rule e(1))
apply (rule dsube)
done
- then have "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)"
+ then have "\<forall>y\<in>cball x d. \<bar>f y\<bar> \<le> k + 2 * \<bar>f x\<bar>"
apply (rule convex_bounds_lemma)
apply (rule ballI)
apply (rule k [rule_format])
@@ -6751,13 +6751,13 @@
assume as: "dist (x - e *\<^sub>R (x - c)) y < e * d"
have *: "y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x"
using \<open>e > 0\<close> by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
- have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
+ have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = \<bar>1/e\<bar> * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
unfolding dist_norm
unfolding norm_scaleR[symmetric]
apply (rule arg_cong[where f=norm])
using \<open>e > 0\<close>
by (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
- also have "\<dots> = abs (1/e) * norm (x - e *\<^sub>R (x - c) - y)"
+ also have "\<dots> = \<bar>1/e\<bar> * norm (x - e *\<^sub>R (x - c) - y)"
by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
also have "\<dots> < d"
using as[unfolded dist_norm] and \<open>e > 0\<close>
@@ -7001,7 +7001,7 @@
proof (rule setsum_mono)
fix i :: 'a
assume i: "i \<in> Basis"
- then have "abs (y\<bullet>i - x\<bullet>i) < ?d"
+ then have "\<bar>y\<bullet>i - x\<bullet>i\<bar> < ?d"
apply -
apply (rule le_less_trans)
using Basis_le_norm[OF i, of "y - x"]
@@ -7186,7 +7186,7 @@
assume "i \<in> d"
with d have i: "i \<in> Basis"
by auto
- have "abs (y\<bullet>i - x\<bullet>i) < ?d"
+ have "\<bar>y\<bullet>i - x\<bullet>i\<bar> < ?d"
apply (rule le_less_trans)
using Basis_le_norm[OF i, of "y - x"]
using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2]
@@ -9860,7 +9860,7 @@
lemma setdist_singletons [simp]: "setdist {x} {y} = dist x y"
by (simp add: setdist_def)
-lemma setdist_Lipschitz: "abs(setdist {x} s - setdist {y} s) \<le> dist x y"
+lemma setdist_Lipschitz: "\<bar>setdist {x} s - setdist {y} s\<bar> \<le> dist x y"
apply (subst setdist_singletons [symmetric])
by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym)
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Dec 28 01:28:28 2015 +0100
@@ -372,7 +372,7 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes "(f has_derivative f') (at x within s)"
and "(f has_derivative f'') (at x within s)"
- and "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < abs d \<and> abs d < e \<and> (x + d *\<^sub>R i) \<in> s"
+ and "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> (x + d *\<^sub>R i) \<in> s"
shows "f' = f''"
proof -
note as = assms(1,2)[unfolded has_derivative_def]
@@ -415,9 +415,9 @@
obtain c where c: "0 < \<bar>c\<bar>" "\<bar>c\<bar> < d \<and> x + c *\<^sub>R i \<in> s"
using assms(3) i d(1) by blast
have *: "norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R i)) =
- norm ((1 / abs c) *\<^sub>R (- (f' (c *\<^sub>R i)) + f'' (c *\<^sub>R i)))"
+ norm ((1 / \<bar>c\<bar>) *\<^sub>R (- (f' (c *\<^sub>R i)) + f'' (c *\<^sub>R i)))"
unfolding scaleR_right_distrib by auto
- also have "\<dots> = norm ((1 / abs c) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))"
+ also have "\<dots> = norm ((1 / \<bar>c\<bar>) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))"
unfolding f'.scaleR f''.scaleR
unfolding scaleR_right_distrib scaleR_minus_right
by auto
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Mon Dec 28 01:28:28 2015 +0100
@@ -82,19 +82,19 @@
lemma infnorm_2:
fixes x :: "real^2"
- shows "infnorm x = max (abs (x$1)) (abs (x$2))"
+ shows "infnorm x = max \<bar>x$1\<bar> \<bar>x$2\<bar>"
unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto
lemma infnorm_eq_1_2:
fixes x :: "real^2"
shows "infnorm x = 1 \<longleftrightarrow>
- abs (x$1) \<le> 1 \<and> abs (x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1)"
+ \<bar>x$1\<bar> \<le> 1 \<and> \<bar>x$2\<bar> \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1)"
unfolding infnorm_2 by auto
lemma infnorm_eq_1_imp:
fixes x :: "real^2"
assumes "infnorm x = 1"
- shows "abs (x$1) \<le> 1" and "abs (x$2) \<le> 1"
+ shows "\<bar>x$1\<bar> \<le> 1" and "\<bar>x$2\<bar> \<le> 1"
using assms unfolding infnorm_eq_1_2 by auto
lemma fashoda_unit:
--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Dec 28 01:28:28 2015 +0100
@@ -499,7 +499,7 @@
lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
by (auto simp: interval_upperbound_def interval_lowerbound_def SUP_def INF_def content_def)
-lemma abs_eq_content: "abs (y - x) = (if x\<le>y then content {x .. y} else content {y..x})"
+lemma abs_eq_content: "\<bar>y - x\<bar> = (if x\<le>y then content {x .. y} else content {y..x})"
by (auto simp: content_real)
lemma content_singleton[simp]: "content {a} = 0"
@@ -2116,7 +2116,7 @@
proof (rule exI [where x=n], clarify)
fix x y
assume xy: "x\<in>cbox (A n) (B n)" "y\<in>cbox (A n) (B n)"
- have "dist x y \<le> setsum (\<lambda>i. abs((x - y)\<bullet>i)) Basis"
+ have "dist x y \<le> setsum (\<lambda>i. \<bar>(x - y)\<bullet>i\<bar>) Basis"
unfolding dist_norm by(rule norm_le_l1)
also have "\<dots> \<le> setsum (\<lambda>i. B n\<bullet>i - A n\<bullet>i) Basis"
proof (rule setsum_mono)
@@ -3140,7 +3140,7 @@
apply (rule has_integralD[OF fj[unfolded interval_split[OF k]] e])
apply (simp add: interval_split[symmetric] k)
done
- let ?d = "\<lambda>x. if x\<bullet>k = c then (d1 x \<inter> d2 x) else ball x (abs(x\<bullet>k - c)) \<inter> d1 x \<inter> d2 x"
+ let ?d = "\<lambda>x. if x\<bullet>k = c then (d1 x \<inter> d2 x) else ball x \<bar>x\<bullet>k - c\<bar> \<inter> d1 x \<inter> d2 x"
have "gauge ?d"
using d1 d2 unfolding gauge_def by auto
then show ?case
@@ -4659,11 +4659,11 @@
lemma interval_doublesplit:
fixes a :: "'a::euclidean_space"
assumes "k \<in> Basis"
- shows "cbox a b \<inter> {x . abs(x\<bullet>k - c) \<le> (e::real)} =
+ shows "cbox a b \<inter> {x . \<bar>x\<bullet>k - c\<bar> \<le> (e::real)} =
cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) (c - e) else a\<bullet>i) *\<^sub>R i)
(\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) (c + e) else b\<bullet>i) *\<^sub>R i)"
proof -
- have *: "\<And>x c e::real. abs(x - c) \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
+ have *: "\<And>x c e::real. \<bar>x - c\<bar> \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
by auto
have **: "\<And>s P Q. s \<inter> {x. P x \<and> Q x} = (s \<inter> {x. Q x}) \<inter> {x. P x}"
by blast
@@ -4675,10 +4675,10 @@
fixes a :: "'a::euclidean_space"
assumes "p division_of (cbox a b)"
and k: "k \<in> Basis"
- shows "{l \<inter> {x. abs(x\<bullet>k - c) \<le> e} |l. l \<in> p \<and> l \<inter> {x. abs(x\<bullet>k - c) \<le> e} \<noteq> {}}
- division_of (cbox a b \<inter> {x. abs(x\<bullet>k - c) \<le> e})"
-proof -
- have *: "\<And>x c. abs (x - c) \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
+ shows "{l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e} |l. l \<in> p \<and> l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e} \<noteq> {}}
+ division_of (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e})"
+proof -
+ have *: "\<And>x c. \<bar>x - c\<bar> \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
by auto
have **: "\<And>p q p' q'. p division_of q \<Longrightarrow> p = p' \<Longrightarrow> q = q' \<Longrightarrow> p' division_of q'"
by auto
@@ -4700,7 +4700,7 @@
fixes a :: "'a::euclidean_space"
assumes "0 < e"
and k: "k \<in> Basis"
- obtains d where "0 < d" and "content (cbox a b \<inter> {x. abs(x\<bullet>k - c) \<le> d}) < e"
+ obtains d where "0 < d" and "content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) < e"
proof (cases "content (cbox a b) = 0")
case True
then have ce: "content (cbox a b) < e"
@@ -4780,7 +4780,7 @@
fix p
assume p: "p tagged_division_of (cbox a b) \<and> (\<lambda>x. ball x d) fine p"
have *: "(\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) =
- (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. abs(x\<bullet>k - c) \<le> d}) *\<^sub>R ?i x)"
+ (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) *\<^sub>R ?i x)"
apply (rule setsum.cong)
apply (rule refl)
unfolding split_paired_all real_scaleR_def mult_cancel_right split_conv
@@ -6695,7 +6695,7 @@
lemma content_image_affinity_cbox:
"content((\<lambda>x::'a::euclidean_space. m *\<^sub>R x + c) ` cbox a b) =
- abs m ^ DIM('a) * content (cbox a b)" (is "?l = ?r")
+ \<bar>m\<bar> ^ DIM('a) * content (cbox a b)" (is "?l = ?r")
proof -
{
presume *: "cbox a b \<noteq> {} \<Longrightarrow> ?thesis"
@@ -6743,7 +6743,7 @@
fixes a :: "'a::euclidean_space"
assumes "(f has_integral i) (cbox a b)"
and "m \<noteq> 0"
- shows "((\<lambda>x. f(m *\<^sub>R x + c)) has_integral ((1 / (abs(m) ^ DIM('a))) *\<^sub>R i)) ((\<lambda>x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` cbox a b)"
+ shows "((\<lambda>x. f(m *\<^sub>R x + c)) has_integral ((1 / (\<bar>m\<bar> ^ DIM('a))) *\<^sub>R i)) ((\<lambda>x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` cbox a b)"
apply (rule has_integral_twiddle)
using assms
apply (safe intro!: interval_image_affinity_interval content_image_affinity_cbox)
@@ -6807,7 +6807,7 @@
lemma content_image_stretch_interval:
"content ((\<lambda>x::'a::euclidean_space. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)::'a) ` cbox a b) =
- abs (setprod m Basis) * content (cbox a b)"
+ \<bar>setprod m Basis\<bar> * content (cbox a b)"
proof (cases "cbox a b = {}")
case True
then show ?thesis
@@ -6847,7 +6847,7 @@
assumes "(f has_integral i) (cbox a b)"
and "\<forall>k\<in>Basis. m k \<noteq> 0"
shows "((\<lambda>x. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) has_integral
- ((1/(abs(setprod m Basis))) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
+ ((1/ \<bar>setprod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
apply (rule has_integral_twiddle[where f=f])
unfolding zero_less_abs_iff content_image_stretch_interval
unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
@@ -8829,8 +8829,8 @@
unfolding fine_inter
proof (safe, goal_cases)
have **: "\<And>i j g1 g2 h1 h2 f1 f2. g1 - h2 \<le> f1 - f2 \<Longrightarrow> f1 - f2 \<le> h1 - g2 \<Longrightarrow>
- abs (i - j) < e / 3 \<Longrightarrow> abs (g2 - i) < e / 3 \<Longrightarrow> abs (g1 - i) < e / 3 \<Longrightarrow>
- abs (h2 - j) < e / 3 \<Longrightarrow> abs (h1 - j) < e / 3 \<Longrightarrow> abs (f1 - f2) < e"
+ \<bar>i - j\<bar> < e / 3 \<Longrightarrow> \<bar>g2 - i\<bar> < e / 3 \<Longrightarrow> \<bar>g1 - i\<bar> < e / 3 \<Longrightarrow>
+ \<bar>h2 - j\<bar> < e / 3 \<Longrightarrow> \<bar>h1 - j\<bar> < e / 3 \<Longrightarrow> \<bar>f1 - f2\<bar> < e"
using \<open>e > 0\<close> by arith
case prems: (1 p1 p2)
note tagged_division_ofD(2-4) note * = this[OF prems(1)] this[OF prems(4)]
@@ -8996,9 +8996,9 @@
have **: "ball 0 B1 \<subseteq> ball (0::'n) (max B1 B2)" "ball 0 B2 \<subseteq> ball (0::'n) (max B1 B2)"
by auto
have *: "\<And>ga gc ha hc fa fc::real.
- abs (ga - i) < e / 3 \<and> abs (gc - i) < e / 3 \<and> abs (ha - j) < e / 3 \<and>
- abs (hc - j) < e / 3 \<and> abs (i - j) < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc \<Longrightarrow>
- abs (fa - fc) < e"
+ \<bar>ga - i\<bar> < e / 3 \<and> \<bar>gc - i\<bar> < e / 3 \<and> \<bar>ha - j\<bar> < e / 3 \<and>
+ \<bar>hc - j\<bar> < e / 3 \<and> \<bar>i - j\<bar> < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc \<Longrightarrow>
+ \<bar>fa - fc\<bar> < e"
by (simp add: abs_real_def split: split_if_asm)
show "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f x else 0) - integral (cbox c d)
(\<lambda>x. if x \<in> s then f x else 0)) < e"
@@ -9875,7 +9875,7 @@
case 3
note comb = integral_combine_tagged_division_topdown[OF assms(1)[rule_format] p(1)]
have *: "\<And>sr sx ss ks kr::real. kr = sr \<longrightarrow> ks = ss \<longrightarrow>
- ks \<le> i \<and> sr \<le> sx \<and> sx \<le> ss \<and> 0 \<le> i\<bullet>1 - kr\<bullet>1 \<and> i\<bullet>1 - kr\<bullet>1 < e/4 \<longrightarrow> abs (sx - i) < e/4"
+ ks \<le> i \<and> sr \<le> sx \<and> sx \<le> ss \<and> 0 \<le> i\<bullet>1 - kr\<bullet>1 \<and> i\<bullet>1 - kr\<bullet>1 < e/4 \<longrightarrow> \<bar>sx - i\<bar> < e/4"
by auto
show ?case
unfolding real_norm_def
@@ -10087,8 +10087,8 @@
apply (subst norm_minus_commute)
apply auto
done
- have *: "\<And>f1 f2 g. abs (f1 - i) < e / 2 \<longrightarrow> abs (f2 - g) < e / 2 \<longrightarrow>
- f1 \<le> f2 \<longrightarrow> f2 \<le> i \<longrightarrow> abs (g - i) < e"
+ have *: "\<And>f1 f2 g. \<bar>f1 - i\<bar> < e / 2 \<longrightarrow> \<bar>f2 - g\<bar> < e / 2 \<longrightarrow>
+ f1 \<le> f2 \<longrightarrow> f2 \<le> i \<longrightarrow> \<bar>g - i\<bar> < e"
unfolding real_inner_1_right by arith
show "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then g x else 0) - i) < e"
unfolding real_norm_def
@@ -10305,7 +10305,7 @@
done
have norm: "norm ig < dia + e"
if "norm sg \<le> dsa"
- and "abs (dsa - dia) < e / 2"
+ and "\<bar>dsa - dia\<bar> < e / 2"
and "norm (sg - ig) < e / 2"
for e dsa dia and sg ig :: 'a
apply (rule le_less_trans[OF norm_triangle_sub[of ig sg]])
@@ -10445,7 +10445,7 @@
(\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on s"
unfolding absolutely_integrable_on_def
using integrable_cmul[of f s c]
- using integrable_cmul[of "\<lambda>x. norm (f x)" s "abs c"]
+ using integrable_cmul[of "\<lambda>x. norm (f x)" s "\<bar>c\<bar>"]
by auto
lemma absolutely_integrable_neg[intro]:
@@ -10463,7 +10463,7 @@
lemma absolutely_integrable_abs[intro]:
"f absolutely_integrable_on s \<Longrightarrow>
- (\<lambda>x. abs(f x::real)) absolutely_integrable_on s"
+ (\<lambda>x. \<bar>f x::real\<bar>) absolutely_integrable_on s"
apply (drule absolutely_integrable_norm)
unfolding real_norm_def
apply assumption
@@ -10510,7 +10510,7 @@
lemma helplemma:
assumes "setsum (\<lambda>x. norm (f x - g x)) s < e"
and "finite s"
- shows "abs (setsum (\<lambda>x. norm(f x)) s - setsum (\<lambda>x. norm(g x)) s) < e"
+ shows "\<bar>setsum (\<lambda>x. norm(f x)) s - setsum (\<lambda>x. norm(g x)) s\<bar> < e"
unfolding setsum_subtractf[symmetric]
apply (rule le_less_trans[OF setsum_abs])
apply (rule le_less_trans[OF _ assms(1)])
@@ -10709,8 +10709,8 @@
done
note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
- have *: "\<And>sni sni' sf sf'. abs (sf' - sni') < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
- sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs (sf - ?S) < e"
+ have *: "\<And>sni sni' sf sf'. \<bar>sf' - sni'\<bar> < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
+ sni \<le> sni' \<and> sf' = sf \<longrightarrow> \<bar>sf - ?S\<bar> < e"
by arith
show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
unfolding real_norm_def
@@ -11061,7 +11061,7 @@
proof -
fix a b :: 'n
assume ab: "ball 0 (K + 1) \<subseteq> cbox a b"
- have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> abs (s - ?S) < e"
+ have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> \<bar>s - ?S\<bar> < e"
by arith
show "norm (integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
unfolding real_norm_def
@@ -11121,8 +11121,8 @@
p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
by (rule fine_division_exists [OF gauge_inter [OF d1(1) d2(1)], of a b])
(auto simp add: fine_inter)
- have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> abs (sf - si) < e / 2 \<longrightarrow>
- abs (sf' - di) < e / 2 \<longrightarrow> di < ?S + e"
+ have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> \<bar>sf - si\<bar> < e / 2 \<longrightarrow>
+ \<bar>sf' - di\<bar> < e / 2 \<longrightarrow> di < ?S + e"
by arith
show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
apply (subst if_P)
@@ -11136,7 +11136,7 @@
unfolding tagged_division_of_def split_def
apply auto
done
- show "abs ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))) < e / 2"
+ show "\<bar>(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e / 2"
using d1(2)[rule_format,OF conjI[OF p(1,2)]]
by (simp only: real_norm_def)
show "(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) = (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x))"
@@ -11295,7 +11295,7 @@
fixes f :: "'a::euclidean_space => 'b::euclidean_space"
and T :: "'c::euclidean_space \<Rightarrow> 'b"
assumes f: "f absolutely_integrable_on s"
- shows "(\<lambda>x. (\<Sum>i\<in>Basis. abs(f x\<bullet>T i) *\<^sub>R i)) absolutely_integrable_on s"
+ shows "(\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>T i\<bar> *\<^sub>R i)) absolutely_integrable_on s"
(is "?Tf absolutely_integrable_on s")
proof -
have if_distrib: "\<And>P A B x. (if P then A else B) *\<^sub>R x = (if P then A *\<^sub>R x else B *\<^sub>R x)"
@@ -11350,7 +11350,7 @@
lemma absolutely_integrable_abs_eq:
fixes f::"'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and>
- (\<lambda>x. (\<Sum>i\<in>Basis. abs(f x\<bullet>i) *\<^sub>R i)::'m) integrable_on s"
+ (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) integrable_on s"
(is "?l = ?r")
proof
assume ?l
@@ -11976,7 +11976,7 @@
apply safe
proof goal_cases
case prems: (1 n)
- have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - Inf ?S) < r"
+ have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> \<bar>ix - Inf ?S\<bar> < r"
by arith
show ?case
unfolding real_norm_def
@@ -12046,7 +12046,7 @@
apply safe
proof goal_cases
case prems: (1 n)
- have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - Sup ?S) < r"
+ have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> \<bar>ix - Sup ?S\<bar> < r"
by arith
show ?case
apply simp
--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Mon Dec 28 01:28:28 2015 +0100
@@ -13,7 +13,7 @@
assumes eucl_sup: "sup x y = (\<Sum>i\<in>Basis. sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x:X. x \<bullet> i) *\<^sub>R i)"
assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x:X. x \<bullet> i) *\<^sub>R i)"
- assumes eucl_abs: "abs x = (\<Sum>i\<in>Basis. abs (x \<bullet> i) *\<^sub>R i)"
+ assumes eucl_abs: "\<bar>x\<bar> = (\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar> *\<^sub>R i)"
begin
subclass order
@@ -55,7 +55,7 @@
and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)"
using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def)
-lemma abs_inner: "i \<in> Basis \<Longrightarrow> abs x \<bullet> i = abs (x \<bullet> i)"
+lemma abs_inner: "i \<in> Basis \<Longrightarrow> \<bar>x\<bar> \<bullet> i = \<bar>x \<bullet> i\<bar>"
by (auto simp: eucl_abs)
lemma
@@ -159,12 +159,13 @@
shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis"
by (cases i) (auto simp: Basis_prod_def)
-instantiation prod::(abs, abs) abs
+instantiation prod :: (abs, abs) abs
begin
-definition "abs x = (abs (fst x), abs (snd x))"
+definition "\<bar>x\<bar> = (\<bar>fst x\<bar>, \<bar>snd x\<bar>)"
-instance proof qed
+instance ..
+
end
instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
@@ -269,7 +270,7 @@
definition "sup x y = (\<chi> i. sup (x $ i) (y $ i))"
definition "Inf X = (\<chi> i. (INF x:X. x $ i))"
definition "Sup X = (\<chi> i. (SUP x:X. x $ i))"
-definition "abs x = (\<chi> i. abs (x $ i))"
+definition "\<bar>x\<bar> = (\<chi> i. \<bar>x $ i\<bar>)"
instance
apply standard
--- a/src/HOL/Multivariate_Analysis/PolyRoots.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy Mon Dec 28 01:28:28 2015 +0100
@@ -169,7 +169,7 @@
qed
qed
-lemma norm_lemma_xy: "\<lbrakk>abs b + 1 \<le> norm(y) - a; norm(x) \<le> a\<rbrakk> \<Longrightarrow> b \<le> norm(x + y)"
+lemma norm_lemma_xy: "\<lbrakk>\<bar>b\<bar> + 1 \<le> norm(y) - a; norm(x) \<le> a\<rbrakk> \<Longrightarrow> b \<le> norm(x + y)"
by (metis abs_add_one_not_less_self add.commute diff_le_eq dual_order.trans le_less_linear
norm_diff_ineq)
@@ -196,7 +196,7 @@
by auto
show ?thesis
unfolding eventually_at_infinity
- proof (rule exI [where x="max M (max 1 ((abs B + 1) / (norm (c (Suc n)) / 2)))"], clarsimp)
+ proof (rule exI [where x="max M (max 1 ((\<bar>B\<bar> + 1) / (norm (c (Suc n)) / 2)))"], clarsimp)
fix z::'a
assume les: "M \<le> norm z" "1 \<le> norm z" "(\<bar>B\<bar> * 2 + 2) / norm (c (Suc n)) \<le> norm z"
then have "\<bar>B\<bar> * 2 + 2 \<le> norm z * norm (c (Suc n))"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 28 01:28:28 2015 +0100
@@ -3201,7 +3201,7 @@
by (simp add: bounded_iff bdd_above_def)
lemma bounded_realI:
- assumes "\<forall>x\<in>s. abs (x::real) \<le> B"
+ assumes "\<forall>x\<in>s. \<bar>x::real\<bar> \<le> B"
shows "bounded s"
unfolding bounded_def dist_real_def
by (metis abs_minus_commute assms diff_0_right)
@@ -3275,7 +3275,7 @@
lemma bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x \<le> b)"
apply (simp add: bounded_iff)
- apply (subgoal_tac "\<And>x (y::real). 0 < 1 + abs y \<and> (x \<le> y \<longrightarrow> x \<le> 1 + abs y)")
+ apply (subgoal_tac "\<And>x (y::real). 0 < 1 + \<bar>y\<bar> \<and> (x \<le> y \<longrightarrow> x \<le> 1 + \<bar>y\<bar>)")
apply metis
apply arith
done
@@ -5905,7 +5905,7 @@
then obtain e where "e>0"
and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> s" using assms(2)[unfolded open_dist, THEN bspec[where x=x]]
by auto
- have "e * abs c > 0"
+ have "e * \<bar>c\<bar> > 0"
using assms(1)[unfolded zero_less_abs_iff[symmetric]] \<open>e>0\<close> by auto
moreover
{
@@ -5923,7 +5923,7 @@
by auto
}
ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *\<^sub>R x) < e \<longrightarrow> x' \<in> op *\<^sub>R c ` s"
- apply (rule_tac x="e * abs c" in exI)
+ apply (rule_tac x="e * \<bar>c\<bar>" in exI)
apply auto
done
}
@@ -6221,22 +6221,22 @@
lemma open_real:
fixes s :: "real set"
- shows "open s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>e>0. \<forall>x'. abs(x' - x) < e --> x' \<in> s)"
+ shows "open s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>e>0. \<forall>x'. \<bar>x' - x\<bar> < e --> x' \<in> s)"
unfolding open_dist dist_norm by simp
lemma islimpt_approachable_real:
fixes s :: "real set"
- shows "x islimpt s \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> s. x' \<noteq> x \<and> abs(x' - x) < e)"
+ shows "x islimpt s \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> s. x' \<noteq> x \<and> \<bar>x' - x\<bar> < e)"
unfolding islimpt_approachable dist_norm by simp
lemma closed_real:
fixes s :: "real set"
- shows "closed s \<longleftrightarrow> (\<forall>x. (\<forall>e>0. \<exists>x' \<in> s. x' \<noteq> x \<and> abs(x' - x) < e) \<longrightarrow> x \<in> s)"
+ shows "closed s \<longleftrightarrow> (\<forall>x. (\<forall>e>0. \<exists>x' \<in> s. x' \<noteq> x \<and> \<bar>x' - x\<bar> < e) \<longrightarrow> x \<in> s)"
unfolding closed_limpt islimpt_approachable dist_norm by simp
lemma continuous_at_real_range:
fixes f :: "'a::real_normed_vector \<Rightarrow> real"
- shows "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'. norm(x' - x) < d --> abs(f x' - f x) < e)"
+ shows "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'. norm(x' - x) < d --> \<bar>f x' - f x\<bar> < e)"
unfolding continuous_at
unfolding Lim_at
unfolding dist_nz[symmetric]
@@ -6255,7 +6255,7 @@
lemma continuous_on_real_range:
fixes f :: "'a::real_normed_vector \<Rightarrow> real"
shows "continuous_on s f \<longleftrightarrow>
- (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d \<longrightarrow> abs(f x' - f x) < e))"
+ (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d \<longrightarrow> \<bar>f x' - f x\<bar> < e))"
unfolding continuous_on_iff dist_norm by simp
text \<open>Hence some handy theorems on distance, diameter etc. of/from a set.\<close>
--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy Mon Dec 28 01:28:28 2015 +0100
@@ -65,7 +65,7 @@
fixes f :: "real \<Rightarrow> real"
assumes contf: "continuous_on {0..1} f" and e: "0 < e"
shows "\<exists>N. \<forall>n x. N \<le> n \<and> x \<in> {0..1}
- \<longrightarrow> abs(f x - (\<Sum>k = 0..n. f(k/n) * Bernstein n k x)) < e"
+ \<longrightarrow> \<bar>f x - (\<Sum>k = 0..n. f(k/n) * Bernstein n k x)\<bar> < e"
proof -
have "bounded (f ` {0..1})"
using compact_continuous_image compact_imp_bounded contf by blast
@@ -110,7 +110,7 @@
assume k: "k \<le> n"
then have kn: "0 \<le> k / n" "k / n \<le> 1"
by (auto simp: divide_simps)
- consider (lessd) "abs(x - k / n) < d" | (ged) "d \<le> abs(x - k / n)"
+ consider (lessd) "\<bar>x - k / n\<bar> < d" | (ged) "d \<le> \<bar>x - k / n\<bar>"
by linarith
then have "\<bar>(f x - f (k/n))\<bar> \<le> e/2 + 2 * M / d\<^sup>2 * (x - k/n)\<^sup>2"
proof cases
@@ -758,7 +758,7 @@
"\<And>x y. x \<in> s \<and> y \<in> s \<and> ~(x = y) \<Longrightarrow> \<exists>f. P(f) \<and> ~(f x = f y)"
"continuous_on s f"
"0 < e"
- shows "\<exists>g. P(g) \<and> (\<forall>x \<in> s. abs(f x - g x) < e)"
+ shows "\<exists>g. P(g) \<and> (\<forall>x \<in> s. \<bar>f x - g x\<bar> < e)"
proof -
interpret PR: function_ring_on "Collect P"
apply unfold_locales
@@ -1081,7 +1081,7 @@
lemma Stone_Weierstrass_real_polynomial_function:
fixes f :: "'a::euclidean_space \<Rightarrow> real"
assumes "compact s" "continuous_on s f" "0 < e"
- shows "\<exists>g. real_polynomial_function g \<and> (\<forall>x \<in> s. abs(f x - g x) < e)"
+ shows "\<exists>g. real_polynomial_function g \<and> (\<forall>x \<in> s. \<bar>f x - g x\<bar> < e)"
proof -
interpret PR: function_ring_on "Collect real_polynomial_function"
apply unfold_locales
@@ -1102,14 +1102,14 @@
proof -
{ fix b :: 'b
assume "b \<in> Basis"
- have "\<exists>p. real_polynomial_function p \<and> (\<forall>x \<in> s. abs(f x \<bullet> b - p x) < e / DIM('b))"
+ have "\<exists>p. real_polynomial_function p \<and> (\<forall>x \<in> s. \<bar>f x \<bullet> b - p x\<bar> < e / DIM('b))"
apply (rule exE [OF Stone_Weierstrass_real_polynomial_function [OF s _, of "\<lambda>x. f x \<bullet> b" "e / card Basis"]])
using e f
apply (auto simp: Euclidean_Space.DIM_positive intro: continuous_intros)
done
}
then obtain pf where pf:
- "\<And>b. b \<in> Basis \<Longrightarrow> real_polynomial_function (pf b) \<and> (\<forall>x \<in> s. abs(f x \<bullet> b - pf b x) < e / DIM('b))"
+ "\<And>b. b \<in> Basis \<Longrightarrow> real_polynomial_function (pf b) \<and> (\<forall>x \<in> s. \<bar>f x \<bullet> b - pf b x\<bar> < e / DIM('b))"
apply (rule bchoice [rule_format, THEN exE])
apply assumption
apply (force simp add: intro: that)
--- a/src/HOL/Multivariate_Analysis/ex/Approximations.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/ex/Approximations.thy Mon Dec 28 01:28:28 2015 +0100
@@ -24,7 +24,7 @@
qed
(*32-bit approximation. SLOW simplification steps: big calculations with the rewriting engine*)
-lemma pi_approx_32: "abs(pi - 13493037705/4294967296) \<le> inverse(2 ^ 32)"
+lemma pi_approx_32: "\<bar>pi - 13493037705/4294967296\<bar> \<le> inverse(2 ^ 32)"
apply (simp only: abs_diff_le_iff)
apply (rule sin_pi6_straddle, simp_all)
using Taylor_sin [of "1686629713/3221225472" 11]
--- a/src/HOL/NSA/HLog.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/HLog.thy Mon Dec 28 01:28:28 2015 +0100
@@ -117,7 +117,7 @@
lemma hlog_hrabs_HInfinite_Infinitesimal:
"[| x : HFinite - Infinitesimal; a : HInfinite; 0 < a |]
- ==> hlog a (abs x) : Infinitesimal"
+ ==> hlog a \<bar>x\<bar> : Infinitesimal"
apply (frule HInfinite_gt_zero_gt_one)
apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2
--- a/src/HOL/NSA/HSeries.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/HSeries.thy Mon Dec 28 01:28:28 2015 +0100
@@ -68,7 +68,7 @@
lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
by (drule_tac f = f in sumhr_split_add [symmetric], simp)
-lemma sumhr_hrabs: "!!m n. abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
+lemma sumhr_hrabs: "!!m n. \<bar>sumhr(m,n,f)\<bar> \<le> sumhr(m,n,%i. \<bar>f i\<bar>)"
unfolding sumhr_app by transfer (rule setsum_abs)
text{* other general version also needed *}
@@ -130,7 +130,7 @@
unfolding sumhr_app by transfer (rule refl)
lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f)
- ==> abs (sumhr(M, N, f)) @= 0"
+ ==> \<bar>sumhr(M, N, f)\<bar> @= 0"
apply (cut_tac x = M and y = N in linorder_less_linear)
apply (auto simp add: approx_refl)
apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
@@ -167,7 +167,7 @@
lemma NSsummable_NSCauchy:
"NSsummable f =
- (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. abs (sumhr(M,N,f)) @= 0)"
+ (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr(M,N,f)\<bar> @= 0)"
apply (auto simp add: summable_NSsummable_iff [symmetric]
summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
@@ -189,14 +189,14 @@
text{*Nonstandard comparison test*}
lemma NSsummable_comparison_test:
- "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |] ==> NSsummable f"
+ "[| \<exists>N. \<forall>n. N \<le> n --> \<bar>f n\<bar> \<le> g n; NSsummable g |] ==> NSsummable f"
apply (fold summable_NSsummable_iff)
apply (rule summable_comparison_test, simp, assumption)
done
lemma NSsummable_rabs_comparison_test:
- "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |]
- ==> NSsummable (%k. abs (f k))"
+ "[| \<exists>N. \<forall>n. N \<le> n --> \<bar>f n\<bar> \<le> g n; NSsummable g |]
+ ==> NSsummable (%k. \<bar>f k\<bar>)"
apply (rule NSsummable_comparison_test)
apply (auto)
done
--- a/src/HOL/NSA/HTranscendental.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/HTranscendental.thy Mon Dec 28 01:28:28 2015 +0100
@@ -103,14 +103,14 @@
lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)"
by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
-lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x\<^sup>2) = abs(x)"
+lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x\<^sup>2) = \<bar>x\<bar>"
by (transfer, simp)
-lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = abs(x)"
+lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = \<bar>x\<bar>"
by (transfer, simp)
lemma hypreal_sqrt_hyperpow_hrabs [simp]:
- "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
+ "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = \<bar>x\<bar>"
by (transfer, simp)
lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
--- a/src/HOL/NSA/HyperDef.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/HyperDef.thy Mon Dec 28 01:28:28 2015 +0100
@@ -216,8 +216,7 @@
lemma star_n_one_num: "1 = star_n (%n. 1)"
by (simp only: star_one_def star_of_def)
-lemma star_n_abs:
- "abs (star_n X) = star_n (%n. abs (X n))"
+lemma star_n_abs: "\<bar>star_n X\<bar> = star_n (%n. \<bar>X n\<bar>)"
by (simp only: star_abs_def starfun_star_n)
lemma hypreal_omega_gt_zero [simp]: "0 < omega"
@@ -280,17 +279,16 @@
subsection{*Absolute Value Function for the Hyperreals*}
-lemma hrabs_add_less:
- "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
+lemma hrabs_add_less: "[| \<bar>x\<bar> < r; \<bar>y\<bar> < s |] ==> \<bar>x + y\<bar> < r + (s::hypreal)"
by (simp add: abs_if split: split_if_asm)
-lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r"
+lemma hrabs_less_gt_zero: "\<bar>x\<bar> < r ==> (0::hypreal) < r"
by (blast intro!: order_le_less_trans abs_ge_zero)
-lemma hrabs_disj: "abs x = (x::'a::abs_if) | abs x = -x"
+lemma hrabs_disj: "\<bar>x\<bar> = (x::'a::abs_if) \<or> \<bar>x\<bar> = -x"
by (simp add: abs_if)
-lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"
+lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = \<bar>x + - z\<bar> ==> y = z | x = y"
by (simp add: abs_if split add: split_if_asm)
@@ -364,8 +362,7 @@
(*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract
result proved in Rings or Fields*)
-lemma hrabs_hrealpow_two [simp]:
- "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"
+lemma hrabs_hrealpow_two [simp]: "\<bar>x ^ Suc (Suc 0)\<bar> = (x::hypreal) ^ Suc (Suc 0)"
by (simp add: abs_mult)
lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
@@ -427,7 +424,7 @@
by transfer (rule power_inverse [symmetric])
lemma hyperpow_hrabs:
- "\<And>r n. abs (r::'a::{linordered_idom} star) pow n = abs (r pow n)"
+ "\<And>r n. \<bar>r::'a::{linordered_idom} star\<bar> pow n = \<bar>r pow n\<bar>"
by transfer (rule power_abs [symmetric])
lemma hyperpow_add:
@@ -460,7 +457,7 @@
by transfer (rule power_one)
lemma hrabs_hyperpow_minus [simp]:
- "\<And>(a::'a::{linordered_idom} star) n. abs((-a) pow n) = abs (a pow n)"
+ "\<And>(a::'a::{linordered_idom} star) n. \<bar>(-a) pow n\<bar> = \<bar>a pow n\<bar>"
by transfer (rule abs_power_minus)
lemma hyperpow_mult:
@@ -473,12 +470,12 @@
by (auto simp add: hyperpow_two zero_le_mult_iff)
lemma hrabs_hyperpow_two [simp]:
- "abs(x pow 2) =
+ "\<bar>x pow 2\<bar> =
(x::'a::{monoid_mult,linordered_ring_strict} star) pow 2"
by (simp only: abs_of_nonneg hyperpow_two_le)
lemma hyperpow_two_hrabs [simp]:
- "abs(x::'a::{linordered_idom} star) pow 2 = x pow 2"
+ "\<bar>x::'a::{linordered_idom} star\<bar> pow 2 = x pow 2"
by (simp add: hyperpow_hrabs)
text{*The precondition could be weakened to @{term "0\<le>x"}*}
--- a/src/HOL/NSA/NSA.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/NSA.thy Mon Dec 28 01:28:28 2015 +0100
@@ -181,7 +181,7 @@
lemma Reals_add_cancel: "\<lbrakk>x + y \<in> \<real>; y \<in> \<real>\<rbrakk> \<Longrightarrow> x \<in> \<real>"
by (drule (1) Reals_diff, simp)
-lemma SReal_hrabs: "(x::hypreal) \<in> \<real> ==> abs x \<in> \<real>"
+lemma SReal_hrabs: "(x::hypreal) \<in> \<real> ==> \<bar>x\<bar> \<in> \<real>"
by (simp add: Reals_eq_Standard)
lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> \<real>"
@@ -280,7 +280,7 @@
lemma HFiniteD: "x \<in> HFinite ==> \<exists>t \<in> Reals. hnorm x < t"
by (simp add: HFinite_def)
-lemma HFinite_hrabs_iff [iff]: "(abs (x::hypreal) \<in> HFinite) = (x \<in> HFinite)"
+lemma HFinite_hrabs_iff [iff]: "(\<bar>x::hypreal\<bar> \<in> HFinite) = (x \<in> HFinite)"
by (simp add: HFinite_def)
lemma HFinite_hnorm_iff [iff]:
@@ -355,7 +355,7 @@
by (simp add: Infinitesimal_def)
lemma Infinitesimal_hrabs_iff [iff]:
- "(abs (x::hypreal) \<in> Infinitesimal) = (x \<in> Infinitesimal)"
+ "(\<bar>x::hypreal\<bar> \<in> Infinitesimal) = (x \<in> Infinitesimal)"
by (simp add: abs_if)
lemma Infinitesimal_of_hypreal_iff [simp]:
@@ -509,7 +509,7 @@
by auto
lemma HFinite_diff_Infinitesimal_hrabs:
- "(x::hypreal) \<in> HFinite - Infinitesimal ==> abs x \<in> HFinite - Infinitesimal"
+ "(x::hypreal) \<in> HFinite - Infinitesimal ==> \<bar>x\<bar> \<in> HFinite - Infinitesimal"
by blast
lemma hnorm_le_Infinitesimal:
@@ -521,11 +521,11 @@
by (erule hnorm_le_Infinitesimal, erule order_less_imp_le)
lemma hrabs_le_Infinitesimal:
- "[| e \<in> Infinitesimal; abs (x::hypreal) \<le> e |] ==> x \<in> Infinitesimal"
+ "[| e \<in> Infinitesimal; \<bar>x::hypreal\<bar> \<le> e |] ==> x \<in> Infinitesimal"
by (erule hnorm_le_Infinitesimal, simp)
lemma hrabs_less_Infinitesimal:
- "[| e \<in> Infinitesimal; abs (x::hypreal) < e |] ==> x \<in> Infinitesimal"
+ "[| e \<in> Infinitesimal; \<bar>x::hypreal\<bar> < e |] ==> x \<in> Infinitesimal"
by (erule hnorm_less_Infinitesimal, simp)
lemma Infinitesimal_interval:
@@ -540,7 +540,7 @@
lemma lemma_Infinitesimal_hyperpow:
- "[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> abs (x pow N) \<le> abs x"
+ "[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> \<bar>x pow N\<bar> \<le> \<bar>x\<bar>"
apply (unfold Infinitesimal_def)
apply (auto intro!: hyperpow_Suc_le_self2
simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero)
@@ -1239,7 +1239,7 @@
"[| (x::hypreal) \<in> HFinite;
isLub \<real> {s. s \<in> \<real> & s < x} t;
r \<in> \<real>; 0 < r |]
- ==> abs (x - t) < r"
+ ==> \<bar>x - t\<bar> < r"
apply (frule lemma_st_part1a)
apply (frule_tac [4] lemma_st_part2a, auto)
apply (drule order_le_imp_less_or_eq)+
@@ -1250,7 +1250,7 @@
lemma lemma_st_part_major2:
"[| (x::hypreal) \<in> HFinite; isLub \<real> {s. s \<in> \<real> & s < x} t |]
- ==> \<forall>r \<in> Reals. 0 < r --> abs (x - t) < r"
+ ==> \<forall>r \<in> Reals. 0 < r --> \<bar>x - t\<bar> < r"
by (blast dest!: lemma_st_part_major)
@@ -1258,7 +1258,7 @@
text{*Existence of real and Standard Part Theorem*}
lemma lemma_st_part_Ex:
"(x::hypreal) \<in> HFinite
- ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> abs (x - t) < r"
+ ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> \<bar>x - t\<bar> < r"
apply (frule lemma_st_part_lub, safe)
apply (frule isLubD1a)
apply (blast dest: lemma_st_part_major2)
@@ -1483,13 +1483,13 @@
apply (simp (no_asm) add: HInfinite_HFinite_iff)
done
-lemma approx_hrabs_disj: "abs (x::hypreal) @= x | abs x @= -x"
+lemma approx_hrabs_disj: "\<bar>x::hypreal\<bar> @= x \<or> \<bar>x\<bar> @= -x"
by (cut_tac x = x in hrabs_disj, auto)
subsection{*Theorems about Monads*}
-lemma monad_hrabs_Un_subset: "monad (abs x) \<le> monad(x::hypreal) Un monad(-x)"
+lemma monad_hrabs_Un_subset: "monad \<bar>x\<bar> \<le> monad(x::hypreal) Un monad(-x)"
by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto)
lemma Infinitesimal_monad_eq: "e \<in> Infinitesimal ==> monad (x+e) = monad x"
@@ -1505,7 +1505,7 @@
apply (simp (no_asm) add: Infinitesimal_monad_zero_iff [symmetric])
done
-lemma monad_zero_hrabs_iff: "((x::hypreal) \<in> monad 0) = (abs x \<in> monad 0)"
+lemma monad_zero_hrabs_iff: "((x::hypreal) \<in> monad 0) = (\<bar>x\<bar> \<in> monad 0)"
apply (rule_tac x1 = x in hrabs_disj [THEN disjE])
apply (auto simp add: monad_zero_minus_iff [symmetric])
done
@@ -1543,7 +1543,7 @@
done
lemma Infinitesimal_approx_hrabs:
- "[| x @= y; (x::hypreal) \<in> Infinitesimal |] ==> abs x @= abs y"
+ "[| x @= y; (x::hypreal) \<in> Infinitesimal |] ==> \<bar>x\<bar> @= \<bar>y\<bar>"
apply (drule Infinitesimal_monad_zero_iff [THEN iffD1])
apply (blast intro: approx_mem_monad_zero monad_zero_hrabs_iff [THEN iffD1] mem_monad_approx approx_trans3)
done
@@ -1577,25 +1577,25 @@
"[|(x::hypreal) < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)
-theorem approx_hrabs: "(x::hypreal) @= y ==> abs x @= abs y"
+theorem approx_hrabs: "(x::hypreal) @= y ==> \<bar>x\<bar> @= \<bar>y\<bar>"
by (drule approx_hnorm, simp)
-lemma approx_hrabs_zero_cancel: "abs(x::hypreal) @= 0 ==> x @= 0"
+lemma approx_hrabs_zero_cancel: "\<bar>x::hypreal\<bar> @= 0 ==> x @= 0"
apply (cut_tac x = x in hrabs_disj)
apply (auto dest: approx_minus)
done
lemma approx_hrabs_add_Infinitesimal:
- "(e::hypreal) \<in> Infinitesimal ==> abs x @= abs(x+e)"
+ "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> @= \<bar>x + e\<bar>"
by (fast intro: approx_hrabs Infinitesimal_add_approx_self)
lemma approx_hrabs_add_minus_Infinitesimal:
- "(e::hypreal) \<in> Infinitesimal ==> abs x @= abs(x + -e)"
+ "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> @= \<bar>x + -e\<bar>"
by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self)
lemma hrabs_add_Infinitesimal_cancel:
"[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
- abs(x+e) = abs(y+e')|] ==> abs x @= abs y"
+ \<bar>x + e\<bar> = \<bar>y + e'\<bar>|] ==> \<bar>x\<bar> @= \<bar>y\<bar>"
apply (drule_tac x = x in approx_hrabs_add_Infinitesimal)
apply (drule_tac x = y in approx_hrabs_add_Infinitesimal)
apply (auto intro: approx_trans2)
@@ -1603,7 +1603,7 @@
lemma hrabs_add_minus_Infinitesimal_cancel:
"[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
- abs(x + -e) = abs(y + -e')|] ==> abs x @= abs y"
+ \<bar>x + -e\<bar> = \<bar>y + -e'\<bar>|] ==> \<bar>x\<bar> @= \<bar>y\<bar>"
apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal)
apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal)
apply (auto intro: approx_trans2)
@@ -1623,8 +1623,8 @@
done
lemma Infinitesimal_add_hrabs_hypreal_of_real_less:
- "[| x \<in> Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |]
- ==> abs (hypreal_of_real r + x) < hypreal_of_real y"
+ "[| x \<in> Infinitesimal; \<bar>hypreal_of_real r\<bar> < hypreal_of_real y |]
+ ==> \<bar>hypreal_of_real r + x\<bar> < hypreal_of_real y"
apply (drule_tac x = "hypreal_of_real r" in approx_hrabs_add_Infinitesimal)
apply (drule approx_sym [THEN bex_Infinitesimal_iff2 [THEN iffD2]])
apply (auto intro!: Infinitesimal_add_hypreal_of_real_less
@@ -1633,8 +1633,8 @@
done
lemma Infinitesimal_add_hrabs_hypreal_of_real_less2:
- "[| x \<in> Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |]
- ==> abs (x + hypreal_of_real r) < hypreal_of_real y"
+ "[| x \<in> Infinitesimal; \<bar>hypreal_of_real r\<bar> < hypreal_of_real y |]
+ ==> \<bar>x + hypreal_of_real r\<bar> < hypreal_of_real y"
apply (rule add.commute [THEN subst])
apply (erule Infinitesimal_add_hrabs_hypreal_of_real_less, assumption)
done
@@ -1738,7 +1738,7 @@
lemma monad_hrabs_less:
"[| y \<in> monad x; 0 < hypreal_of_real e |]
- ==> abs (y - x) < hypreal_of_real e"
+ ==> \<bar>y - x\<bar> < hypreal_of_real e"
apply (drule mem_monad_approx [THEN approx_sym])
apply (drule bex_Infinitesimal_iff [THEN iffD2])
apply (auto dest!: InfinitesimalD)
@@ -1901,7 +1901,7 @@
apply (rule st_le, auto)
done
-lemma st_hrabs: "x \<in> HFinite ==> abs(st x) = st(abs x)"
+lemma st_hrabs: "x \<in> HFinite ==> \<bar>st x\<bar> = st \<bar>x\<bar>"
apply (simp add: linorder_not_le st_zero_le abs_if st_minus
linorder_not_less)
apply (auto dest!: st_zero_ge [OF order_less_imp_le])
@@ -2077,12 +2077,12 @@
lemma finite_real_of_nat_le_real: "finite {n::nat. real n \<le> u}"
by (auto simp add: lemma_real_le_Un_eq lemma_finite_omega_set finite_real_of_nat_less_real)
-lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. abs(real n) \<le> u}"
+lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. \<bar>real n\<bar> \<le> u}"
apply (simp (no_asm) add: finite_real_of_nat_le_real)
done
lemma rabs_real_of_nat_le_real_FreeUltrafilterNat:
- "\<not> eventually (\<lambda>n. abs(real n) \<le> u) FreeUltrafilterNat"
+ "\<not> eventually (\<lambda>n. \<bar>real n\<bar> \<le> u) FreeUltrafilterNat"
by (blast intro!: FreeUltrafilterNat.finite finite_rabs_real_of_nat_le_real)
lemma FreeUltrafilterNat_nat_gt_real: "eventually (\<lambda>n. u < real n) FreeUltrafilterNat"
@@ -2092,8 +2092,8 @@
done
(*--------------------------------------------------------------
- The complement of {n. abs(real n) \<le> u} =
- {n. u < abs (real n)} is in FreeUltrafilterNat
+ The complement of {n. \<bar>real n\<bar> \<le> u} =
+ {n. u < \<bar>real n\<bar>} is in FreeUltrafilterNat
by property of (free) ultrafilters
--------------------------------------------------------------*)
--- a/src/HOL/NSA/NSComplex.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/NSComplex.thy Mon Dec 28 01:28:28 2015 +0100
@@ -228,8 +228,8 @@
subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
lemma hcomplex_of_hypreal_abs:
- "hcomplex_of_hypreal (abs x) =
- hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
+ "hcomplex_of_hypreal \<bar>x\<bar> =
+ hcomplex_of_hypreal (hcmod (hcomplex_of_hypreal x))"
by simp
lemma HComplex_inject [simp]:
@@ -447,10 +447,10 @@
"!!y. hIm (iii * hcomplex_of_hypreal y) = y"
by transfer simp
-lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y"
+lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = \<bar>y\<bar>"
by transfer (simp add: norm_complex_def)
-lemma hcmod_mult_i2 [simp]: "!!y. hcmod (hcomplex_of_hypreal y * iii) = abs y"
+lemma hcmod_mult_i2 [simp]: "!!y. hcmod (hcomplex_of_hypreal y * iii) = \<bar>y\<bar>"
by transfer (simp add: norm_complex_def)
(*---------------------------------------------------------------------------*)
@@ -506,11 +506,10 @@
by transfer (simp add: cmod_unit_one)
lemma hcmod_complex_polar [simp]:
- "!!r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
- abs r"
+ "!!r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = \<bar>r\<bar>"
by transfer (simp add: cmod_complex_polar)
-lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = abs r"
+lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = \<bar>r\<bar>"
by transfer (rule complex_mod_rcis)
(*---------------------------------------------------------------------------*)
--- a/src/HOL/NSA/NatStar.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/NatStar.thy Mon Dec 28 01:28:28 2015 +0100
@@ -96,7 +96,7 @@
text{*Nonstandard extension with absolute value*}
-lemma starfun_abs: "!!N. ( *f* (%n. abs (f n))) N = abs(( *f* f) N)"
+lemma starfun_abs: "!!N. ( *f* (%n. \<bar>f n\<bar>)) N = \<bar>( *f* f) N\<bar>"
by (transfer, rule refl)
text{*The hyperpow function as a nonstandard extension of realpow*}
--- a/src/HOL/NSA/Star.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/Star.thy Mon Dec 28 01:28:28 2015 +0100
@@ -282,8 +282,7 @@
text{*Alternative definition for hrabs with rabs function
applied entrywise to equivalence class representative.
This is easily proved using starfun and ns extension thm*}
-lemma hypreal_hrabs:
- "abs (star_n X) = star_n (%n. abs (X n))"
+lemma hypreal_hrabs: "\<bar>star_n X\<bar> = star_n (%n. \<bar>X n\<bar>)"
by (simp only: starfun_rabs_hrabs [symmetric] starfun)
text{*nonstandard extension of set through nonstandard extension
@@ -291,13 +290,12 @@
where we replace rabs by some arbitrary function f and hrabs
by its NS extenson. See second NS set extension below.*}
lemma STAR_rabs_add_minus:
- "*s* {x. abs (x + - y) < r} =
- {x. abs(x + -star_of y) < star_of r}"
+ "*s* {x. \<bar>x + - y\<bar> < r} = {x. \<bar>x + -star_of y\<bar> < star_of r}"
by (transfer, rule refl)
lemma STAR_starfun_rabs_add_minus:
- "*s* {x. abs (f x + - y) < r} =
- {x. abs(( *f* f) x + -star_of y) < star_of r}"
+ "*s* {x. \<bar>f x + - y\<bar> < r} =
+ {x. \<bar>( *f* f) x + -star_of y\<bar> < star_of r}"
by (transfer, rule refl)
text{*Another characterization of Infinitesimal and one of @= relation.
--- a/src/HOL/NSA/StarDef.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/NSA/StarDef.thy Mon Dec 28 01:28:28 2015 +0100
@@ -583,7 +583,7 @@
lemma Standard_inverse: "x \<in> Standard \<Longrightarrow> inverse x \<in> Standard"
by (simp add: star_inverse_def)
-lemma Standard_abs: "x \<in> Standard \<Longrightarrow> abs x \<in> Standard"
+lemma Standard_abs: "x \<in> Standard \<Longrightarrow> \<bar>x\<bar> \<in> Standard"
by (simp add: star_abs_def)
lemma Standard_mod: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x mod y \<in> Standard"
@@ -618,7 +618,7 @@
lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
by transfer (rule refl)
-lemma star_of_abs: "star_of (abs x) = abs (star_of x)"
+lemma star_of_abs: "star_of \<bar>x\<bar> = \<bar>star_of x\<bar>"
by transfer (rule refl)
text {* @{term star_of} preserves numerals *}
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Mon Dec 28 01:28:28 2015 +0100
@@ -53,7 +53,7 @@
definition zcongm :: "int => int => int => bool"
where "zcongm m = (\<lambda>a b. zcong a b m)"
-lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
+lemma abs_eq_1_iff [iff]: "(\<bar>z\<bar> = (1::int)) = (z = 1 \<or> z = -1)"
-- \<open>LCP: not sure why this lemma is needed now\<close>
by (auto simp add: abs_if)
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Mon Dec 28 01:28:28 2015 +0100
@@ -566,7 +566,7 @@
definition
zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
- "zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"
+ "zgcd i j = int (gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>))"
lemma zgcd_zdvd1 [iff, algebra]: "zgcd i j dvd i"
by (simp add: zgcd_def int_dvd_iff)
@@ -611,7 +611,7 @@
done
qed
-lemma int_nat_abs: "int (nat (abs x)) = abs x" by arith
+lemma int_nat_abs: "int (nat \<bar>x\<bar>) = \<bar>x\<bar>" by arith
lemma zgcd_greatest:
assumes "k dvd m" and "k dvd n"
@@ -654,10 +654,10 @@
with zgcd_pos show "?g' = 1" by simp
qed
-lemma zgcd_0 [simp, algebra]: "zgcd m 0 = abs m"
+lemma zgcd_0 [simp, algebra]: "zgcd m 0 = \<bar>m\<bar>"
by (simp add: zgcd_def abs_if)
-lemma zgcd_0_left [simp, algebra]: "zgcd 0 m = abs m"
+lemma zgcd_0_left [simp, algebra]: "zgcd 0 m = \<bar>m\<bar>"
by (simp add: zgcd_def abs_if)
lemma zgcd_non_0: "0 < n ==> zgcd m n = zgcd n (m mod n)"
@@ -704,7 +704,7 @@
add: minus_mult_right nat_mult_distrib zgcd_def abs_if
mult_less_0_iff gcd_mult_distrib2 [symmetric] of_nat_mult)
-lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n"
+lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = \<bar>k\<bar> * zgcd m n"
by (simp add: abs_if zgcd_zmult_distrib2)
lemma zgcd_self [simp]: "0 \<le> m ==> zgcd m m = m"
@@ -717,7 +717,7 @@
by (cut_tac k = k and m = n and n = 1 in zgcd_zmult_distrib2, simp_all)
-definition "zlcm i j = int (lcm(nat(abs i)) (nat(abs j)))"
+definition "zlcm i j = int (lcm (nat \<bar>i\<bar>) (nat \<bar>j\<bar>))"
lemma dvd_zlcm_self1[simp, algebra]: "i dvd zlcm i j"
by(simp add:zlcm_def dvd_int_iff)
@@ -729,7 +729,7 @@
lemma dvd_imp_dvd_zlcm1:
assumes "k dvd i" shows "k dvd (zlcm i j)"
proof -
- have "nat(abs k) dvd nat(abs i)" using \<open>k dvd i\<close>
+ have "nat \<bar>k\<bar> dvd nat \<bar>i\<bar>" using \<open>k dvd i\<close>
by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
qed
@@ -737,16 +737,16 @@
lemma dvd_imp_dvd_zlcm2:
assumes "k dvd j" shows "k dvd (zlcm i j)"
proof -
- have "nat(abs k) dvd nat(abs j)" using \<open>k dvd j\<close>
+ have "nat \<bar>k\<bar> dvd nat \<bar>j\<bar>" using \<open>k dvd j\<close>
by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
qed
-lemma zdvd_self_abs1: "(d::int) dvd (abs d)"
+lemma zdvd_self_abs1: "(d::int) dvd \<bar>d\<bar>"
by (case_tac "d <0", simp_all)
-lemma zdvd_self_abs2: "(abs (d::int)) dvd d"
+lemma zdvd_self_abs2: "\<bar>d::int\<bar> dvd d"
by (case_tac "d<0", simp_all)
(* lcm a b is positive for positive a and b *)
@@ -776,8 +776,8 @@
and bnz: "b \<noteq> 0"
shows "0 < zlcm a b"
proof-
- let ?na = "nat (abs a)"
- let ?nb = "nat (abs b)"
+ let ?na = "nat \<bar>a\<bar>"
+ let ?nb = "nat \<bar>b\<bar>"
have nap: "?na >0" using anz by simp
have nbp: "?nb >0" using bnz by simp
have "0 < lcm ?na ?nb" by (rule lcm_pos[OF nap nbp])
--- a/src/HOL/Probability/Bochner_Integration.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy Mon Dec 28 01:28:28 2015 +0100
@@ -2352,7 +2352,7 @@
lemma integral_0_iff:
fixes f :: "'a \<Rightarrow> real"
- shows "integrable M f \<Longrightarrow> (\<integral>x. abs (f x) \<partial>M) = 0 \<longleftrightarrow> emeasure M {x\<in>space M. f x \<noteq> 0} = 0"
+ shows "integrable M f \<Longrightarrow> (\<integral>x. \<bar>f x\<bar> \<partial>M) = 0 \<longleftrightarrow> emeasure M {x\<in>space M. f x \<noteq> 0} = 0"
using integral_norm_eq_0_iff[of M f] by simp
lemma (in finite_measure) integrable_const[intro!, simp]: "integrable M (\<lambda>x. a)"
--- a/src/HOL/Probability/Interval_Integral.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Probability/Interval_Integral.thy Mon Dec 28 01:28:28 2015 +0100
@@ -1087,7 +1087,7 @@
lemma interval_integral_norm2:
"interval_lebesgue_integrable lborel a b f \<Longrightarrow>
- norm (LBINT t=a..b. f t) \<le> abs (LBINT t=a..b. norm (f t))"
+ norm (LBINT t=a..b. f t) \<le> \<bar>LBINT t=a..b. norm (f t)\<bar>"
proof (induct a b rule: linorder_wlog)
case (sym a b) then show ?case
by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b])
--- a/src/HOL/Probability/Lebesgue_Measure.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Mon Dec 28 01:28:28 2015 +0100
@@ -695,13 +695,13 @@
lemma lborel_distr_mult':
assumes "(c::real) \<noteq> 0"
- shows "lborel = density (distr lborel borel (op * c)) (\<lambda>_. abs c)"
+ shows "lborel = density (distr lborel borel (op * c)) (\<lambda>_. \<bar>c\<bar>)"
proof-
have "lborel = density lborel (\<lambda>_. 1)" by (rule density_1[symmetric])
- also from assms have "(\<lambda>_. 1 :: ereal) = (\<lambda>_. inverse (abs c) * abs c)" by (intro ext) simp
- also have "density lborel ... = density (density lborel (\<lambda>_. inverse (abs c))) (\<lambda>_. abs c)"
+ also from assms have "(\<lambda>_. 1 :: ereal) = (\<lambda>_. inverse \<bar>c\<bar> * \<bar>c\<bar>)" by (intro ext) simp
+ also have "density lborel ... = density (density lborel (\<lambda>_. inverse \<bar>c\<bar>)) (\<lambda>_. \<bar>c\<bar>)"
by (subst density_density_eq) auto
- also from assms have "density lborel (\<lambda>_. inverse (abs c)) = distr lborel borel (op * c)"
+ also from assms have "density lborel (\<lambda>_. inverse \<bar>c\<bar>) = distr lborel borel (op * c)"
by (rule lborel_distr_mult[symmetric])
finally show ?thesis .
qed
--- a/src/HOL/Probability/Set_Integral.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Probability/Set_Integral.thy Mon Dec 28 01:28:28 2015 +0100
@@ -65,7 +65,7 @@
*)
(*
-lemma indicator_abs_eq: "\<And>A x. abs (indicator A x) = ((indicator A x) :: real)"
+lemma indicator_abs_eq: "\<And>A x. \<bar>indicator A x\<bar> = ((indicator A x) :: real)"
by (auto simp add: indicator_def)
*)
@@ -517,7 +517,7 @@
"CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
(*
-lemma cmod_mult: "cmod ((a :: real) * (x :: complex)) = abs a * cmod x"
+lemma cmod_mult: "cmod ((a :: real) * (x :: complex)) = \<bar>a\<bar> * cmod x"
apply (simp add: norm_mult)
by (subst norm_mult, auto)
*)
--- a/src/HOL/SMT_Examples/SMT_Examples.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy Mon Dec 28 01:28:28 2015 +0100
@@ -258,7 +258,7 @@
lemma "(3 :: int) + 1 = 4" by smt
lemma "x + (y + z) = y + (z + (x::int))" by smt
lemma "max (3::int) 8 > 5" by smt
-lemma "abs (x :: real) + abs y \<ge> abs (x + y)" by smt
+lemma "\<bar>x :: real\<bar> + \<bar>y\<bar> \<ge> \<bar>x + y\<bar>" by smt
lemma "P ((2::int) < 3) = P True" by smt
lemma "x + 3 \<ge> 4 \<or> x < (1::int)" by smt
@@ -303,9 +303,9 @@
processor.
*}
-lemma "\<lbrakk> x3 = abs x2 - x1; x4 = abs x3 - x2; x5 = abs x4 - x3;
- x6 = abs x5 - x4; x7 = abs x6 - x5; x8 = abs x7 - x6;
- x9 = abs x8 - x7; x10 = abs x9 - x8; x11 = abs x10 - x9 \<rbrakk>
+lemma "\<lbrakk> x3 = \<bar>x2\<bar> - x1; x4 = \<bar>x3\<bar> - x2; x5 = \<bar>x4\<bar> - x3;
+ x6 = \<bar>x5\<bar> - x4; x7 = \<bar>x6\<bar> - x5; x8 = \<bar>x7\<bar> - x6;
+ x9 = \<bar>x8\<bar> - x7; x10 = \<bar>x9\<bar> - x8; x11 = \<bar>x10\<bar> - x9 \<rbrakk>
\<Longrightarrow> x1 = x10 \<and> x2 = (x11::int)"
by smt
@@ -320,7 +320,7 @@
lemma
assumes "x \<noteq> (0::real)"
- shows "x + x \<noteq> (let P = (abs x > 1) in if P \<or> \<not> P then 4 else 2) * x"
+ shows "x + x \<noteq> (let P = (\<bar>x\<bar> > 1) in if P \<or> \<not> P then 4 else 2) * x"
using assms [[z3_extensions]] by smt
--- a/src/HOL/SMT_Examples/SMT_Tests.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Mon Dec 28 01:28:28 2015 +0100
@@ -336,11 +336,11 @@
by smt+
lemma
- "abs (x::int) \<ge> 0"
- "(abs x = 0) = (x = 0)"
- "(x \<ge> 0) = (abs x = x)"
- "(x \<le> 0) = (abs x = -x)"
- "abs (abs x) = abs x"
+ "\<bar>x::int\<bar> \<ge> 0"
+ "(\<bar>x\<bar> = 0) = (x = 0)"
+ "(x \<ge> 0) = (\<bar>x\<bar> = x)"
+ "(x \<le> 0) = (\<bar>x\<bar> = -x)"
+ "\<bar>\<bar>x\<bar>\<bar> = \<bar>x\<bar>"
by smt+
lemma
@@ -349,7 +349,7 @@
"z < x \<and> z < y \<longrightarrow> z < min x y"
"min x y = min y x"
"x \<ge> 0 \<longrightarrow> min x 0 = 0"
- "min x y \<le> abs (x + y)"
+ "min x y \<le> \<bar>x + y\<bar>"
by smt+
lemma
@@ -358,7 +358,7 @@
"z > x \<and> z > y \<longrightarrow> z > max x y"
"max x y = max y x"
"x \<ge> 0 \<longrightarrow> max x 0 = x"
- "max x y \<ge> - abs x - abs y"
+ "max x y \<ge> - \<bar>x\<bar> - \<bar>y\<bar>"
by smt+
lemma
@@ -448,11 +448,11 @@
by smt+
lemma
- "abs (x::real) \<ge> 0"
- "(abs x = 0) = (x = 0)"
- "(x \<ge> 0) = (abs x = x)"
- "(x \<le> 0) = (abs x = -x)"
- "abs (abs x) = abs x"
+ "\<bar>x::real\<bar> \<ge> 0"
+ "(\<bar>x\<bar> = 0) = (x = 0)"
+ "(x \<ge> 0) = (\<bar>x\<bar> = x)"
+ "(x \<le> 0) = (\<bar>x\<bar> = -x)"
+ "\<bar>\<bar>x\<bar>\<bar> = \<bar>x\<bar>"
by smt+
lemma
@@ -461,7 +461,7 @@
"z < x \<and> z < y \<longrightarrow> z < min x y"
"min x y = min y x"
"x \<ge> 0 \<longrightarrow> min x 0 = 0"
- "min x y \<le> abs (x + y)"
+ "min x y \<le> \<bar>x + y\<bar>"
by smt+
lemma
@@ -470,7 +470,7 @@
"z > x \<and> z > y \<longrightarrow> z > max x y"
"max x y = max y x"
"x \<ge> 0 \<longrightarrow> max x 0 = x"
- "max x y \<ge> - abs x - abs y"
+ "max x y \<ge> - \<bar>x\<bar> - \<bar>y\<bar>"
by smt+
lemma
--- a/src/HOL/Word/Bit_Representation.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Mon Dec 28 01:28:28 2015 +0100
@@ -172,7 +172,7 @@
lemma bin_abs_lem:
"bin = (w BIT b) ==> bin ~= -1 --> bin ~= 0 -->
- nat (abs w) < nat (abs bin)"
+ nat \<bar>w\<bar> < nat \<bar>bin\<bar>"
apply clarsimp
apply (unfold Bit_def)
apply (cases b)
--- a/src/HOL/ex/Arith_Examples.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/ex/Arith_Examples.thy Mon Dec 28 01:28:28 2015 +0100
@@ -63,13 +63,13 @@
lemma "(i::int) < j ==> min i j < max i j"
by linarith
-lemma "(0::int) <= abs i"
+lemma "(0::int) <= \<bar>i\<bar>"
by linarith
-lemma "(i::int) <= abs i"
+lemma "(i::int) <= \<bar>i\<bar>"
by linarith
-lemma "abs (abs (i::int)) = abs i"
+lemma "\<bar>\<bar>i::int\<bar>\<bar> = \<bar>i\<bar>"
by linarith
text \<open>Also testing subgoals with bound variables.\<close>
@@ -127,7 +127,7 @@
lemma "-(i::int) * 1 = 0 ==> i = 0"
by linarith
-lemma "[| (0::int) < abs i; abs i * 1 < abs i * j |] ==> 1 < abs i * j"
+lemma "[| (0::int) < \<bar>i\<bar>; \<bar>i\<bar> * 1 < \<bar>i\<bar> * j |] ==> 1 < \<bar>i\<bar> * j"
by linarith
@@ -227,13 +227,13 @@
text \<open>Splitting of inequalities of different type.\<close>
lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==>
- a + b <= nat (max (abs i) (abs j))"
+ a + b <= nat (max \<bar>i\<bar> \<bar>j\<bar>)"
by linarith
text \<open>Again, but different order.\<close>
lemma "[| (i::int) ~= j; (a::nat) ~= b; a < 2; b < 2 |] ==>
- a + b <= nat (max (abs i) (abs j))"
+ a + b <= nat (max \<bar>i\<bar> \<bar>j\<bar>)"
by linarith
end
--- a/src/HOL/ex/Dedekind_Real.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy Mon Dec 28 01:28:28 2015 +0100
@@ -1231,7 +1231,7 @@
real_less_def: "x < (y::real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
definition
- real_abs_def: "abs (r::real) = (if r < 0 then - r else r)"
+ real_abs_def: "\<bar>r::real\<bar> = (if r < 0 then - r else r)"
definition
real_sgn_def: "sgn (x::real) = (if x=0 then 0 else if 0<x then 1 else - 1)"
--- a/src/HOL/ex/Normalization_by_Evaluation.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy Mon Dec 28 01:28:28 2015 +0100
@@ -92,14 +92,14 @@
lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization
lemma "(-4::int) * 2 = -8" by normalization
-lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
+lemma "\<bar>(-4::int) + 2 * 1\<bar> = 2" by normalization
lemma "(2::int) + 3 = 5" by normalization
lemma "(2::int) + 3 * (- 4) * (- 1) = 14" by normalization
lemma "(2::int) + 3 * (- 4) * 1 + 0 = -10" by normalization
lemma "(2::int) < 3" by normalization
lemma "(2::int) <= 3" by normalization
-lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
-lemma "4 - 42 * abs (3 + (-7::int)) = -164" by normalization
+lemma "\<bar>(-4::int) + 2 * 1\<bar> = 2" by normalization
+lemma "4 - 42 * \<bar>3 + (-7::int)\<bar> = -164" by normalization
lemma "(if (0::nat) \<le> (x::nat) then 0::nat else x) = 0" by normalization
lemma "4 = Suc (Suc (Suc (Suc 0)))" by normalization
lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization
--- a/src/HOL/ex/PresburgerEx.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/ex/PresburgerEx.thy Mon Dec 28 01:28:28 2015 +0100
@@ -100,9 +100,9 @@
Warning: it takes (in 2006) over 4.2 minutes!\<close>
-lemma "\<lbrakk> x3 = abs x2 - x1; x4 = abs x3 - x2; x5 = abs x4 - x3;
- x6 = abs x5 - x4; x7 = abs x6 - x5; x8 = abs x7 - x6;
- x9 = abs x8 - x7; x10 = abs x9 - x8; x11 = abs x10 - x9 \<rbrakk>
+lemma "\<lbrakk> x3 = \<bar>x2\<bar> - x1; x4 = \<bar>x3\<bar> - x2; x5 = \<bar>x4\<bar> - x3;
+ x6 = \<bar>x5\<bar> - x4; x7 = \<bar>x6\<bar> - x5; x8 = \<bar>x7\<bar> - x6;
+ x9 = \<bar>x8\<bar> - x7; x10 = \<bar>x9\<bar> - x8; x11 = \<bar>x10\<bar> - x9 \<rbrakk>
\<Longrightarrow> x1 = x10 & x2 = (x11::int)"
by arith
--- a/src/HOL/ex/Set_Theory.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/ex/Set_Theory.thy Mon Dec 28 01:28:28 2015 +0100
@@ -193,8 +193,8 @@
\<comment> \<open>Example 7.\<close>
by force
-lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
- \<longrightarrow> (\<exists>A::int set. -2 \<in> A & (\<forall>y. abs y \<notin> A))"
+lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> \<bar>v\<bar>)
+ \<longrightarrow> (\<exists>A::int set. -2 \<in> A & (\<forall>y. \<bar>y\<bar> \<notin> A))"
\<comment> \<open>Example 8 needs a small hint.\<close>
by force
\<comment> \<open>not \<open>blast\<close>, which can't simplify \<open>-2 < 0\<close>\<close>