--- a/src/HOL/Conditionally_Complete_Lattices.thy Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Thu Dec 10 13:38:40 2015 +0000
@@ -413,11 +413,11 @@
lemma less_cSupD:
"X \<noteq> {} \<Longrightarrow> z < Sup X \<Longrightarrow> \<exists>x\<in>X. z < x"
- by (metis less_cSup_iff not_leE bdd_above_def)
+ by (metis less_cSup_iff not_le_imp_less bdd_above_def)
lemma cInf_lessD:
"X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z"
- by (metis cInf_less_iff not_leE bdd_below_def)
+ by (metis cInf_less_iff not_le_imp_less bdd_below_def)
lemma complete_interval:
assumes "a < b" and "P a" and "\<not> P b"
--- a/src/HOL/Decision_Procs/Approximation.thy Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Dec 10 13:38:40 2015 +0000
@@ -2335,7 +2335,7 @@
thus ?th1 ?th2
using Float_representation_aux[of m e]
unfolding x_def[symmetric]
- by (auto dest: not_leE)
+ by (auto dest: not_le_imp_less)
qed
lemma ln_shifted_float:
--- a/src/HOL/Library/Disjoint_Sets.thy Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/Library/Disjoint_Sets.thy Thu Dec 10 13:38:40 2015 +0000
@@ -79,7 +79,7 @@
"(\<And>n. A n \<subseteq> A (Suc n)) \<Longrightarrow> disjoint_family (\<lambda>i. A (Suc i) - A i)"
using lift_Suc_mono_le[of A]
by (auto simp add: disjoint_family_on_def)
- (metis insert_absorb insert_subset le_SucE le_antisym not_leE less_imp_le)
+ (metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le)
lemma disjoint_family_on_disjoint_image:
"disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)"
--- a/src/HOL/List.thy Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/List.thy Thu Dec 10 13:38:40 2015 +0000
@@ -3958,7 +3958,7 @@
lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
apply (case_tac "k \<le> i")
apply (simp add: min_def)
-apply (drule not_leE)
+apply (drule not_le_imp_less)
apply (simp add: min_def)
apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
apply simp
--- a/src/HOL/Matrix_LP/Matrix.thy Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/Matrix_LP/Matrix.thy Thu Dec 10 13:38:40 2015 +0000
@@ -875,7 +875,7 @@
apply (subst RepAbs_matrix)
apply auto
apply (simp add: Suc_le_eq)
-apply (rule not_leE)
+apply (rule not_le_imp_less)
apply (subst nrows_le)
by simp
qed
@@ -891,7 +891,7 @@
apply (subst RepAbs_matrix)
apply auto
apply (simp add: Suc_le_eq)
-apply (rule not_leE)
+apply (rule not_le_imp_less)
apply (subst ncols_le)
by simp
qed
--- a/src/HOL/Metis_Examples/Big_O.thy Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy Thu Dec 10 13:38:40 2015 +0000
@@ -25,7 +25,7 @@
\<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
by (metis (no_types) abs_ge_zero
algebra_simps mult.comm_neutral
- mult_nonpos_nonneg not_leE order_trans zero_less_one)
+ mult_nonpos_nonneg not_le_imp_less order_trans zero_less_one)
(*** Now various verions with an increasing shrink factor ***)
@@ -686,7 +686,7 @@
apply simp
apply (subst abs_of_nonneg)
apply (drule_tac x = x in spec) back
- apply (metis diff_less_0_iff_less linorder_not_le not_leE xt1(12) xt1(6))
+ apply (metis diff_less_0_iff_less linorder_not_le not_le_imp_less xt1(12) xt1(6))
apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
by (metis abs_ge_zero linorder_linear max.absorb1 max.commute)
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Dec 10 13:38:40 2015 +0000
@@ -9,21 +9,6 @@
imports Brouwer_Fixpoint Operator_Norm Uniform_Limit
begin
-lemma netlimit_at_vector: (* TODO: move *)
- fixes a :: "'a::real_normed_vector"
- shows "netlimit (at a) = a"
-proof (cases "\<exists>x. x \<noteq> a")
- case True then obtain x where x: "x \<noteq> a" ..
- have "\<not> trivial_limit (at a)"
- unfolding trivial_limit_def eventually_at dist_norm
- apply clarsimp
- apply (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI)
- apply (simp add: norm_sgn sgn_zero_iff x)
- done
- then show ?thesis
- by (rule netlimit_within [of a UNIV])
-qed simp
-
declare has_derivative_bounded_linear[dest]
subsection \<open>Derivatives\<close>
--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Thu Dec 10 13:38:40 2015 +0000
@@ -12,24 +12,47 @@
begin
lemma cSup_abs_le: (* TODO: move to Conditionally_Complete_Lattices.thy? *)
- fixes S :: "real set"
+ fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
apply (auto simp add: abs_le_iff intro: cSup_least)
by (metis bdd_aboveI cSup_upper neg_le_iff_le order_trans)
lemma cInf_abs_ge:
- fixes S :: "real set"
- shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
- using cSup_abs_le [of "uminus ` S"]
- by (fastforce simp add: Inf_real_def)
+ fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
+ assumes "S \<noteq> {}" and bdd: "\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a"
+ shows "\<bar>Inf S\<bar> \<le> a"
+proof -
+ have "Sup (uminus ` S) = - (Inf S)"
+ proof (rule antisym)
+ show "- (Inf S) \<le> Sup(uminus ` S)"
+ apply (subst minus_le_iff)
+ apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>])
+ apply (subst minus_le_iff)
+ apply (rule cSup_upper, force)
+ using bdd apply (force simp add: abs_le_iff bdd_above_def)
+ done
+ next
+ show "Sup (uminus ` S) \<le> - Inf S"
+ apply (rule cSup_least)
+ using \<open>S \<noteq> {}\<close> apply (force simp add: )
+ apply clarsimp
+ apply (rule cInf_lower)
+ apply assumption
+ using bdd apply (simp add: bdd_below_def)
+ apply (rule_tac x="-a" in exI)
+ apply force
+ done
+ qed
+ with cSup_abs_le [of "uminus ` S"] assms show ?thesis by fastforce
+qed
lemma cSup_asclose:
- fixes S :: "real set"
+ fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
assumes S: "S \<noteq> {}"
and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
shows "\<bar>Sup S - l\<bar> \<le> e"
proof -
- have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
+ have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
by arith
have "bdd_above S"
using b by (auto intro!: bdd_aboveI[of _ "l + e"])
@@ -53,26 +76,6 @@
by (simp add: Inf_real_def)
qed
-lemma cSup_finite_ge_iff:
- fixes S :: "real set"
- shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Sup S \<longleftrightarrow> (\<exists>x\<in>S. a \<le> x)"
- by (metis cSup_eq_Max Max_ge_iff)
-
-lemma cSup_finite_le_iff:
- fixes S :: "real set"
- shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Sup S \<longleftrightarrow> (\<forall>x\<in>S. a \<ge> x)"
- by (metis cSup_eq_Max Max_le_iff)
-
-lemma cInf_finite_ge_iff:
- fixes S :: "real set"
- shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)"
- by (metis cInf_eq_Min Min_ge_iff)
-
-lemma cInf_finite_le_iff:
- fixes S :: "real set"
- shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)"
- by (metis cInf_eq_Min Min_le_iff)
-
lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
@@ -87,7 +90,6 @@
lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
-lemma conjunctD5: assumes "a \<and> b \<and> c \<and> d \<and> e" shows a b c d e using assms by auto
declare norm_triangle_ineq4[intro]
@@ -5145,17 +5147,11 @@
done
}
assume as': "p \<noteq> {}"
- from real_arch_simple[of "Sup((\<lambda>(x,k). norm(f x)) ` p)"] guess N ..
+ from real_arch_simple[of "Max((\<lambda>(x,k). norm(f x)) ` p)"] guess N ..
then have N: "\<forall>x\<in>(\<lambda>(x, k). norm (f x)) ` p. x \<le> real N"
- apply (subst(asm) cSup_finite_le_iff)
- using as as'
- apply auto
- done
+ by (meson Max_ge as(1) dual_order.trans finite_imageI tagged_division_of_finite)
have "\<forall>i. \<exists>q. q tagged_division_of (cbox a b) \<and> (d i) fine q \<and> (\<forall>(x, k)\<in>p. k \<subseteq> (d i) x \<longrightarrow> (x, k) \<in> q)"
- apply rule
- apply (rule tagged_division_finer[OF as(1) d(1)])
- apply auto
- done
+ by (auto intro: tagged_division_finer[OF as(1) d(1)])
from choice[OF this] guess q .. note q=conjunctD3[OF this[rule_format]]
have *: "\<And>i. (\<Sum>(x, k)\<in>q i. content k *\<^sub>R indicator s x) \<ge> (0::real)"
apply (rule setsum_nonneg)
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Dec 10 13:38:40 2015 +0000
@@ -2560,6 +2560,21 @@
shows "netlimit (at x within S) = x"
using assms by (metis at_within_interior netlimit_at)
+lemma netlimit_at_vector:
+ fixes a :: "'a::real_normed_vector"
+ shows "netlimit (at a) = a"
+proof (cases "\<exists>x. x \<noteq> a")
+ case True then obtain x where x: "x \<noteq> a" ..
+ have "\<not> trivial_limit (at a)"
+ unfolding trivial_limit_def eventually_at dist_norm
+ apply clarsimp
+ apply (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI)
+ apply (simp add: norm_sgn sgn_zero_iff x)
+ done
+ then show ?thesis
+ by (rule netlimit_within [of a UNIV])
+qed simp
+
text\<open>Useful lemmas on closure and set of possible sequential limits.\<close>
--- a/src/HOL/Orderings.thy Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/Orderings.thy Thu Dec 10 13:38:40 2015 +0000
@@ -82,7 +82,7 @@
"a \<noteq> top \<longleftrightarrow> a \<prec> top"
by (auto simp add: order_iff_strict intro: not_eq_order_implies_strict extremum)
-end
+end
subsection \<open>Syntactic orders\<close>
@@ -97,7 +97,7 @@
less_eq ("(_/ <= _)" [51, 51] 50) and
less ("op <") and
less ("(_/ < _)" [51, 51] 50)
-
+
notation (xsymbols)
less_eq ("op \<le>") and
less_eq ("(_/ \<le> _)" [51, 51] 50)
@@ -149,13 +149,13 @@
text \<open>Transitivity.\<close>
lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
-by (auto simp add: less_le_not_le intro: order_trans)
+by (auto simp add: less_le_not_le intro: order_trans)
lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
-by (auto simp add: less_le_not_le intro: order_trans)
+by (auto simp add: less_le_not_le intro: order_trans)
lemma less_le_trans: "x < y \<Longrightarrow> y \<le> z \<Longrightarrow> x < z"
-by (auto simp add: less_le_not_le intro: order_trans)
+by (auto simp add: less_le_not_le intro: order_trans)
text \<open>Useful for simplification, but too risky to include by default.\<close>
@@ -360,8 +360,7 @@
lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y"
unfolding not_less .
-(*FIXME inappropriate name (or delete altogether)*)
-lemma not_leE: "\<not> y \<le> x \<Longrightarrow> x < y"
+lemma not_le_imp_less: "\<not> y \<le> x \<Longrightarrow> x < y"
unfolding not_le .
text \<open>Dual order\<close>
@@ -516,11 +515,11 @@
is not a parameter of the locale. *)
declare less_irrefl [THEN notE, order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"]
-
+
declare order_refl [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"]
-
+
declare less_imp_le [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"]
-
+
declare antisym [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"]
declare eq_refl [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"]
@@ -528,9 +527,9 @@
declare sym [THEN eq_refl, order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"]
declare less_trans [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
-
+
declare less_le_trans [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
-
+
declare le_less_trans [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
declare order_trans [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
@@ -950,7 +949,7 @@
"(x::'a::order) > y ==> y > z ==> x > z"
"(a::'a::order) >= b ==> a ~= b ==> a > b"
"(a::'a::order) ~= b ==> a >= b ==> a > b"
- "a = f b ==> b > c ==> (!!x y. x > y ==> f x > f y) ==> a > f c"
+ "a = f b ==> b > c ==> (!!x y. x > y ==> f x > f y) ==> a > f c"
"a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==> f a > c"
"a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
"a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c"
@@ -990,11 +989,11 @@
lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9
-(*
+(*
Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands
for the wrong thing in an Isar proof.
- The extra transitivity rules can be used as follows:
+ The extra transitivity rules can be used as follows:
lemma "(a::'a::order) > z"
proof -
@@ -1145,7 +1144,7 @@
with \<open>f x \<le> f y\<close> show False by simp
qed
qed
-
+
lemma strict_mono_less:
assumes "strict_mono f"
shows "f x < f y \<longleftrightarrow> x < y"
@@ -1317,10 +1316,10 @@
end
-class no_top = order +
+class no_top = order +
assumes gt_ex: "\<exists>y. x < y"
-class no_bot = order +
+class no_bot = order +
assumes lt_ex: "\<exists>y. y < x"
class unbounded_dense_linorder = dense_linorder + no_top + no_bot
--- a/src/HOL/UNITY/SubstAx.thy Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/UNITY/SubstAx.thy Thu Dec 10 13:38:40 2015 +0000
@@ -361,7 +361,7 @@
apply (simp add: Image_singleton, clarify)
apply (case_tac "m<l")
apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
-apply (blast intro: not_leE subset_imp_LeadsTo)
+apply (blast intro: not_le_imp_less subset_imp_LeadsTo)
done
--- a/src/HOL/UNITY/WFair.thy Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/UNITY/WFair.thy Thu Dec 10 13:38:40 2015 +0000
@@ -488,7 +488,7 @@
apply clarify
apply (case_tac "m<l")
apply (blast intro: leadsTo_weaken_R diff_less_mono2)
-apply (blast intro: not_leE subset_imp_leadsTo)
+apply (blast intro: not_le_imp_less subset_imp_leadsTo)
done
--- a/src/HOL/Word/Word.thy Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/Word/Word.thy Thu Dec 10 13:38:40 2015 +0000
@@ -3599,7 +3599,7 @@
apply (simp (no_asm), arith)
apply (simp (no_asm), arith)
apply (rule notI [THEN notnotD],
- drule leI not_leE,
+ drule leI not_le_imp_less,
drule sbintrunc_inc sbintrunc_dec,
simp)+
done