author haftmann Sat Mar 07 15:20:32 2009 +0100 (2009-03-07) changeset 30352 047f183c43b0 parent 30333 e9971af27b11 child 30353 f977e10af7e2 child 30374 7311a1546d85
restructured theory Set.thy
 src/HOL/Set.thy file | annotate | diff | revisions
     1.1 --- a/src/HOL/Set.thy	Sat Mar 07 10:06:58 2009 +0100
1.2 +++ b/src/HOL/Set.thy	Sat Mar 07 15:20:32 2009 +0100
1.3 @@ -8,27 +8,28 @@
1.4  imports Lattices
1.5  begin
1.6
1.7 +subsection {* Basic operations *}
1.8 +
1.9 +subsubsection {* Comprehension and membership *}
1.10 +
1.11  text {* A set in HOL is simply a predicate. *}
1.12
1.13 -
1.14 -subsection {* Basic syntax *}
1.15 -
1.16  global
1.17
1.18  types 'a set = "'a => bool"
1.19
1.20  consts
1.21 -  Collect       :: "('a => bool) => 'a set"              -- "comprehension"
1.22 -  "op :"        :: "'a => 'a set => bool"                -- "membership"
1.23 -  insert        :: "'a => 'a set => 'a set"
1.24 -  Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
1.25 -  Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
1.26 -  Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
1.27 -  Pow           :: "'a set => 'a set set"                -- "powerset"
1.28 -  image         :: "('a => 'b) => 'a set => 'b set"      (infixr "" 90)
1.29 +  Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set"
1.30 +  "op :" :: "'a => 'a set => bool"
1.31
1.32  local
1.33
1.34 +syntax
1.35 +  "@Coll"       :: "pttrn => bool => 'a set"              ("(1{_./ _})")
1.36 +
1.37 +translations
1.38 +  "{x. P}"      == "Collect (%x. P)"
1.39 +
1.40  notation
1.41    "op :"  ("op :") and
1.42    "op :"  ("(_/ : _)" [50, 51] 50)
1.43 @@ -52,126 +53,51 @@
1.44    not_mem  ("op \<notin>") and
1.45    not_mem  ("(_/ \<notin> _)" [50, 51] 50)
1.46
1.47 -syntax
1.48 -  "@Coll"       :: "pttrn => bool => 'a set"              ("(1{_./ _})")
1.49 -
1.50 -translations
1.51 -  "{x. P}"      == "Collect (%x. P)"
1.52 -
1.53 -definition empty :: "'a set" ("{}") where
1.54 -  "empty \<equiv> {x. False}"
1.55 -
1.56 -definition UNIV :: "'a set" where
1.57 -  "UNIV \<equiv> {x. True}"
1.58 -
1.59 -syntax
1.60 -  "@Finset"     :: "args => 'a set"                       ("{(_)}")
1.61 -
1.62 -translations
1.63 -  "{x, xs}"     == "insert x {xs}"
1.64 -  "{x}"         == "insert x {}"
1.65 -
1.66 -definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
1.67 -  "A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
1.68 -
1.69 -definition Un :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
1.70 -  "A Un B \<equiv> {x. x \<in> A \<or> x \<in> B}"
1.71 -
1.72 -notation (xsymbols)
1.73 -  "Int"  (infixl "\<inter>" 70) and
1.74 -  "Un"  (infixl "\<union>" 65)
1.75 -
1.76 -notation (HTML output)
1.77 -  "Int"  (infixl "\<inter>" 70) and
1.78 -  "Un"  (infixl "\<union>" 65)
1.79 -
1.80 -syntax
1.81 -  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
1.82 -  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
1.83 -  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3EX! _:_./ _)" [0, 0, 10] 10)
1.84 -  "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST _:_./ _)" [0, 0, 10] 10)
1.85 -
1.86 -syntax (HOL)
1.87 -  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3! _:_./ _)" [0, 0, 10] 10)
1.88 -  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
1.89 -  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3?! _:_./ _)" [0, 0, 10] 10)
1.90 -
1.91 -syntax (xsymbols)
1.92 -  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
1.93 -  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
1.94 -  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
1.95 -  "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
1.96 -
1.97 -syntax (HTML output)
1.98 -  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
1.99 -  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
1.100 -  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
1.101 -
1.102 -translations
1.103 -  "ALL x:A. P"  == "Ball A (%x. P)"
1.104 -  "EX x:A. P"   == "Bex A (%x. P)"
1.105 -  "EX! x:A. P"  == "Bex1 A (%x. P)"
1.106 -  "LEAST x:A. P" => "LEAST x. x:A & P"
1.107 -
1.108 -definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
1.109 -  "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
1.110 -
1.111 -definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
1.112 -  "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
1.113 -
1.114 -definition Inter :: "'a set set \<Rightarrow> 'a set" where
1.115 -  "Inter S \<equiv> INTER S (\<lambda>x. x)"
1.116 -
1.117 -definition Union :: "'a set set \<Rightarrow> 'a set" where
1.118 -  "Union S \<equiv> UNION S (\<lambda>x. x)"
1.119 -
1.120 -notation (xsymbols)
1.121 -  Inter  ("\<Inter>_" [90] 90) and
1.122 -  Union  ("\<Union>_" [90] 90)
1.123 -
1.124 -
1.125 -subsection {* Additional concrete syntax *}
1.126 -
1.127 -syntax
1.128 -  "@SetCompr"   :: "'a => idts => bool => 'a set"         ("(1{_ |/_./ _})")
1.129 -  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ :/ _./ _})")
1.130 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
1.131 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
1.132 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 10] 10)
1.133 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 10] 10)
1.134 -
1.135 -syntax (xsymbols)
1.136 -  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ \<in>/ _./ _})")
1.137 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
1.138 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
1.139 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
1.140 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
1.141 -
1.142 -syntax (latex output)
1.143 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
1.144 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
1.145 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
1.146 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
1.147 -
1.148 -translations
1.149 -  "{x:A. P}"    => "{x. x:A & P}"
1.150 -  "INT x y. B"  == "INT x. INT y. B"
1.151 -  "INT x. B"    == "CONST INTER CONST UNIV (%x. B)"
1.152 -  "INT x. B"    == "INT x:CONST UNIV. B"
1.153 -  "INT x:A. B"  == "CONST INTER A (%x. B)"
1.154 -  "UN x y. B"   == "UN x. UN y. B"
1.155 -  "UN x. B"     == "CONST UNION CONST UNIV (%x. B)"
1.156 -  "UN x. B"     == "UN x:CONST UNIV. B"
1.157 -  "UN x:A. B"   == "CONST UNION A (%x. B)"
1.158 -
1.159 -text {*
1.160 -  Note the difference between ordinary xsymbol syntax of indexed
1.161 -  unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
1.162 -  and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
1.163 -  former does not make the index expression a subscript of the
1.164 -  union/intersection symbol because this leads to problems with nested
1.165 -  subscripts in Proof General.
1.166 -*}
1.167 +defs
1.168 +  Collect_def [code]: "Collect P \<equiv> P"
1.169 +  mem_def [code]: "x \<in> S \<equiv> S x"
1.170 +
1.171 +text {* Relating predicates and sets *}
1.172 +
1.173 +lemma mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"
1.174 +  by (simp add: Collect_def mem_def)
1.175 +
1.176 +lemma Collect_mem_eq [simp]: "{x. x:A} = A"
1.177 +  by (simp add: Collect_def mem_def)
1.178 +
1.179 +lemma CollectI: "P(a) ==> a : {x. P(x)}"
1.180 +  by simp
1.181 +
1.182 +lemma CollectD: "a : {x. P(x)} ==> P(a)"
1.183 +  by simp
1.184 +
1.185 +lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
1.186 +  by simp
1.187 +
1.188 +lemmas CollectE = CollectD [elim_format]
1.189 +
1.190 +lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
1.191 +  apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
1.192 +   apply (rule Collect_mem_eq)
1.193 +  apply (rule Collect_mem_eq)
1.194 +  done
1.195 +
1.196 +(* Due to Brian Huffman *)
1.197 +lemma expand_set_eq: "(A = B) = (ALL x. (x:A) = (x:B))"
1.198 +by(auto intro:set_ext)
1.199 +
1.200 +lemma equalityCE [elim]:
1.201 +    "A = B ==> (c \<in> A ==> c \<in> B ==> P) ==> (c \<notin> A ==> c \<notin> B ==> P) ==> P"
1.202 +  by blast
1.203 +
1.204 +lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)"
1.205 +  by simp
1.206 +
1.207 +lemma eqelem_imp_iff: "x = y ==> (x : A) = (y : A)"
1.208 +  by simp
1.209 +
1.210 +
1.211 +subsubsection {* Subset relation, empty and universal set *}
1.212
1.213  abbreviation
1.214    subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
1.215 @@ -213,12 +139,557 @@
1.216    supset_eq  ("op \<supseteq>") and
1.217    supset_eq  ("(_/ \<supseteq> _)" [50, 51] 50)
1.218
1.219 -abbreviation
1.220 -  range :: "('a => 'b) => 'b set" where -- "of function"
1.221 -  "range f == f  UNIV"
1.222 -
1.223 -
1.224 -subsubsection "Bounded quantifiers"
1.225 +definition empty :: "'a set" ("{}") where
1.226 +  "empty \<equiv> {x. False}"
1.227 +
1.228 +definition UNIV :: "'a set" where
1.229 +  "UNIV \<equiv> {x. True}"
1.230 +
1.231 +lemma subsetI [atp,intro!]: "(!!x. x:A ==> x:B) ==> A \<subseteq> B"
1.232 +  by (auto simp add: mem_def intro: predicate1I)
1.233 +
1.234 +text {*
1.235 +  \medskip Map the type @{text "'a set => anything"} to just @{typ
1.236 +  'a}; for overloading constants whose first argument has type @{typ
1.237 +  "'a set"}.
1.238 +*}
1.239 +
1.240 +lemma subsetD [elim]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
1.241 +  -- {* Rule in Modus Ponens style. *}
1.242 +  by (unfold mem_def) blast
1.243 +
1.244 +declare subsetD [intro?] -- FIXME
1.245 +
1.246 +lemma rev_subsetD: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
1.247 +  -- {* The same, with reversed premises for use with @{text erule} --
1.248 +      cf @{text rev_mp}. *}
1.249 +  by (rule subsetD)
1.250 +
1.251 +declare rev_subsetD [intro?] -- FIXME
1.252 +
1.253 +text {*
1.254 +  \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
1.255 +*}
1.256 +
1.257 +ML {*
1.258 +  fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
1.259 +*}
1.260 +
1.261 +lemma subsetCE [elim]: "A \<subseteq>  B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
1.262 +  -- {* Classical elimination rule. *}
1.263 +  by (unfold mem_def) blast
1.264 +
1.265 +text {*
1.266 +  \medskip Takes assumptions @{prop "A \<subseteq> B"}; @{prop "c \<in> A"} and
1.267 +  creates the assumption @{prop "c \<in> B"}.
1.268 +*}
1.269 +
1.270 +ML {*
1.271 +  fun set_mp_tac i = etac @{thm subsetCE} i THEN mp_tac i
1.272 +*}
1.273 +
1.274 +lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
1.275 +  by blast
1.276 +
1.277 +lemma subset_refl [simp,atp]: "A \<subseteq> A"
1.278 +  by fast
1.279 +
1.280 +lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"
1.281 +  by blast
1.282 +
1.283 +lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
1.284 +  -- {* Anti-symmetry of the subset relation. *}
1.285 +  by (iprover intro: set_ext subsetD)
1.286 +
1.287 +text {*
1.288 +  \medskip Equality rules from ZF set theory -- are they appropriate
1.289 +  here?
1.290 +*}
1.291 +
1.292 +lemma equalityD1: "A = B ==> A \<subseteq> B"
1.293 +  by (simp add: subset_refl)
1.294 +
1.295 +lemma equalityD2: "A = B ==> B \<subseteq> A"
1.296 +  by (simp add: subset_refl)
1.297 +
1.298 +text {*
1.299 +  \medskip Be careful when adding this to the claset as @{text
1.300 +  subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{}
1.301 +  \<subseteq> A"} and @{prop "A \<subseteq> {}"} and then back to @{prop "A = {}"}!
1.302 +*}
1.303 +
1.304 +lemma equalityE: "A = B ==> (A \<subseteq> B ==> B \<subseteq> A ==> P) ==> P"
1.305 +  by (simp add: subset_refl)
1.306 +
1.307 +lemma empty_iff [simp]: "(c : {}) = False"
1.308 +  by (simp add: empty_def)
1.309 +
1.310 +lemma emptyE [elim!]: "a : {} ==> P"
1.311 +  by simp
1.312 +
1.313 +lemma empty_subsetI [iff]: "{} \<subseteq> A"
1.314 +    -- {* One effect is to delete the ASSUMPTION @{prop "{} \<subseteq> A"} *}
1.315 +  by blast
1.316 +
1.317 +lemma bot_set_eq: "bot = {}"
1.318 +  by (iprover intro!: subset_antisym empty_subsetI bot_least)
1.319 +
1.320 +lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"
1.321 +  by blast
1.322 +
1.323 +lemma equals0D: "A = {} ==> a \<notin> A"
1.324 +    -- {* Use for reasoning about disjointness *}
1.325 +  by blast
1.326 +
1.327 +lemma UNIV_I [simp]: "x : UNIV"
1.328 +  by (simp add: UNIV_def)
1.329 +
1.330 +declare UNIV_I [intro]  -- {* unsafe makes it less likely to cause problems *}
1.331 +
1.332 +lemma UNIV_witness [intro?]: "EX x. x : UNIV"
1.333 +  by simp
1.334 +
1.335 +lemma subset_UNIV [simp]: "A \<subseteq> UNIV"
1.336 +  by (rule subsetI) (rule UNIV_I)
1.337 +
1.338 +lemma top_set_eq: "top = UNIV"
1.339 +  by (iprover intro!: subset_antisym subset_UNIV top_greatest)
1.340 +
1.341 +lemma UNIV_eq_I: "(\<And>x. x \<in> A) \<Longrightarrow> UNIV = A"
1.342 +  by auto
1.343 +
1.344 +lemma UNIV_not_empty [iff]: "UNIV ~= {}"
1.345 +  by blast
1.346 +
1.347 +lemma psubsetI [intro!,noatp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
1.348 +  by (unfold less_le) blast
1.349 +
1.350 +lemma psubsetE [elim!,noatp]:
1.351 +    "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
1.352 +  by (unfold less_le) blast
1.353 +
1.354 +lemma psubset_eq: "(A \<subset> B) = (A \<subseteq> B & A \<noteq> B)"
1.355 +  by (simp only: less_le)
1.356 +
1.357 +lemma psubset_imp_subset: "A \<subset> B ==> A \<subseteq> B"
1.358 +  by (simp add: psubset_eq)
1.359 +
1.360 +lemma psubset_trans: "[| A \<subset> B; B \<subset> C |] ==> A \<subset> C"
1.361 +apply (unfold less_le)
1.362 +apply (auto dest: subset_antisym)
1.363 +done
1.364 +
1.365 +lemma psubsetD: "[| A \<subset> B; c \<in> A |] ==> c \<in> B"
1.366 +apply (unfold less_le)
1.367 +apply (auto dest: subsetD)
1.368 +done
1.369 +
1.370 +lemma psubset_subset_trans: "A \<subset> B ==> B \<subseteq> C ==> A \<subset> C"
1.371 +  by (auto simp add: psubset_eq)
1.372 +
1.373 +lemma subset_psubset_trans: "A \<subseteq> B ==> B \<subset> C ==> A \<subset> C"
1.374 +  by (auto simp add: psubset_eq)
1.375 +
1.376 +lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\<forall>x. \<not> P x)"
1.377 +by blast
1.378 +
1.379 +lemma empty_Collect_eq [simp]: "({} = Collect P) = (\<forall>x. \<not> P x)"
1.380 +by blast
1.381 +
1.382 +subsubsection {* Intersection and union *}
1.383 +
1.384 +definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
1.385 +  "A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
1.386 +
1.387 +definition Un :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
1.388 +  "A Un B \<equiv> {x. x \<in> A \<or> x \<in> B}"
1.389 +
1.390 +notation (xsymbols)
1.391 +  "Int"  (infixl "\<inter>" 70) and
1.392 +  "Un"  (infixl "\<union>" 65)
1.393 +
1.394 +notation (HTML output)
1.395 +  "Int"  (infixl "\<inter>" 70) and
1.396 +  "Un"  (infixl "\<union>" 65)
1.397 +
1.398 +lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
1.399 +  by (unfold Int_def) blast
1.400 +
1.401 +lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B"
1.402 +  by simp
1.403 +
1.404 +lemma IntD1: "c : A Int B ==> c:A"
1.405 +  by simp
1.406 +
1.407 +lemma IntD2: "c : A Int B ==> c:B"
1.408 +  by simp
1.409 +
1.410 +lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"
1.411 +  by simp
1.412 +
1.413 +lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
1.414 +  by (unfold Un_def) blast
1.415 +
1.416 +lemma UnI1 [elim?]: "c:A ==> c : A Un B"
1.417 +  by simp
1.418 +
1.419 +lemma UnI2 [elim?]: "c:B ==> c : A Un B"
1.420 +  by simp
1.421 +
1.422 +text {*
1.423 +  \medskip Classical introduction rule: no commitment to @{prop A} vs
1.424 +  @{prop B}.
1.425 +*}
1.426 +
1.427 +lemma UnCI [intro!]: "(c~:B ==> c:A) ==> c : A Un B"
1.428 +  by auto
1.429 +
1.430 +lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"
1.431 +  by (unfold Un_def) blast
1.432 +
1.433 +lemma Int_lower1: "A \<inter> B \<subseteq> A"
1.434 +  by blast
1.435 +
1.436 +lemma Int_lower2: "A \<inter> B \<subseteq> B"
1.437 +  by blast
1.438 +
1.439 +lemma Int_greatest: "C \<subseteq> A ==> C \<subseteq> B ==> C \<subseteq> A \<inter> B"
1.440 +  by blast
1.441 +
1.442 +lemma inf_set_eq: "inf A B = A \<inter> B"
1.443 +  apply (rule subset_antisym)
1.444 +  apply (rule Int_greatest)
1.445 +  apply (rule inf_le1)
1.446 +  apply (rule inf_le2)
1.447 +  apply (rule inf_greatest)
1.448 +  apply (rule Int_lower1)
1.449 +  apply (rule Int_lower2)
1.450 +  done
1.451 +
1.452 +lemma Un_upper1: "A \<subseteq> A \<union> B"
1.453 +  by blast
1.454 +
1.455 +lemma Un_upper2: "B \<subseteq> A \<union> B"
1.456 +  by blast
1.457 +
1.458 +lemma Un_least: "A \<subseteq> C ==> B \<subseteq> C ==> A \<union> B \<subseteq> C"
1.459 +  by blast
1.460 +
1.461 +lemma sup_set_eq: "sup A B = A \<union> B"
1.462 +  apply (rule subset_antisym)
1.463 +  apply (rule sup_least)
1.464 +  apply (rule Un_upper1)
1.465 +  apply (rule Un_upper2)
1.466 +  apply (rule Un_least)
1.467 +  apply (rule sup_ge1)
1.468 +  apply (rule sup_ge2)
1.469 +  done
1.470 +
1.471 +lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"
1.472 +  by blast
1.473 +
1.474 +lemma Collect_disj_eq: "{x. P x | Q x} = {x. P x} \<union> {x. Q x}"
1.475 +  by blast
1.476 +
1.477 +lemma subset_empty [simp]: "(A \<subseteq> {}) = (A = {})"
1.478 +  by blast
1.479 +
1.480 +lemma not_psubset_empty [iff]: "\<not> (A \<subset> {})"
1.481 +  by (unfold less_le) blast
1.482 +
1.483 +lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"
1.484 +  -- {* supersedes @{text "Collect_False_empty"} *}
1.485 +  by auto
1.486 +
1.487 +
1.488 +subsubsection {* Complement and set difference *}
1.489 +
1.490 +instantiation bool :: minus
1.491 +begin
1.492 +
1.493 +definition
1.494 +  bool_diff_def: "A - B \<longleftrightarrow> A \<and> \<not> B"
1.495 +
1.496 +instance ..
1.497 +
1.498 +end
1.499 +
1.500 +instantiation "fun" :: (type, minus) minus
1.501 +begin
1.502 +
1.503 +definition
1.504 +  fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
1.505 +
1.506 +instance ..
1.507 +
1.508 +end
1.509 +
1.510 +instantiation bool :: uminus
1.511 +begin
1.512 +
1.513 +definition
1.514 +  bool_Compl_def: "- A \<longleftrightarrow> \<not> A"
1.515 +
1.516 +instance ..
1.517 +
1.518 +end
1.519 +
1.520 +instantiation "fun" :: (type, uminus) uminus
1.521 +begin
1.522 +
1.523 +definition
1.524 +  fun_Compl_def: "- A = (\<lambda>x. - A x)"
1.525 +
1.526 +instance ..
1.527 +
1.528 +end
1.529 +
1.530 +lemma Compl_iff [simp]: "(c \<in> -A) = (c \<notin> A)"
1.531 +  by (simp add: mem_def fun_Compl_def bool_Compl_def)
1.532 +
1.533 +lemma ComplI [intro!]: "(c \<in> A ==> False) ==> c \<in> -A"
1.534 +  by (unfold mem_def fun_Compl_def bool_Compl_def) blast
1.535 +
1.536 +text {*
1.537 +  \medskip This form, with negated conclusion, works well with the
1.538 +  Classical prover.  Negated assumptions behave like formulae on the
1.539 +  right side of the notional turnstile ... *}
1.540 +
1.541 +lemma ComplD [dest!]: "c : -A ==> c~:A"
1.542 +  by (simp add: mem_def fun_Compl_def bool_Compl_def)
1.543 +
1.544 +lemmas ComplE = ComplD [elim_format]
1.545 +
1.546 +lemma Compl_eq: "- A = {x. ~ x : A}" by blast
1.547 +
1.548 +lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
1.549 +  by (simp add: mem_def fun_diff_def bool_diff_def)
1.550 +
1.551 +lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"
1.552 +  by simp
1.553 +
1.554 +lemma DiffD1: "c : A - B ==> c : A"
1.555 +  by simp
1.556 +
1.557 +lemma DiffD2: "c : A - B ==> c : B ==> P"
1.558 +  by simp
1.559 +
1.560 +lemma DiffE [elim!]: "c : A - B ==> (c:A ==> c~:B ==> P) ==> P"
1.561 +  by simp
1.562 +
1.563 +lemma set_diff_eq: "A - B = {x. x : A & ~ x : B}" by blast
1.564 +
1.565 +lemma Compl_eq_Diff_UNIV: "-A = (UNIV - A)"
1.566 +by blast
1.567 +
1.568 +lemma psubset_imp_ex_mem: "A \<subset> B ==> \<exists>b. b \<in> (B - A)"
1.569 +  by (unfold less_le) blast
1.570 +
1.571 +lemma Diff_subset: "A - B \<subseteq> A"
1.572 +  by blast
1.573 +
1.574 +lemma Diff_subset_conv: "(A - B \<subseteq> C) = (A \<subseteq> B \<union> C)"
1.575 +by blast
1.576 +
1.577 +lemma Collect_imp_eq: "{x. P x --> Q x} = -{x. P x} \<union> {x. Q x}"
1.578 +  by blast
1.579 +
1.580 +lemma Collect_neg_eq: "{x. \<not> P x} = - {x. P x}"
1.581 +  by blast
1.582 +
1.583 +
1.584 +subsubsection {* Set enumerations *}
1.585 +
1.586 +global
1.587 +
1.588 +consts
1.589 +  insert        :: "'a => 'a set => 'a set"
1.590 +
1.591 +local
1.592 +
1.593 +defs
1.594 +  insert_def:   "insert a B == {x. x=a} Un B"
1.595 +
1.596 +syntax
1.597 +  "@Finset"     :: "args => 'a set"                       ("{(_)}")
1.598 +
1.599 +translations
1.600 +  "{x, xs}"     == "insert x {xs}"
1.601 +  "{x}"         == "insert x {}"
1.602 +
1.603 +lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"
1.604 +  by (unfold insert_def) blast
1.605 +
1.606 +lemma insertI1: "a : insert a B"
1.607 +  by simp
1.608 +
1.609 +lemma insertI2: "a : B ==> a : insert b B"
1.610 +  by simp
1.611 +
1.612 +lemma insertE [elim!]: "a : insert b A ==> (a = b ==> P) ==> (a:A ==> P) ==> P"
1.613 +  by (unfold insert_def) blast
1.614 +
1.615 +lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B"
1.616 +  -- {* Classical introduction rule. *}
1.617 +  by auto
1.618 +
1.619 +lemma subset_insert_iff: "(A \<subseteq> insert x B) = (if x:A then A - {x} \<subseteq> B else A \<subseteq> B)"
1.620 +  by auto
1.621 +
1.622 +lemma set_insert:
1.623 +  assumes "x \<in> A"
1.624 +  obtains B where "A = insert x B" and "x \<notin> B"
1.625 +proof
1.626 +  from assms show "A = insert x (A - {x})" by blast
1.627 +next
1.628 +  show "x \<notin> A - {x}" by blast
1.629 +qed
1.630 +
1.631 +lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"
1.632 +by auto
1.633 +
1.634 +lemma insert_is_Un: "insert a A = {a} Un A"
1.635 +  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"} *}
1.636 +  by blast
1.637 +
1.638 +lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
1.639 +  by blast
1.640 +
1.641 +lemmas empty_not_insert = insert_not_empty [symmetric, standard]
1.642 +declare empty_not_insert [simp]
1.643 +
1.644 +lemma insert_absorb: "a \<in> A ==> insert a A = A"
1.645 +  -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}
1.646 +  -- {* with \emph{quadratic} running time *}
1.647 +  by blast
1.648 +
1.649 +lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"
1.650 +  by blast
1.651 +
1.652 +lemma insert_commute: "insert x (insert y A) = insert y (insert x A)"
1.653 +  by blast
1.654 +
1.655 +lemma insert_subset [simp]: "(insert x A \<subseteq> B) = (x \<in> B & A \<subseteq> B)"
1.656 +  by blast
1.657 +
1.658 +lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B"
1.659 +  -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *}
1.660 +  apply (rule_tac x = "A - {a}" in exI, blast)
1.661 +  done
1.662 +
1.663 +lemma insert_Collect: "insert a (Collect P) = {u. u \<noteq> a --> P u}"
1.664 +  by auto
1.665 +
1.666 +lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
1.667 +  by blast
1.668 +
1.669 +lemma insert_disjoint [simp,noatp]:
1.670 + "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
1.671 + "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
1.672 +  by auto
1.673 +
1.674 +lemma disjoint_insert [simp,noatp]:
1.675 + "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
1.676 + "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
1.677 +  by auto
1.678 +
1.679 +text {* Singletons, using insert *}
1.680 +
1.681 +lemma singletonI [intro!,noatp]: "a : {a}"
1.682 +    -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
1.683 +  by (rule insertI1)
1.684 +
1.685 +lemma singletonD [dest!,noatp]: "b : {a} ==> b = a"
1.686 +  by blast
1.687 +
1.688 +lemmas singletonE = singletonD [elim_format]
1.689 +
1.690 +lemma singleton_iff: "(b : {a}) = (b = a)"
1.691 +  by blast
1.692 +
1.693 +lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
1.694 +  by blast
1.695 +
1.696 +lemma singleton_insert_inj_eq [iff,noatp]:
1.697 +     "({b} = insert a A) = (a = b & A \<subseteq> {b})"
1.698 +  by blast
1.699 +
1.700 +lemma singleton_insert_inj_eq' [iff,noatp]:
1.701 +     "(insert a A = {b}) = (a = b & A \<subseteq> {b})"
1.702 +  by blast
1.703 +
1.704 +lemma subset_singletonD: "A \<subseteq> {x} ==> A = {} | A = {x}"
1.705 +  by fast
1.706 +
1.707 +lemma singleton_conv [simp]: "{x. x = a} = {a}"
1.708 +  by blast
1.709 +
1.710 +lemma singleton_conv2 [simp]: "{x. a = x} = {a}"
1.711 +  by blast
1.712 +
1.713 +lemma diff_single_insert: "A - {x} \<subseteq> B ==> x \<in> A ==> A \<subseteq> insert x B"
1.714 +  by blast
1.715 +
1.716 +lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)"
1.717 +  by (blast elim: equalityE)
1.718 +
1.719 +lemma psubset_insert_iff:
1.720 +  "(A \<subset> insert x B) = (if x \<in> B then A \<subset> B else if x \<in> A then A - {x} \<subset> B else A \<subseteq> B)"
1.721 +  by (auto simp add: less_le subset_insert_iff)
1.722 +
1.723 +lemma subset_insertI: "B \<subseteq> insert a B"
1.724 +  by (rule subsetI) (erule insertI2)
1.725 +
1.726 +lemma subset_insertI2: "A \<subseteq> B \<Longrightarrow> A \<subseteq> insert b B"
1.727 +  by blast
1.728 +
1.729 +lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)"
1.730 +  by blast
1.731 +
1.732 +
1.733 +subsubsection {* Bounded quantifiers and operators *}
1.734 +
1.735 +global
1.736 +
1.737 +consts
1.738 +  Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
1.739 +  Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
1.740 +  Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
1.741 +
1.742 +local
1.743 +
1.744 +defs
1.745 +  Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
1.746 +  Bex_def:      "Bex A P        == EX x. x:A & P(x)"
1.747 +  Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
1.748 +
1.749 +syntax
1.750 +  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
1.751 +  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
1.752 +  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3EX! _:_./ _)" [0, 0, 10] 10)
1.753 +  "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST _:_./ _)" [0, 0, 10] 10)
1.754 +
1.755 +syntax (HOL)
1.756 +  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3! _:_./ _)" [0, 0, 10] 10)
1.757 +  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
1.758 +  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3?! _:_./ _)" [0, 0, 10] 10)
1.759 +
1.760 +syntax (xsymbols)
1.761 +  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
1.762 +  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
1.763 +  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
1.764 +  "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
1.765 +
1.766 +syntax (HTML output)
1.767 +  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
1.768 +  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
1.769 +  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
1.770 +
1.771 +translations
1.772 +  "ALL x:A. P"  == "Ball A (%x. P)"
1.773 +  "EX x:A. P"   == "Bex A (%x. P)"
1.774 +  "EX! x:A. P"  == "Bex1 A (%x. P)"
1.775 +  "LEAST x:A. P" => "LEAST x. x:A & P"
1.776
1.777  syntax (output)
1.778    "_setlessAll" :: "[idt, 'a, bool] => bool"  ("(3ALL _<_./ _)"  [0, 0, 10] 10)
1.779 @@ -249,11 +720,11 @@
1.780    "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
1.781
1.782  translations
1.783 - "\<forall>A\<subset>B. P"   =>  "ALL A. A \<subset> B --> P"
1.784 - "\<exists>A\<subset>B. P"   =>  "EX A. A \<subset> B & P"
1.785 - "\<forall>A\<subseteq>B. P"   =>  "ALL A. A \<subseteq> B --> P"
1.786 - "\<exists>A\<subseteq>B. P"   =>  "EX A. A \<subseteq> B & P"
1.787 - "\<exists>!A\<subseteq>B. P"  =>  "EX! A. A \<subseteq> B & P"
1.788 +  "\<forall>A\<subset>B. P"   =>  "ALL A. A \<subset> B --> P"
1.789 +  "\<exists>A\<subset>B. P"   =>  "EX A. A \<subset> B & P"
1.790 +  "\<forall>A\<subseteq>B. P"   =>  "ALL A. A \<subseteq> B --> P"
1.791 +  "\<exists>A\<subseteq>B. P"   =>  "EX A. A \<subseteq> B & P"
1.792 +  "\<exists>!A\<subseteq>B. P"  =>  "EX! A. A \<subseteq> B & P"
1.793
1.794  print_translation {*
1.795  let
1.796 @@ -287,13 +758,22 @@
1.797  end
1.798  *}
1.799
1.800 -
1.801  text {*
1.802    \medskip Translate between @{text "{e | x1...xn. P}"} and @{text
1.803    "{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is
1.804    only translated if @{text "[0..n] subset bvs(e)"}.
1.805  *}
1.806
1.807 +syntax
1.808 +  "@SetCompr"   :: "'a => idts => bool => 'a set"         ("(1{_ |/_./ _})")
1.809 +  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ :/ _./ _})")
1.810 +
1.811 +syntax (xsymbols)
1.812 +  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ \<in>/ _./ _})")
1.813 +
1.814 +translations
1.815 +  "{x:A. P}"    => "{x. x:A & P}"
1.816 +
1.817  parse_translation {*
1.818    let
1.819      val ex_tr = snd (mk_binder_tr ("EX ", "Ex"));
1.820 @@ -311,18 +791,6 @@
1.821    in [("@SetCompr", setcompr_tr)] end;
1.822  *}
1.823
1.824 -(* To avoid eta-contraction of body: *)
1.825 -print_translation {*
1.826 -let
1.827 -  fun btr' syn [A, Abs abs] =
1.828 -    let val (x, t) = atomic_abs_tr' abs
1.829 -    in Syntax.const syn $x$ A $t end 1.830 -in 1.831 -[(@{const_syntax Ball}, btr' "_Ball"), (@{const_syntax Bex}, btr' "_Bex"), 1.832 - (@{const_syntax UNION}, btr' "@UNION"),(@{const_syntax INTER}, btr' "@INTER")] 1.833 -end 1.834 -*} 1.835 - 1.836 print_translation {* 1.837 let 1.838 val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY")); 1.839 @@ -352,90 +820,6 @@ 1.840 in [("Collect", setcompr_tr')] end; 1.841 *} 1.842 1.843 - 1.844 -subsection {* Rules and definitions *} 1.845 - 1.846 -text {* Isomorphisms between predicates and sets. *} 1.847 - 1.848 -defs 1.849 - mem_def [code]: "x : S == S x" 1.850 - Collect_def [code]: "Collect P == P" 1.851 - 1.852 -defs 1.853 - Ball_def: "Ball A P == ALL x. x:A --> P(x)" 1.854 - Bex_def: "Bex A P == EX x. x:A & P(x)" 1.855 - Bex1_def: "Bex1 A P == EX! x. x:A & P(x)" 1.856 - 1.857 -instantiation "fun" :: (type, minus) minus 1.858 -begin 1.859 - 1.860 -definition 1.861 - fun_diff_def: "A - B = (%x. A x - B x)" 1.862 - 1.863 -instance .. 1.864 - 1.865 -end 1.866 - 1.867 -instantiation bool :: minus 1.868 -begin 1.869 - 1.870 -definition 1.871 - bool_diff_def: "A - B = (A & ~ B)" 1.872 - 1.873 -instance .. 1.874 - 1.875 -end 1.876 - 1.877 -instantiation "fun" :: (type, uminus) uminus 1.878 -begin 1.879 - 1.880 -definition 1.881 - fun_Compl_def: "- A = (%x. - A x)" 1.882 - 1.883 -instance .. 1.884 - 1.885 -end 1.886 - 1.887 -instantiation bool :: uminus 1.888 -begin 1.889 - 1.890 -definition 1.891 - bool_Compl_def: "- A = (~ A)" 1.892 - 1.893 -instance .. 1.894 - 1.895 -end 1.896 - 1.897 -defs 1.898 - Pow_def: "Pow A == {B. B <= A}" 1.899 - insert_def: "insert a B == {x. x=a} Un B" 1.900 - image_def: "fA == {y. EX x:A. y = f(x)}" 1.901 - 1.902 - 1.903 -subsection {* Lemmas and proof tool setup *} 1.904 - 1.905 -subsubsection {* Relating predicates and sets *} 1.906 - 1.907 -lemma mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)" 1.908 - by (simp add: Collect_def mem_def) 1.909 - 1.910 -lemma Collect_mem_eq [simp]: "{x. x:A} = A" 1.911 - by (simp add: Collect_def mem_def) 1.912 - 1.913 -lemma CollectI: "P(a) ==> a : {x. P(x)}" 1.914 - by simp 1.915 - 1.916 -lemma CollectD: "a : {x. P(x)} ==> P(a)" 1.917 - by simp 1.918 - 1.919 -lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}" 1.920 - by simp 1.921 - 1.922 -lemmas CollectE = CollectD [elim_format] 1.923 - 1.924 - 1.925 -subsubsection {* Bounded quantifiers *} 1.926 - 1.927 lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x" 1.928 by (simp add: Ball_def) 1.929 1.930 @@ -526,8 +910,25 @@ 1.931 Addsimprocs [defBALL_regroup, defBEX_regroup]; 1.932 *} 1.933 1.934 - 1.935 -subsubsection {* Congruence rules *} 1.936 +text {* 1.937 + \medskip Eta-contracting these four rules (to remove @{text P}) 1.938 + causes them to be ignored because of their interaction with 1.939 + congruence rules. 1.940 +*} 1.941 + 1.942 +lemma ball_UNIV [simp]: "Ball UNIV P = All P" 1.943 + by (simp add: Ball_def) 1.944 + 1.945 +lemma bex_UNIV [simp]: "Bex UNIV P = Ex P" 1.946 + by (simp add: Bex_def) 1.947 + 1.948 +lemma ball_empty [simp]: "Ball {} P = True" 1.949 + by (simp add: Ball_def) 1.950 + 1.951 +lemma bex_empty [simp]: "Bex {} P = False" 1.952 + by (simp add: Bex_def) 1.953 + 1.954 +text {* Congruence rules *} 1.955 1.956 lemma ball_cong: 1.957 "A = B ==> (!!x. x:B ==> P x = Q x) ==> 1.958 @@ -549,347 +950,423 @@ 1.959 (EX x:A. P x) = (EX x:B. Q x)" 1.960 by (simp add: simp_implies_def Bex_def cong: conj_cong) 1.961 1.962 - 1.963 -subsubsection {* Subsets *} 1.964 - 1.965 -lemma subsetI [atp,intro!]: "(!!x. x:A ==> x:B) ==> A \<subseteq> B" 1.966 - by (auto simp add: mem_def intro: predicate1I) 1.967 - 1.968 -text {* 1.969 - \medskip Map the type @{text "'a set => anything"} to just @{typ 1.970 - 'a}; for overloading constants whose first argument has type @{typ 1.971 - "'a set"}. 1.972 -*} 1.973 - 1.974 -lemma subsetD [elim]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B" 1.975 - -- {* Rule in Modus Ponens style. *} 1.976 - by (unfold mem_def) blast 1.977 - 1.978 -declare subsetD [intro?] -- FIXME 1.979 - 1.980 -lemma rev_subsetD: "c \<in> A ==> A \<subseteq> B ==> c \<in> B" 1.981 - -- {* The same, with reversed premises for use with @{text erule} -- 1.982 - cf @{text rev_mp}. *} 1.983 - by (rule subsetD) 1.984 - 1.985 -declare rev_subsetD [intro?] -- FIXME 1.986 - 1.987 -text {* 1.988 - \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}. 1.989 -*} 1.990 - 1.991 -ML {* 1.992 - fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) 1.993 -*} 1.994 - 1.995 -lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P" 1.996 - -- {* Classical elimination rule. *} 1.997 - by (unfold mem_def) blast 1.998 - 1.999 lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast 1.1000 1.1001 +lemma atomize_ball: 1.1002 + "(!!x. x \<in> A ==> P x) == Trueprop (\<forall>x\<in>A. P x)" 1.1003 + by (simp only: Ball_def atomize_all atomize_imp) 1.1004 + 1.1005 +lemmas [symmetric, rulify] = atomize_ball 1.1006 + and [symmetric, defn] = atomize_ball 1.1007 + 1.1008 + 1.1009 +subsubsection {* Image of a set under a function. *} 1.1010 + 1.1011 text {* 1.1012 - \medskip Takes assumptions @{prop "A \<subseteq> B"}; @{prop "c \<in> A"} and 1.1013 - creates the assumption @{prop "c \<in> B"}. 1.1014 -*} 1.1015 - 1.1016 -ML {* 1.1017 - fun set_mp_tac i = etac @{thm subsetCE} i THEN mp_tac i 1.1018 + Frequently @{term b} does not have the syntactic form of @{term "f x"}. 1.1019 *} 1.1020 1.1021 -lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A" 1.1022 +global 1.1023 + 1.1024 +consts 1.1025 + image :: "('a => 'b) => 'a set => 'b set" (infixr "" 90) 1.1026 + 1.1027 +local 1.1028 + 1.1029 +defs 1.1030 + image_def [noatp]: "fA == {y. EX x:A. y = f(x)}" 1.1031 + 1.1032 +lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : fA" 1.1033 + by (unfold image_def) blast 1.1034 + 1.1035 +lemma imageI: "x : A ==> f x : f  A" 1.1036 + by (rule image_eqI) (rule refl) 1.1037 + 1.1038 +lemma rev_image_eqI: "x:A ==> b = f x ==> b : fA" 1.1039 + -- {* This version's more effective when we already have the 1.1040 + required @{term x}. *} 1.1041 + by (unfold image_def) blast 1.1042 + 1.1043 +lemma imageE [elim!]: 1.1044 + "b : (%x. f x)A ==> (!!x. b = f x ==> x:A ==> P) ==> P" 1.1045 + -- {* The eta-expansion gives variable-name preservation. *} 1.1046 + by (unfold image_def) blast 1.1047 + 1.1048 +lemma image_Un: "f(A Un B) = fA Un fB" 1.1049 by blast 1.1050 1.1051 -lemma subset_refl [simp,atp]: "A \<subseteq> A" 1.1052 - by fast 1.1053 - 1.1054 -lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C" 1.1055 +lemma image_iff: "(z : fA) = (EX x:A. z = f x)" 1.1056 + by blast 1.1057 + 1.1058 +lemma image_subset_iff: "(fA \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)" 1.1059 + -- {* This rewrite rule would confuse users if made default. *} 1.1060 by blast 1.1061 1.1062 - 1.1063 -subsubsection {* Equality *} 1.1064 - 1.1065 -lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B" 1.1066 - apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals]) 1.1067 - apply (rule Collect_mem_eq) 1.1068 - apply (rule Collect_mem_eq) 1.1069 +lemma subset_image_iff: "(B \<subseteq> fA) = (EX AA. AA \<subseteq> A & B = fAA)" 1.1070 + apply safe 1.1071 + prefer 2 apply fast 1.1072 + apply (rule_tac x = "{a. a : A & f a : B}" in exI, fast) 1.1073 done 1.1074 1.1075 -(* Due to Brian Huffman *) 1.1076 -lemma expand_set_eq: "(A = B) = (ALL x. (x:A) = (x:B))" 1.1077 -by(auto intro:set_ext) 1.1078 - 1.1079 -lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B" 1.1080 - -- {* Anti-symmetry of the subset relation. *} 1.1081 - by (iprover intro: set_ext subsetD) 1.1082 - 1.1083 -lemmas equalityI [intro!] = subset_antisym 1.1084 +lemma image_subsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> fA \<subseteq> B" 1.1085 + -- {* Replaces the three steps @{text subsetI}, @{text imageE}, 1.1086 + @{text hypsubst}, but breaks too many existing proofs. *} 1.1087 + by blast 1.1088 + 1.1089 +lemma image_empty [simp]: "f{} = {}" 1.1090 + by blast 1.1091 + 1.1092 +lemma image_insert [simp]: "f  insert a B = insert (f a) (fB)" 1.1093 + by blast 1.1094 + 1.1095 +lemma image_constant: "x \<in> A ==> (\<lambda>x. c)  A = {c}" 1.1096 + by auto 1.1097 + 1.1098 +lemma image_constant_conv: "(%x. c)  A = (if A = {} then {} else {c})" 1.1099 +by auto 1.1100 + 1.1101 +lemma image_image: "f  (g  A) = (\<lambda>x. f (g x))  A" 1.1102 + by blast 1.1103 + 1.1104 +lemma insert_image [simp]: "x \<in> A ==> insert (f x) (fA) = fA" 1.1105 + by blast 1.1106 + 1.1107 +lemma image_is_empty [iff]: "(fA = {}) = (A = {})" 1.1108 + by blast 1.1109 + 1.1110 + 1.1111 +lemma image_Collect [noatp]: "f  {x. P x} = {f x | x. P x}" 1.1112 + -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS, 1.1113 + with its implicit quantifier and conjunction. Also image enjoys better 1.1114 + equational properties than does the RHS. *} 1.1115 + by blast 1.1116 + 1.1117 +lemma if_image_distrib [simp]: 1.1118 + "(\<lambda>x. if P x then f x else g x)  S 1.1119 + = (f  (S \<inter> {x. P x})) \<union> (g  (S \<inter> {x. \<not> P x}))" 1.1120 + by (auto simp add: image_def) 1.1121 + 1.1122 +lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> fM = gN" 1.1123 + by (simp add: image_def) 1.1124 + 1.1125 + 1.1126 +subsection {* Set reasoning tools *} 1.1127 1.1128 text {* 1.1129 - \medskip Equality rules from ZF set theory -- are they appropriate 1.1130 - here? 1.1131 -*} 1.1132 - 1.1133 -lemma equalityD1: "A = B ==> A \<subseteq> B" 1.1134 - by (simp add: subset_refl) 1.1135 - 1.1136 -lemma equalityD2: "A = B ==> B \<subseteq> A" 1.1137 - by (simp add: subset_refl) 1.1138 - 1.1139 -text {* 1.1140 - \medskip Be careful when adding this to the claset as @{text 1.1141 - subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{} 1.1142 - \<subseteq> A"} and @{prop "A \<subseteq> {}"} and then back to @{prop "A = {}"}! 1.1143 + Rewrite rules for boolean case-splitting: faster than @{text 1.1144 + "split_if [split]"}. 1.1145 *} 1.1146 1.1147 -lemma equalityE: "A = B ==> (A \<subseteq> B ==> B \<subseteq> A ==> P) ==> P" 1.1148 - by (simp add: subset_refl) 1.1149 - 1.1150 -lemma equalityCE [elim]: 1.1151 - "A = B ==> (c \<in> A ==> c \<in> B ==> P) ==> (c \<notin> A ==> c \<notin> B ==> P) ==> P" 1.1152 - by blast 1.1153 - 1.1154 -lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)" 1.1155 - by simp 1.1156 - 1.1157 -lemma eqelem_imp_iff: "x = y ==> (x : A) = (y : A)" 1.1158 - by simp 1.1159 - 1.1160 - 1.1161 -subsubsection {* The universal set -- UNIV *} 1.1162 - 1.1163 -lemma UNIV_I [simp]: "x : UNIV" 1.1164 - by (simp add: UNIV_def) 1.1165 - 1.1166 -declare UNIV_I [intro] -- {* unsafe makes it less likely to cause problems *} 1.1167 - 1.1168 -lemma UNIV_witness [intro?]: "EX x. x : UNIV" 1.1169 - by simp 1.1170 - 1.1171 -lemma subset_UNIV [simp]: "A \<subseteq> UNIV" 1.1172 - by (rule subsetI) (rule UNIV_I) 1.1173 +lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))" 1.1174 + by (rule split_if) 1.1175 + 1.1176 +lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))" 1.1177 + by (rule split_if) 1.1178 1.1179 text {* 1.1180 - \medskip Eta-contracting these two rules (to remove @{text P}) 1.1181 - causes them to be ignored because of their interaction with 1.1182 - congruence rules. 1.1183 + Split ifs on either side of the membership relation. Not for @{text 1.1184 + "[simp]"} -- can cause goals to blow up! 1.1185 +*} 1.1186 + 1.1187 +lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))" 1.1188 + by (rule split_if) 1.1189 + 1.1190 +lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))" 1.1191 + by (rule split_if [where P="%S. a : S"]) 1.1192 + 1.1193 +lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2 1.1194 + 1.1195 +(*Would like to add these, but the existing code only searches for the 1.1196 + outer-level constant, which in this case is just "op :"; we instead need 1.1197 + to use term-nets to associate patterns with rules. Also, if a rule fails to 1.1198 + apply, then the formula should be kept. 1.1199 + [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]), 1.1200 + ("Int", [IntD1,IntD2]), 1.1201 + ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])] 1.1202 + *) 1.1203 + 1.1204 +ML {* 1.1205 + val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs; 1.1206 +*} 1.1207 +declaration {* fn _ => 1.1208 + Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs)) 1.1209 *} 1.1210 1.1211 -lemma ball_UNIV [simp]: "Ball UNIV P = All P" 1.1212 - by (simp add: Ball_def) 1.1213 - 1.1214 -lemma bex_UNIV [simp]: "Bex UNIV P = Ex P" 1.1215 - by (simp add: Bex_def) 1.1216 - 1.1217 -lemma UNIV_eq_I: "(\<And>x. x \<in> A) \<Longrightarrow> UNIV = A" 1.1218 - by auto 1.1219 - 1.1220 - 1.1221 -subsubsection {* The empty set *} 1.1222 - 1.1223 -lemma empty_iff [simp]: "(c : {}) = False" 1.1224 - by (simp add: empty_def) 1.1225 - 1.1226 -lemma emptyE [elim!]: "a : {} ==> P" 1.1227 - by simp 1.1228 - 1.1229 -lemma empty_subsetI [iff]: "{} \<subseteq> A" 1.1230 - -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *} 1.1231 - by blast 1.1232 - 1.1233 -lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}" 1.1234 - by blast 1.1235 - 1.1236 -lemma equals0D: "A = {} ==> a \<notin> A" 1.1237 - -- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *} 1.1238 - by blast 1.1239 - 1.1240 -lemma ball_empty [simp]: "Ball {} P = True" 1.1241 - by (simp add: Ball_def) 1.1242 - 1.1243 -lemma bex_empty [simp]: "Bex {} P = False" 1.1244 - by (simp add: Bex_def) 1.1245 - 1.1246 -lemma UNIV_not_empty [iff]: "UNIV ~= {}" 1.1247 - by (blast elim: equalityE) 1.1248 - 1.1249 - 1.1250 -subsubsection {* The Powerset operator -- Pow *} 1.1251 - 1.1252 -lemma Pow_iff [iff]: "(A \<in> Pow B) = (A \<subseteq> B)" 1.1253 - by (simp add: Pow_def) 1.1254 - 1.1255 -lemma PowI: "A \<subseteq> B ==> A \<in> Pow B" 1.1256 - by (simp add: Pow_def) 1.1257 - 1.1258 -lemma PowD: "A \<in> Pow B ==> A \<subseteq> B" 1.1259 - by (simp add: Pow_def) 1.1260 - 1.1261 -lemma Pow_bottom: "{} \<in> Pow B" 1.1262 - by simp 1.1263 - 1.1264 -lemma Pow_top: "A \<in> Pow A" 1.1265 - by (simp add: subset_refl) 1.1266 - 1.1267 - 1.1268 -subsubsection {* Set complement *} 1.1269 - 1.1270 -lemma Compl_iff [simp]: "(c \<in> -A) = (c \<notin> A)" 1.1271 - by (simp add: mem_def fun_Compl_def bool_Compl_def) 1.1272 - 1.1273 -lemma ComplI [intro!]: "(c \<in> A ==> False) ==> c \<in> -A" 1.1274 - by (unfold mem_def fun_Compl_def bool_Compl_def) blast 1.1275 - 1.1276 -text {* 1.1277 - \medskip This form, with negated conclusion, works well with the 1.1278 - Classical prover. Negated assumptions behave like formulae on the 1.1279 - right side of the notional turnstile ... *} 1.1280 - 1.1281 -lemma ComplD [dest!]: "c : -A ==> c~:A" 1.1282 - by (simp add: mem_def fun_Compl_def bool_Compl_def) 1.1283 - 1.1284 -lemmas ComplE = ComplD [elim_format] 1.1285 - 1.1286 -lemma Compl_eq: "- A = {x. ~ x : A}" by blast 1.1287 - 1.1288 - 1.1289 -subsubsection {* Binary union -- Un *} 1.1290 - 1.1291 -lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)" 1.1292 - by (unfold Un_def) blast 1.1293 - 1.1294 -lemma UnI1 [elim?]: "c:A ==> c : A Un B" 1.1295 - by simp 1.1296 - 1.1297 -lemma UnI2 [elim?]: "c:B ==> c : A Un B" 1.1298 - by simp 1.1299 +text {* Transitivity rules for calculational reasoning *} 1.1300 + 1.1301 +lemma set_rev_mp: "x:A ==> A \<subseteq> B ==> x:B" 1.1302 + by (rule subsetD) 1.1303 + 1.1304 +lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B" 1.1305 + by (rule subsetD) 1.1306 + 1.1307 +lemmas basic_trans_rules [trans] = 1.1308 + order_trans_rules set_rev_mp set_mp 1.1309 + 1.1310 + 1.1311 +subsection {* Complete lattices *} 1.1312 + 1.1313 +notation 1.1314 + less_eq (infix "\<sqsubseteq>" 50) and 1.1315 + less (infix "\<sqsubset>" 50) and 1.1316 + inf (infixl "\<sqinter>" 70) and 1.1317 + sup (infixl "\<squnion>" 65) 1.1318 + 1.1319 +class complete_lattice = lattice + bot + top + 1.1320 + fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900) 1.1321 + and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900) 1.1322 + assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x" 1.1323 + and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A" 1.1324 + assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A" 1.1325 + and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z" 1.1326 +begin 1.1327 + 1.1328 +lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}" 1.1329 + by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) 1.1330 + 1.1331 +lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}" 1.1332 + by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) 1.1333 + 1.1334 +lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}" 1.1335 + unfolding Sup_Inf by auto 1.1336 + 1.1337 +lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}" 1.1338 + unfolding Inf_Sup by auto 1.1339 + 1.1340 +lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A" 1.1341 + by (auto intro: antisym Inf_greatest Inf_lower) 1.1342 + 1.1343 +lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A" 1.1344 + by (auto intro: antisym Sup_least Sup_upper) 1.1345 + 1.1346 +lemma Inf_singleton [simp]: 1.1347 + "\<Sqinter>{a} = a" 1.1348 + by (auto intro: antisym Inf_lower Inf_greatest) 1.1349 + 1.1350 +lemma Sup_singleton [simp]: 1.1351 + "\<Squnion>{a} = a" 1.1352 + by (auto intro: antisym Sup_upper Sup_least) 1.1353 + 1.1354 +lemma Inf_insert_simp: 1.1355 + "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)" 1.1356 + by (cases "A = {}") (simp_all, simp add: Inf_insert) 1.1357 + 1.1358 +lemma Sup_insert_simp: 1.1359 + "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)" 1.1360 + by (cases "A = {}") (simp_all, simp add: Sup_insert) 1.1361 + 1.1362 +lemma Inf_binary: 1.1363 + "\<Sqinter>{a, b} = a \<sqinter> b" 1.1364 + by (simp add: Inf_insert_simp) 1.1365 + 1.1366 +lemma Sup_binary: 1.1367 + "\<Squnion>{a, b} = a \<squnion> b" 1.1368 + by (simp add: Sup_insert_simp) 1.1369 + 1.1370 +lemma bot_def: 1.1371 + "bot = \<Squnion>{}" 1.1372 + by (auto intro: antisym Sup_least) 1.1373 + 1.1374 +lemma top_def: 1.1375 + "top = \<Sqinter>{}" 1.1376 + by (auto intro: antisym Inf_greatest) 1.1377 + 1.1378 +lemma sup_bot [simp]: 1.1379 + "x \<squnion> bot = x" 1.1380 + using bot_least [of x] by (simp add: le_iff_sup sup_commute) 1.1381 + 1.1382 +lemma inf_top [simp]: 1.1383 + "x \<sqinter> top = x" 1.1384 + using top_greatest [of x] by (simp add: le_iff_inf inf_commute) 1.1385 + 1.1386 +definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where 1.1387 + "SUPR A f == \<Squnion> (f  A)" 1.1388 + 1.1389 +definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where 1.1390 + "INFI A f == \<Sqinter> (f  A)" 1.1391 + 1.1392 +end 1.1393 + 1.1394 +syntax 1.1395 + "_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" [0, 10] 10) 1.1396 + "_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" [0, 10] 10) 1.1397 + "_INF1" :: "pttrns => 'b => 'b" ("(3INF _./ _)" [0, 10] 10) 1.1398 + "_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" [0, 10] 10) 1.1399 + 1.1400 +translations 1.1401 + "SUP x y. B" == "SUP x. SUP y. B" 1.1402 + "SUP x. B" == "CONST SUPR CONST UNIV (%x. B)" 1.1403 + "SUP x. B" == "SUP x:CONST UNIV. B" 1.1404 + "SUP x:A. B" == "CONST SUPR A (%x. B)" 1.1405 + "INF x y. B" == "INF x. INF y. B" 1.1406 + "INF x. B" == "CONST INFI CONST UNIV (%x. B)" 1.1407 + "INF x. B" == "INF x:CONST UNIV. B" 1.1408 + "INF x:A. B" == "CONST INFI A (%x. B)" 1.1409 + 1.1410 +(* To avoid eta-contraction of body: *) 1.1411 +print_translation {* 1.1412 +let 1.1413 + fun btr' syn (A :: Abs abs :: ts) = 1.1414 + let val (x,t) = atomic_abs_tr' abs 1.1415 + in list_comb (Syntax.const syn$ x $A$ t, ts) end
1.1416 +  val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const
1.1417 +in
1.1418 +[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")]
1.1419 +end
1.1420 +*}
1.1421 +
1.1422 +context complete_lattice
1.1423 +begin
1.1424 +
1.1425 +lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
1.1426 +  by (auto simp add: SUPR_def intro: Sup_upper)
1.1427 +
1.1428 +lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
1.1429 +  by (auto simp add: SUPR_def intro: Sup_least)
1.1430 +
1.1431 +lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
1.1432 +  by (auto simp add: INFI_def intro: Inf_lower)
1.1433 +
1.1434 +lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
1.1435 +  by (auto simp add: INFI_def intro: Inf_greatest)
1.1436 +
1.1437 +lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
1.1438 +  by (auto intro: antisym SUP_leI le_SUPI)
1.1439 +
1.1440 +lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
1.1441 +  by (auto intro: antisym INF_leI le_INFI)
1.1442 +
1.1443 +end
1.1444 +
1.1445 +subsubsection {* Bool as complete lattice *}
1.1446 +
1.1447 +instantiation bool :: complete_lattice
1.1448 +begin
1.1449 +
1.1450 +definition
1.1451 +  Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
1.1452 +
1.1453 +definition
1.1454 +  Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
1.1455 +
1.1456 +instance
1.1457 +  by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
1.1458 +
1.1459 +end
1.1460 +
1.1461 +lemma Inf_empty_bool [simp]:
1.1462 +  "\<Sqinter>{}"
1.1463 +  unfolding Inf_bool_def by auto
1.1464 +
1.1465 +lemma not_Sup_empty_bool [simp]:
1.1466 +  "\<not> Sup {}"
1.1467 +  unfolding Sup_bool_def by auto
1.1468 +
1.1469 +
1.1470 +subsubsection {* Fun as complete lattice *}
1.1471 +
1.1472 +instantiation "fun" :: (type, complete_lattice) complete_lattice
1.1473 +begin
1.1474 +
1.1475 +definition
1.1476 +  Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
1.1477 +
1.1478 +definition
1.1479 +  Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
1.1480 +
1.1481 +instance
1.1482 +  by intro_classes
1.1483 +    (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
1.1484 +      intro: Inf_lower Sup_upper Inf_greatest Sup_least)
1.1485 +
1.1486 +end
1.1487 +
1.1488 +lemma Inf_empty_fun:
1.1489 +  "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
1.1490 +  by rule (auto simp add: Inf_fun_def)
1.1491 +
1.1492 +lemma Sup_empty_fun:
1.1493 +  "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
1.1494 +  by rule (auto simp add: Sup_fun_def)
1.1495 +
1.1496 +no_notation
1.1497 +  less_eq  (infix "\<sqsubseteq>" 50) and
1.1498 +  less (infix "\<sqsubset>" 50) and
1.1499 +  inf  (infixl "\<sqinter>" 70) and
1.1500 +  sup  (infixl "\<squnion>" 65) and
1.1501 +  Inf  ("\<Sqinter>_" [900] 900) and
1.1502 +  Sup  ("\<Squnion>_" [900] 900)
1.1503 +
1.1504 +
1.1505 +subsection {* Further operations *}
1.1506 +
1.1507 +subsubsection {* Big families as specialisation of lattice operations *}
1.1508 +
1.1509 +definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
1.1510 +  "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
1.1511 +
1.1512 +definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
1.1513 +  "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
1.1514 +
1.1515 +definition Inter :: "'a set set \<Rightarrow> 'a set" where
1.1516 +  "Inter S \<equiv> INTER S (\<lambda>x. x)"
1.1517 +
1.1518 +definition Union :: "'a set set \<Rightarrow> 'a set" where
1.1519 +  "Union S \<equiv> UNION S (\<lambda>x. x)"
1.1520 +
1.1521 +notation (xsymbols)
1.1522 +  Inter  ("\<Inter>_" [90] 90) and
1.1523 +  Union  ("\<Union>_" [90] 90)
1.1524 +
1.1525 +syntax
1.1526 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
1.1527 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
1.1528 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 10] 10)
1.1529 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 10] 10)
1.1530 +
1.1531 +syntax (xsymbols)
1.1532 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
1.1533 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
1.1534 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
1.1535 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
1.1536 +
1.1537 +syntax (latex output)
1.1538 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
1.1539 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
1.1540 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
1.1541 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
1.1542 +
1.1543 +translations
1.1544 +  "INT x y. B"  == "INT x. INT y. B"
1.1545 +  "INT x. B"    == "CONST INTER CONST UNIV (%x. B)"
1.1546 +  "INT x. B"    == "INT x:CONST UNIV. B"
1.1547 +  "INT x:A. B"  == "CONST INTER A (%x. B)"
1.1548 +  "UN x y. B"   == "UN x. UN y. B"
1.1549 +  "UN x. B"     == "CONST UNION CONST UNIV (%x. B)"
1.1550 +  "UN x. B"     == "UN x:CONST UNIV. B"
1.1551 +  "UN x:A. B"   == "CONST UNION A (%x. B)"
1.1552
1.1553  text {*
1.1554 -  \medskip Classical introduction rule: no commitment to @{prop A} vs
1.1555 -  @{prop B}.
1.1556 +  Note the difference between ordinary xsymbol syntax of indexed
1.1557 +  unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
1.1558 +  and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
1.1559 +  former does not make the index expression a subscript of the
1.1560 +  union/intersection symbol because this leads to problems with nested
1.1561 +  subscripts in Proof General.
1.1562  *}
1.1563
1.1564 -lemma UnCI [intro!]: "(c~:B ==> c:A) ==> c : A Un B"
1.1565 -  by auto
1.1566 -
1.1567 -lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"
1.1568 -  by (unfold Un_def) blast
1.1569 -
1.1570 -
1.1571 -subsubsection {* Binary intersection -- Int *}
1.1572 -
1.1573 -lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
1.1574 -  by (unfold Int_def) blast
1.1575 -
1.1576 -lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B"
1.1577 -  by simp
1.1578 -
1.1579 -lemma IntD1: "c : A Int B ==> c:A"
1.1580 -  by simp
1.1581 -
1.1582 -lemma IntD2: "c : A Int B ==> c:B"
1.1583 -  by simp
1.1584 -
1.1585 -lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"
1.1586 -  by simp
1.1587 -
1.1588 -
1.1589 -subsubsection {* Set difference *}
1.1590 -
1.1591 -lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
1.1592 -  by (simp add: mem_def fun_diff_def bool_diff_def)
1.1593 -
1.1594 -lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"
1.1595 -  by simp
1.1596 -
1.1597 -lemma DiffD1: "c : A - B ==> c : A"
1.1598 -  by simp
1.1599 -
1.1600 -lemma DiffD2: "c : A - B ==> c : B ==> P"
1.1601 -  by simp
1.1602 -
1.1603 -lemma DiffE [elim!]: "c : A - B ==> (c:A ==> c~:B ==> P) ==> P"
1.1604 -  by simp
1.1605 -
1.1606 -lemma set_diff_eq: "A - B = {x. x : A & ~ x : B}" by blast
1.1607 -
1.1608 -lemma Compl_eq_Diff_UNIV: "-A = (UNIV - A)"
1.1609 -by blast
1.1610 -
1.1611 -
1.1612 -subsubsection {* Augmenting a set -- insert *}
1.1613 -
1.1614 -lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"
1.1615 -  by (unfold insert_def) blast
1.1616 -
1.1617 -lemma insertI1: "a : insert a B"
1.1618 -  by simp
1.1619 -
1.1620 -lemma insertI2: "a : B ==> a : insert b B"
1.1621 -  by simp
1.1622 -
1.1623 -lemma insertE [elim!]: "a : insert b A ==> (a = b ==> P) ==> (a:A ==> P) ==> P"
1.1624 -  by (unfold insert_def) blast
1.1625 -
1.1626 -lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B"
1.1627 -  -- {* Classical introduction rule. *}
1.1628 -  by auto
1.1629 -
1.1630 -lemma subset_insert_iff: "(A \<subseteq> insert x B) = (if x:A then A - {x} \<subseteq> B else A \<subseteq> B)"
1.1631 -  by auto
1.1632 -
1.1633 -lemma set_insert:
1.1634 -  assumes "x \<in> A"
1.1635 -  obtains B where "A = insert x B" and "x \<notin> B"
1.1636 -proof
1.1637 -  from assms show "A = insert x (A - {x})" by blast
1.1638 -next
1.1639 -  show "x \<notin> A - {x}" by blast
1.1640 -qed
1.1641 -
1.1642 -lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"
1.1643 -by auto
1.1644 -
1.1645 -subsubsection {* Singletons, using insert *}
1.1646 -
1.1647 -lemma singletonI [intro!,noatp]: "a : {a}"
1.1648 -    -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
1.1649 -  by (rule insertI1)
1.1650 -
1.1651 -lemma singletonD [dest!,noatp]: "b : {a} ==> b = a"
1.1652 -  by blast
1.1653 -
1.1654 -lemmas singletonE = singletonD [elim_format]
1.1655 -
1.1656 -lemma singleton_iff: "(b : {a}) = (b = a)"
1.1657 -  by blast
1.1658 -
1.1659 -lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
1.1660 -  by blast
1.1661 -
1.1662 -lemma singleton_insert_inj_eq [iff,noatp]:
1.1663 -     "({b} = insert a A) = (a = b & A \<subseteq> {b})"
1.1664 -  by blast
1.1665 -
1.1666 -lemma singleton_insert_inj_eq' [iff,noatp]:
1.1667 -     "(insert a A = {b}) = (a = b & A \<subseteq> {b})"
1.1668 -  by blast
1.1669 -
1.1670 -lemma subset_singletonD: "A \<subseteq> {x} ==> A = {} | A = {x}"
1.1671 -  by fast
1.1672 -
1.1673 -lemma singleton_conv [simp]: "{x. x = a} = {a}"
1.1674 -  by blast
1.1675 -
1.1676 -lemma singleton_conv2 [simp]: "{x. a = x} = {a}"
1.1677 -  by blast
1.1678 -
1.1679 -lemma diff_single_insert: "A - {x} \<subseteq> B ==> x \<in> A ==> A \<subseteq> insert x B"
1.1680 -  by blast
1.1681 -
1.1682 -lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)"
1.1683 -  by (blast elim: equalityE)
1.1684 -
1.1685 +(* To avoid eta-contraction of body: *)
1.1686 +(*FIXME  integrate with / factor out from similar situations*)
1.1687 +print_translation {*
1.1688 +let
1.1689 +  fun btr' syn [A, Abs abs] =
1.1690 +    let val (x, t) = atomic_abs_tr' abs
1.1691 +    in Syntax.const syn $x$ A $t end 1.1692 +in 1.1693 +[(@{const_syntax Ball}, btr' "_Ball"), (@{const_syntax Bex}, btr' "_Bex"), 1.1694 + (@{const_syntax UNION}, btr' "@UNION"),(@{const_syntax INTER}, btr' "@INTER")] 1.1695 +end 1.1696 +*} 1.1697 1.1698 subsubsection {* Unions of families *} 1.1699 1.1700 @@ -918,6 +1395,9 @@ 1.1701 "A = B ==> (!!x. x:B =simp=> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)" 1.1702 by (simp add: UNION_def simp_implies_def) 1.1703 1.1704 +lemma image_eq_UN: "fA = (UN x:A. {f x})" 1.1705 + by blast 1.1706 + 1.1707 1.1708 subsubsection {* Intersections of families *} 1.1709 1.1710 @@ -977,175 +1457,6 @@ 1.1711 @{prop "X:C"}. *} 1.1712 by (unfold Inter_def) blast 1.1713 1.1714 -text {* 1.1715 - \medskip Image of a set under a function. Frequently @{term b} does 1.1716 - not have the syntactic form of @{term "f x"}. 1.1717 -*} 1.1718 - 1.1719 -declare image_def [noatp] 1.1720 - 1.1721 -lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : fA" 1.1722 - by (unfold image_def) blast 1.1723 - 1.1724 -lemma imageI: "x : A ==> f x : f  A" 1.1725 - by (rule image_eqI) (rule refl) 1.1726 - 1.1727 -lemma rev_image_eqI: "x:A ==> b = f x ==> b : fA" 1.1728 - -- {* This version's more effective when we already have the 1.1729 - required @{term x}. *} 1.1730 - by (unfold image_def) blast 1.1731 - 1.1732 -lemma imageE [elim!]: 1.1733 - "b : (%x. f x)A ==> (!!x. b = f x ==> x:A ==> P) ==> P" 1.1734 - -- {* The eta-expansion gives variable-name preservation. *} 1.1735 - by (unfold image_def) blast 1.1736 - 1.1737 -lemma image_Un: "f(A Un B) = fA Un fB" 1.1738 - by blast 1.1739 - 1.1740 -lemma image_eq_UN: "fA = (UN x:A. {f x})" 1.1741 - by blast 1.1742 - 1.1743 -lemma image_iff: "(z : fA) = (EX x:A. z = f x)" 1.1744 - by blast 1.1745 - 1.1746 -lemma image_subset_iff: "(fA \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)" 1.1747 - -- {* This rewrite rule would confuse users if made default. *} 1.1748 - by blast 1.1749 - 1.1750 -lemma subset_image_iff: "(B \<subseteq> fA) = (EX AA. AA \<subseteq> A & B = fAA)" 1.1751 - apply safe 1.1752 - prefer 2 apply fast 1.1753 - apply (rule_tac x = "{a. a : A & f a : B}" in exI, fast) 1.1754 - done 1.1755 - 1.1756 -lemma image_subsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> fA \<subseteq> B" 1.1757 - -- {* Replaces the three steps @{text subsetI}, @{text imageE}, 1.1758 - @{text hypsubst}, but breaks too many existing proofs. *} 1.1759 - by blast 1.1760 - 1.1761 -text {* 1.1762 - \medskip Range of a function -- just a translation for image! 1.1763 -*} 1.1764 - 1.1765 -lemma range_eqI: "b = f x ==> b \<in> range f" 1.1766 - by simp 1.1767 - 1.1768 -lemma rangeI: "f x \<in> range f" 1.1769 - by simp 1.1770 - 1.1771 -lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P" 1.1772 - by blast 1.1773 - 1.1774 - 1.1775 -subsubsection {* Set reasoning tools *} 1.1776 - 1.1777 -text {* 1.1778 - Rewrite rules for boolean case-splitting: faster than @{text 1.1779 - "split_if [split]"}. 1.1780 -*} 1.1781 - 1.1782 -lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))" 1.1783 - by (rule split_if) 1.1784 - 1.1785 -lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))" 1.1786 - by (rule split_if) 1.1787 - 1.1788 -text {* 1.1789 - Split ifs on either side of the membership relation. Not for @{text 1.1790 - "[simp]"} -- can cause goals to blow up! 1.1791 -*} 1.1792 - 1.1793 -lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))" 1.1794 - by (rule split_if) 1.1795 - 1.1796 -lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))" 1.1797 - by (rule split_if [where P="%S. a : S"]) 1.1798 - 1.1799 -lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2 1.1800 - 1.1801 -lemmas mem_simps = 1.1802 - insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff 1.1803 - mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff 1.1804 - -- {* Each of these has ALREADY been added @{text "[simp]"} above. *} 1.1805 - 1.1806 -(*Would like to add these, but the existing code only searches for the 1.1807 - outer-level constant, which in this case is just "op :"; we instead need 1.1808 - to use term-nets to associate patterns with rules. Also, if a rule fails to 1.1809 - apply, then the formula should be kept. 1.1810 - [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]), 1.1811 - ("Int", [IntD1,IntD2]), 1.1812 - ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])] 1.1813 - *) 1.1814 - 1.1815 -ML {* 1.1816 - val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs; 1.1817 -*} 1.1818 -declaration {* fn _ => 1.1819 - Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs)) 1.1820 -*} 1.1821 - 1.1822 - 1.1823 -subsubsection {* The proper subset'' relation *} 1.1824 - 1.1825 -lemma psubsetI [intro!,noatp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B" 1.1826 - by (unfold less_le) blast 1.1827 - 1.1828 -lemma psubsetE [elim!,noatp]: 1.1829 - "[|A \<subset> B; [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R" 1.1830 - by (unfold less_le) blast 1.1831 - 1.1832 -lemma psubset_insert_iff: 1.1833 - "(A \<subset> insert x B) = (if x \<in> B then A \<subset> B else if x \<in> A then A - {x} \<subset> B else A \<subseteq> B)" 1.1834 - by (auto simp add: less_le subset_insert_iff) 1.1835 - 1.1836 -lemma psubset_eq: "(A \<subset> B) = (A \<subseteq> B & A \<noteq> B)" 1.1837 - by (simp only: less_le) 1.1838 - 1.1839 -lemma psubset_imp_subset: "A \<subset> B ==> A \<subseteq> B" 1.1840 - by (simp add: psubset_eq) 1.1841 - 1.1842 -lemma psubset_trans: "[| A \<subset> B; B \<subset> C |] ==> A \<subset> C" 1.1843 -apply (unfold less_le) 1.1844 -apply (auto dest: subset_antisym) 1.1845 -done 1.1846 - 1.1847 -lemma psubsetD: "[| A \<subset> B; c \<in> A |] ==> c \<in> B" 1.1848 -apply (unfold less_le) 1.1849 -apply (auto dest: subsetD) 1.1850 -done 1.1851 - 1.1852 -lemma psubset_subset_trans: "A \<subset> B ==> B \<subseteq> C ==> A \<subset> C" 1.1853 - by (auto simp add: psubset_eq) 1.1854 - 1.1855 -lemma subset_psubset_trans: "A \<subseteq> B ==> B \<subset> C ==> A \<subset> C" 1.1856 - by (auto simp add: psubset_eq) 1.1857 - 1.1858 -lemma psubset_imp_ex_mem: "A \<subset> B ==> \<exists>b. b \<in> (B - A)" 1.1859 - by (unfold less_le) blast 1.1860 - 1.1861 -lemma atomize_ball: 1.1862 - "(!!x. x \<in> A ==> P x) == Trueprop (\<forall>x\<in>A. P x)" 1.1863 - by (simp only: Ball_def atomize_all atomize_imp) 1.1864 - 1.1865 -lemmas [symmetric, rulify] = atomize_ball 1.1866 - and [symmetric, defn] = atomize_ball 1.1867 - 1.1868 - 1.1869 -subsection {* Further set-theory lemmas *} 1.1870 - 1.1871 -subsubsection {* Derived rules involving subsets. *} 1.1872 - 1.1873 -text {* @{text insert}. *} 1.1874 - 1.1875 -lemma subset_insertI: "B \<subseteq> insert a B" 1.1876 - by (rule subsetI) (erule insertI2) 1.1877 - 1.1878 -lemma subset_insertI2: "A \<subseteq> B \<Longrightarrow> A \<subseteq> insert b B" 1.1879 - by blast 1.1880 - 1.1881 -lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)" 1.1882 - by blast 1.1883 1.1884 1.1885 text {* \medskip Big Union -- least upper bound of a set. *} 1.1886 @@ -1156,6 +1467,14 @@ 1.1887 lemma Union_least: "(!!X. X \<in> A ==> X \<subseteq> C) ==> Union A \<subseteq> C" 1.1888 by (iprover intro: subsetI elim: UnionE dest: subsetD) 1.1889 1.1890 +lemma Sup_set_eq: "Sup S = \<Union>S" 1.1891 + apply (rule subset_antisym) 1.1892 + apply (rule Sup_least) 1.1893 + apply (erule Union_upper) 1.1894 + apply (rule Union_least) 1.1895 + apply (erule Sup_upper) 1.1896 + done 1.1897 + 1.1898 1.1899 text {* \medskip General union. *} 1.1900 1.1901 @@ -1178,76 +1497,21 @@ 1.1902 lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A" 1.1903 by (iprover intro: InterI subsetI dest: subsetD) 1.1904 1.1905 +lemma Inf_set_eq: "Inf S = \<Inter>S" 1.1906 + apply (rule subset_antisym) 1.1907 + apply (rule Inter_greatest) 1.1908 + apply (erule Inf_lower) 1.1909 + apply (rule Inf_greatest) 1.1910 + apply (erule Inter_lower) 1.1911 + done 1.1912 + 1.1913 lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a" 1.1914 by blast 1.1915 1.1916 lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)" 1.1917 by (iprover intro: INT_I subsetI dest: subsetD) 1.1918 1.1919 - 1.1920 -text {* \medskip Finite Union -- the least upper bound of two sets. *} 1.1921 - 1.1922 -lemma Un_upper1: "A \<subseteq> A \<union> B" 1.1923 - by blast 1.1924 - 1.1925 -lemma Un_upper2: "B \<subseteq> A \<union> B" 1.1926 - by blast 1.1927 - 1.1928 -lemma Un_least: "A \<subseteq> C ==> B \<subseteq> C ==> A \<union> B \<subseteq> C" 1.1929 - by blast 1.1930 - 1.1931 - 1.1932 -text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *} 1.1933 - 1.1934 -lemma Int_lower1: "A \<inter> B \<subseteq> A" 1.1935 - by blast 1.1936 - 1.1937 -lemma Int_lower2: "A \<inter> B \<subseteq> B" 1.1938 - by blast 1.1939 - 1.1940 -lemma Int_greatest: "C \<subseteq> A ==> C \<subseteq> B ==> C \<subseteq> A \<inter> B" 1.1941 - by blast 1.1942 - 1.1943 - 1.1944 -text {* \medskip Set difference. *} 1.1945 - 1.1946 -lemma Diff_subset: "A - B \<subseteq> A" 1.1947 - by blast 1.1948 - 1.1949 -lemma Diff_subset_conv: "(A - B \<subseteq> C) = (A \<subseteq> B \<union> C)" 1.1950 -by blast 1.1951 - 1.1952 - 1.1953 -subsubsection {* Equalities involving union, intersection, inclusion, etc. *} 1.1954 - 1.1955 -text {* @{text "{}"}. *} 1.1956 - 1.1957 -lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})" 1.1958 - -- {* supersedes @{text "Collect_False_empty"} *} 1.1959 - by auto 1.1960 - 1.1961 -lemma subset_empty [simp]: "(A \<subseteq> {}) = (A = {})" 1.1962 - by blast 1.1963 - 1.1964 -lemma not_psubset_empty [iff]: "\<not> (A < {})" 1.1965 - by (unfold less_le) blast 1.1966 - 1.1967 -lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\<forall>x. \<not> P x)" 1.1968 -by blast 1.1969 - 1.1970 -lemma empty_Collect_eq [simp]: "({} = Collect P) = (\<forall>x. \<not> P x)" 1.1971 -by blast 1.1972 - 1.1973 -lemma Collect_neg_eq: "{x. \<not> P x} = - {x. P x}" 1.1974 - by blast 1.1975 - 1.1976 -lemma Collect_disj_eq: "{x. P x | Q x} = {x. P x} \<union> {x. Q x}" 1.1977 - by blast 1.1978 - 1.1979 -lemma Collect_imp_eq: "{x. P x --> Q x} = -{x. P x} \<union> {x. Q x}" 1.1980 - by blast 1.1981 - 1.1982 -lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}" 1.1983 +lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)" 1.1984 by blast 1.1985 1.1986 lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})" 1.1987 @@ -1263,97 +1527,59 @@ 1.1988 by blast 1.1989 1.1990 1.1991 -text {* \medskip @{text insert}. *} 1.1992 - 1.1993 -lemma insert_is_Un: "insert a A = {a} Un A" 1.1994 - -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"} *} 1.1995 - by blast 1.1996 - 1.1997 -lemma insert_not_empty [simp]: "insert a A \<noteq> {}" 1.1998 - by blast 1.1999 - 1.2000 -lemmas empty_not_insert = insert_not_empty [symmetric, standard] 1.2001 -declare empty_not_insert [simp] 1.2002 - 1.2003 -lemma insert_absorb: "a \<in> A ==> insert a A = A" 1.2004 - -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *} 1.2005 - -- {* with \emph{quadratic} running time *} 1.2006 - by blast 1.2007 - 1.2008 -lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A" 1.2009 - by blast 1.2010 - 1.2011 -lemma insert_commute: "insert x (insert y A) = insert y (insert x A)" 1.2012 - by blast 1.2013 - 1.2014 -lemma insert_subset [simp]: "(insert x A \<subseteq> B) = (x \<in> B & A \<subseteq> B)" 1.2015 - by blast 1.2016 - 1.2017 -lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B" 1.2018 - -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *} 1.2019 - apply (rule_tac x = "A - {a}" in exI, blast) 1.2020 - done 1.2021 - 1.2022 -lemma insert_Collect: "insert a (Collect P) = {u. u \<noteq> a --> P u}" 1.2023 - by auto 1.2024 - 1.2025 -lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)" 1.2026 - by blast 1.2027 - 1.2028 -lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)" 1.2029 +subsubsection {* The Powerset operator -- Pow *} 1.2030 + 1.2031 +global 1.2032 + 1.2033 +consts 1.2034 + Pow :: "'a set => 'a set set" 1.2035 + 1.2036 +local 1.2037 + 1.2038 +defs 1.2039 + Pow_def: "Pow A == {B. B <= A}" 1.2040 + 1.2041 +lemma Pow_iff [iff]: "(A \<in> Pow B) = (A \<subseteq> B)" 1.2042 + by (simp add: Pow_def) 1.2043 + 1.2044 +lemma PowI: "A \<subseteq> B ==> A \<in> Pow B" 1.2045 + by (simp add: Pow_def) 1.2046 + 1.2047 +lemma PowD: "A \<in> Pow B ==> A \<subseteq> B" 1.2048 + by (simp add: Pow_def) 1.2049 + 1.2050 +lemma Pow_bottom: "{} \<in> Pow B" 1.2051 + by simp 1.2052 + 1.2053 +lemma Pow_top: "A \<in> Pow A" 1.2054 + by (simp add: subset_refl) 1.2055 + 1.2056 + 1.2057 + 1.2058 +subsubsection {* Getting the Contents of a Singleton Set *} 1.2059 + 1.2060 +definition contents :: "'a set \<Rightarrow> 'a" where 1.2061 + [code del]: "contents X = (THE x. X = {x})" 1.2062 + 1.2063 +lemma contents_eq [simp]: "contents {x} = x" 1.2064 + by (simp add: contents_def) 1.2065 + 1.2066 + 1.2067 +subsubsection {* Range of a function -- just a translation for image! *} 1.2068 + 1.2069 +abbreviation 1.2070 + range :: "('a => 'b) => 'b set" where -- "of function" 1.2071 + "range f == f  UNIV" 1.2072 + 1.2073 +lemma range_eqI: "b = f x ==> b \<in> range f" 1.2074 + by simp 1.2075 + 1.2076 +lemma rangeI: "f x \<in> range f" 1.2077 + by simp 1.2078 + 1.2079 +lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P" 1.2080 by blast 1.2081 1.2082 -lemma insert_disjoint [simp,noatp]: 1.2083 - "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})" 1.2084 - "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)" 1.2085 - by auto 1.2086 - 1.2087 -lemma disjoint_insert [simp,noatp]: 1.2088 - "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})" 1.2089 - "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)" 1.2090 - by auto 1.2091 - 1.2092 -text {* \medskip @{text image}. *} 1.2093 - 1.2094 -lemma image_empty [simp]: "f{} = {}" 1.2095 - by blast 1.2096 - 1.2097 -lemma image_insert [simp]: "f  insert a B = insert (f a) (fB)" 1.2098 - by blast 1.2099 - 1.2100 -lemma image_constant: "x \<in> A ==> (\<lambda>x. c)  A = {c}" 1.2101 - by auto 1.2102 - 1.2103 -lemma image_constant_conv: "(%x. c)  A = (if A = {} then {} else {c})" 1.2104 -by auto 1.2105 - 1.2106 -lemma image_image: "f  (g  A) = (\<lambda>x. f (g x))  A" 1.2107 - by blast 1.2108 - 1.2109 -lemma insert_image [simp]: "x \<in> A ==> insert (f x) (fA) = fA" 1.2110 - by blast 1.2111 - 1.2112 -lemma image_is_empty [iff]: "(fA = {}) = (A = {})" 1.2113 - by blast 1.2114 - 1.2115 - 1.2116 -lemma image_Collect [noatp]: "f  {x. P x} = {f x | x. P x}" 1.2117 - -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS, 1.2118 - with its implicit quantifier and conjunction. Also image enjoys better 1.2119 - equational properties than does the RHS. *} 1.2120 - by blast 1.2121 - 1.2122 -lemma if_image_distrib [simp]: 1.2123 - "(\<lambda>x. if P x then f x else g x)  S 1.2124 - = (f  (S \<inter> {x. P x})) \<union> (g  (S \<inter> {x. \<not> P x}))" 1.2125 - by (auto simp add: image_def) 1.2126 - 1.2127 -lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> fM = gN" 1.2128 - by (simp add: image_def) 1.2129 - 1.2130 - 1.2131 -text {* \medskip @{text range}. *} 1.2132 - 1.2133 lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f" 1.2134 by auto 1.2135 1.2136 @@ -1361,6 +1587,8 @@ 1.2137 by (subst image_image, simp) 1.2138 1.2139 1.2140 +subsection {* Further rules and properties *} 1.2141 + 1.2142 text {* \medskip @{text Int} *} 1.2143 1.2144 lemma Int_absorb [simp]: "A \<inter> A = A" 1.2145 @@ -2048,6 +2276,16 @@ 1.2146 lemma Compl_anti_mono: "A \<subseteq> B ==> -B \<subseteq> -A" 1.2147 by blast 1.2148 1.2149 +lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B" 1.2150 + apply (fold inf_set_eq sup_set_eq) 1.2151 + apply (erule mono_inf) 1.2152 + done 1.2153 + 1.2154 +lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)" 1.2155 + apply (fold inf_set_eq sup_set_eq) 1.2156 + apply (erule mono_sup) 1.2157 + done 1.2158 + 1.2159 text {* \medskip Monotonicity of implications. *} 1.2160 1.2161 lemma in_mono: "A \<subseteq> B ==> x \<in> A --> x \<in> B" 1.2162 @@ -2090,15 +2328,12 @@ 1.2163 by iprover 1.2164 1.2165 1.2166 -subsection {* Inverse image of a function *} 1.2167 +subsubsection {* Inverse image of a function *} 1.2168 1.2169 constdefs 1.2170 vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-" 90) 1.2171 [code del]: "f - B == {x. f x : B}" 1.2172 1.2173 - 1.2174 -subsubsection {* Basic rules *} 1.2175 - 1.2176 lemma vimage_eq [simp]: "(a : f - B) = (f a : B)" 1.2177 by (unfold vimage_def) blast 1.2178 1.2179 @@ -2117,9 +2352,6 @@ 1.2180 lemma vimageD: "a : f - A ==> f a : A" 1.2181 by (unfold vimage_def) fast 1.2182 1.2183 - 1.2184 -subsubsection {* Equations *} 1.2185 - 1.2186 lemma vimage_empty [simp]: "f - {} = {}" 1.2187 by blast 1.2188 1.2189 @@ -2184,28 +2416,7 @@ 1.2190 by blast 1.2191 1.2192 1.2193 -subsection {* Getting the Contents of a Singleton Set *} 1.2194 - 1.2195 -definition contents :: "'a set \<Rightarrow> 'a" where 1.2196 - [code del]: "contents X = (THE x. X = {x})" 1.2197 - 1.2198 -lemma contents_eq [simp]: "contents {x} = x" 1.2199 - by (simp add: contents_def) 1.2200 - 1.2201 - 1.2202 -subsection {* Transitivity rules for calculational reasoning *} 1.2203 - 1.2204 -lemma set_rev_mp: "x:A ==> A \<subseteq> B ==> x:B" 1.2205 - by (rule subsetD) 1.2206 - 1.2207 -lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B" 1.2208 - by (rule subsetD) 1.2209 - 1.2210 -lemmas basic_trans_rules [trans] = 1.2211 - order_trans_rules set_rev_mp set_mp 1.2212 - 1.2213 - 1.2214 -subsection {* Least value operator *} 1.2215 +subsubsection {* Least value operator *} 1.2216 1.2217 lemma Least_mono: 1.2218 "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y 1.2219 @@ -2218,7 +2429,7 @@ 1.2220 done 1.2221 1.2222 1.2223 -subsection {* Rudimentary code generation *} 1.2224 +subsubsection {* Rudimentary code generation *} 1.2225 1.2226 lemma empty_code [code]: "{} x \<longleftrightarrow> False" 1.2227 unfolding empty_def Collect_def .. 1.2228 @@ -2239,257 +2450,13 @@ 1.2229 unfolding vimage_def Collect_def mem_def .. 1.2230 1.2231 1.2232 -subsection {* Complete lattices *} 1.2233 - 1.2234 -notation 1.2235 - less_eq (infix "\<sqsubseteq>" 50) and 1.2236 - less (infix "\<sqsubset>" 50) and 1.2237 - inf (infixl "\<sqinter>" 70) and 1.2238 - sup (infixl "\<squnion>" 65) 1.2239 - 1.2240 -class complete_lattice = lattice + bot + top + 1.2241 - fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900) 1.2242 - and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900) 1.2243 - assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x" 1.2244 - and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A" 1.2245 - assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A" 1.2246 - and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z" 1.2247 -begin 1.2248 - 1.2249 -lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}" 1.2250 - by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) 1.2251 - 1.2252 -lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}" 1.2253 - by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) 1.2254 - 1.2255 -lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}" 1.2256 - unfolding Sup_Inf by auto 1.2257 - 1.2258 -lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}" 1.2259 - unfolding Inf_Sup by auto 1.2260 - 1.2261 -lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A" 1.2262 - by (auto intro: antisym Inf_greatest Inf_lower) 1.2263 - 1.2264 -lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A" 1.2265 - by (auto intro: antisym Sup_least Sup_upper) 1.2266 - 1.2267 -lemma Inf_singleton [simp]: 1.2268 - "\<Sqinter>{a} = a" 1.2269 - by (auto intro: antisym Inf_lower Inf_greatest) 1.2270 - 1.2271 -lemma Sup_singleton [simp]: 1.2272 - "\<Squnion>{a} = a" 1.2273 - by (auto intro: antisym Sup_upper Sup_least) 1.2274 - 1.2275 -lemma Inf_insert_simp: 1.2276 - "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)" 1.2277 - by (cases "A = {}") (simp_all, simp add: Inf_insert) 1.2278 - 1.2279 -lemma Sup_insert_simp: 1.2280 - "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)" 1.2281 - by (cases "A = {}") (simp_all, simp add: Sup_insert) 1.2282 - 1.2283 -lemma Inf_binary: 1.2284 - "\<Sqinter>{a, b} = a \<sqinter> b" 1.2285 - by (simp add: Inf_insert_simp) 1.2286 - 1.2287 -lemma Sup_binary: 1.2288 - "\<Squnion>{a, b} = a \<squnion> b" 1.2289 - by (simp add: Sup_insert_simp) 1.2290 - 1.2291 -lemma bot_def: 1.2292 - "bot = \<Squnion>{}" 1.2293 - by (auto intro: antisym Sup_least) 1.2294 - 1.2295 -lemma top_def: 1.2296 - "top = \<Sqinter>{}" 1.2297 - by (auto intro: antisym Inf_greatest) 1.2298 - 1.2299 -lemma sup_bot [simp]: 1.2300 - "x \<squnion> bot = x" 1.2301 - using bot_least [of x] by (simp add: le_iff_sup sup_commute) 1.2302 - 1.2303 -lemma inf_top [simp]: 1.2304 - "x \<sqinter> top = x" 1.2305 - using top_greatest [of x] by (simp add: le_iff_inf inf_commute) 1.2306 - 1.2307 -definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where 1.2308 - "SUPR A f == \<Squnion> (f  A)" 1.2309 - 1.2310 -definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where 1.2311 - "INFI A f == \<Sqinter> (f  A)" 1.2312 - 1.2313 -end 1.2314 - 1.2315 -syntax 1.2316 - "_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" [0, 10] 10) 1.2317 - "_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" [0, 10] 10) 1.2318 - "_INF1" :: "pttrns => 'b => 'b" ("(3INF _./ _)" [0, 10] 10) 1.2319 - "_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" [0, 10] 10) 1.2320 - 1.2321 -translations 1.2322 - "SUP x y. B" == "SUP x. SUP y. B" 1.2323 - "SUP x. B" == "CONST SUPR CONST UNIV (%x. B)" 1.2324 - "SUP x. B" == "SUP x:CONST UNIV. B" 1.2325 - "SUP x:A. B" == "CONST SUPR A (%x. B)" 1.2326 - "INF x y. B" == "INF x. INF y. B" 1.2327 - "INF x. B" == "CONST INFI CONST UNIV (%x. B)" 1.2328 - "INF x. B" == "INF x:CONST UNIV. B" 1.2329 - "INF x:A. B" == "CONST INFI A (%x. B)" 1.2330 - 1.2331 -(* To avoid eta-contraction of body: *) 1.2332 -print_translation {* 1.2333 -let 1.2334 - fun btr' syn (A :: Abs abs :: ts) = 1.2335 - let val (x,t) = atomic_abs_tr' abs 1.2336 - in list_comb (Syntax.const syn$ x $A$ t, ts) end
1.2337 -  val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const
1.2338 -in
1.2339 -[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")]
1.2340 -end
1.2341 -*}
1.2342 -
1.2343 -context complete_lattice
1.2344 -begin
1.2345 -
1.2346 -lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
1.2347 -  by (auto simp add: SUPR_def intro: Sup_upper)
1.2348 -
1.2349 -lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
1.2350 -  by (auto simp add: SUPR_def intro: Sup_least)
1.2351 -
1.2352 -lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
1.2353 -  by (auto simp add: INFI_def intro: Inf_lower)
1.2354 -
1.2355 -lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
1.2356 -  by (auto simp add: INFI_def intro: Inf_greatest)
1.2357 -
1.2358 -lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
1.2359 -  by (auto intro: antisym SUP_leI le_SUPI)
1.2360 -
1.2361 -lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
1.2362 -  by (auto intro: antisym INF_leI le_INFI)
1.2363 -
1.2364 -end
1.2365 -
1.2366 -
1.2367 -subsection {* Bool as complete lattice *}
1.2368 -
1.2369 -instantiation bool :: complete_lattice
1.2370 -begin
1.2371 -
1.2372 -definition
1.2373 -  Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
1.2374 -
1.2375 -definition
1.2376 -  Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
1.2377 -
1.2378 -instance
1.2379 -  by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
1.2380 -
1.2381 -end
1.2382 -
1.2383 -lemma Inf_empty_bool [simp]:
1.2384 -  "\<Sqinter>{}"
1.2385 -  unfolding Inf_bool_def by auto
1.2386 -
1.2387 -lemma not_Sup_empty_bool [simp]:
1.2388 -  "\<not> Sup {}"
1.2389 -  unfolding Sup_bool_def by auto
1.2390 -
1.2391 -
1.2392 -subsection {* Fun as complete lattice *}
1.2393 -
1.2394 -instantiation "fun" :: (type, complete_lattice) complete_lattice
1.2395 -begin
1.2396 -
1.2397 -definition
1.2398 -  Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
1.2399 -
1.2400 -definition
1.2401 -  Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
1.2402 -
1.2403 -instance
1.2404 -  by intro_classes
1.2405 -    (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
1.2406 -      intro: Inf_lower Sup_upper Inf_greatest Sup_least)
1.2407 -
1.2408 -end
1.2409 -
1.2410 -lemma Inf_empty_fun:
1.2411 -  "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
1.2412 -  by rule (auto simp add: Inf_fun_def)
1.2413 -
1.2414 -lemma Sup_empty_fun:
1.2415 -  "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
1.2416 -  by rule (auto simp add: Sup_fun_def)
1.2417 -
1.2418 -
1.2419 -subsection {* Set as lattice *}
1.2420 -
1.2421 -lemma inf_set_eq: "A \<sqinter> B = A \<inter> B"
1.2422 -  apply (rule subset_antisym)
1.2423 -  apply (rule Int_greatest)
1.2424 -  apply (rule inf_le1)
1.2425 -  apply (rule inf_le2)
1.2426 -  apply (rule inf_greatest)
1.2427 -  apply (rule Int_lower1)
1.2428 -  apply (rule Int_lower2)
1.2429 -  done
1.2430 -
1.2431 -lemma sup_set_eq: "A \<squnion> B = A \<union> B"
1.2432 -  apply (rule subset_antisym)
1.2433 -  apply (rule sup_least)
1.2434 -  apply (rule Un_upper1)
1.2435 -  apply (rule Un_upper2)
1.2436 -  apply (rule Un_least)
1.2437 -  apply (rule sup_ge1)
1.2438 -  apply (rule sup_ge2)
1.2439 -  done
1.2440 -
1.2441 -lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
1.2442 -  apply (fold inf_set_eq sup_set_eq)
1.2443 -  apply (erule mono_inf)
1.2444 -  done
1.2445 -
1.2446 -lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
1.2447 -  apply (fold inf_set_eq sup_set_eq)
1.2448 -  apply (erule mono_sup)
1.2449 -  done
1.2450 -
1.2451 -lemma Inf_set_eq: "\<Sqinter>S = \<Inter>S"
1.2452 -  apply (rule subset_antisym)
1.2453 -  apply (rule Inter_greatest)
1.2454 -  apply (erule Inf_lower)
1.2455 -  apply (rule Inf_greatest)
1.2456 -  apply (erule Inter_lower)
1.2457 -  done
1.2458 -
1.2459 -lemma Sup_set_eq: "\<Squnion>S = \<Union>S"
1.2460 -  apply (rule subset_antisym)
1.2461 -  apply (rule Sup_least)
1.2462 -  apply (erule Union_upper)
1.2463 -  apply (rule Union_least)
1.2464 -  apply (erule Sup_upper)
1.2465 -  done
1.2466 -
1.2467 -lemma top_set_eq: "top = UNIV"
1.2468 -  by (iprover intro!: subset_antisym subset_UNIV top_greatest)
1.2469 -
1.2470 -lemma bot_set_eq: "bot = {}"
1.2471 -  by (iprover intro!: subset_antisym empty_subsetI bot_least)
1.2472 -
1.2473 -no_notation
1.2474 -  less_eq  (infix "\<sqsubseteq>" 50) and
1.2475 -  less (infix "\<sqsubset>" 50) and
1.2476 -  inf  (infixl "\<sqinter>" 70) and
1.2477 -  sup  (infixl "\<squnion>" 65) and
1.2478 -  Inf  ("\<Sqinter>_" [900] 900) and
1.2479 -  Sup  ("\<Squnion>_" [900] 900)
1.2480 -
1.2481 -
1.2482 -subsection {* Basic ML bindings *}
1.2483 +subsection {* Misc theorem and ML bindings *}
1.2484 +
1.2485 +lemmas equalityI = subset_antisym
1.2486 +lemmas mem_simps =
1.2487 +  insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
1.2488 +  mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
1.2489 +  -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
1.2490
1.2491  ML {*
1.2492  val Ball_def = @{thm Ball_def}
`