# HG changeset patch
# User wenzelm
# Date 1313926583 -7200
# Node ID b7f9e764532a110d9c7c17be2911e41e8a17e84b
# Parent  63cddfbc5a098a8ab5afc8b702c7340486ab140c# Parent  a93d25fb14fce9c5099c27f6b1b4d93e8056656f
merged

diff -r a93d25fb14fc -r b7f9e764532a src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sun Aug 21 13:23:29 2011 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Aug 21 13:36:23 2011 +0200
@@ -712,7 +712,7 @@
         case False
         hence "real ?DIV \<le> 1" unfolding less_float_def by auto
 
-        have "0 \<le> x / ?R" using `0 \<le> real x` `0 < ?R` unfolding real_0_le_divide_iff by auto
+        have "0 \<le> x / ?R" using `0 \<le> real x` `0 < ?R` unfolding zero_le_divide_iff by auto
         hence "0 \<le> real ?DIV" using monotone by (rule order_trans)
 
         have "arctan x = 2 * arctan (x / ?R)" using arctan_half unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left .
diff -r a93d25fb14fc -r b7f9e764532a src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Sun Aug 21 13:23:29 2011 +0200
+++ b/src/HOL/Groups.thy	Sun Aug 21 13:36:23 2011 +0200
@@ -411,6 +411,10 @@
   ultimately show "a = - b" by simp
 qed
 
+lemma add_eq_0_iff: "x + y = 0 \<longleftrightarrow> y = - x"
+  unfolding eq_neg_iff_add_eq_0 [symmetric]
+  by (rule equation_minus_iff)
+
 end
 
 class ab_group_add = minus + uminus + comm_monoid_add +
@@ -466,7 +470,7 @@
 (* FIXME: duplicates right_minus_eq from class group_add *)
 (* but only this one is declared as a simp rule. *)
 lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
-by (simp add: algebra_simps)
+  by (rule right_minus_eq)
 
 lemma diff_eq_diff_eq:
   "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
diff -r a93d25fb14fc -r b7f9e764532a src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Sun Aug 21 13:23:29 2011 +0200
+++ b/src/HOL/Limits.thy	Sun Aug 21 13:36:23 2011 +0200
@@ -216,6 +216,13 @@
   "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
   unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
 
+abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
+  where "trivial_limit F \<equiv> F = bot"
+
+lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
+  by (rule eventually_False [symmetric])
+
+
 subsection {* Map function for filters *}
 
 definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
@@ -259,9 +266,11 @@
   then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
 qed auto
 
-lemma sequentially_bot [simp]: "sequentially \<noteq> bot"
+lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
   unfolding filter_eq_iff eventually_sequentially by auto
 
+lemmas trivial_limit_sequentially = sequentially_bot
+
 lemma eventually_False_sequentially [simp]:
   "\<not> eventually (\<lambda>n. False) sequentially"
   by (simp add: eventually_False)
@@ -272,12 +281,6 @@
   by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
 
 
-definition trivial_limit :: "'a filter \<Rightarrow> bool"
-  where "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
-
-lemma trivial_limit_sequentially [intro]: "\<not> trivial_limit sequentially"
-  by (auto simp add: trivial_limit_def eventually_sequentially)
-
 subsection {* Standard filters *}
 
 definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70)
diff -r a93d25fb14fc -r b7f9e764532a src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Aug 21 13:23:29 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Aug 21 13:36:23 2011 +0200
@@ -1168,7 +1168,7 @@
       thus ?thesis unfolding obt1(5) obt2(5) unfolding * and ** using False
         apply(rule_tac x="((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI) defer
         apply(rule convex_convex_hull[of s, unfolded convex_def, rule_format]) using obt1(4) obt2(4)
-        unfolding add_divide_distrib[THEN sym] and real_0_le_divide_iff
+        unfolding add_divide_distrib[THEN sym] and zero_le_divide_iff
         by (auto simp add: scaleR_left_distrib scaleR_right_distrib)
     qed note * = this
     have u1:"u1 \<le> 1" unfolding obt1(3)[THEN sym] and not_le using obt1(2) by auto
diff -r a93d25fb14fc -r b7f9e764532a src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Aug 21 13:23:29 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Aug 21 13:36:23 2011 +0200
@@ -966,13 +966,8 @@
 lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
   unfolding trivial_limit_def by (auto elim: eventually_rev_mp)
 
-lemma eventually_False: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net"
-  unfolding trivial_limit_def ..
-
 lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
-  apply (safe elim!: trivial_limit_eventually)
-  apply (simp add: eventually_False [symmetric])
-  done
+  by (simp add: filter_eq_iff)
 
 text{* Combining theorems for "eventually" *}
 
diff -r a93d25fb14fc -r b7f9e764532a src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Sun Aug 21 13:23:29 2011 +0200
+++ b/src/HOL/Nat_Numeral.thy	Sun Aug 21 13:36:23 2011 +0200
@@ -129,6 +129,14 @@
 
 end
 
+context idom
+begin
+
+lemma power2_eq_iff: "x\<twosuperior> = y\<twosuperior> \<longleftrightarrow> x = y \<or> x = - y"
+  unfolding power2_eq_square by (rule square_eq_iff)
+
+end
+
 context linordered_ring
 begin
 
diff -r a93d25fb14fc -r b7f9e764532a src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Sun Aug 21 13:23:29 2011 +0200
+++ b/src/HOL/NthRoot.thy	Sun Aug 21 13:36:23 2011 +0200
@@ -629,7 +629,7 @@
 apply (rule_tac y = "u/sqrt 2" in order_le_less_trans)
 apply (erule_tac [2] lemma_real_divide_sqrt_less)
 apply (rule power2_le_imp_le)
-apply (auto simp add: real_0_le_divide_iff power_divide)
+apply (auto simp add: zero_le_divide_iff power_divide)
 apply (rule_tac t = "u\<twosuperior>" in real_sum_of_halves [THEN subst])
 apply (rule add_mono)
 apply (auto simp add: four_x_squared intro: power_mono)
diff -r a93d25fb14fc -r b7f9e764532a src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Sun Aug 21 13:23:29 2011 +0200
+++ b/src/HOL/RealDef.thy	Sun Aug 21 13:36:23 2011 +0200
@@ -1553,11 +1553,6 @@
 
 subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
 
-text{*Needed in this non-standard form by Hyperreal/Transcendental*}
-lemma real_0_le_divide_iff:
-     "((0::real) \<le> x/y) = ((x \<le> 0 | 0 \<le> y) & (0 \<le> x | y \<le> 0))"
-by (auto simp add: zero_le_divide_iff)
-
 lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" 
 by arith
 
@@ -1606,36 +1601,11 @@
   shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n"
 by (simp add: power_commutes split add: nat_diff_split)
 
-text {* TODO: no longer real-specific; rename and move elsewhere *}
-lemma realpow_two_diff:
-  fixes x :: "'a::comm_ring_1"
-  shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
-by (simp add: algebra_simps)
-
-text {* TODO: move elsewhere *}
-lemma add_eq_0_iff:
-  fixes x y :: "'a::group_add"
-  shows "x + y = 0 \<longleftrightarrow> y = - x"
-by (auto dest: minus_unique)
-
-text {* TODO: no longer real-specific; rename and move elsewhere *}
-lemma realpow_two_disj:
-  fixes x :: "'a::idom"
-  shows "(x^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
-using realpow_two_diff [of x y]
-by (auto simp add: add_eq_0_iff)
-
 text {* FIXME: declare this [simp] for all types, or not at all *}
 lemma real_two_squares_add_zero_iff [simp]:
   "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"
 by (rule sum_squares_eq_zero_iff)
 
-text {* TODO: no longer real-specific; rename and move elsewhere *}
-lemma real_squared_diff_one_factored:
-  fixes x :: "'a::ring_1"
-  shows "x * x - 1 = (x + 1) * (x - 1)"
-by (simp add: algebra_simps)
-
 text {* FIXME: declare this [simp] for all types, or not at all *}
 lemma realpow_two_sum_zero_iff [simp]:
      "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
@@ -1674,13 +1644,13 @@
 lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
 by (force simp add: abs_le_iff)
 
-lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)"
+lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)"
 by (simp add: abs_if)
 
 lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
 by (rule abs_of_nonneg [OF real_of_nat_ge_zero])
 
-lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x"
+lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x"
 by simp
  
 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
diff -r a93d25fb14fc -r b7f9e764532a src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun Aug 21 13:23:29 2011 +0200
+++ b/src/HOL/Rings.thy	Sun Aug 21 13:36:23 2011 +0200
@@ -270,6 +270,10 @@
 subclass ring ..
 subclass comm_semiring_0_cancel ..
 
+lemma square_diff_square_factored:
+  "x * x - y * y = (x + y) * (x - y)"
+  by (simp add: algebra_simps)
+
 end
 
 class ring_1 = ring + zero_neq_one + monoid_mult
@@ -277,6 +281,10 @@
 
 subclass semiring_1_cancel ..
 
+lemma square_diff_one_factored:
+  "x * x - 1 = (x + 1) * (x - 1)"
+  by (simp add: algebra_simps)
+
 end
 
 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult