# HG changeset patch
# User hoelzl
# Date 1361358282 -3600
# Node ID d63ec23c9125f7203e48807f204c8b42c9914dd8
# Parent  62c033d7f3d8ad84c16d6cc2b1616070e2d88013
move auxiliary lemmas from Library/Extended_Reals to HOL image

diff -r 62c033d7f3d8 -r d63ec23c9125 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Mon Mar 04 09:57:54 2013 +0100
+++ b/src/HOL/Complete_Lattices.thy	Wed Feb 20 12:04:42 2013 +0100
@@ -89,6 +89,22 @@
   by (simp add: fun_eq_iff SUP_def
     complete_lattice.INF_def [OF dual_complete_lattice])
 
+lemma Sup_eqI:
+  "(\<And>y. y \<in> A \<Longrightarrow> y \<le> x) \<Longrightarrow> (\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> \<Squnion>A = x"
+  by (blast intro: antisym Sup_least Sup_upper)
+
+lemma Inf_eqI:
+  "(\<And>i. i \<in> A \<Longrightarrow> x \<le> i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x) \<Longrightarrow> \<Sqinter>A = x"
+  by (blast intro: antisym Inf_greatest Inf_lower)
+
+lemma SUP_eqI:
+  "(\<And>i. i \<in> A \<Longrightarrow> f i \<le> x) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> (\<Squnion>i\<in>A. f i) = x"
+  unfolding SUP_def by (rule Sup_eqI) auto
+
+lemma INF_eqI:
+  "(\<And>i. i \<in> A \<Longrightarrow> x \<le> f i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<ge> y) \<Longrightarrow> x \<ge> y) \<Longrightarrow> (\<Sqinter>i\<in>A. f i) = x"
+  unfolding INF_def by (rule Inf_eqI) auto
+
 lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
   by (auto simp add: INF_def intro: Inf_lower)
 
@@ -242,6 +258,18 @@
   ultimately show ?thesis by (rule Sup_upper2)
 qed
 
+lemma SUPR_eq:
+  assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j"
+  assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
+  shows "(SUP i:A. f i) = (SUP j:B. g j)"
+  by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
+
+lemma INFI_eq:
+  assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
+  assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
+  shows "(INF i:A. f i) = (INF j:B. g j)"
+  by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
+
 lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
   by (auto intro: Inf_greatest Inf_lower)
 
@@ -378,6 +406,12 @@
   "(\<Squnion>b. A b) = A True \<squnion> A False"
   by (simp add: UNIV_bool SUP_insert sup_commute)
 
+lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
+  by (blast intro: Sup_upper2 Inf_lower ex_in_conv)
+
+lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
+  unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
+
 end
 
 class complete_distrib_lattice = complete_lattice +
@@ -530,9 +564,31 @@
   "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
   unfolding INF_def by auto
 
+lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
+proof safe
+  fix y assume "x \<le> \<Squnion>A" "y < x"
+  then have "y < \<Squnion>A" by auto
+  then show "\<exists>a\<in>A. y < a"
+    unfolding less_Sup_iff .
+qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper)
+
+lemma le_SUP_iff: "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
+  unfolding le_Sup_iff SUP_def by simp
+
+lemma Inf_le_iff: "\<Sqinter>A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
+proof safe
+  fix y assume "x \<ge> \<Sqinter>A" "y > x"
+  then have "y > \<Sqinter>A" by auto
+  then show "\<exists>a\<in>A. y > a"
+    unfolding Inf_less_iff .
+qed (auto elim!: allE[of _ "\<Sqinter>A"] simp add: not_le[symmetric] Inf_lower)
+
+lemma INF_le_iff:
+  "INFI A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
+  unfolding Inf_le_iff INF_def by simp
+
 end
 
-
 subsection {* Complete lattice on @{typ bool} *}
 
 instantiation bool :: complete_lattice
diff -r 62c033d7f3d8 -r d63ec23c9125 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Mon Mar 04 09:57:54 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Wed Feb 20 12:04:42 2013 +0100
@@ -18,79 +18,6 @@
 
 *}
 
-lemma LIMSEQ_SUP:
-  fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
-  assumes "incseq X"
-  shows "X ----> (SUP i. X i)"
-  using `incseq X`
-  by (intro increasing_tendsto)
-     (auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans)
-
-lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
-  by (cases P) (simp_all add: eventually_False)
-
-lemma (in complete_lattice) Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
-  by (metis Sup_upper2 Inf_lower ex_in_conv)
-
-lemma (in complete_lattice) INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
-  unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
-
-lemma (in complete_linorder) le_Sup_iff:
-  "x \<le> Sup A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
-proof safe
-  fix y assume "x \<le> Sup A" "y < x"
-  then have "y < Sup A" by auto
-  then show "\<exists>a\<in>A. y < a"
-    unfolding less_Sup_iff .
-qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] Sup_upper)
-
-lemma (in complete_linorder) le_SUP_iff:
-  "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
-  unfolding le_Sup_iff SUP_def by simp
-
-lemma (in complete_linorder) Inf_le_iff:
-  "Inf A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
-proof safe
-  fix y assume "x \<ge> Inf A" "y > x"
-  then have "y > Inf A" by auto
-  then show "\<exists>a\<in>A. y > a"
-    unfolding Inf_less_iff .
-qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] Inf_lower)
-
-lemma (in complete_linorder) le_INF_iff:
-  "INFI A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
-  unfolding Inf_le_iff INF_def by simp
-
-lemma (in complete_lattice) Sup_eqI:
-  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
-  assumes "\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y"
-  shows "Sup A = x"
-  by (metis antisym Sup_least Sup_upper assms)
-
-lemma (in complete_lattice) Inf_eqI:
-  assumes "\<And>i. i \<in> A \<Longrightarrow> x \<le> i"
-  assumes "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x"
-  shows "Inf A = x"
-  by (metis antisym Inf_greatest Inf_lower assms)
-
-lemma (in complete_lattice) SUP_eqI:
-  "(\<And>i. i \<in> A \<Longrightarrow> f i \<le> x) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> (SUP i:A. f i) = x"
-  unfolding SUP_def by (rule Sup_eqI) auto
-
-lemma (in complete_lattice) INF_eqI:
-  "(\<And>i. i \<in> A \<Longrightarrow> x \<le> f i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<ge> y) \<Longrightarrow> x \<ge> y) \<Longrightarrow> (INF i:A. f i) = x"
-  unfolding INF_def by (rule Inf_eqI) auto
-
-lemma (in complete_lattice) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
-proof
-  assume "{x..} = UNIV"
-  show "x = bot"
-  proof (rule ccontr)
-    assume "x \<noteq> bot" then have "bot \<notin> {x..}" by (simp add: le_less)
-    then show False using `{x..} = UNIV` by simp
-  qed
-qed auto
-
 lemma SUPR_pair:
   "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
   by (rule antisym) (auto intro!: SUP_least SUP_upper2)
@@ -1447,43 +1374,6 @@
     by (auto simp: top_ereal_def)
 qed
 
-lemma ereal_le_Sup:
-  fixes x :: ereal
-  shows "(x <= (SUP i:A. f i)) <-> (ALL y. y < x --> (EX i. i : A & y <= f i))" (is "?lhs = ?rhs")
-proof-
-{ assume "?rhs"
-  { assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i)<x" by (simp add: not_le)
-    then obtain y where y_def: "(SUP i:A. f i)<y & y<x" using ereal_dense by auto
-    then obtain i where "i : A & y <= f i" using `?rhs` by auto
-    hence "y <= (SUP i:A. f i)" using SUP_upper[of i A f] by auto
-    hence False using y_def by auto
-  } hence "?lhs" by auto
-}
-moreover
-{ assume "?lhs" hence "?rhs"
-  by (metis less_SUP_iff order_less_imp_le order_less_le_trans)
-} ultimately show ?thesis by auto
-qed
-
-lemma ereal_Inf_le:
-  fixes x :: ereal
-  shows "((INF i:A. f i) <= x) <-> (ALL y. x < y --> (EX i. i : A & f i <= y))"
-(is "?lhs <-> ?rhs")
-proof-
-{ assume "?rhs"
-  { assume "~((INF i:A. f i) <= x)" hence "x < (INF i:A. f i)" by (simp add: not_le)
-    then obtain y where y_def: "x<y & y<(INF i:A. f i)" using ereal_dense by auto
-    then obtain i where "i : A & f i <= y" using `?rhs` by auto
-    hence "(INF i:A. f i) <= y" using INF_lower[of i A f] by auto
-    hence False using y_def by auto
-  } hence "?lhs" by auto
-}
-moreover
-{ assume "?lhs" hence "?rhs"
-  by (metis INF_less_iff order_le_less order_less_le_trans)
-} ultimately show ?thesis by auto
-qed
-
 lemma Inf_less:
   fixes x :: ereal
   assumes "(INF i:A. f i) < x"
@@ -1495,44 +1385,6 @@
   thus False using assms by auto
 qed
 
-lemma same_INF:
-  assumes "ALL e:A. f e = g e"
-  shows "(INF e:A. f e) = (INF e:A. g e)"
-proof-
-have "f ` A = g ` A" unfolding image_def using assms by auto
-thus ?thesis unfolding INF_def by auto
-qed
-
-lemma same_SUP:
-  assumes "ALL e:A. f e = g e"
-  shows "(SUP e:A. f e) = (SUP e:A. g e)"
-proof-
-have "f ` A = g ` A" unfolding image_def using assms by auto
-thus ?thesis unfolding SUP_def by auto
-qed
-
-lemma SUPR_eq:
-  assumes "\<forall>i\<in>A. \<exists>j\<in>B. f i \<le> g j"
-  assumes "\<forall>j\<in>B. \<exists>i\<in>A. g j \<le> f i"
-  shows "(SUP i:A. f i) = (SUP j:B. g j)"
-proof (intro antisym)
-  show "(SUP i:A. f i) \<le> (SUP j:B. g j)"
-    using assms by (metis SUP_least SUP_upper2)
-  show "(SUP i:B. g i) \<le> (SUP j:A. f j)"
-    using assms by (metis SUP_least SUP_upper2)
-qed
-
-lemma INFI_eq:
-  assumes "\<forall>i\<in>A. \<exists>j\<in>B. f i \<ge> g j"
-  assumes "\<forall>j\<in>B. \<exists>i\<in>A. g j \<ge> f i"
-  shows "(INF i:A. f i) = (INF j:B. g j)"
-proof (intro antisym)
-  show "(INF i:A. f i) \<le> (INF j:B. g j)"
-    using assms by (metis INF_greatest INF_lower2)
-  show "(INF i:B. g i) \<le> (INF j:A. f j)"
-    using assms by (metis INF_greatest INF_lower2)
-qed
-
 lemma SUP_ereal_le_addI:
   fixes f :: "'i \<Rightarrow> ereal"
   assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
diff -r 62c033d7f3d8 -r d63ec23c9125 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Mar 04 09:57:54 2013 +0100
+++ b/src/HOL/Limits.thy	Wed Feb 20 12:04:42 2013 +0100
@@ -264,6 +264,9 @@
 lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
   by (rule eventually_False [symmetric])
 
+lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
+  by (cases P) (simp_all add: eventually_False)
+
 
 subsection {* Map function for filters *}
 
diff -r 62c033d7f3d8 -r d63ec23c9125 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Mon Mar 04 09:57:54 2013 +0100
+++ b/src/HOL/SEQ.thy	Wed Feb 20 12:04:42 2013 +0100
@@ -322,6 +322,16 @@
   shows "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
   using trivial_limit_sequentially by (rule tendsto_const_iff)
 
+lemma LIMSEQ_SUP:
+  "incseq X \<Longrightarrow> X ----> (SUP i. X i :: 'a :: {complete_linorder, linorder_topology})"
+  by (intro increasing_tendsto)
+     (auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans)
+
+lemma LIMSEQ_INF:
+  "decseq X \<Longrightarrow> X ----> (INF i. X i :: 'a :: {complete_linorder, linorder_topology})"
+  by (intro decreasing_tendsto)
+     (auto simp: INF_lower INF_less_iff decseq_def eventually_sequentially intro: le_less_trans)
+
 lemma LIMSEQ_ignore_initial_segment:
   "f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
 apply (rule topological_tendstoI)
diff -r 62c033d7f3d8 -r d63ec23c9125 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Mar 04 09:57:54 2013 +0100
+++ b/src/HOL/Set_Interval.thy	Wed Feb 20 12:04:42 2013 +0100
@@ -330,6 +330,20 @@
   shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
   using atLeastLessThan_inj assms by auto
 
+context complete_lattice
+begin
+
+lemma atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
+  by (auto simp: set_eq_iff intro: le_bot)
+
+lemma atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top"
+  by (auto simp: set_eq_iff intro: top_le)
+
+lemma atLeastAtMost_eq_UNIV_iff: "{x..y} = UNIV \<longleftrightarrow> (x = bot \<and> y = top)"
+  by (auto simp: set_eq_iff intro: top_le le_bot)
+
+end
+
 subsubsection {* Intersection *}
 
 context linorder