# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1449754720 0
# Node ID dcbe9f756ae0ca7c89a63040d9126a20d5439424
# Parent  5daa82ba4078c7720df7ded3f627ead14a4da8bd
not_leE -> not_le_imp_less and other tidying

diff -r 5daa82ba4078 -r dcbe9f756ae0 src/HOL/Conditionally_Complete_Lattices.thy
--- 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"
diff -r 5daa82ba4078 -r dcbe9f756ae0 src/HOL/Decision_Procs/Approximation.thy
--- 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:
diff -r 5daa82ba4078 -r dcbe9f756ae0 src/HOL/Library/Disjoint_Sets.thy
--- 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)"
diff -r 5daa82ba4078 -r dcbe9f756ae0 src/HOL/List.thy
--- 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
diff -r 5daa82ba4078 -r dcbe9f756ae0 src/HOL/Matrix_LP/Matrix.thy
--- 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
diff -r 5daa82ba4078 -r dcbe9f756ae0 src/HOL/Metis_Examples/Big_O.thy
--- 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)
 
diff -r 5daa82ba4078 -r dcbe9f756ae0 src/HOL/Multivariate_Analysis/Derivative.thy
--- 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>
diff -r 5daa82ba4078 -r dcbe9f756ae0 src/HOL/Multivariate_Analysis/Integration.thy
--- 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)
diff -r 5daa82ba4078 -r dcbe9f756ae0 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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>
 
diff -r 5daa82ba4078 -r dcbe9f756ae0 src/HOL/Orderings.thy
--- 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
diff -r 5daa82ba4078 -r dcbe9f756ae0 src/HOL/UNITY/SubstAx.thy
--- 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
 
 
diff -r 5daa82ba4078 -r dcbe9f756ae0 src/HOL/UNITY/WFair.thy
--- 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
 
 
diff -r 5daa82ba4078 -r dcbe9f756ae0 src/HOL/Word/Word.thy
--- 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