# HG changeset patch
# User haftmann
# Date 1398516802 -7200
# Node ID 678a52e676b67c85316c6b57ed01ab2b344597f5
# Parent  2b3710a4fa94f0d658c2e254b9cbb6532d94474f
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)

diff -r 2b3710a4fa94 -r 678a52e676b6 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Sat Apr 26 13:25:46 2014 +0200
+++ b/src/HOL/Complete_Lattices.thy	Sat Apr 26 14:53:22 2014 +0200
@@ -758,35 +758,93 @@
 
 subsection {* Complete lattice on unary and binary predicates *}
 
-lemma INF1_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
-  by auto
-
-lemma INF2_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
+lemma Inf1_I: 
+  "(\<And>P. P \<in> A \<Longrightarrow> P a) \<Longrightarrow> (\<Sqinter>A) a"
   by auto
 
-lemma INF1_D: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
+lemma INF1_I:
+  "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
+  by simp
+
+lemma INF2_I:
+  "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
+  by simp
+
+lemma Inf2_I: 
+  "(\<And>r. r \<in> A \<Longrightarrow> r a b) \<Longrightarrow> (\<Sqinter>A) a b"
   by auto
 
-lemma INF2_D: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
+lemma Inf1_D:
+  "(\<Sqinter>A) a \<Longrightarrow> P \<in> A \<Longrightarrow> P a"
   by auto
 
-lemma INF1_E: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> (B a b \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
+lemma INF1_D:
+  "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
+  by simp
+
+lemma Inf2_D:
+  "(\<Sqinter>A) a b \<Longrightarrow> r \<in> A \<Longrightarrow> r a b"
   by auto
 
-lemma INF2_E: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> (B a b c \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
-  by auto
+lemma INF2_D:
+  "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
+  by simp
+
+lemma Inf1_E:
+  assumes "(\<Sqinter>A) a"
+  obtains "P a" | "P \<notin> A"
+  using assms by auto
 
-lemma SUP1_I: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
+lemma INF1_E:
+  assumes "(\<Sqinter>x\<in>A. B x) b"
+  obtains "B a b" | "a \<notin> A"
+  using assms by auto
+
+lemma Inf2_E:
+  assumes "(\<Sqinter>A) a b"
+  obtains "r a b" | "r \<notin> A"
+  using assms by auto
+
+lemma INF2_E:
+  assumes "(\<Sqinter>x\<in>A. B x) b c"
+  obtains "B a b c" | "a \<notin> A"
+  using assms by auto
+
+lemma Sup1_I:
+  "P \<in> A \<Longrightarrow> P a \<Longrightarrow> (\<Squnion>A) a"
   by auto
 
-lemma SUP2_I: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
+lemma SUP1_I:
+  "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
+  by auto
+
+lemma Sup2_I:
+  "r \<in> A \<Longrightarrow> r a b \<Longrightarrow> (\<Squnion>A) a b"
+  by auto
+
+lemma SUP2_I:
+  "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
   by auto
 
-lemma SUP1_E: "(\<Squnion>x\<in>A. B x) b \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b \<Longrightarrow> R) \<Longrightarrow> R"
-  by auto
+lemma Sup1_E:
+  assumes "(\<Squnion>A) a"
+  obtains P where "P \<in> A" and "P a"
+  using assms by auto
+
+lemma SUP1_E:
+  assumes "(\<Squnion>x\<in>A. B x) b"
+  obtains x where "x \<in> A" and "B x b"
+  using assms by auto
 
-lemma SUP2_E: "(\<Squnion>x\<in>A. B x) b c \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b c \<Longrightarrow> R) \<Longrightarrow> R"
-  by auto
+lemma Sup2_E:
+  assumes "(\<Squnion>A) a b"
+  obtains r where "r \<in> A" "r a b"
+  using assms by auto
+
+lemma SUP2_E:
+  assumes "(\<Squnion>x\<in>A. B x) b c"
+  obtains x where "x \<in> A" "B x b c"
+  using assms by auto
 
 
 subsection {* Complete lattice on @{typ "_ set"} *}
diff -r 2b3710a4fa94 -r 678a52e676b6 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Apr 26 13:25:46 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Apr 26 14:53:22 2014 +0200
@@ -3291,7 +3291,8 @@
 
 lemma filter_from_subbase_not_bot:
   "\<forall>X \<subseteq> B. finite X \<longrightarrow> Inf X \<noteq> bot \<Longrightarrow> filter_from_subbase B \<noteq> bot"
-  unfolding trivial_limit_def eventually_filter_from_subbase by auto
+  unfolding trivial_limit_def eventually_filter_from_subbase
+    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
 
 lemma closure_iff_nhds_not_empty:
   "x \<in> closure X \<longleftrightarrow> (\<forall>A. \<forall>S\<subseteq>A. open S \<longrightarrow> x \<in> S \<longrightarrow> X \<inter> A \<noteq> {})"
diff -r 2b3710a4fa94 -r 678a52e676b6 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Apr 26 13:25:46 2014 +0200
+++ b/src/HOL/Relation.thy	Sat Apr 26 14:53:22 2014 +0200
@@ -30,15 +30,25 @@
 declare sup2E [elim!]
 declare sup1CI [intro!]
 declare sup2CI [intro!]
+declare Inf1_I [intro!]
 declare INF1_I [intro!]
+declare Inf2_I [intro!]
 declare INF2_I [intro!]
+declare Inf1_D [elim]
 declare INF1_D [elim]
+declare Inf2_D [elim]
 declare INF2_D [elim]
+declare Inf1_E [elim]
 declare INF1_E [elim]
+declare Inf2_E [elim]
 declare INF2_E [elim]
+declare Sup1_I [intro]
 declare SUP1_I [intro]
+declare Sup2_I [intro]
 declare SUP2_I [intro]
+declare Sup1_E [elim!]
 declare SUP1_E [elim!]
+declare Sup2_E [elim!]
 declare SUP2_E [elim!]
 
 subsection {* Fundamental *}