src/HOL/Complete_Lattice.thy
changeset 41080 294956ff285b
parent 40872 7c556a9240de
child 41082 9ff94e7cc3b3
     1.1 --- a/src/HOL/Complete_Lattice.thy	Wed Dec 08 14:52:23 2010 +0100
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Wed Dec 08 14:52:23 2010 +0100
     1.3 @@ -44,14 +44,22 @@
     1.4  lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
     1.5    by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
     1.6  
     1.7 -lemma Inf_empty:
     1.8 +lemma Inf_empty [simp]:
     1.9    "\<Sqinter>{} = \<top>"
    1.10    by (auto intro: antisym Inf_greatest)
    1.11  
    1.12 -lemma Sup_empty:
    1.13 +lemma Sup_empty [simp]:
    1.14    "\<Squnion>{} = \<bottom>"
    1.15    by (auto intro: antisym Sup_least)
    1.16  
    1.17 +lemma Inf_UNIV [simp]:
    1.18 +  "\<Sqinter>UNIV = \<bottom>"
    1.19 +  by (simp add: Sup_Inf Sup_empty [symmetric])
    1.20 +
    1.21 +lemma Sup_UNIV [simp]:
    1.22 +  "\<Squnion>UNIV = \<top>"
    1.23 +  by (simp add: Inf_Sup Inf_empty [symmetric])
    1.24 +
    1.25  lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
    1.26    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
    1.27  
    1.28 @@ -74,14 +82,6 @@
    1.29    "\<Squnion>{a, b} = a \<squnion> b"
    1.30    by (simp add: Sup_empty Sup_insert)
    1.31  
    1.32 -lemma Inf_UNIV:
    1.33 -  "\<Sqinter>UNIV = bot"
    1.34 -  by (simp add: Sup_Inf Sup_empty [symmetric])
    1.35 -
    1.36 -lemma Sup_UNIV:
    1.37 -  "\<Squnion>UNIV = top"
    1.38 -  by (simp add: Inf_Sup Inf_empty [symmetric])
    1.39 -
    1.40  lemma Sup_le_iff: "Sup A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
    1.41    by (auto intro: Sup_least dest: Sup_upper)
    1.42  
    1.43 @@ -117,10 +117,16 @@
    1.44  end
    1.45  
    1.46  syntax
    1.47 -  "_SUP1"     :: "pttrns => 'b => 'b"           ("(3SUP _./ _)" [0, 10] 10)
    1.48 -  "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
    1.49 -  "_INF1"     :: "pttrns => 'b => 'b"           ("(3INF _./ _)" [0, 10] 10)
    1.50 -  "_INF"      :: "pttrn => 'a set => 'b => 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
    1.51 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
    1.52 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
    1.53 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
    1.54 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
    1.55 +
    1.56 +syntax (xsymbols)
    1.57 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    1.58 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    1.59 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    1.60 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    1.61  
    1.62  translations
    1.63    "SUP x y. B"   == "SUP x. SUP y. B"
    1.64 @@ -212,25 +218,17 @@
    1.65  begin
    1.66  
    1.67  definition
    1.68 -  Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
    1.69 +  "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
    1.70  
    1.71  definition
    1.72 -  Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
    1.73 +  "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
    1.74  
    1.75  instance proof
    1.76  qed (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
    1.77  
    1.78  end
    1.79  
    1.80 -lemma Inf_empty_bool [simp]:
    1.81 -  "\<Sqinter>{}"
    1.82 -  unfolding Inf_bool_def by auto
    1.83 -
    1.84 -lemma not_Sup_empty_bool [simp]:
    1.85 -  "\<not> \<Squnion>{}"
    1.86 -  unfolding Sup_bool_def by auto
    1.87 -
    1.88 -lemma INFI_bool_eq:
    1.89 +lemma INFI_bool_eq [simp]:
    1.90    "INFI = Ball"
    1.91  proof (rule ext)+
    1.92    fix A :: "'a set"
    1.93 @@ -239,7 +237,7 @@
    1.94      by (auto simp add: Ball_def INFI_def Inf_bool_def)
    1.95  qed
    1.96  
    1.97 -lemma SUPR_bool_eq:
    1.98 +lemma SUPR_bool_eq [simp]:
    1.99    "SUPR = Bex"
   1.100  proof (rule ext)+
   1.101    fix A :: "'a set"
   1.102 @@ -252,36 +250,32 @@
   1.103  begin
   1.104  
   1.105  definition
   1.106 -  Inf_fun_def: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
   1.107 +  "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
   1.108 +
   1.109 +lemma Inf_apply:
   1.110 +  "(\<Sqinter>A) x = \<Sqinter>{y. \<exists>f\<in>A. y = f x}"
   1.111 +  by (simp add: Inf_fun_def)
   1.112  
   1.113  definition
   1.114 -  Sup_fun_def: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
   1.115 +  "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
   1.116 +
   1.117 +lemma Sup_apply:
   1.118 +  "(\<Squnion>A) x = \<Squnion>{y. \<exists>f\<in>A. y = f x}"
   1.119 +  by (simp add: Sup_fun_def)
   1.120  
   1.121  instance proof
   1.122 -qed (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
   1.123 +qed (auto simp add: le_fun_def Inf_apply Sup_apply
   1.124    intro: Inf_lower Sup_upper Inf_greatest Sup_least)
   1.125  
   1.126  end
   1.127  
   1.128 -lemma SUPR_fun_expand:
   1.129 -  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
   1.130 -  shows "(SUP y:A. f y) = (\<lambda>x. SUP y:A. f y x)"
   1.131 -  by (auto intro!: arg_cong[where f=Sup] ext[where 'a='b]
   1.132 -           simp: SUPR_def Sup_fun_def)
   1.133 +lemma INFI_apply:
   1.134 +  "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
   1.135 +  by (auto intro: arg_cong [of _ _ Inf] simp add: INFI_def Inf_apply)
   1.136  
   1.137 -lemma INFI_fun_expand:
   1.138 -  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
   1.139 -  shows "(INF y:A. f y) x = (INF y:A. f y x)"
   1.140 -  by (auto intro!: arg_cong[where f=Inf] ext[where 'a='b]
   1.141 -           simp: INFI_def Inf_fun_def)
   1.142 -
   1.143 -lemma Inf_empty_fun:
   1.144 -  "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
   1.145 -  by (simp add: Inf_fun_def)
   1.146 -
   1.147 -lemma Sup_empty_fun:
   1.148 -  "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
   1.149 -  by (simp add: Sup_fun_def)
   1.150 +lemma SUPR_apply:
   1.151 +  "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   1.152 +  by (auto intro: arg_cong [of _ _ Sup] simp add: SUPR_def Sup_apply)
   1.153  
   1.154  
   1.155  subsection {* Union *}
   1.156 @@ -572,7 +566,7 @@
   1.157    by blast
   1.158  
   1.159  lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
   1.160 -  by blast
   1.161 +  by (fact Inf_empty)
   1.162  
   1.163  lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
   1.164    by blast
   1.165 @@ -871,6 +865,12 @@
   1.166    top ("\<top>") and
   1.167    bot ("\<bottom>")
   1.168  
   1.169 +no_syntax (xsymbols)
   1.170 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
   1.171 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
   1.172 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   1.173 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   1.174 +
   1.175  lemmas mem_simps =
   1.176    insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
   1.177    mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff