src/HOL/Lattices.thy
changeset 24345 86a3557a9ebb
parent 24164 911b46812018
child 24514 540eaf87e42d
     1.1 --- a/src/HOL/Lattices.thy	Mon Aug 20 18:07:28 2007 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Mon Aug 20 18:07:29 2007 +0200
     1.3 @@ -327,26 +327,21 @@
     1.4  
     1.5  class complete_lattice = lattice +
     1.6    fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
     1.7 +    and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
     1.8    assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
     1.9 -  assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
    1.10 +     and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
    1.11 +  assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
    1.12 +     and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
    1.13  begin
    1.14  
    1.15 -definition
    1.16 -  Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
    1.17 -where
    1.18 -  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<^loc>\<le> b}"
    1.19 -
    1.20  lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<^loc>\<le> a}"
    1.21 -  unfolding Sup_def by (auto intro: Inf_greatest Inf_lower)
    1.22 +  by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least)
    1.23  
    1.24 -lemma Sup_upper: "x \<in> A \<Longrightarrow> x \<^loc>\<le> \<Squnion>A"
    1.25 -  by (auto simp: Sup_def intro: Inf_greatest)
    1.26 -
    1.27 -lemma Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<^loc>\<le> z) \<Longrightarrow> \<Squnion>A \<^loc>\<le> z"
    1.28 -  by (auto simp: Sup_def intro: Inf_lower)
    1.29 +lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<^loc>\<le> b}"
    1.30 +  by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least)
    1.31  
    1.32  lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
    1.33 -  unfolding Sup_def by auto
    1.34 +  unfolding Sup_Inf by auto
    1.35  
    1.36  lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
    1.37    unfolding Inf_Sup by auto
    1.38 @@ -367,7 +362,7 @@
    1.39    apply (erule Inf_lower)
    1.40    done
    1.41  
    1.42 -lemma Sup_insert [code func]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    1.43 +lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    1.44    apply (rule antisym)
    1.45    apply (rule Sup_least)
    1.46    apply (erule insertE)
    1.47 @@ -387,7 +382,7 @@
    1.48    "\<Sqinter>{a} = a"
    1.49    by (auto intro: antisym Inf_lower Inf_greatest)
    1.50  
    1.51 -lemma Sup_singleton [simp, code func]:
    1.52 +lemma Sup_singleton [simp]:
    1.53    "\<Squnion>{a} = a"
    1.54    by (auto intro: antisym Sup_upper Sup_least)
    1.55  
    1.56 @@ -491,23 +486,8 @@
    1.57  
    1.58  instance bool :: complete_lattice
    1.59    Inf_bool_def: "Inf A \<equiv> \<forall>x\<in>A. x"
    1.60 -  apply intro_classes
    1.61 -  apply (unfold Inf_bool_def)
    1.62 -  apply (iprover intro!: le_boolI elim: ballE)
    1.63 -  apply (iprover intro!: ballI le_boolI elim: ballE le_boolE)
    1.64 -  done
    1.65 -
    1.66 -theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
    1.67 -  apply (rule order_antisym)
    1.68 -  apply (rule Sup_least)
    1.69 -  apply (rule le_boolI)
    1.70 -  apply (erule bexI, assumption)
    1.71 -  apply (rule le_boolI)
    1.72 -  apply (erule bexE)
    1.73 -  apply (rule le_boolE)
    1.74 -  apply (rule Sup_upper)
    1.75 -  apply assumption+
    1.76 -  done
    1.77 +  Sup_bool_def: "Sup A \<equiv> \<exists>x\<in>A. x"
    1.78 +  by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
    1.79  
    1.80  lemma Inf_empty_bool [simp]:
    1.81    "Inf {}"
    1.82 @@ -515,7 +495,7 @@
    1.83  
    1.84  lemma not_Sup_empty_bool [simp]:
    1.85    "\<not> Sup {}"
    1.86 -  unfolding Sup_def Inf_bool_def by auto
    1.87 +  unfolding Sup_bool_def by auto
    1.88  
    1.89  lemma top_bool_eq: "top = True"
    1.90    by (iprover intro!: order_antisym le_boolI top_greatest)
    1.91 @@ -541,17 +521,10 @@
    1.92  
    1.93  instance set :: (type) complete_lattice
    1.94    Inf_set_def: "Inf S \<equiv> \<Inter>S"
    1.95 -  by intro_classes (auto simp add: Inf_set_def)
    1.96 -
    1.97 -lemmas [code func del] = Inf_set_def
    1.98 +  Sup_set_def: "Sup S \<equiv> \<Union>S"
    1.99 +  by intro_classes (auto simp add: Inf_set_def Sup_set_def)
   1.100  
   1.101 -theorem Sup_set_eq: "Sup S = \<Union>S"
   1.102 -  apply (rule subset_antisym)
   1.103 -  apply (rule Sup_least)
   1.104 -  apply (erule Union_upper)
   1.105 -  apply (rule Union_least)
   1.106 -  apply (erule Sup_upper)
   1.107 -  done
   1.108 +lemmas [code func del] = Inf_set_def Sup_set_def
   1.109  
   1.110  lemma top_set_eq: "top = UNIV"
   1.111    by (iprover intro!: subset_antisym subset_UNIV top_greatest)
   1.112 @@ -581,36 +554,12 @@
   1.113  
   1.114  instance "fun" :: (type, complete_lattice) complete_lattice
   1.115    Inf_fun_def: "Inf A \<equiv> (\<lambda>x. Inf {y. \<exists>f\<in>A. y = f x})"
   1.116 -  apply intro_classes
   1.117 -  apply (unfold Inf_fun_def)
   1.118 -  apply (rule le_funI)
   1.119 -  apply (rule Inf_lower)
   1.120 -  apply (rule CollectI)
   1.121 -  apply (rule bexI)
   1.122 -  apply (rule refl)
   1.123 -  apply assumption
   1.124 -  apply (rule le_funI)
   1.125 -  apply (rule Inf_greatest)
   1.126 -  apply (erule CollectE)
   1.127 -  apply (erule bexE)
   1.128 -  apply (iprover elim: le_funE)
   1.129 -  done
   1.130 +  Sup_fun_def: "Sup A \<equiv> (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
   1.131 +  by intro_classes
   1.132 +    (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
   1.133 +      intro: Inf_lower Sup_upper Inf_greatest Sup_least)
   1.134  
   1.135 -lemmas [code func del] = Inf_fun_def
   1.136 -
   1.137 -theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
   1.138 -  apply (rule order_antisym)
   1.139 -  apply (rule Sup_least)
   1.140 -  apply (rule le_funI)
   1.141 -  apply (rule Sup_upper)
   1.142 -  apply fast
   1.143 -  apply (rule le_funI)
   1.144 -  apply (rule Sup_least)
   1.145 -  apply (erule CollectE)
   1.146 -  apply (erule bexE)
   1.147 -  apply (drule le_funD [OF Sup_upper])
   1.148 -  apply simp
   1.149 -  done
   1.150 +lemmas [code func del] = Inf_fun_def Sup_fun_def
   1.151  
   1.152  lemma Inf_empty_fun:
   1.153    "Inf {} = (\<lambda>_. Inf {})"
   1.154 @@ -618,11 +567,7 @@
   1.155  
   1.156  lemma Sup_empty_fun:
   1.157    "Sup {} = (\<lambda>_. Sup {})"
   1.158 -proof -
   1.159 -  have aux: "\<And>x. {y. \<exists>f. y = f x} = UNIV" by auto
   1.160 -  show ?thesis
   1.161 -  by (auto simp add: Sup_def Inf_fun_def Inf_binary inf_bool_eq aux)
   1.162 -qed
   1.163 +  by rule (auto simp add: Sup_fun_def)
   1.164  
   1.165  lemma top_fun_eq: "top = (\<lambda>x. top)"
   1.166    by (iprover intro!: order_antisym le_funI top_greatest)