author haftmann Mon Jul 20 09:52:09 2009 +0200 (2009-07-20) changeset 32078 1c14f77201d4 parent 32075 e8e0fb5da77a parent 32077 3698947146b2 child 32079 5dc52b199815 child 32081 1b7a901e2edc child 32113 bafffa63ebfd
merged
 src/HOL/List.thy file | annotate | diff | revisions src/HOL/Set.thy file | annotate | diff | revisions
```     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
```