--- 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 .
--- 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"
--- 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)
--- 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
--- 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" *}
--- 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
--- 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)
--- 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)"
--- 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