author haftmann Sat Apr 26 14:53:22 2014 +0200 (2014-04-26) changeset 56742 678a52e676b6 parent 56741 2b3710a4fa94 child 56762 539fe017905a
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
```     1.1 --- a/src/HOL/Complete_Lattices.thy	Sat Apr 26 13:25:46 2014 +0200
1.2 +++ b/src/HOL/Complete_Lattices.thy	Sat Apr 26 14:53:22 2014 +0200
1.3 @@ -758,35 +758,93 @@
1.4
1.5  subsection {* Complete lattice on unary and binary predicates *}
1.6
1.7 -lemma INF1_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
1.8 -  by auto
1.9 -
1.10 -lemma INF2_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
1.11 +lemma Inf1_I:
1.12 +  "(\<And>P. P \<in> A \<Longrightarrow> P a) \<Longrightarrow> (\<Sqinter>A) a"
1.13    by auto
1.14
1.15 -lemma INF1_D: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
1.16 +lemma INF1_I:
1.17 +  "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
1.18 +  by simp
1.19 +
1.20 +lemma INF2_I:
1.21 +  "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
1.22 +  by simp
1.23 +
1.24 +lemma Inf2_I:
1.25 +  "(\<And>r. r \<in> A \<Longrightarrow> r a b) \<Longrightarrow> (\<Sqinter>A) a b"
1.26    by auto
1.27
1.28 -lemma INF2_D: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
1.29 +lemma Inf1_D:
1.30 +  "(\<Sqinter>A) a \<Longrightarrow> P \<in> A \<Longrightarrow> P a"
1.31    by auto
1.32
1.33 -lemma INF1_E: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> (B a b \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
1.34 +lemma INF1_D:
1.35 +  "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
1.36 +  by simp
1.37 +
1.38 +lemma Inf2_D:
1.39 +  "(\<Sqinter>A) a b \<Longrightarrow> r \<in> A \<Longrightarrow> r a b"
1.40    by auto
1.41
1.42 -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"
1.43 -  by auto
1.44 +lemma INF2_D:
1.45 +  "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
1.46 +  by simp
1.47 +
1.48 +lemma Inf1_E:
1.49 +  assumes "(\<Sqinter>A) a"
1.50 +  obtains "P a" | "P \<notin> A"
1.51 +  using assms by auto
1.52
1.53 -lemma SUP1_I: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
1.54 +lemma INF1_E:
1.55 +  assumes "(\<Sqinter>x\<in>A. B x) b"
1.56 +  obtains "B a b" | "a \<notin> A"
1.57 +  using assms by auto
1.58 +
1.59 +lemma Inf2_E:
1.60 +  assumes "(\<Sqinter>A) a b"
1.61 +  obtains "r a b" | "r \<notin> A"
1.62 +  using assms by auto
1.63 +
1.64 +lemma INF2_E:
1.65 +  assumes "(\<Sqinter>x\<in>A. B x) b c"
1.66 +  obtains "B a b c" | "a \<notin> A"
1.67 +  using assms by auto
1.68 +
1.69 +lemma Sup1_I:
1.70 +  "P \<in> A \<Longrightarrow> P a \<Longrightarrow> (\<Squnion>A) a"
1.71    by auto
1.72
1.73 -lemma SUP2_I: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
1.74 +lemma SUP1_I:
1.75 +  "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
1.76 +  by auto
1.77 +
1.78 +lemma Sup2_I:
1.79 +  "r \<in> A \<Longrightarrow> r a b \<Longrightarrow> (\<Squnion>A) a b"
1.80 +  by auto
1.81 +
1.82 +lemma SUP2_I:
1.83 +  "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
1.84    by auto
1.85
1.86 -lemma SUP1_E: "(\<Squnion>x\<in>A. B x) b \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b \<Longrightarrow> R) \<Longrightarrow> R"
1.87 -  by auto
1.88 +lemma Sup1_E:
1.89 +  assumes "(\<Squnion>A) a"
1.90 +  obtains P where "P \<in> A" and "P a"
1.91 +  using assms by auto
1.92 +
1.93 +lemma SUP1_E:
1.94 +  assumes "(\<Squnion>x\<in>A. B x) b"
1.95 +  obtains x where "x \<in> A" and "B x b"
1.96 +  using assms by auto
1.97
1.98 -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"
1.99 -  by auto
1.100 +lemma Sup2_E:
1.101 +  assumes "(\<Squnion>A) a b"
1.102 +  obtains r where "r \<in> A" "r a b"
1.103 +  using assms by auto
1.104 +
1.105 +lemma SUP2_E:
1.106 +  assumes "(\<Squnion>x\<in>A. B x) b c"
1.107 +  obtains x where "x \<in> A" "B x b c"
1.108 +  using assms by auto
1.109
1.110
1.111  subsection {* Complete lattice on @{typ "_ set"} *}
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Apr 26 13:25:46 2014 +0200
2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Apr 26 14:53:22 2014 +0200
2.3 @@ -3291,7 +3291,8 @@
2.4
2.5  lemma filter_from_subbase_not_bot:
2.6    "\<forall>X \<subseteq> B. finite X \<longrightarrow> Inf X \<noteq> bot \<Longrightarrow> filter_from_subbase B \<noteq> bot"
2.7 -  unfolding trivial_limit_def eventually_filter_from_subbase by auto
2.8 +  unfolding trivial_limit_def eventually_filter_from_subbase
2.9 +    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
2.10
2.11  lemma closure_iff_nhds_not_empty:
2.12    "x \<in> closure X \<longleftrightarrow> (\<forall>A. \<forall>S\<subseteq>A. open S \<longrightarrow> x \<in> S \<longrightarrow> X \<inter> A \<noteq> {})"
```
```     3.1 --- a/src/HOL/Relation.thy	Sat Apr 26 13:25:46 2014 +0200
3.2 +++ b/src/HOL/Relation.thy	Sat Apr 26 14:53:22 2014 +0200
3.3 @@ -30,15 +30,25 @@
3.4  declare sup2E [elim!]
3.5  declare sup1CI [intro!]
3.6  declare sup2CI [intro!]
3.7 +declare Inf1_I [intro!]
3.8  declare INF1_I [intro!]
3.9 +declare Inf2_I [intro!]
3.10  declare INF2_I [intro!]
3.11 +declare Inf1_D [elim]
3.12  declare INF1_D [elim]
3.13 +declare Inf2_D [elim]
3.14  declare INF2_D [elim]
3.15 +declare Inf1_E [elim]
3.16  declare INF1_E [elim]
3.17 +declare Inf2_E [elim]
3.18  declare INF2_E [elim]
3.19 +declare Sup1_I [intro]
3.20  declare SUP1_I [intro]
3.21 +declare Sup2_I [intro]
3.22  declare SUP2_I [intro]
3.23 +declare Sup1_E [elim!]
3.24  declare SUP1_E [elim!]
3.25 +declare Sup2_E [elim!]
3.26  declare SUP2_E [elim!]
3.27
3.28  subsection {* Fundamental *}
```