src/HOL/RealDef.thy
changeset 44344 49be3e7d4762
parent 44278 1220ecb81e8f
child 44346 00dd3c4dabe0
equal deleted inserted replaced
44343:e5294bcf58a4 44344:49be3e7d4762
  1672 
  1672 
  1673 (* FIXME: redundant, but used by Integration/RealRandVar.thy in AFP *)
  1673 (* FIXME: redundant, but used by Integration/RealRandVar.thy in AFP *)
  1674 lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
  1674 lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
  1675 by (force simp add: abs_le_iff)
  1675 by (force simp add: abs_le_iff)
  1676 
  1676 
  1677 lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)"
  1677 lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)"
  1678 by (simp add: abs_if)
  1678 by (simp add: abs_if)
  1679 
  1679 
  1680 lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
  1680 lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
  1681 by (rule abs_of_nonneg [OF real_of_nat_ge_zero])
  1681 by (rule abs_of_nonneg [OF real_of_nat_ge_zero])
  1682 
  1682 
  1683 lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x"
  1683 lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x"
  1684 by simp
  1684 by simp
  1685  
  1685  
  1686 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
  1686 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
  1687 by simp
  1687 by simp
  1688 
  1688