restructured theory Set.thy
authorhaftmann
Sat Mar 07 15:20:32 2009 +0100 (2009-03-07)
changeset 30352047f183c43b0
parent 30333 e9971af27b11
child 30353 f977e10af7e2
child 30374 7311a1546d85
restructured theory Set.thy
src/HOL/Set.thy
     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:    "f`A            == {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]:    "f`A == {y. EX x:A. y = f(x)}"
  1.1031 +
  1.1032 +lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A"
  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 : f`A"
  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) = f`A Un f`B"
  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 : f`A) = (EX x:A. z = f x)"
  1.1056 +  by blast
  1.1057 +
  1.1058 +lemma image_subset_iff: "(f`A \<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> f`A) = (EX AA. AA \<subseteq> A & B = f`AA)"
  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) ==> f`A \<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) (f`B)"
  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) (f`A) = f`A"
  1.1105 +  by blast
  1.1106 +
  1.1107 +lemma image_is_empty [iff]: "(f`A = {}) = (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) ==> f`M = g`N"
  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: "f`A = (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 : f`A"
  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 : f`A"
  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) = f`A Un f`B"
  1.1738 -  by blast
  1.1739 -
  1.1740 -lemma image_eq_UN: "f`A = (UN x:A. {f x})"
  1.1741 -  by blast
  1.1742 -
  1.1743 -lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
  1.1744 -  by blast
  1.1745 -
  1.1746 -lemma image_subset_iff: "(f`A \<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> f`A) = (EX AA. AA \<subseteq> A & B = f`AA)"
  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) ==> f`A \<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) (f`B)"
  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) (f`A) = f`A"
  1.2110 -  by blast
  1.2111 -
  1.2112 -lemma image_is_empty [iff]: "(f`A = {}) = (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) ==> f`M = g`N"
  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}