more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
authorhaftmann
Sat Apr 26 14:53:22 2014 +0200 (2014-04-26)
changeset 56742678a52e676b6
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)
src/HOL/Complete_Lattices.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Relation.thy
     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 *}