author haftmann Sun Jul 10 15:45:35 2011 +0200 (2011-07-10) changeset 43741 fac11b64713c parent 43740 3316e6831801 child 43742 d033a34a490a
tuned proofs and notation
```     1.1 --- a/src/HOL/Complete_Lattice.thy	Sun Jul 10 14:26:07 2011 +0200
1.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 10 15:45:35 2011 +0200
1.3 @@ -85,47 +85,47 @@
1.4  lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
1.5    by (auto intro: Inf_greatest dest: Inf_lower)
1.6
1.7 -lemma Sup_le_iff: "Sup A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
1.8 +lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
1.9    by (auto intro: Sup_least dest: Sup_upper)
1.10
1.11  lemma Inf_mono:
1.12    assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b"
1.13 -  shows "Inf A \<sqsubseteq> Inf B"
1.14 +  shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B"
1.15  proof (rule Inf_greatest)
1.16    fix b assume "b \<in> B"
1.17    with assms obtain a where "a \<in> A" and "a \<sqsubseteq> b" by blast
1.18 -  from `a \<in> A` have "Inf A \<sqsubseteq> a" by (rule Inf_lower)
1.19 -  with `a \<sqsubseteq> b` show "Inf A \<sqsubseteq> b" by auto
1.20 +  from `a \<in> A` have "\<Sqinter>A \<sqsubseteq> a" by (rule Inf_lower)
1.21 +  with `a \<sqsubseteq> b` show "\<Sqinter>A \<sqsubseteq> b" by auto
1.22  qed
1.23
1.24  lemma Sup_mono:
1.25    assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
1.26 -  shows "Sup A \<sqsubseteq> Sup B"
1.27 +  shows "\<Squnion>A \<sqsubseteq> \<Squnion>B"
1.28  proof (rule Sup_least)
1.29    fix a assume "a \<in> A"
1.30    with assms obtain b where "b \<in> B" and "a \<sqsubseteq> b" by blast
1.31 -  from `b \<in> B` have "b \<sqsubseteq> Sup B" by (rule Sup_upper)
1.32 -  with `a \<sqsubseteq> b` show "a \<sqsubseteq> Sup B" by auto
1.33 +  from `b \<in> B` have "b \<sqsubseteq> \<Squnion>B" by (rule Sup_upper)
1.34 +  with `a \<sqsubseteq> b` show "a \<sqsubseteq> \<Squnion>B" by auto
1.35  qed
1.36
1.37  lemma top_le:
1.38 -  "top \<sqsubseteq> x \<Longrightarrow> x = top"
1.39 +  "\<top> \<sqsubseteq> x \<Longrightarrow> x = \<top>"
1.40    by (rule antisym) auto
1.41
1.42  lemma le_bot:
1.43 -  "x \<sqsubseteq> bot \<Longrightarrow> x = bot"
1.44 +  "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
1.45    by (rule antisym) auto
1.46
1.47 -lemma not_less_bot[simp]: "\<not> (x \<sqsubset> bot)"
1.48 +lemma not_less_bot[simp]: "\<not> (x \<sqsubset> \<bottom>)"
1.49    using bot_least[of x] by (auto simp: le_less)
1.50
1.51 -lemma not_top_less[simp]: "\<not> (top \<sqsubset> x)"
1.52 +lemma not_top_less[simp]: "\<not> (\<top> \<sqsubset> x)"
1.53    using top_greatest[of x] by (auto simp: le_less)
1.54
1.55 -lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> Sup A"
1.56 +lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
1.57    using Sup_upper[of u A] by auto
1.58
1.59 -lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> Inf A \<sqsubseteq> v"
1.60 +lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
1.61    using Inf_lower[of u A] by auto
1.62
1.63  definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.64 @@ -172,22 +172,22 @@
1.65  lemma INF_cong: "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> INFI A f = INFI A g"
1.66    by (simp add: INFI_def cong: image_cong)
1.67
1.68 -lemma le_SUPI: "i : A \<Longrightarrow> M i \<sqsubseteq> (SUP i:A. M i)"
1.69 +lemma le_SUPI: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> (\<Squnion>i\<in>A. M i)"
1.70    by (auto simp add: SUPR_def intro: Sup_upper)
1.71
1.72 -lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> M i \<Longrightarrow> u \<sqsubseteq> (SUP i:A. M i)"
1.73 +lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> M i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. M i)"
1.74    using le_SUPI[of i A M] by auto
1.75
1.76 -lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<sqsubseteq> u) \<Longrightarrow> (SUP i:A. M i) \<sqsubseteq> u"
1.77 +lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> M i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. M i) \<sqsubseteq> u"
1.78    by (auto simp add: SUPR_def intro: Sup_least)
1.79
1.80 -lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<sqsubseteq> M i"
1.81 +lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. M i) \<sqsubseteq> M i"
1.82    by (auto simp add: INFI_def intro: Inf_lower)
1.83
1.84 -lemma INF_leI2: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> u \<Longrightarrow> (INF i:A. M i) \<sqsubseteq> u"
1.85 +lemma INF_leI2: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. M i) \<sqsubseteq> u"
1.86    using INF_leI[of i A M] by auto
1.87
1.88 -lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (INF i:A. M i)"
1.89 +lemma le_INFI: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. M i)"
1.90    by (auto simp add: INFI_def intro: Inf_greatest)
1.91
1.92  lemma SUP_le_iff: "(SUP i:A. M i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. M i \<sqsubseteq> u)"
1.93 @@ -328,27 +328,27 @@
1.95  qed
1.96
1.97 -lemma Inter_iff [simp,no_atp]: "(A : Inter C) = (ALL X:C. A:X)"
1.98 +lemma Inter_iff [simp,no_atp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)"
1.99    by (unfold Inter_eq) blast
1.100
1.101 -lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
1.102 +lemma InterI [intro!]: "(\<And>X. X \<in> C \<Longrightarrow> A \<in> X) \<Longrightarrow> A \<in> \<Inter>C"
1.104
1.105  text {*
1.106    \medskip A ``destruct'' rule -- every @{term X} in @{term C}
1.107 -  contains @{term A} as an element, but @{prop "A:X"} can hold when
1.108 -  @{prop "X:C"} does not!  This rule is analogous to @{text spec}.
1.109 +  contains @{term A} as an element, but @{prop "A \<in> X"} can hold when
1.110 +  @{prop "X \<in> C"} does not!  This rule is analogous to @{text spec}.
1.111  *}
1.112
1.113 -lemma InterD [elim, Pure.elim]: "A : Inter C ==> X:C ==> A:X"
1.114 +lemma InterD [elim, Pure.elim]: "A \<in> \<Inter>C \<Longrightarrow> X \<in> C \<Longrightarrow> A \<in> X"
1.115    by auto
1.116
1.117 -lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
1.118 +lemma InterE [elim]: "A \<in> \<Inter>C \<Longrightarrow> (X \<notin> C \<Longrightarrow> R) \<Longrightarrow> (A \<in> X \<Longrightarrow> R) \<Longrightarrow> R"
1.119    -- {* ``Classical'' elimination rule -- does not require proving
1.120 -    @{prop "X:C"}. *}
1.121 +    @{prop "X \<in> C"}. *}
1.122    by (unfold Inter_eq) blast
1.123
1.124 -lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
1.125 +lemma Inter_lower: "B \<in> A \<Longrightarrow> \<Inter>A \<subseteq> B"
1.126    by (fact Inf_lower)
1.127
1.128  lemma (in complete_lattice) Inf_less_eq:
1.129 @@ -380,18 +380,23 @@
1.130  lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
1.131    by (fact Inf_insert)
1.132
1.133 +lemma (in complete_lattice) Inf_inter_less: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
1.134 +  by (auto intro: Inf_greatest Inf_lower)
1.135 +
1.136  lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
1.137 -  by blast
1.138 +  by (fact Inf_inter_less)
1.139 +
1.140 +(*lemma (in complete_lattice) Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"*)
1.141
1.142  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
1.143    by blast
1.144
1.145  lemma Inter_UNIV_conv [simp,no_atp]:
1.146 -  "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
1.147 -  "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
1.148 +  "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
1.149 +  "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
1.150    by blast+
1.151
1.152 -lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B"
1.153 +lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B"
1.154    by blast
1.155
1.156
```