merged
authorhaftmann
Sun Jul 10 21:39:03 2011 +0200 (2011-07-10)
changeset 43742d033a34a490a
parent 43738 e40d2eddf2c0
parent 43741 fac11b64713c
child 43743 8786e36b8142
child 43753 fe5e846c0839
merged
     1.1 --- a/src/HOL/Complete_Lattice.thy	Sun Jul 10 19:33:27 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 10 21:39:03 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,60 +328,75 @@
    1.94      by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
    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.103    by (simp add: Inter_eq)
   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 -  by blast
   1.126 +lemma Inter_lower: "B \<in> A \<Longrightarrow> \<Inter>A \<subseteq> B"
   1.127 +  by (fact Inf_lower)
   1.128 +
   1.129 +lemma (in complete_lattice) Inf_less_eq:
   1.130 +  assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
   1.131 +    and "A \<noteq> {}"
   1.132 +  shows "\<Sqinter>A \<le> u"
   1.133 +proof -
   1.134 +  from `A \<noteq> {}` obtain v where "v \<in> A" by blast
   1.135 +  moreover with assms have "v \<sqsubseteq> u" by blast
   1.136 +  ultimately show ?thesis by (rule Inf_lower2)
   1.137 +qed
   1.138  
   1.139  lemma Inter_subset:
   1.140    "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"
   1.141 -  by blast
   1.142 +  by (fact Inf_less_eq)
   1.143  
   1.144  lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
   1.145 -  by (iprover intro: InterI subsetI dest: subsetD)
   1.146 +  by (fact Inf_greatest)
   1.147  
   1.148  lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
   1.149 -  by blast
   1.150 +  by (fact Inf_binary [symmetric])
   1.151  
   1.152  lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
   1.153    by (fact Inf_empty)
   1.154  
   1.155  lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
   1.156 -  by blast
   1.157 +  by (fact Inf_UNIV)
   1.158  
   1.159  lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
   1.160 -  by blast
   1.161 +  by (fact Inf_insert)
   1.162 +
   1.163 +lemma (in complete_lattice) Inf_inter_less: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
   1.164 +  by (auto intro: Inf_greatest Inf_lower)
   1.165  
   1.166  lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
   1.167 -  by blast
   1.168 +  by (fact Inf_inter_less)
   1.169 +
   1.170 +(*lemma (in complete_lattice) Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"*)
   1.171  
   1.172  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
   1.173    by blast
   1.174  
   1.175  lemma Inter_UNIV_conv [simp,no_atp]:
   1.176 -  "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
   1.177 -  "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
   1.178 +  "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
   1.179 +  "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
   1.180    by blast+
   1.181  
   1.182 -lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B"
   1.183 +lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B"
   1.184    by blast
   1.185  
   1.186