merged
authorhaftmann
Mon Jul 20 09:52:09 2009 +0200 (2009-07-20)
changeset 320781c14f77201d4
parent 32075 e8e0fb5da77a
parent 32077 3698947146b2
child 32079 5dc52b199815
child 32081 1b7a901e2edc
child 32113 bafffa63ebfd
merged
src/HOL/List.thy
src/HOL/Set.thy
     2.1 --- a/src/HOL/Set.thy	Mon Jul 20 08:32:07 2009 +0200
     2.2 +++ b/src/HOL/Set.thy	Mon Jul 20 09:52:09 2009 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  
     2.5  text {* A set in HOL is simply a predicate. *}
     2.6  
     2.7 -subsection {* Basic syntax *}
     2.8 +subsection {* Basic definitions and syntax *}
     2.9  
    2.10  global
    2.11  
    2.12 @@ -19,9 +19,6 @@
    2.13  consts
    2.14    Collect       :: "('a => bool) => 'a set"              -- "comprehension"
    2.15    "op :"        :: "'a => 'a set => bool"                -- "membership"
    2.16 -  Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
    2.17 -  Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
    2.18 -  Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
    2.19  
    2.20  local
    2.21  
    2.22 @@ -29,6 +26,10 @@
    2.23    "op :"  ("op :") and
    2.24    "op :"  ("(_/ : _)" [50, 51] 50)
    2.25  
    2.26 +defs
    2.27 +  mem_def [code]: "x : S == S x"
    2.28 +  Collect_def [code]: "Collect P == P"
    2.29 +
    2.30  abbreviation
    2.31    "not_mem x A == ~ (x : A)" -- "non-membership"
    2.32  
    2.33 @@ -84,6 +85,20 @@
    2.34    "{x, xs}"     == "CONST insert x {xs}"
    2.35    "{x}"         == "CONST insert x {}"
    2.36  
    2.37 +global
    2.38 +
    2.39 +consts
    2.40 +  Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
    2.41 +  Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
    2.42 +  Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
    2.43 +
    2.44 +local
    2.45 +
    2.46 +defs
    2.47 +  Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
    2.48 +  Bex_def:      "Bex A P        == EX x. x:A & P(x)"
    2.49 +  Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
    2.50 +
    2.51  syntax
    2.52    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
    2.53    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
    2.54 @@ -112,65 +127,18 @@
    2.55    "EX! x:A. P"  == "Bex1 A (%x. P)"
    2.56    "LEAST x:A. P" => "LEAST x. x:A & P"
    2.57  
    2.58 -definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
    2.59 -  "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
    2.60 -
    2.61 -definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
    2.62 -  "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
    2.63 -
    2.64 -definition Inter :: "'a set set \<Rightarrow> 'a set" where
    2.65 -  "Inter S \<equiv> INTER S (\<lambda>x. x)"
    2.66 -
    2.67 -definition Union :: "'a set set \<Rightarrow> 'a set" where
    2.68 -  "Union S \<equiv> UNION S (\<lambda>x. x)"
    2.69 -
    2.70 -notation (xsymbols)
    2.71 -  Inter  ("\<Inter>_" [90] 90) and
    2.72 -  Union  ("\<Union>_" [90] 90)
    2.73 -
    2.74  
    2.75  subsection {* Additional concrete syntax *}
    2.76  
    2.77  syntax
    2.78    "@SetCompr"   :: "'a => idts => bool => 'a set"         ("(1{_ |/_./ _})")
    2.79    "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ :/ _./ _})")
    2.80 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
    2.81 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
    2.82 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 10] 10)
    2.83 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 10] 10)
    2.84  
    2.85  syntax (xsymbols)
    2.86    "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ \<in>/ _./ _})")
    2.87 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
    2.88 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
    2.89 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
    2.90 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
    2.91 -
    2.92 -syntax (latex output)
    2.93 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    2.94 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    2.95 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
    2.96 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
    2.97  
    2.98  translations
    2.99    "{x:A. P}"    => "{x. x:A & P}"
   2.100 -  "INT x y. B"  == "INT x. INT y. B"
   2.101 -  "INT x. B"    == "CONST INTER CONST UNIV (%x. B)"
   2.102 -  "INT x. B"    == "INT x:CONST UNIV. B"
   2.103 -  "INT x:A. B"  == "CONST INTER A (%x. B)"
   2.104 -  "UN x y. B"   == "UN x. UN y. B"
   2.105 -  "UN x. B"     == "CONST UNION CONST UNIV (%x. B)"
   2.106 -  "UN x. B"     == "UN x:CONST UNIV. B"
   2.107 -  "UN x:A. B"   == "CONST UNION A (%x. B)"
   2.108 -
   2.109 -text {*
   2.110 -  Note the difference between ordinary xsymbol syntax of indexed
   2.111 -  unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
   2.112 -  and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
   2.113 -  former does not make the index expression a subscript of the
   2.114 -  union/intersection symbol because this leads to problems with nested
   2.115 -  subscripts in Proof General.
   2.116 -*}
   2.117  
   2.118  abbreviation
   2.119    subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   2.120 @@ -313,10 +281,7 @@
   2.121    fun btr' syn [A, Abs abs] =
   2.122      let val (x, t) = atomic_abs_tr' abs
   2.123      in Syntax.const syn $ x $ A $ t end
   2.124 -in
   2.125 -[(@{const_syntax Ball}, btr' "_Ball"), (@{const_syntax Bex}, btr' "_Bex"),
   2.126 - (@{const_syntax UNION}, btr' "@UNION"),(@{const_syntax INTER}, btr' "@INTER")]
   2.127 -end
   2.128 +in [(@{const_syntax Ball}, btr' "_Ball"), (@{const_syntax Bex}, btr' "_Bex")] end
   2.129  *}
   2.130  
   2.131  print_translation {*
   2.132 @@ -349,30 +314,6 @@
   2.133  *}
   2.134  
   2.135  
   2.136 -subsection {* Rules and definitions *}
   2.137 -
   2.138 -text {* Isomorphisms between predicates and sets. *}
   2.139 -
   2.140 -defs
   2.141 -  mem_def [code]: "x : S == S x"
   2.142 -  Collect_def [code]: "Collect P == P"
   2.143 -
   2.144 -defs
   2.145 -  Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
   2.146 -  Bex_def:      "Bex A P        == EX x. x:A & P(x)"
   2.147 -  Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
   2.148 -
   2.149 -definition Pow :: "'a set => 'a set set" where
   2.150 -  Pow_def: "Pow A = {B. B \<le> A}"
   2.151 -
   2.152 -definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
   2.153 -  image_def: "f ` A = {y. EX x:A. y = f(x)}"
   2.154 -
   2.155 -abbreviation
   2.156 -  range :: "('a => 'b) => 'b set" where -- "of function"
   2.157 -  "range f == f ` UNIV"
   2.158 -
   2.159 -
   2.160  subsection {* Lemmas and proof tool setup *}
   2.161  
   2.162  subsubsection {* Relating predicates and sets *}
   2.163 @@ -671,6 +612,9 @@
   2.164  
   2.165  subsubsection {* The Powerset operator -- Pow *}
   2.166  
   2.167 +definition Pow :: "'a set => 'a set set" where
   2.168 +  Pow_def: "Pow A = {B. B \<le> A}"
   2.169 +
   2.170  lemma Pow_iff [iff]: "(A \<in> Pow B) = (A \<subseteq> B)"
   2.171    by (simp add: Pow_def)
   2.172  
   2.173 @@ -846,12 +790,397 @@
   2.174    by (blast elim: equalityE)
   2.175  
   2.176  
   2.177 -subsubsection {* Unions of families *}
   2.178 +subsubsection {* Image of a set under a function *}
   2.179 +
   2.180 +text {*
   2.181 +  Frequently @{term b} does not have the syntactic form of @{term "f x"}.
   2.182 +*}
   2.183 +
   2.184 +definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
   2.185 +  image_def [noatp]: "f ` A = {y. EX x:A. y = f(x)}"
   2.186 +
   2.187 +abbreviation
   2.188 +  range :: "('a => 'b) => 'b set" where -- "of function"
   2.189 +  "range f == f ` UNIV"
   2.190 +
   2.191 +lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A"
   2.192 +  by (unfold image_def) blast
   2.193 +
   2.194 +lemma imageI: "x : A ==> f x : f ` A"
   2.195 +  by (rule image_eqI) (rule refl)
   2.196 +
   2.197 +lemma rev_image_eqI: "x:A ==> b = f x ==> b : f`A"
   2.198 +  -- {* This version's more effective when we already have the
   2.199 +    required @{term x}. *}
   2.200 +  by (unfold image_def) blast
   2.201 +
   2.202 +lemma imageE [elim!]:
   2.203 +  "b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P"
   2.204 +  -- {* The eta-expansion gives variable-name preservation. *}
   2.205 +  by (unfold image_def) blast
   2.206 +
   2.207 +lemma image_Un: "f`(A Un B) = f`A Un f`B"
   2.208 +  by blast
   2.209 +
   2.210 +lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
   2.211 +  by blast
   2.212 +
   2.213 +lemma image_subset_iff: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
   2.214 +  -- {* This rewrite rule would confuse users if made default. *}
   2.215 +  by blast
   2.216 +
   2.217 +lemma subset_image_iff: "(B \<subseteq> f`A) = (EX AA. AA \<subseteq> A & B = f`AA)"
   2.218 +  apply safe
   2.219 +   prefer 2 apply fast
   2.220 +  apply (rule_tac x = "{a. a : A & f a : B}" in exI, fast)
   2.221 +  done
   2.222 +
   2.223 +lemma image_subsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f`A \<subseteq> B"
   2.224 +  -- {* Replaces the three steps @{text subsetI}, @{text imageE},
   2.225 +    @{text hypsubst}, but breaks too many existing proofs. *}
   2.226 +  by blast
   2.227  
   2.228  text {*
   2.229 -  @{term [source] "UN x:A. B x"} is @{term "Union (B`A)"}.
   2.230 +  \medskip Range of a function -- just a translation for image!
   2.231 +*}
   2.232 +
   2.233 +lemma range_eqI: "b = f x ==> b \<in> range f"
   2.234 +  by simp
   2.235 +
   2.236 +lemma rangeI: "f x \<in> range f"
   2.237 +  by simp
   2.238 +
   2.239 +lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P"
   2.240 +  by blast
   2.241 +
   2.242 +
   2.243 +subsection {* Complete lattices *}
   2.244 +
   2.245 +notation
   2.246 +  less_eq  (infix "\<sqsubseteq>" 50) and
   2.247 +  less (infix "\<sqsubset>" 50) and
   2.248 +  inf  (infixl "\<sqinter>" 70) and
   2.249 +  sup  (infixl "\<squnion>" 65)
   2.250 +
   2.251 +class complete_lattice = lattice + bot + top +
   2.252 +  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
   2.253 +    and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
   2.254 +  assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
   2.255 +     and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
   2.256 +  assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
   2.257 +     and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
   2.258 +begin
   2.259 +
   2.260 +lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
   2.261 +  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
   2.262 +
   2.263 +lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
   2.264 +  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
   2.265 +
   2.266 +lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
   2.267 +  unfolding Sup_Inf by (auto simp add: UNIV_def)
   2.268 +
   2.269 +lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
   2.270 +  unfolding Inf_Sup by (auto simp add: UNIV_def)
   2.271 +
   2.272 +lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   2.273 +  by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
   2.274 +
   2.275 +lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
   2.276 +  by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
   2.277 +
   2.278 +lemma Inf_singleton [simp]:
   2.279 +  "\<Sqinter>{a} = a"
   2.280 +  by (auto intro: antisym Inf_lower Inf_greatest)
   2.281 +
   2.282 +lemma Sup_singleton [simp]:
   2.283 +  "\<Squnion>{a} = a"
   2.284 +  by (auto intro: antisym Sup_upper Sup_least)
   2.285 +
   2.286 +lemma Inf_insert_simp:
   2.287 +  "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)"
   2.288 +  by (cases "A = {}") (simp_all, simp add: Inf_insert)
   2.289 +
   2.290 +lemma Sup_insert_simp:
   2.291 +  "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)"
   2.292 +  by (cases "A = {}") (simp_all, simp add: Sup_insert)
   2.293 +
   2.294 +lemma Inf_binary:
   2.295 +  "\<Sqinter>{a, b} = a \<sqinter> b"
   2.296 +  by (auto simp add: Inf_insert_simp)
   2.297 +
   2.298 +lemma Sup_binary:
   2.299 +  "\<Squnion>{a, b} = a \<squnion> b"
   2.300 +  by (auto simp add: Sup_insert_simp)
   2.301 +
   2.302 +lemma bot_def:
   2.303 +  "bot = \<Squnion>{}"
   2.304 +  by (auto intro: antisym Sup_least)
   2.305 +
   2.306 +lemma top_def:
   2.307 +  "top = \<Sqinter>{}"
   2.308 +  by (auto intro: antisym Inf_greatest)
   2.309 +
   2.310 +lemma sup_bot [simp]:
   2.311 +  "x \<squnion> bot = x"
   2.312 +  using bot_least [of x] by (simp add: le_iff_sup sup_commute)
   2.313 +
   2.314 +lemma inf_top [simp]:
   2.315 +  "x \<sqinter> top = x"
   2.316 +  using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
   2.317 +
   2.318 +definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   2.319 +  "SUPR A f == \<Squnion> (f ` A)"
   2.320 +
   2.321 +definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   2.322 +  "INFI A f == \<Sqinter> (f ` A)"
   2.323 +
   2.324 +end
   2.325 +
   2.326 +syntax
   2.327 +  "_SUP1"     :: "pttrns => 'b => 'b"           ("(3SUP _./ _)" [0, 10] 10)
   2.328 +  "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3SUP _:_./ _)" [0, 10] 10)
   2.329 +  "_INF1"     :: "pttrns => 'b => 'b"           ("(3INF _./ _)" [0, 10] 10)
   2.330 +  "_INF"      :: "pttrn => 'a set => 'b => 'b"  ("(3INF _:_./ _)" [0, 10] 10)
   2.331 +
   2.332 +translations
   2.333 +  "SUP x y. B"   == "SUP x. SUP y. B"
   2.334 +  "SUP x. B"     == "CONST SUPR CONST UNIV (%x. B)"
   2.335 +  "SUP x. B"     == "SUP x:CONST UNIV. B"
   2.336 +  "SUP x:A. B"   == "CONST SUPR A (%x. B)"
   2.337 +  "INF x y. B"   == "INF x. INF y. B"
   2.338 +  "INF x. B"     == "CONST INFI CONST UNIV (%x. B)"
   2.339 +  "INF x. B"     == "INF x:CONST UNIV. B"
   2.340 +  "INF x:A. B"   == "CONST INFI A (%x. B)"
   2.341 +
   2.342 +(* To avoid eta-contraction of body: *)
   2.343 +print_translation {*
   2.344 +let
   2.345 +  fun btr' syn (A :: Abs abs :: ts) =
   2.346 +    let val (x,t) = atomic_abs_tr' abs
   2.347 +    in list_comb (Syntax.const syn $ x $ A $ t, ts) end
   2.348 +  val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const
   2.349 +in
   2.350 +[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")]
   2.351 +end
   2.352  *}
   2.353  
   2.354 +context complete_lattice
   2.355 +begin
   2.356 +
   2.357 +lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
   2.358 +  by (auto simp add: SUPR_def intro: Sup_upper)
   2.359 +
   2.360 +lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
   2.361 +  by (auto simp add: SUPR_def intro: Sup_least)
   2.362 +
   2.363 +lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
   2.364 +  by (auto simp add: INFI_def intro: Inf_lower)
   2.365 +
   2.366 +lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
   2.367 +  by (auto simp add: INFI_def intro: Inf_greatest)
   2.368 +
   2.369 +lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
   2.370 +  by (auto intro: antisym SUP_leI le_SUPI)
   2.371 +
   2.372 +lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
   2.373 +  by (auto intro: antisym INF_leI le_INFI)
   2.374 +
   2.375 +end
   2.376 +
   2.377 +
   2.378 +subsection {* Bool as complete lattice *}
   2.379 +
   2.380 +instantiation bool :: complete_lattice
   2.381 +begin
   2.382 +
   2.383 +definition
   2.384 +  Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
   2.385 +
   2.386 +definition
   2.387 +  Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
   2.388 +
   2.389 +instance proof
   2.390 +qed (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
   2.391 +
   2.392 +end
   2.393 +
   2.394 +lemma Inf_empty_bool [simp]:
   2.395 +  "\<Sqinter>{}"
   2.396 +  unfolding Inf_bool_def by auto
   2.397 +
   2.398 +lemma not_Sup_empty_bool [simp]:
   2.399 +  "\<not> \<Squnion>{}"
   2.400 +  unfolding Sup_bool_def by auto
   2.401 +
   2.402 +
   2.403 +subsection {* Fun as complete lattice *}
   2.404 +
   2.405 +instantiation "fun" :: (type, complete_lattice) complete_lattice
   2.406 +begin
   2.407 +
   2.408 +definition
   2.409 +  Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
   2.410 +
   2.411 +definition
   2.412 +  Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
   2.413 +
   2.414 +instance proof
   2.415 +qed (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
   2.416 +  intro: Inf_lower Sup_upper Inf_greatest Sup_least)
   2.417 +
   2.418 +end
   2.419 +
   2.420 +lemma Inf_empty_fun:
   2.421 +  "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
   2.422 +  by rule (simp add: Inf_fun_def, simp add: empty_def)
   2.423 +
   2.424 +lemma Sup_empty_fun:
   2.425 +  "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
   2.426 +  by rule (simp add: Sup_fun_def, simp add: empty_def)
   2.427 +
   2.428 +
   2.429 +subsection {* Set as lattice *}
   2.430 +
   2.431 +definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   2.432 +  "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
   2.433 +
   2.434 +definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   2.435 +  "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
   2.436 +
   2.437 +definition Inter :: "'a set set \<Rightarrow> 'a set" where
   2.438 +  "Inter S \<equiv> INTER S (\<lambda>x. x)"
   2.439 +
   2.440 +definition Union :: "'a set set \<Rightarrow> 'a set" where
   2.441 +  "Union S \<equiv> UNION S (\<lambda>x. x)"
   2.442 +
   2.443 +notation (xsymbols)
   2.444 +  Inter  ("\<Inter>_" [90] 90) and
   2.445 +  Union  ("\<Union>_" [90] 90)
   2.446 +
   2.447 +syntax
   2.448 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
   2.449 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
   2.450 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 10] 10)
   2.451 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 10] 10)
   2.452 +
   2.453 +syntax (xsymbols)
   2.454 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
   2.455 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
   2.456 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
   2.457 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
   2.458 +
   2.459 +syntax (latex output)
   2.460 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
   2.461 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
   2.462 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
   2.463 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
   2.464 +
   2.465 +translations
   2.466 +  "INT x y. B"  == "INT x. INT y. B"
   2.467 +  "INT x. B"    == "CONST INTER CONST UNIV (%x. B)"
   2.468 +  "INT x. B"    == "INT x:CONST UNIV. B"
   2.469 +  "INT x:A. B"  == "CONST INTER A (%x. B)"
   2.470 +  "UN x y. B"   == "UN x. UN y. B"
   2.471 +  "UN x. B"     == "CONST UNION CONST UNIV (%x. B)"
   2.472 +  "UN x. B"     == "UN x:CONST UNIV. B"
   2.473 +  "UN x:A. B"   == "CONST UNION A (%x. B)"
   2.474 +
   2.475 +text {*
   2.476 +  Note the difference between ordinary xsymbol syntax of indexed
   2.477 +  unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
   2.478 +  and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
   2.479 +  former does not make the index expression a subscript of the
   2.480 +  union/intersection symbol because this leads to problems with nested
   2.481 +  subscripts in Proof General.
   2.482 +*}
   2.483 +
   2.484 +(* To avoid eta-contraction of body: *)
   2.485 +print_translation {*
   2.486 +let
   2.487 +  fun btr' syn [A, Abs abs] =
   2.488 +    let val (x, t) = atomic_abs_tr' abs
   2.489 +    in Syntax.const syn $ x $ A $ t end
   2.490 +in [(@{const_syntax UNION}, btr' "@UNION"),(@{const_syntax INTER}, btr' "@INTER")] end
   2.491 +*}
   2.492 +
   2.493 +lemma Inter_image_eq [simp]:
   2.494 +  "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
   2.495 +  by (auto simp add: Inter_def INTER_def image_def)
   2.496 +
   2.497 +lemma Union_image_eq [simp]:
   2.498 +  "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
   2.499 +  by (auto simp add: Union_def UNION_def image_def)
   2.500 +
   2.501 +lemma inf_set_eq: "A \<sqinter> B = A \<inter> B"
   2.502 +  by (simp add: inf_fun_eq inf_bool_eq Int_def Collect_def mem_def)
   2.503 +
   2.504 +lemma sup_set_eq: "A \<squnion> B = A \<union> B"
   2.505 +  by (simp add: sup_fun_eq sup_bool_eq Un_def Collect_def mem_def)
   2.506 +
   2.507 +lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
   2.508 +  apply (fold inf_set_eq sup_set_eq)
   2.509 +  apply (erule mono_inf)
   2.510 +  done
   2.511 +
   2.512 +lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
   2.513 +  apply (fold inf_set_eq sup_set_eq)
   2.514 +  apply (erule mono_sup)
   2.515 +  done
   2.516 +
   2.517 +lemma top_set_eq: "top = UNIV"
   2.518 +  by (iprover intro!: subset_antisym subset_UNIV top_greatest)
   2.519 +
   2.520 +lemma bot_set_eq: "bot = {}"
   2.521 +  by (iprover intro!: subset_antisym empty_subsetI bot_least)
   2.522 +
   2.523 +lemma Inter_eq:
   2.524 +  "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
   2.525 +  by (simp add: Inter_def INTER_def)
   2.526 +
   2.527 +lemma Union_eq:
   2.528 +  "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
   2.529 +  by (simp add: Union_def UNION_def)
   2.530 +
   2.531 +lemma Inf_set_eq:
   2.532 +  "\<Sqinter>S = \<Inter>S"
   2.533 +proof (rule set_ext)
   2.534 +  fix x
   2.535 +  have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
   2.536 +    by auto
   2.537 +  then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
   2.538 +    by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
   2.539 +qed
   2.540 +
   2.541 +lemma Sup_set_eq:
   2.542 +  "\<Squnion>S = \<Union>S"
   2.543 +proof (rule set_ext)
   2.544 +  fix x
   2.545 +  have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
   2.546 +    by auto
   2.547 +  then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
   2.548 +    by (simp add: Union_eq Sup_fun_def Sup_bool_def) (simp add: mem_def)
   2.549 +qed
   2.550 +
   2.551 +lemma INFI_set_eq:
   2.552 +  "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
   2.553 +  by (simp add: INFI_def Inf_set_eq)
   2.554 +
   2.555 +lemma SUPR_set_eq:
   2.556 +  "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
   2.557 +  by (simp add: SUPR_def Sup_set_eq)
   2.558 +  
   2.559 +no_notation
   2.560 +  less_eq  (infix "\<sqsubseteq>" 50) and
   2.561 +  less (infix "\<sqsubset>" 50) and
   2.562 +  inf  (infixl "\<sqinter>" 70) and
   2.563 +  sup  (infixl "\<squnion>" 65) and
   2.564 +  Inf  ("\<Sqinter>_" [900] 900) and
   2.565 +  Sup  ("\<Squnion>_" [900] 900)
   2.566 +
   2.567 +
   2.568 +subsubsection {* Unions of families *}
   2.569 +
   2.570  declare UNION_def [noatp]
   2.571  
   2.572  lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
   2.573 @@ -873,11 +1202,12 @@
   2.574      "A = B ==> (!!x. x:B =simp=> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"
   2.575    by (simp add: UNION_def simp_implies_def)
   2.576  
   2.577 +lemma image_eq_UN: "f`A = (UN x:A. {f x})"
   2.578 +  by blast
   2.579 +
   2.580  
   2.581  subsubsection {* Intersections of families *}
   2.582  
   2.583 -text {* @{term [source] "INT x:A. B x"} is @{term "Inter (B`A)"}. *}
   2.584 -
   2.585  lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
   2.586    by (unfold INTER_def) blast
   2.587  
   2.588 @@ -932,66 +1262,6 @@
   2.589      @{prop "X:C"}. *}
   2.590    by (unfold Inter_def) blast
   2.591  
   2.592 -text {*
   2.593 -  \medskip Image of a set under a function.  Frequently @{term b} does
   2.594 -  not have the syntactic form of @{term "f x"}.
   2.595 -*}
   2.596 -
   2.597 -declare image_def [noatp]
   2.598 -
   2.599 -lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A"
   2.600 -  by (unfold image_def) blast
   2.601 -
   2.602 -lemma imageI: "x : A ==> f x : f ` A"
   2.603 -  by (rule image_eqI) (rule refl)
   2.604 -
   2.605 -lemma rev_image_eqI: "x:A ==> b = f x ==> b : f`A"
   2.606 -  -- {* This version's more effective when we already have the
   2.607 -    required @{term x}. *}
   2.608 -  by (unfold image_def) blast
   2.609 -
   2.610 -lemma imageE [elim!]:
   2.611 -  "b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P"
   2.612 -  -- {* The eta-expansion gives variable-name preservation. *}
   2.613 -  by (unfold image_def) blast
   2.614 -
   2.615 -lemma image_Un: "f`(A Un B) = f`A Un f`B"
   2.616 -  by blast
   2.617 -
   2.618 -lemma image_eq_UN: "f`A = (UN x:A. {f x})"
   2.619 -  by blast
   2.620 -
   2.621 -lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
   2.622 -  by blast
   2.623 -
   2.624 -lemma image_subset_iff: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
   2.625 -  -- {* This rewrite rule would confuse users if made default. *}
   2.626 -  by blast
   2.627 -
   2.628 -lemma subset_image_iff: "(B \<subseteq> f`A) = (EX AA. AA \<subseteq> A & B = f`AA)"
   2.629 -  apply safe
   2.630 -   prefer 2 apply fast
   2.631 -  apply (rule_tac x = "{a. a : A & f a : B}" in exI, fast)
   2.632 -  done
   2.633 -
   2.634 -lemma image_subsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f`A \<subseteq> B"
   2.635 -  -- {* Replaces the three steps @{text subsetI}, @{text imageE},
   2.636 -    @{text hypsubst}, but breaks too many existing proofs. *}
   2.637 -  by blast
   2.638 -
   2.639 -text {*
   2.640 -  \medskip Range of a function -- just a translation for image!
   2.641 -*}
   2.642 -
   2.643 -lemma range_eqI: "b = f x ==> b \<in> range f"
   2.644 -  by simp
   2.645 -
   2.646 -lemma rangeI: "f x \<in> range f"
   2.647 -  by simp
   2.648 -
   2.649 -lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P"
   2.650 -  by blast
   2.651 -
   2.652  
   2.653  subsubsection {* Set reasoning tools *}
   2.654  
   2.655 @@ -1632,15 +1902,9 @@
   2.656      "u \<in> A ==> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
   2.657    by blast
   2.658  
   2.659 -lemma Union_image_eq [simp]: "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
   2.660 -  by blast
   2.661 -
   2.662  lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
   2.663    by blast
   2.664  
   2.665 -lemma Inter_image_eq [simp]: "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
   2.666 -  by blast
   2.667 -
   2.668  lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
   2.669    by auto
   2.670  
   2.671 @@ -2219,256 +2483,6 @@
   2.672    unfolding vimage_def Collect_def mem_def ..
   2.673  
   2.674  
   2.675 -subsection {* Complete lattices *}
   2.676 -
   2.677 -notation
   2.678 -  less_eq  (infix "\<sqsubseteq>" 50) and
   2.679 -  less (infix "\<sqsubset>" 50) and
   2.680 -  inf  (infixl "\<sqinter>" 70) and
   2.681 -  sup  (infixl "\<squnion>" 65)
   2.682 -
   2.683 -class complete_lattice = lattice + bot + top +
   2.684 -  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
   2.685 -    and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
   2.686 -  assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
   2.687 -     and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
   2.688 -  assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
   2.689 -     and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
   2.690 -begin
   2.691 -
   2.692 -lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
   2.693 -  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
   2.694 -
   2.695 -lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
   2.696 -  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
   2.697 -
   2.698 -lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
   2.699 -  unfolding Sup_Inf by auto
   2.700 -
   2.701 -lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
   2.702 -  unfolding Inf_Sup by auto
   2.703 -
   2.704 -lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   2.705 -  by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
   2.706 -
   2.707 -lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
   2.708 -  by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
   2.709 -
   2.710 -lemma Inf_singleton [simp]:
   2.711 -  "\<Sqinter>{a} = a"
   2.712 -  by (auto intro: antisym Inf_lower Inf_greatest)
   2.713 -
   2.714 -lemma Sup_singleton [simp]:
   2.715 -  "\<Squnion>{a} = a"
   2.716 -  by (auto intro: antisym Sup_upper Sup_least)
   2.717 -
   2.718 -lemma Inf_insert_simp:
   2.719 -  "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)"
   2.720 -  by (cases "A = {}") (simp_all, simp add: Inf_insert)
   2.721 -
   2.722 -lemma Sup_insert_simp:
   2.723 -  "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)"
   2.724 -  by (cases "A = {}") (simp_all, simp add: Sup_insert)
   2.725 -
   2.726 -lemma Inf_binary:
   2.727 -  "\<Sqinter>{a, b} = a \<sqinter> b"
   2.728 -  by (simp add: Inf_insert_simp)
   2.729 -
   2.730 -lemma Sup_binary:
   2.731 -  "\<Squnion>{a, b} = a \<squnion> b"
   2.732 -  by (simp add: Sup_insert_simp)
   2.733 -
   2.734 -lemma bot_def:
   2.735 -  "bot = \<Squnion>{}"
   2.736 -  by (auto intro: antisym Sup_least)
   2.737 -
   2.738 -lemma top_def:
   2.739 -  "top = \<Sqinter>{}"
   2.740 -  by (auto intro: antisym Inf_greatest)
   2.741 -
   2.742 -lemma sup_bot [simp]:
   2.743 -  "x \<squnion> bot = x"
   2.744 -  using bot_least [of x] by (simp add: le_iff_sup sup_commute)
   2.745 -
   2.746 -lemma inf_top [simp]:
   2.747 -  "x \<sqinter> top = x"
   2.748 -  using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
   2.749 -
   2.750 -definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   2.751 -  "SUPR A f == \<Squnion> (f ` A)"
   2.752 -
   2.753 -definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   2.754 -  "INFI A f == \<Sqinter> (f ` A)"
   2.755 -
   2.756 -end
   2.757 -
   2.758 -syntax
   2.759 -  "_SUP1"     :: "pttrns => 'b => 'b"           ("(3SUP _./ _)" [0, 10] 10)
   2.760 -  "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3SUP _:_./ _)" [0, 10] 10)
   2.761 -  "_INF1"     :: "pttrns => 'b => 'b"           ("(3INF _./ _)" [0, 10] 10)
   2.762 -  "_INF"      :: "pttrn => 'a set => 'b => 'b"  ("(3INF _:_./ _)" [0, 10] 10)
   2.763 -
   2.764 -translations
   2.765 -  "SUP x y. B"   == "SUP x. SUP y. B"
   2.766 -  "SUP x. B"     == "CONST SUPR CONST UNIV (%x. B)"
   2.767 -  "SUP x. B"     == "SUP x:CONST UNIV. B"
   2.768 -  "SUP x:A. B"   == "CONST SUPR A (%x. B)"
   2.769 -  "INF x y. B"   == "INF x. INF y. B"
   2.770 -  "INF x. B"     == "CONST INFI CONST UNIV (%x. B)"
   2.771 -  "INF x. B"     == "INF x:CONST UNIV. B"
   2.772 -  "INF x:A. B"   == "CONST INFI A (%x. B)"
   2.773 -
   2.774 -(* To avoid eta-contraction of body: *)
   2.775 -print_translation {*
   2.776 -let
   2.777 -  fun btr' syn (A :: Abs abs :: ts) =
   2.778 -    let val (x,t) = atomic_abs_tr' abs
   2.779 -    in list_comb (Syntax.const syn $ x $ A $ t, ts) end
   2.780 -  val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const
   2.781 -in
   2.782 -[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")]
   2.783 -end
   2.784 -*}
   2.785 -
   2.786 -context complete_lattice
   2.787 -begin
   2.788 -
   2.789 -lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
   2.790 -  by (auto simp add: SUPR_def intro: Sup_upper)
   2.791 -
   2.792 -lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
   2.793 -  by (auto simp add: SUPR_def intro: Sup_least)
   2.794 -
   2.795 -lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
   2.796 -  by (auto simp add: INFI_def intro: Inf_lower)
   2.797 -
   2.798 -lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
   2.799 -  by (auto simp add: INFI_def intro: Inf_greatest)
   2.800 -
   2.801 -lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
   2.802 -  by (auto intro: antisym SUP_leI le_SUPI)
   2.803 -
   2.804 -lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
   2.805 -  by (auto intro: antisym INF_leI le_INFI)
   2.806 -
   2.807 -end
   2.808 -
   2.809 -
   2.810 -subsection {* Bool as complete lattice *}
   2.811 -
   2.812 -instantiation bool :: complete_lattice
   2.813 -begin
   2.814 -
   2.815 -definition
   2.816 -  Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
   2.817 -
   2.818 -definition
   2.819 -  Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
   2.820 -
   2.821 -instance
   2.822 -  by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
   2.823 -
   2.824 -end
   2.825 -
   2.826 -lemma Inf_empty_bool [simp]:
   2.827 -  "\<Sqinter>{}"
   2.828 -  unfolding Inf_bool_def by auto
   2.829 -
   2.830 -lemma not_Sup_empty_bool [simp]:
   2.831 -  "\<not> \<Squnion>{}"
   2.832 -  unfolding Sup_bool_def by auto
   2.833 -
   2.834 -
   2.835 -subsection {* Fun as complete lattice *}
   2.836 -
   2.837 -instantiation "fun" :: (type, complete_lattice) complete_lattice
   2.838 -begin
   2.839 -
   2.840 -definition
   2.841 -  Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
   2.842 -
   2.843 -definition
   2.844 -  Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
   2.845 -
   2.846 -instance
   2.847 -  by intro_classes
   2.848 -    (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
   2.849 -      intro: Inf_lower Sup_upper Inf_greatest Sup_least)
   2.850 -
   2.851 -end
   2.852 -
   2.853 -lemma Inf_empty_fun:
   2.854 -  "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
   2.855 -  by rule (auto simp add: Inf_fun_def)
   2.856 -
   2.857 -lemma Sup_empty_fun:
   2.858 -  "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
   2.859 -  by rule (auto simp add: Sup_fun_def)
   2.860 -
   2.861 -
   2.862 -subsection {* Set as lattice *}
   2.863 -
   2.864 -lemma inf_set_eq: "A \<sqinter> B = A \<inter> B"
   2.865 -  apply (rule subset_antisym)
   2.866 -  apply (rule Int_greatest)
   2.867 -  apply (rule inf_le1)
   2.868 -  apply (rule inf_le2)
   2.869 -  apply (rule inf_greatest)
   2.870 -  apply (rule Int_lower1)
   2.871 -  apply (rule Int_lower2)
   2.872 -  done
   2.873 -
   2.874 -lemma sup_set_eq: "A \<squnion> B = A \<union> B"
   2.875 -  apply (rule subset_antisym)
   2.876 -  apply (rule sup_least)
   2.877 -  apply (rule Un_upper1)
   2.878 -  apply (rule Un_upper2)
   2.879 -  apply (rule Un_least)
   2.880 -  apply (rule sup_ge1)
   2.881 -  apply (rule sup_ge2)
   2.882 -  done
   2.883 -
   2.884 -lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
   2.885 -  apply (fold inf_set_eq sup_set_eq)
   2.886 -  apply (erule mono_inf)
   2.887 -  done
   2.888 -
   2.889 -lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
   2.890 -  apply (fold inf_set_eq sup_set_eq)
   2.891 -  apply (erule mono_sup)
   2.892 -  done
   2.893 -
   2.894 -lemma Inf_set_eq: "\<Sqinter>S = \<Inter>S"
   2.895 -  apply (rule subset_antisym)
   2.896 -  apply (rule Inter_greatest)
   2.897 -  apply (erule Inf_lower)
   2.898 -  apply (rule Inf_greatest)
   2.899 -  apply (erule Inter_lower)
   2.900 -  done
   2.901 -
   2.902 -lemma Sup_set_eq: "\<Squnion>S = \<Union>S"
   2.903 -  apply (rule subset_antisym)
   2.904 -  apply (rule Sup_least)
   2.905 -  apply (erule Union_upper)
   2.906 -  apply (rule Union_least)
   2.907 -  apply (erule Sup_upper)
   2.908 -  done
   2.909 -  
   2.910 -lemma top_set_eq: "top = UNIV"
   2.911 -  by (iprover intro!: subset_antisym subset_UNIV top_greatest)
   2.912 -
   2.913 -lemma bot_set_eq: "bot = {}"
   2.914 -  by (iprover intro!: subset_antisym empty_subsetI bot_least)
   2.915 -
   2.916 -no_notation
   2.917 -  less_eq  (infix "\<sqsubseteq>" 50) and
   2.918 -  less (infix "\<sqsubset>" 50) and
   2.919 -  inf  (infixl "\<sqinter>" 70) and
   2.920 -  sup  (infixl "\<squnion>" 65) and
   2.921 -  Inf  ("\<Sqinter>_" [900] 900) and
   2.922 -  Sup  ("\<Squnion>_" [900] 900)
   2.923 -
   2.924 -
   2.925  subsection {* Misc theorem and ML bindings *}
   2.926  
   2.927  lemmas equalityI = subset_antisym