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