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,31 +549,440 @@
1.959 (EX x:A. P x) = (EX x:B. Q x)"
1.960 by (simp add: simp_implies_def Bex_def cong: conj_cong)
1.961
1.962 +
1.963 +subsubsection {* Subsets *}
1.964 +
1.965 +lemma subsetI [atp,intro!]: "(!!x. x:A ==> x:B) ==> A \<subseteq> B"
1.966 + by (auto simp add: mem_def intro: predicate1I)
1.967 +
1.968 +text {*
1.969 + \medskip Map the type @{text "'a set => anything"} to just @{typ
1.970 + 'a}; for overloading constants whose first argument has type @{typ
1.971 + "'a set"}.
1.972 +*}
1.973 +
1.974 +lemma subsetD [elim]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
1.975 + -- {* Rule in Modus Ponens style. *}
1.976 + by (unfold mem_def) blast
1.977 +
1.978 +declare subsetD [intro?] -- FIXME
1.979 +
1.980 +lemma rev_subsetD: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
1.981 + -- {* The same, with reversed premises for use with @{text erule} --
1.982 + cf @{text rev_mp}. *}
1.983 + by (rule subsetD)
1.984 +
1.985 +declare rev_subsetD [intro?] -- FIXME
1.986 +
1.987 +text {*
1.988 + \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
1.989 +*}
1.990 +
1.991 +ML {*
1.992 + fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
1.993 +*}
1.994 +
1.995 +lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
1.996 + -- {* Classical elimination rule. *}
1.997 + by (unfold mem_def) blast
1.998 +
1.999 lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
1.1000
1.1001 -lemma atomize_ball:
1.1002 - "(!!x. x \<in> A ==> P x) == Trueprop (\<forall>x\<in>A. P x)"
1.1003 - by (simp only: Ball_def atomize_all atomize_imp)
1.1004 -
1.1005 -lemmas [symmetric, rulify] = atomize_ball
1.1006 - and [symmetric, defn] = atomize_ball
1.1007 -
1.1008 -
1.1009 -subsubsection {* Image of a set under a function. *}
1.1010 -
1.1011 text {*
1.1012 - Frequently @{term b} does not have the syntactic form of @{term "f x"}.
1.1013 + \medskip Takes assumptions @{prop "A \<subseteq> B"}; @{prop "c \<in> A"} and
1.1014 + creates the assumption @{prop "c \<in> B"}.
1.1015 *}
1.1016
1.1017 -global
1.1018 -
1.1019 -consts
1.1020 - image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90)
1.1021 -
1.1022 -local
1.1023 -
1.1024 -defs
1.1025 - image_def [noatp]: "f`A == {y. EX x:A. y = f(x)}"
1.1026 +ML {*
1.1027 + fun set_mp_tac i = etac @{thm subsetCE} i THEN mp_tac i
1.1028 +*}
1.1029 +
1.1030 +lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
1.1031 + by blast
1.1032 +
1.1033 +lemma subset_refl [simp,atp]: "A \<subseteq> A"
1.1034 + by fast
1.1035 +
1.1036 +lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"
1.1037 + by blast
1.1038 +
1.1039 +
1.1040 +subsubsection {* Equality *}
1.1041 +
1.1042 +lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
1.1043 + apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
1.1044 + apply (rule Collect_mem_eq)
1.1045 + apply (rule Collect_mem_eq)
1.1046 + done
1.1047 +
1.1048 +(* Due to Brian Huffman *)
1.1049 +lemma expand_set_eq: "(A = B) = (ALL x. (x:A) = (x:B))"
1.1050 +by(auto intro:set_ext)
1.1051 +
1.1052 +lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
1.1053 + -- {* Anti-symmetry of the subset relation. *}
1.1054 + by (iprover intro: set_ext subsetD)
1.1055 +
1.1056 +lemmas equalityI [intro!] = subset_antisym
1.1057 +
1.1058 +text {*
1.1059 + \medskip Equality rules from ZF set theory -- are they appropriate
1.1060 + here?
1.1061 +*}
1.1062 +
1.1063 +lemma equalityD1: "A = B ==> A \<subseteq> B"
1.1064 + by (simp add: subset_refl)
1.1065 +
1.1066 +lemma equalityD2: "A = B ==> B \<subseteq> A"
1.1067 + by (simp add: subset_refl)
1.1068 +
1.1069 +text {*
1.1070 + \medskip Be careful when adding this to the claset as @{text
1.1071 + subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{}
1.1072 + \<subseteq> A"} and @{prop "A \<subseteq> {}"} and then back to @{prop "A = {}"}!
1.1073 +*}
1.1074 +
1.1075 +lemma equalityE: "A = B ==> (A \<subseteq> B ==> B \<subseteq> A ==> P) ==> P"
1.1076 + by (simp add: subset_refl)
1.1077 +
1.1078 +lemma equalityCE [elim]:
1.1079 + "A = B ==> (c \<in> A ==> c \<in> B ==> P) ==> (c \<notin> A ==> c \<notin> B ==> P) ==> P"
1.1080 + by blast
1.1081 +
1.1082 +lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)"
1.1083 + by simp
1.1084 +
1.1085 +lemma eqelem_imp_iff: "x = y ==> (x : A) = (y : A)"
1.1086 + by simp
1.1087 +
1.1088 +
1.1089 +subsubsection {* The universal set -- UNIV *}
1.1090 +
1.1091 +lemma UNIV_I [simp]: "x : UNIV"
1.1092 + by (simp add: UNIV_def)
1.1093 +
1.1094 +declare UNIV_I [intro] -- {* unsafe makes it less likely to cause problems *}
1.1095 +
1.1096 +lemma UNIV_witness [intro?]: "EX x. x : UNIV"
1.1097 + by simp
1.1098 +
1.1099 +lemma subset_UNIV [simp]: "A \<subseteq> UNIV"
1.1100 + by (rule subsetI) (rule UNIV_I)
1.1101 +
1.1102 +text {*
1.1103 + \medskip Eta-contracting these two rules (to remove @{text P})
1.1104 + causes them to be ignored because of their interaction with
1.1105 + congruence rules.
1.1106 +*}
1.1107 +
1.1108 +lemma ball_UNIV [simp]: "Ball UNIV P = All P"
1.1109 + by (simp add: Ball_def)
1.1110 +
1.1111 +lemma bex_UNIV [simp]: "Bex UNIV P = Ex P"
1.1112 + by (simp add: Bex_def)
1.1113 +
1.1114 +lemma UNIV_eq_I: "(\<And>x. x \<in> A) \<Longrightarrow> UNIV = A"
1.1115 + by auto
1.1116 +
1.1117 +
1.1118 +subsubsection {* The empty set *}
1.1119 +
1.1120 +lemma empty_iff [simp]: "(c : {}) = False"
1.1121 + by (simp add: empty_def)
1.1122 +
1.1123 +lemma emptyE [elim!]: "a : {} ==> P"
1.1124 + by simp
1.1125 +
1.1126 +lemma empty_subsetI [iff]: "{} \<subseteq> A"
1.1127 + -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}
1.1128 + by blast
1.1129 +
1.1130 +lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"
1.1131 + by blast
1.1132 +
1.1133 +lemma equals0D: "A = {} ==> a \<notin> A"
1.1134 + -- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *}
1.1135 + by blast
1.1136 +
1.1137 +lemma ball_empty [simp]: "Ball {} P = True"
1.1138 + by (simp add: Ball_def)
1.1139 +
1.1140 +lemma bex_empty [simp]: "Bex {} P = False"
1.1141 + by (simp add: Bex_def)
1.1142 +
1.1143 +lemma UNIV_not_empty [iff]: "UNIV ~= {}"
1.1144 + by (blast elim: equalityE)
1.1145 +
1.1146 +
1.1147 +subsubsection {* The Powerset operator -- Pow *}
1.1148 +
1.1149 +lemma Pow_iff [iff]: "(A \<in> Pow B) = (A \<subseteq> B)"
1.1150 + by (simp add: Pow_def)
1.1151 +
1.1152 +lemma PowI: "A \<subseteq> B ==> A \<in> Pow B"
1.1153 + by (simp add: Pow_def)
1.1154 +
1.1155 +lemma PowD: "A \<in> Pow B ==> A \<subseteq> B"
1.1156 + by (simp add: Pow_def)
1.1157 +
1.1158 +lemma Pow_bottom: "{} \<in> Pow B"
1.1159 + by simp
1.1160 +
1.1161 +lemma Pow_top: "A \<in> Pow A"
1.1162 + by (simp add: subset_refl)
1.1163 +
1.1164 +
1.1165 +subsubsection {* Set complement *}
1.1166 +
1.1167 +lemma Compl_iff [simp]: "(c \<in> -A) = (c \<notin> A)"
1.1168 + by (simp add: mem_def fun_Compl_def bool_Compl_def)
1.1169 +
1.1170 +lemma ComplI [intro!]: "(c \<in> A ==> False) ==> c \<in> -A"
1.1171 + by (unfold mem_def fun_Compl_def bool_Compl_def) blast
1.1172 +
1.1173 +text {*
1.1174 + \medskip This form, with negated conclusion, works well with the
1.1175 + Classical prover. Negated assumptions behave like formulae on the
1.1176 + right side of the notional turnstile ... *}
1.1177 +
1.1178 +lemma ComplD [dest!]: "c : -A ==> c~:A"
1.1179 + by (simp add: mem_def fun_Compl_def bool_Compl_def)
1.1180 +
1.1181 +lemmas ComplE = ComplD [elim_format]
1.1182 +
1.1183 +lemma Compl_eq: "- A = {x. ~ x : A}" by blast
1.1184 +
1.1185 +
1.1186 +subsubsection {* Binary union -- Un *}
1.1187 +
1.1188 +lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
1.1189 + by (unfold Un_def) blast
1.1190 +
1.1191 +lemma UnI1 [elim?]: "c:A ==> c : A Un B"
1.1192 + by simp
1.1193 +
1.1194 +lemma UnI2 [elim?]: "c:B ==> c : A Un B"
1.1195 + by simp
1.1196 +
1.1197 +text {*
1.1198 + \medskip Classical introduction rule: no commitment to @{prop A} vs
1.1199 + @{prop B}.
1.1200 +*}
1.1201 +
1.1202 +lemma UnCI [intro!]: "(c~:B ==> c:A) ==> c : A Un B"
1.1203 + by auto
1.1204 +
1.1205 +lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"
1.1206 + by (unfold Un_def) blast
1.1207 +
1.1208 +
1.1209 +subsubsection {* Binary intersection -- Int *}
1.1210 +
1.1211 +lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
1.1212 + by (unfold Int_def) blast
1.1213 +
1.1214 +lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B"
1.1215 + by simp
1.1216 +
1.1217 +lemma IntD1: "c : A Int B ==> c:A"
1.1218 + by simp
1.1219 +
1.1220 +lemma IntD2: "c : A Int B ==> c:B"
1.1221 + by simp
1.1222 +
1.1223 +lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"
1.1224 + by simp
1.1225 +
1.1226 +
1.1227 +subsubsection {* Set difference *}
1.1228 +
1.1229 +lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
1.1230 + by (simp add: mem_def fun_diff_def bool_diff_def)
1.1231 +
1.1232 +lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"
1.1233 + by simp
1.1234 +
1.1235 +lemma DiffD1: "c : A - B ==> c : A"
1.1236 + by simp
1.1237 +
1.1238 +lemma DiffD2: "c : A - B ==> c : B ==> P"
1.1239 + by simp
1.1240 +
1.1241 +lemma DiffE [elim!]: "c : A - B ==> (c:A ==> c~:B ==> P) ==> P"
1.1242 + by simp
1.1243 +
1.1244 +lemma set_diff_eq: "A - B = {x. x : A & ~ x : B}" by blast
1.1245 +
1.1246 +lemma Compl_eq_Diff_UNIV: "-A = (UNIV - A)"
1.1247 +by blast
1.1248 +
1.1249 +
1.1250 +subsubsection {* Augmenting a set -- insert *}
1.1251 +
1.1252 +lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"
1.1253 + by (unfold insert_def) blast
1.1254 +
1.1255 +lemma insertI1: "a : insert a B"
1.1256 + by simp
1.1257 +
1.1258 +lemma insertI2: "a : B ==> a : insert b B"
1.1259 + by simp
1.1260 +
1.1261 +lemma insertE [elim!]: "a : insert b A ==> (a = b ==> P) ==> (a:A ==> P) ==> P"
1.1262 + by (unfold insert_def) blast
1.1263 +
1.1264 +lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B"
1.1265 + -- {* Classical introduction rule. *}
1.1266 + by auto
1.1267 +
1.1268 +lemma subset_insert_iff: "(A \<subseteq> insert x B) = (if x:A then A - {x} \<subseteq> B else A \<subseteq> B)"
1.1269 + by auto
1.1270 +
1.1271 +lemma set_insert:
1.1272 + assumes "x \<in> A"
1.1273 + obtains B where "A = insert x B" and "x \<notin> B"
1.1274 +proof
1.1275 + from assms show "A = insert x (A - {x})" by blast
1.1276 +next
1.1277 + show "x \<notin> A - {x}" by blast
1.1278 +qed
1.1279 +
1.1280 +lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"
1.1281 +by auto
1.1282 +
1.1283 +subsubsection {* Singletons, using insert *}
1.1284 +
1.1285 +lemma singletonI [intro!,noatp]: "a : {a}"
1.1286 + -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
1.1287 + by (rule insertI1)
1.1288 +
1.1289 +lemma singletonD [dest!,noatp]: "b : {a} ==> b = a"
1.1290 + by blast
1.1291 +
1.1292 +lemmas singletonE = singletonD [elim_format]
1.1293 +
1.1294 +lemma singleton_iff: "(b : {a}) = (b = a)"
1.1295 + by blast
1.1296 +
1.1297 +lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
1.1298 + by blast
1.1299 +
1.1300 +lemma singleton_insert_inj_eq [iff,noatp]:
1.1301 + "({b} = insert a A) = (a = b & A \<subseteq> {b})"
1.1302 + by blast
1.1303 +
1.1304 +lemma singleton_insert_inj_eq' [iff,noatp]:
1.1305 + "(insert a A = {b}) = (a = b & A \<subseteq> {b})"
1.1306 + by blast
1.1307 +
1.1308 +lemma subset_singletonD: "A \<subseteq> {x} ==> A = {} | A = {x}"
1.1309 + by fast
1.1310 +
1.1311 +lemma singleton_conv [simp]: "{x. x = a} = {a}"
1.1312 + by blast
1.1313 +
1.1314 +lemma singleton_conv2 [simp]: "{x. a = x} = {a}"
1.1315 + by blast
1.1316 +
1.1317 +lemma diff_single_insert: "A - {x} \<subseteq> B ==> x \<in> A ==> A \<subseteq> insert x B"
1.1318 + by blast
1.1319 +
1.1320 +lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)"
1.1321 + by (blast elim: equalityE)
1.1322 +
1.1323 +
1.1324 +subsubsection {* Unions of families *}
1.1325 +
1.1326 +text {*
1.1327 + @{term [source] "UN x:A. B x"} is @{term "Union (B`A)"}.
1.1328 +*}
1.1329 +
1.1330 +declare UNION_def [noatp]
1.1331 +
1.1332 +lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
1.1333 + by (unfold UNION_def) blast
1.1334 +
1.1335 +lemma UN_I [intro]: "a:A ==> b: B a ==> b: (UN x:A. B x)"
1.1336 + -- {* The order of the premises presupposes that @{term A} is rigid;
1.1337 + @{term b} may be flexible. *}
1.1338 + by auto
1.1339 +
1.1340 +lemma UN_E [elim!]: "b : (UN x:A. B x) ==> (!!x. x:A ==> b: B x ==> R) ==> R"
1.1341 + by (unfold UNION_def) blast
1.1342 +
1.1343 +lemma UN_cong [cong]:
1.1344 + "A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"
1.1345 + by (simp add: UNION_def)
1.1346 +
1.1347 +lemma strong_UN_cong:
1.1348 + "A = B ==> (!!x. x:B =simp=> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"
1.1349 + by (simp add: UNION_def simp_implies_def)
1.1350 +
1.1351 +
1.1352 +subsubsection {* Intersections of families *}
1.1353 +
1.1354 +text {* @{term [source] "INT x:A. B x"} is @{term "Inter (B`A)"}. *}
1.1355 +
1.1356 +lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
1.1357 + by (unfold INTER_def) blast
1.1358 +
1.1359 +lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)"
1.1360 + by (unfold INTER_def) blast
1.1361 +
1.1362 +lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"
1.1363 + by auto
1.1364 +
1.1365 +lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R"
1.1366 + -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *}
1.1367 + by (unfold INTER_def) blast
1.1368 +
1.1369 +lemma INT_cong [cong]:
1.1370 + "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)"
1.1371 + by (simp add: INTER_def)
1.1372 +
1.1373 +
1.1374 +subsubsection {* Union *}
1.1375 +
1.1376 +lemma Union_iff [simp,noatp]: "(A : Union C) = (EX X:C. A:X)"
1.1377 + by (unfold Union_def) blast
1.1378 +
1.1379 +lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C"
1.1380 + -- {* The order of the premises presupposes that @{term C} is rigid;
1.1381 + @{term A} may be flexible. *}
1.1382 + by auto
1.1383 +
1.1384 +lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R"
1.1385 + by (unfold Union_def) blast
1.1386 +
1.1387 +
1.1388 +subsubsection {* Inter *}
1.1389 +
1.1390 +lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
1.1391 + by (unfold Inter_def) blast
1.1392 +
1.1393 +lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
1.1394 + by (simp add: Inter_def)
1.1395 +
1.1396 +text {*
1.1397 + \medskip A ``destruct'' rule -- every @{term X} in @{term C}
1.1398 + contains @{term A} as an element, but @{prop "A:X"} can hold when
1.1399 + @{prop "X:C"} does not! This rule is analogous to @{text spec}.
1.1400 +*}
1.1401 +
1.1402 +lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
1.1403 + by auto
1.1404 +
1.1405 +lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
1.1406 + -- {* ``Classical'' elimination rule -- does not require proving
1.1407 + @{prop "X:C"}. *}
1.1408 + by (unfold Inter_def) blast
1.1409 +
1.1410 +text {*
1.1411 + \medskip Image of a set under a function. Frequently @{term b} does
1.1412 + not have the syntactic form of @{term "f x"}.
1.1413 +*}
1.1414 +
1.1415 +declare image_def [noatp]
1.1416
1.1417 lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A"
1.1418 by (unfold image_def) blast
1.1419 @@ -995,6 +1003,9 @@
1.1420 lemma image_Un: "f`(A Un B) = f`A Un f`B"
1.1421 by blast
1.1422
1.1423 +lemma image_eq_UN: "f`A = (UN x:A. {f x})"
1.1424 + by blast
1.1425 +
1.1426 lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
1.1427 by blast
1.1428
1.1429 @@ -1013,44 +1024,21 @@
1.1430 @{text hypsubst}, but breaks too many existing proofs. *}
1.1431 by blast
1.1432
1.1433 -lemma image_empty [simp]: "f`{} = {}"
1.1434 +text {*
1.1435 + \medskip Range of a function -- just a translation for image!
1.1436 +*}
1.1437 +
1.1438 +lemma range_eqI: "b = f x ==> b \<in> range f"
1.1439 + by simp
1.1440 +
1.1441 +lemma rangeI: "f x \<in> range f"
1.1442 + by simp
1.1443 +
1.1444 +lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P"
1.1445 by blast
1.1446
1.1447 -lemma image_insert [simp]: "f ` insert a B = insert (f a) (f`B)"
1.1448 - by blast
1.1449 -
1.1450 -lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
1.1451 - by auto
1.1452 -
1.1453 -lemma image_constant_conv: "(%x. c) ` A = (if A = {} then {} else {c})"
1.1454 -by auto
1.1455 -
1.1456 -lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
1.1457 - by blast
1.1458 -
1.1459 -lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
1.1460 - by blast
1.1461 -
1.1462 -lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
1.1463 - by blast
1.1464 -
1.1465 -
1.1466 -lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"
1.1467 - -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
1.1468 - with its implicit quantifier and conjunction. Also image enjoys better
1.1469 - equational properties than does the RHS. *}
1.1470 - by blast
1.1471 -
1.1472 -lemma if_image_distrib [simp]:
1.1473 - "(\<lambda>x. if P x then f x else g x) ` S
1.1474 - = (f ` (S \<inter> {x. P x})) \<union> (g ` (S \<inter> {x. \<not> P x}))"
1.1475 - by (auto simp add: image_def)
1.1476 -
1.1477 -lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> f`M = g`N"
1.1478 - by (simp add: image_def)
1.1479 -
1.1480 -
1.1481 -subsection {* Set reasoning tools *}
1.1482 +
1.1483 +subsubsection {* Set reasoning tools *}
1.1484
1.1485 text {*
1.1486 Rewrite rules for boolean case-splitting: faster than @{text
1.1487 @@ -1076,6 +1064,11 @@
1.1488
1.1489 lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
1.1490
1.1491 +lemmas mem_simps =
1.1492 + insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
1.1493 + mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
1.1494 + -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
1.1495 +
1.1496 (*Would like to add these, but the existing code only searches for the
1.1497 outer-level constant, which in this case is just "op :"; we instead need
1.1498 to use term-nets to associate patterns with rules. Also, if a rule fails to
1.1499 @@ -1092,371 +1085,67 @@
1.1500 Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
1.1501 *}
1.1502
1.1503 -text {* Transitivity rules for calculational reasoning *}
1.1504 -
1.1505 -lemma set_rev_mp: "x:A ==> A \<subseteq> B ==> x:B"
1.1506 - by (rule subsetD)
1.1507 -
1.1508 -lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
1.1509 - by (rule subsetD)
1.1510 -
1.1511 -lemmas basic_trans_rules [trans] =
1.1512 - order_trans_rules set_rev_mp set_mp
1.1513 -
1.1514 -
1.1515 -subsection {* Complete lattices *}
1.1516 -
1.1517 -notation
1.1518 - less_eq (infix "\<sqsubseteq>" 50) and
1.1519 - less (infix "\<sqsubset>" 50) and
1.1520 - inf (infixl "\<sqinter>" 70) and
1.1521 - sup (infixl "\<squnion>" 65)
1.1522 -
1.1523 -class complete_lattice = lattice + bot + top +
1.1524 - fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
1.1525 - and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
1.1526 - assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
1.1527 - and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
1.1528 - assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
1.1529 - and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
1.1530 -begin
1.1531 -
1.1532 -lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
1.1533 - by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
1.1534 -
1.1535 -lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
1.1536 - by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
1.1537 -
1.1538 -lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
1.1539 - unfolding Sup_Inf by auto
1.1540 -
1.1541 -lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
1.1542 - unfolding Inf_Sup by auto
1.1543 -
1.1544 -lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
1.1545 - by (auto intro: antisym Inf_greatest Inf_lower)
1.1546 -
1.1547 -lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
1.1548 - by (auto intro: antisym Sup_least Sup_upper)
1.1549 -
1.1550 -lemma Inf_singleton [simp]:
1.1551 - "\<Sqinter>{a} = a"
1.1552 - by (auto intro: antisym Inf_lower Inf_greatest)
1.1553 -
1.1554 -lemma Sup_singleton [simp]:
1.1555 - "\<Squnion>{a} = a"
1.1556 - by (auto intro: antisym Sup_upper Sup_least)
1.1557 -
1.1558 -lemma Inf_insert_simp:
1.1559 - "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)"
1.1560 - by (cases "A = {}") (simp_all, simp add: Inf_insert)
1.1561 -
1.1562 -lemma Sup_insert_simp:
1.1563 - "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)"
1.1564 - by (cases "A = {}") (simp_all, simp add: Sup_insert)
1.1565 -
1.1566 -lemma Inf_binary:
1.1567 - "\<Sqinter>{a, b} = a \<sqinter> b"
1.1568 - by (simp add: Inf_insert_simp)
1.1569 -
1.1570 -lemma Sup_binary:
1.1571 - "\<Squnion>{a, b} = a \<squnion> b"
1.1572 - by (simp add: Sup_insert_simp)
1.1573 -
1.1574 -lemma bot_def:
1.1575 - "bot = \<Squnion>{}"
1.1576 - by (auto intro: antisym Sup_least)
1.1577 -
1.1578 -lemma top_def:
1.1579 - "top = \<Sqinter>{}"
1.1580 - by (auto intro: antisym Inf_greatest)
1.1581 -
1.1582 -lemma sup_bot [simp]:
1.1583 - "x \<squnion> bot = x"
1.1584 - using bot_least [of x] by (simp add: le_iff_sup sup_commute)
1.1585 -
1.1586 -lemma inf_top [simp]:
1.1587 - "x \<sqinter> top = x"
1.1588 - using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
1.1589 -
1.1590 -definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.1591 - "SUPR A f == \<Squnion> (f ` A)"
1.1592 -
1.1593 -definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.1594 - "INFI A f == \<Sqinter> (f ` A)"
1.1595 -
1.1596 -end
1.1597 -
1.1598 -syntax
1.1599 - "_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" [0, 10] 10)
1.1600 - "_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" [0, 10] 10)
1.1601 - "_INF1" :: "pttrns => 'b => 'b" ("(3INF _./ _)" [0, 10] 10)
1.1602 - "_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" [0, 10] 10)
1.1603 -
1.1604 -translations
1.1605 - "SUP x y. B" == "SUP x. SUP y. B"
1.1606 - "SUP x. B" == "CONST SUPR CONST UNIV (%x. B)"
1.1607 - "SUP x. B" == "SUP x:CONST UNIV. B"
1.1608 - "SUP x:A. B" == "CONST SUPR A (%x. B)"
1.1609 - "INF x y. B" == "INF x. INF y. B"
1.1610 - "INF x. B" == "CONST INFI CONST UNIV (%x. B)"
1.1611 - "INF x. B" == "INF x:CONST UNIV. B"
1.1612 - "INF x:A. B" == "CONST INFI A (%x. B)"
1.1613 -
1.1614 -(* To avoid eta-contraction of body: *)
1.1615 -print_translation {*
1.1616 -let
1.1617 - fun btr' syn (A :: Abs abs :: ts) =
1.1618 - let val (x,t) = atomic_abs_tr' abs
1.1619 - in list_comb (Syntax.const syn $ x $ A $ t, ts) end
1.1620 - val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const
1.1621 -in
1.1622 -[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")]
1.1623 -end
1.1624 -*}
1.1625 -
1.1626 -context complete_lattice
1.1627 -begin
1.1628 -
1.1629 -lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
1.1630 - by (auto simp add: SUPR_def intro: Sup_upper)
1.1631 -
1.1632 -lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
1.1633 - by (auto simp add: SUPR_def intro: Sup_least)
1.1634 -
1.1635 -lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
1.1636 - by (auto simp add: INFI_def intro: Inf_lower)
1.1637 -
1.1638 -lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
1.1639 - by (auto simp add: INFI_def intro: Inf_greatest)
1.1640 -
1.1641 -lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
1.1642 - by (auto intro: antisym SUP_leI le_SUPI)
1.1643 -
1.1644 -lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
1.1645 - by (auto intro: antisym INF_leI le_INFI)
1.1646 -
1.1647 -end
1.1648 -
1.1649 -subsubsection {* Bool as complete lattice *}
1.1650 -
1.1651 -instantiation bool :: complete_lattice
1.1652 -begin
1.1653 -
1.1654 -definition
1.1655 - Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
1.1656 -
1.1657 -definition
1.1658 - Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
1.1659 -
1.1660 -instance
1.1661 - by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
1.1662 -
1.1663 -end
1.1664 -
1.1665 -lemma Inf_empty_bool [simp]:
1.1666 - "\<Sqinter>{}"
1.1667 - unfolding Inf_bool_def by auto
1.1668 -
1.1669 -lemma not_Sup_empty_bool [simp]:
1.1670 - "\<not> Sup {}"
1.1671 - unfolding Sup_bool_def by auto
1.1672 -
1.1673 -
1.1674 -subsubsection {* Fun as complete lattice *}
1.1675 -
1.1676 -instantiation "fun" :: (type, complete_lattice) complete_lattice
1.1677 -begin
1.1678 -
1.1679 -definition
1.1680 - Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
1.1681 -
1.1682 -definition
1.1683 - Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
1.1684 -
1.1685 -instance
1.1686 - by intro_classes
1.1687 - (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
1.1688 - intro: Inf_lower Sup_upper Inf_greatest Sup_least)
1.1689 -
1.1690 -end
1.1691 -
1.1692 -lemma Inf_empty_fun:
1.1693 - "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
1.1694 - by rule (auto simp add: Inf_fun_def)
1.1695 -
1.1696 -lemma Sup_empty_fun:
1.1697 - "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
1.1698 - by rule (auto simp add: Sup_fun_def)
1.1699 -
1.1700 -no_notation
1.1701 - less_eq (infix "\<sqsubseteq>" 50) and
1.1702 - less (infix "\<sqsubset>" 50) and
1.1703 - inf (infixl "\<sqinter>" 70) and
1.1704 - sup (infixl "\<squnion>" 65) and
1.1705 - Inf ("\<Sqinter>_" [900] 900) and
1.1706 - Sup ("\<Squnion>_" [900] 900)
1.1707 -
1.1708 -
1.1709 -subsection {* Further operations *}
1.1710 -
1.1711 -subsubsection {* Big families as specialisation of lattice operations *}
1.1712 -
1.1713 -definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
1.1714 - "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
1.1715 -
1.1716 -definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
1.1717 - "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
1.1718 -
1.1719 -definition Inter :: "'a set set \<Rightarrow> 'a set" where
1.1720 - "Inter S \<equiv> INTER S (\<lambda>x. x)"
1.1721 -
1.1722 -definition Union :: "'a set set \<Rightarrow> 'a set" where
1.1723 - "Union S \<equiv> UNION S (\<lambda>x. x)"
1.1724 -
1.1725 -notation (xsymbols)
1.1726 - Inter ("\<Inter>_" [90] 90) and
1.1727 - Union ("\<Union>_" [90] 90)
1.1728 -
1.1729 -syntax
1.1730 - "@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)
1.1731 - "@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10)
1.1732 - "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 10] 10)
1.1733 - "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 10] 10)
1.1734 -
1.1735 -syntax (xsymbols)
1.1736 - "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" [0, 10] 10)
1.1737 - "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" [0, 10] 10)
1.1738 - "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
1.1739 - "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
1.1740 -
1.1741 -syntax (latex output)
1.1742 - "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
1.1743 - "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
1.1744 - "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
1.1745 - "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
1.1746 -
1.1747 -translations
1.1748 - "INT x y. B" == "INT x. INT y. B"
1.1749 - "INT x. B" == "CONST INTER CONST UNIV (%x. B)"
1.1750 - "INT x. B" == "INT x:CONST UNIV. B"
1.1751 - "INT x:A. B" == "CONST INTER A (%x. B)"
1.1752 - "UN x y. B" == "UN x. UN y. B"
1.1753 - "UN x. B" == "CONST UNION CONST UNIV (%x. B)"
1.1754 - "UN x. B" == "UN x:CONST UNIV. B"
1.1755 - "UN x:A. B" == "CONST UNION A (%x. B)"
1.1756 -
1.1757 -text {*
1.1758 - Note the difference between ordinary xsymbol syntax of indexed
1.1759 - unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
1.1760 - and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
1.1761 - former does not make the index expression a subscript of the
1.1762 - union/intersection symbol because this leads to problems with nested
1.1763 - subscripts in Proof General.
1.1764 -*}
1.1765 -
1.1766 -(* To avoid eta-contraction of body: *)
1.1767 -(*FIXME integrate with / factor out from similar situations*)
1.1768 -print_translation {*
1.1769 -let
1.1770 - fun btr' syn [A, Abs abs] =
1.1771 - let val (x, t) = atomic_abs_tr' abs
1.1772 - in Syntax.const syn $ x $ A $ t end
1.1773 -in
1.1774 -[(@{const_syntax Ball}, btr' "_Ball"), (@{const_syntax Bex}, btr' "_Bex"),
1.1775 - (@{const_syntax UNION}, btr' "@UNION"),(@{const_syntax INTER}, btr' "@INTER")]
1.1776 -end
1.1777 -*}
1.1778 -
1.1779 -subsubsection {* Unions of families *}
1.1780 -
1.1781 -text {*
1.1782 - @{term [source] "UN x:A. B x"} is @{term "Union (B`A)"}.
1.1783 -*}
1.1784 -
1.1785 -declare UNION_def [noatp]
1.1786 -
1.1787 -lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
1.1788 - by (unfold UNION_def) blast
1.1789 -
1.1790 -lemma UN_I [intro]: "a:A ==> b: B a ==> b: (UN x:A. B x)"
1.1791 - -- {* The order of the premises presupposes that @{term A} is rigid;
1.1792 - @{term b} may be flexible. *}
1.1793 - by auto
1.1794 -
1.1795 -lemma UN_E [elim!]: "b : (UN x:A. B x) ==> (!!x. x:A ==> b: B x ==> R) ==> R"
1.1796 - by (unfold UNION_def) blast
1.1797 -
1.1798 -lemma UN_cong [cong]:
1.1799 - "A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"
1.1800 - by (simp add: UNION_def)
1.1801 -
1.1802 -lemma strong_UN_cong:
1.1803 - "A = B ==> (!!x. x:B =simp=> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"
1.1804 - by (simp add: UNION_def simp_implies_def)
1.1805 -
1.1806 -lemma image_eq_UN: "f`A = (UN x:A. {f x})"
1.1807 +
1.1808 +subsubsection {* The ``proper subset'' relation *}
1.1809 +
1.1810 +lemma psubsetI [intro!,noatp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
1.1811 + by (unfold less_le) blast
1.1812 +
1.1813 +lemma psubsetE [elim!,noatp]:
1.1814 + "[|A \<subset> B; [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
1.1815 + by (unfold less_le) blast
1.1816 +
1.1817 +lemma psubset_insert_iff:
1.1818 + "(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.1819 + by (auto simp add: less_le subset_insert_iff)
1.1820 +
1.1821 +lemma psubset_eq: "(A \<subset> B) = (A \<subseteq> B & A \<noteq> B)"
1.1822 + by (simp only: less_le)
1.1823 +
1.1824 +lemma psubset_imp_subset: "A \<subset> B ==> A \<subseteq> B"
1.1825 + by (simp add: psubset_eq)
1.1826 +
1.1827 +lemma psubset_trans: "[| A \<subset> B; B \<subset> C |] ==> A \<subset> C"
1.1828 +apply (unfold less_le)
1.1829 +apply (auto dest: subset_antisym)
1.1830 +done
1.1831 +
1.1832 +lemma psubsetD: "[| A \<subset> B; c \<in> A |] ==> c \<in> B"
1.1833 +apply (unfold less_le)
1.1834 +apply (auto dest: subsetD)
1.1835 +done
1.1836 +
1.1837 +lemma psubset_subset_trans: "A \<subset> B ==> B \<subseteq> C ==> A \<subset> C"
1.1838 + by (auto simp add: psubset_eq)
1.1839 +
1.1840 +lemma subset_psubset_trans: "A \<subseteq> B ==> B \<subset> C ==> A \<subset> C"
1.1841 + by (auto simp add: psubset_eq)
1.1842 +
1.1843 +lemma psubset_imp_ex_mem: "A \<subset> B ==> \<exists>b. b \<in> (B - A)"
1.1844 + by (unfold less_le) blast
1.1845 +
1.1846 +lemma atomize_ball:
1.1847 + "(!!x. x \<in> A ==> P x) == Trueprop (\<forall>x\<in>A. P x)"
1.1848 + by (simp only: Ball_def atomize_all atomize_imp)
1.1849 +
1.1850 +lemmas [symmetric, rulify] = atomize_ball
1.1851 + and [symmetric, defn] = atomize_ball
1.1852 +
1.1853 +
1.1854 +subsection {* Further set-theory lemmas *}
1.1855 +
1.1856 +subsubsection {* Derived rules involving subsets. *}
1.1857 +
1.1858 +text {* @{text insert}. *}
1.1859 +
1.1860 +lemma subset_insertI: "B \<subseteq> insert a B"
1.1861 + by (rule subsetI) (erule insertI2)
1.1862 +
1.1863 +lemma subset_insertI2: "A \<subseteq> B \<Longrightarrow> A \<subseteq> insert b B"
1.1864 by blast
1.1865
1.1866 -
1.1867 -subsubsection {* Intersections of families *}
1.1868 -
1.1869 -text {* @{term [source] "INT x:A. B x"} is @{term "Inter (B`A)"}. *}
1.1870 -
1.1871 -lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
1.1872 - by (unfold INTER_def) blast
1.1873 -
1.1874 -lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)"
1.1875 - by (unfold INTER_def) blast
1.1876 -
1.1877 -lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"
1.1878 - by auto
1.1879 -
1.1880 -lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R"
1.1881 - -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *}
1.1882 - by (unfold INTER_def) blast
1.1883 -
1.1884 -lemma INT_cong [cong]:
1.1885 - "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)"
1.1886 - by (simp add: INTER_def)
1.1887 -
1.1888 -
1.1889 -subsubsection {* Union *}
1.1890 -
1.1891 -lemma Union_iff [simp,noatp]: "(A : Union C) = (EX X:C. A:X)"
1.1892 - by (unfold Union_def) blast
1.1893 -
1.1894 -lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C"
1.1895 - -- {* The order of the premises presupposes that @{term C} is rigid;
1.1896 - @{term A} may be flexible. *}
1.1897 - by auto
1.1898 -
1.1899 -lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R"
1.1900 - by (unfold Union_def) blast
1.1901 -
1.1902 -
1.1903 -subsubsection {* Inter *}
1.1904 -
1.1905 -lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
1.1906 - by (unfold Inter_def) blast
1.1907 -
1.1908 -lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
1.1909 - by (simp add: Inter_def)
1.1910 -
1.1911 -text {*
1.1912 - \medskip A ``destruct'' rule -- every @{term X} in @{term C}
1.1913 - contains @{term A} as an element, but @{prop "A:X"} can hold when
1.1914 - @{prop "X:C"} does not! This rule is analogous to @{text spec}.
1.1915 -*}
1.1916 -
1.1917 -lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
1.1918 - by auto
1.1919 -
1.1920 -lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
1.1921 - -- {* ``Classical'' elimination rule -- does not require proving
1.1922 - @{prop "X:C"}. *}
1.1923 - by (unfold Inter_def) blast
1.1924 -
1.1925 +lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)"
1.1926 + by blast
1.1927
1.1928
1.1929 text {* \medskip Big Union -- least upper bound of a set. *}
1.1930 @@ -1467,14 +1156,6 @@
1.1931 lemma Union_least: "(!!X. X \<in> A ==> X \<subseteq> C) ==> Union A \<subseteq> C"
1.1932 by (iprover intro: subsetI elim: UnionE dest: subsetD)
1.1933
1.1934 -lemma Sup_set_eq: "Sup S = \<Union>S"
1.1935 - apply (rule subset_antisym)
1.1936 - apply (rule Sup_least)
1.1937 - apply (erule Union_upper)
1.1938 - apply (rule Union_least)
1.1939 - apply (erule Sup_upper)
1.1940 - done
1.1941 -
1.1942
1.1943 text {* \medskip General union. *}
1.1944
1.1945 @@ -1497,89 +1178,182 @@
1.1946 lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
1.1947 by (iprover intro: InterI subsetI dest: subsetD)
1.1948
1.1949 -lemma Inf_set_eq: "Inf S = \<Inter>S"
1.1950 - apply (rule subset_antisym)
1.1951 - apply (rule Inter_greatest)
1.1952 - apply (erule Inf_lower)
1.1953 - apply (rule Inf_greatest)
1.1954 - apply (erule Inter_lower)
1.1955 - done
1.1956 -
1.1957 lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
1.1958 by blast
1.1959
1.1960 lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
1.1961 by (iprover intro: INT_I subsetI dest: subsetD)
1.1962
1.1963 +
1.1964 +text {* \medskip Finite Union -- the least upper bound of two sets. *}
1.1965 +
1.1966 +lemma Un_upper1: "A \<subseteq> A \<union> B"
1.1967 + by blast
1.1968 +
1.1969 +lemma Un_upper2: "B \<subseteq> A \<union> B"
1.1970 + by blast
1.1971 +
1.1972 +lemma Un_least: "A \<subseteq> C ==> B \<subseteq> C ==> A \<union> B \<subseteq> C"
1.1973 + by blast
1.1974 +
1.1975 +
1.1976 +text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *}
1.1977 +
1.1978 +lemma Int_lower1: "A \<inter> B \<subseteq> A"
1.1979 + by blast
1.1980 +
1.1981 +lemma Int_lower2: "A \<inter> B \<subseteq> B"
1.1982 + by blast
1.1983 +
1.1984 +lemma Int_greatest: "C \<subseteq> A ==> C \<subseteq> B ==> C \<subseteq> A \<inter> B"
1.1985 + by blast
1.1986 +
1.1987 +
1.1988 +text {* \medskip Set difference. *}
1.1989 +
1.1990 +lemma Diff_subset: "A - B \<subseteq> A"
1.1991 + by blast
1.1992 +
1.1993 +lemma Diff_subset_conv: "(A - B \<subseteq> C) = (A \<subseteq> B \<union> C)"
1.1994 +by blast
1.1995 +
1.1996 +
1.1997 +subsubsection {* Equalities involving union, intersection, inclusion, etc. *}
1.1998 +
1.1999 +text {* @{text "{}"}. *}
1.2000 +
1.2001 +lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"
1.2002 + -- {* supersedes @{text "Collect_False_empty"} *}
1.2003 + by auto
1.2004 +
1.2005 +lemma subset_empty [simp]: "(A \<subseteq> {}) = (A = {})"
1.2006 + by blast
1.2007 +
1.2008 +lemma not_psubset_empty [iff]: "\<not> (A < {})"
1.2009 + by (unfold less_le) blast
1.2010 +
1.2011 +lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\<forall>x. \<not> P x)"
1.2012 +by blast
1.2013 +
1.2014 +lemma empty_Collect_eq [simp]: "({} = Collect P) = (\<forall>x. \<not> P x)"
1.2015 +by blast
1.2016 +
1.2017 +lemma Collect_neg_eq: "{x. \<not> P x} = - {x. P x}"
1.2018 + by blast
1.2019 +
1.2020 +lemma Collect_disj_eq: "{x. P x | Q x} = {x. P x} \<union> {x. Q x}"
1.2021 + by blast
1.2022 +
1.2023 +lemma Collect_imp_eq: "{x. P x --> Q x} = -{x. P x} \<union> {x. Q x}"
1.2024 + by blast
1.2025 +
1.2026 +lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"
1.2027 + by blast
1.2028 +
1.2029 +lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})"
1.2030 + by blast
1.2031 +
1.2032 +lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
1.2033 + by blast
1.2034 +
1.2035 +lemma Collect_ex_eq [noatp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
1.2036 + by blast
1.2037 +
1.2038 +lemma Collect_bex_eq [noatp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
1.2039 + by blast
1.2040 +
1.2041 +
1.2042 +text {* \medskip @{text insert}. *}
1.2043 +
1.2044 +lemma insert_is_Un: "insert a A = {a} Un A"
1.2045 + -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"} *}
1.2046 + by blast
1.2047 +
1.2048 +lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
1.2049 + by blast
1.2050 +
1.2051 +lemmas empty_not_insert = insert_not_empty [symmetric, standard]
1.2052 +declare empty_not_insert [simp]
1.2053 +
1.2054 +lemma insert_absorb: "a \<in> A ==> insert a A = A"
1.2055 + -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}
1.2056 + -- {* with \emph{quadratic} running time *}
1.2057 + by blast
1.2058 +
1.2059 +lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"
1.2060 + by blast
1.2061 +
1.2062 +lemma insert_commute: "insert x (insert y A) = insert y (insert x A)"
1.2063 + by blast
1.2064 +
1.2065 +lemma insert_subset [simp]: "(insert x A \<subseteq> B) = (x \<in> B & A \<subseteq> B)"
1.2066 + by blast
1.2067 +
1.2068 +lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B"
1.2069 + -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *}
1.2070 + apply (rule_tac x = "A - {a}" in exI, blast)
1.2071 + done
1.2072 +
1.2073 +lemma insert_Collect: "insert a (Collect P) = {u. u \<noteq> a --> P u}"
1.2074 + by auto
1.2075 +
1.2076 lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
1.2077 by blast
1.2078
1.2079 -lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})"
1.2080 +lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
1.2081 by blast
1.2082
1.2083 -lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
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 Collect_ex_eq [noatp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
1.2100 +lemma image_insert [simp]: "f ` insert a B = insert (f a) (f`B)"
1.2101 by blast
1.2102
1.2103 -lemma Collect_bex_eq [noatp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
1.2104 +lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
1.2105 + by auto
1.2106 +
1.2107 +lemma image_constant_conv: "(%x. c) ` A = (if A = {} then {} else {c})"
1.2108 +by auto
1.2109 +
1.2110 +lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
1.2111 by blast
1.2112
1.2113 -
1.2114 -subsubsection {* The Powerset operator -- Pow *}
1.2115 -
1.2116 -global
1.2117 -
1.2118 -consts
1.2119 - Pow :: "'a set => 'a set set"
1.2120 -
1.2121 -local
1.2122 -
1.2123 -defs
1.2124 - Pow_def: "Pow A == {B. B <= A}"
1.2125 -
1.2126 -lemma Pow_iff [iff]: "(A \<in> Pow B) = (A \<subseteq> B)"
1.2127 - by (simp add: Pow_def)
1.2128 -
1.2129 -lemma PowI: "A \<subseteq> B ==> A \<in> Pow B"
1.2130 - by (simp add: Pow_def)
1.2131 -
1.2132 -lemma PowD: "A \<in> Pow B ==> A \<subseteq> B"
1.2133 - by (simp add: Pow_def)
1.2134 -
1.2135 -lemma Pow_bottom: "{} \<in> Pow B"
1.2136 - by simp
1.2137 -
1.2138 -lemma Pow_top: "A \<in> Pow A"
1.2139 - by (simp add: subset_refl)
1.2140 -
1.2141 -
1.2142 -
1.2143 -subsubsection {* Getting the Contents of a Singleton Set *}
1.2144 -
1.2145 -definition contents :: "'a set \<Rightarrow> 'a" where
1.2146 - [code del]: "contents X = (THE x. X = {x})"
1.2147 -
1.2148 -lemma contents_eq [simp]: "contents {x} = x"
1.2149 - by (simp add: contents_def)
1.2150 -
1.2151 -
1.2152 -subsubsection {* Range of a function -- just a translation for image! *}
1.2153 -
1.2154 -abbreviation
1.2155 - range :: "('a => 'b) => 'b set" where -- "of function"
1.2156 - "range f == f ` UNIV"
1.2157 -
1.2158 -lemma range_eqI: "b = f x ==> b \<in> range f"
1.2159 - by simp
1.2160 -
1.2161 -lemma rangeI: "f x \<in> range f"
1.2162 - by simp
1.2163 -
1.2164 -lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P"
1.2165 +lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
1.2166 by blast
1.2167
1.2168 +lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
1.2169 + by blast
1.2170 +
1.2171 +
1.2172 +lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"
1.2173 + -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
1.2174 + with its implicit quantifier and conjunction. Also image enjoys better
1.2175 + equational properties than does the RHS. *}
1.2176 + by blast
1.2177 +
1.2178 +lemma if_image_distrib [simp]:
1.2179 + "(\<lambda>x. if P x then f x else g x) ` S
1.2180 + = (f ` (S \<inter> {x. P x})) \<union> (g ` (S \<inter> {x. \<not> P x}))"
1.2181 + by (auto simp add: image_def)
1.2182 +
1.2183 +lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> f`M = g`N"
1.2184 + by (simp add: image_def)
1.2185 +
1.2186 +
1.2187 +text {* \medskip @{text range}. *}
1.2188 +
1.2189 lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
1.2190 by auto
1.2191
1.2192 @@ -1587,8 +1361,6 @@
1.2193 by (subst image_image, simp)
1.2194
1.2195
1.2196 -subsection {* Further rules and properties *}
1.2197 -
1.2198 text {* \medskip @{text Int} *}
1.2199
1.2200 lemma Int_absorb [simp]: "A \<inter> A = A"
1.2201 @@ -2276,16 +2048,6 @@
1.2202 lemma Compl_anti_mono: "A \<subseteq> B ==> -B \<subseteq> -A"
1.2203 by blast
1.2204
1.2205 -lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
1.2206 - apply (fold inf_set_eq sup_set_eq)
1.2207 - apply (erule mono_inf)
1.2208 - done
1.2209 -
1.2210 -lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
1.2211 - apply (fold inf_set_eq sup_set_eq)
1.2212 - apply (erule mono_sup)
1.2213 - done
1.2214 -
1.2215 text {* \medskip Monotonicity of implications. *}
1.2216
1.2217 lemma in_mono: "A \<subseteq> B ==> x \<in> A --> x \<in> B"
1.2218 @@ -2328,12 +2090,15 @@
1.2219 by iprover
1.2220
1.2221
1.2222 -subsubsection {* Inverse image of a function *}
1.2223 +subsection {* Inverse image of a function *}
1.2224
1.2225 constdefs
1.2226 vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-`" 90)
1.2227 [code del]: "f -` B == {x. f x : B}"
1.2228
1.2229 +
1.2230 +subsubsection {* Basic rules *}
1.2231 +
1.2232 lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
1.2233 by (unfold vimage_def) blast
1.2234
1.2235 @@ -2352,6 +2117,9 @@
1.2236 lemma vimageD: "a : f -` A ==> f a : A"
1.2237 by (unfold vimage_def) fast
1.2238
1.2239 +
1.2240 +subsubsection {* Equations *}
1.2241 +
1.2242 lemma vimage_empty [simp]: "f -` {} = {}"
1.2243 by blast
1.2244
1.2245 @@ -2416,7 +2184,28 @@
1.2246 by blast
1.2247
1.2248
1.2249 -subsubsection {* Least value operator *}
1.2250 +subsection {* Getting the Contents of a Singleton Set *}
1.2251 +
1.2252 +definition contents :: "'a set \<Rightarrow> 'a" where
1.2253 + [code del]: "contents X = (THE x. X = {x})"
1.2254 +
1.2255 +lemma contents_eq [simp]: "contents {x} = x"
1.2256 + by (simp add: contents_def)
1.2257 +
1.2258 +
1.2259 +subsection {* Transitivity rules for calculational reasoning *}
1.2260 +
1.2261 +lemma set_rev_mp: "x:A ==> A \<subseteq> B ==> x:B"
1.2262 + by (rule subsetD)
1.2263 +
1.2264 +lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
1.2265 + by (rule subsetD)
1.2266 +
1.2267 +lemmas basic_trans_rules [trans] =
1.2268 + order_trans_rules set_rev_mp set_mp
1.2269 +
1.2270 +
1.2271 +subsection {* Least value operator *}
1.2272
1.2273 lemma Least_mono:
1.2274 "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
1.2275 @@ -2429,7 +2218,7 @@
1.2276 done
1.2277
1.2278
1.2279 -subsubsection {* Rudimentary code generation *}
1.2280 +subsection {* Rudimentary code generation *}
1.2281
1.2282 lemma empty_code [code]: "{} x \<longleftrightarrow> False"
1.2283 unfolding empty_def Collect_def ..
1.2284 @@ -2450,13 +2239,257 @@
1.2285 unfolding vimage_def Collect_def mem_def ..
1.2286
1.2287
1.2288 -subsection {* Misc theorem and ML bindings *}
1.2289 -
1.2290 -lemmas equalityI = subset_antisym
1.2291 -lemmas mem_simps =
1.2292 - insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
1.2293 - mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
1.2294 - -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
1.2295 +subsection {* Complete lattices *}
1.2296 +
1.2297 +notation
1.2298 + less_eq (infix "\<sqsubseteq>" 50) and
1.2299 + less (infix "\<sqsubset>" 50) and
1.2300 + inf (infixl "\<sqinter>" 70) and
1.2301 + sup (infixl "\<squnion>" 65)
1.2302 +
1.2303 +class complete_lattice = lattice + bot + top +
1.2304 + fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
1.2305 + and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
1.2306 + assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
1.2307 + and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
1.2308 + assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
1.2309 + and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
1.2310 +begin
1.2311 +
1.2312 +lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
1.2313 + by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
1.2314 +
1.2315 +lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
1.2316 + by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
1.2317 +
1.2318 +lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
1.2319 + unfolding Sup_Inf by auto
1.2320 +
1.2321 +lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
1.2322 + unfolding Inf_Sup by auto
1.2323 +
1.2324 +lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
1.2325 + by (auto intro: antisym Inf_greatest Inf_lower)
1.2326 +
1.2327 +lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
1.2328 + by (auto intro: antisym Sup_least Sup_upper)
1.2329 +
1.2330 +lemma Inf_singleton [simp]:
1.2331 + "\<Sqinter>{a} = a"
1.2332 + by (auto intro: antisym Inf_lower Inf_greatest)
1.2333 +
1.2334 +lemma Sup_singleton [simp]:
1.2335 + "\<Squnion>{a} = a"
1.2336 + by (auto intro: antisym Sup_upper Sup_least)
1.2337 +
1.2338 +lemma Inf_insert_simp:
1.2339 + "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)"
1.2340 + by (cases "A = {}") (simp_all, simp add: Inf_insert)
1.2341 +
1.2342 +lemma Sup_insert_simp:
1.2343 + "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)"
1.2344 + by (cases "A = {}") (simp_all, simp add: Sup_insert)
1.2345 +
1.2346 +lemma Inf_binary:
1.2347 + "\<Sqinter>{a, b} = a \<sqinter> b"
1.2348 + by (simp add: Inf_insert_simp)
1.2349 +
1.2350 +lemma Sup_binary:
1.2351 + "\<Squnion>{a, b} = a \<squnion> b"
1.2352 + by (simp add: Sup_insert_simp)
1.2353 +
1.2354 +lemma bot_def:
1.2355 + "bot = \<Squnion>{}"
1.2356 + by (auto intro: antisym Sup_least)
1.2357 +
1.2358 +lemma top_def:
1.2359 + "top = \<Sqinter>{}"
1.2360 + by (auto intro: antisym Inf_greatest)
1.2361 +
1.2362 +lemma sup_bot [simp]:
1.2363 + "x \<squnion> bot = x"
1.2364 + using bot_least [of x] by (simp add: le_iff_sup sup_commute)
1.2365 +
1.2366 +lemma inf_top [simp]:
1.2367 + "x \<sqinter> top = x"
1.2368 + using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
1.2369 +
1.2370 +definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.2371 + "SUPR A f == \<Squnion> (f ` A)"
1.2372 +
1.2373 +definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.2374 + "INFI A f == \<Sqinter> (f ` A)"
1.2375 +
1.2376 +end
1.2377 +
1.2378 +syntax
1.2379 + "_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" [0, 10] 10)
1.2380 + "_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" [0, 10] 10)
1.2381 + "_INF1" :: "pttrns => 'b => 'b" ("(3INF _./ _)" [0, 10] 10)
1.2382 + "_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" [0, 10] 10)
1.2383 +
1.2384 +translations
1.2385 + "SUP x y. B" == "SUP x. SUP y. B"
1.2386 + "SUP x. B" == "CONST SUPR CONST UNIV (%x. B)"
1.2387 + "SUP x. B" == "SUP x:CONST UNIV. B"
1.2388 + "SUP x:A. B" == "CONST SUPR A (%x. B)"
1.2389 + "INF x y. B" == "INF x. INF y. B"
1.2390 + "INF x. B" == "CONST INFI CONST UNIV (%x. B)"
1.2391 + "INF x. B" == "INF x:CONST UNIV. B"
1.2392 + "INF x:A. B" == "CONST INFI A (%x. B)"
1.2393 +
1.2394 +(* To avoid eta-contraction of body: *)
1.2395 +print_translation {*
1.2396 +let
1.2397 + fun btr' syn (A :: Abs abs :: ts) =
1.2398 + let val (x,t) = atomic_abs_tr' abs
1.2399 + in list_comb (Syntax.const syn $ x $ A $ t, ts) end
1.2400 + val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const
1.2401 +in
1.2402 +[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")]
1.2403 +end
1.2404 +*}
1.2405 +
1.2406 +context complete_lattice
1.2407 +begin
1.2408 +
1.2409 +lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
1.2410 + by (auto simp add: SUPR_def intro: Sup_upper)
1.2411 +
1.2412 +lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
1.2413 + by (auto simp add: SUPR_def intro: Sup_least)
1.2414 +
1.2415 +lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
1.2416 + by (auto simp add: INFI_def intro: Inf_lower)
1.2417 +
1.2418 +lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
1.2419 + by (auto simp add: INFI_def intro: Inf_greatest)
1.2420 +
1.2421 +lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
1.2422 + by (auto intro: antisym SUP_leI le_SUPI)
1.2423 +
1.2424 +lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
1.2425 + by (auto intro: antisym INF_leI le_INFI)
1.2426 +
1.2427 +end
1.2428 +
1.2429 +
1.2430 +subsection {* Bool as complete lattice *}
1.2431 +
1.2432 +instantiation bool :: complete_lattice
1.2433 +begin
1.2434 +
1.2435 +definition
1.2436 + Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
1.2437 +
1.2438 +definition
1.2439 + Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
1.2440 +
1.2441 +instance
1.2442 + by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
1.2443 +
1.2444 +end
1.2445 +
1.2446 +lemma Inf_empty_bool [simp]:
1.2447 + "\<Sqinter>{}"
1.2448 + unfolding Inf_bool_def by auto
1.2449 +
1.2450 +lemma not_Sup_empty_bool [simp]:
1.2451 + "\<not> Sup {}"
1.2452 + unfolding Sup_bool_def by auto
1.2453 +
1.2454 +
1.2455 +subsection {* Fun as complete lattice *}
1.2456 +
1.2457 +instantiation "fun" :: (type, complete_lattice) complete_lattice
1.2458 +begin
1.2459 +
1.2460 +definition
1.2461 + Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
1.2462 +
1.2463 +definition
1.2464 + Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
1.2465 +
1.2466 +instance
1.2467 + by intro_classes
1.2468 + (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
1.2469 + intro: Inf_lower Sup_upper Inf_greatest Sup_least)
1.2470 +
1.2471 +end
1.2472 +
1.2473 +lemma Inf_empty_fun:
1.2474 + "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
1.2475 + by rule (auto simp add: Inf_fun_def)
1.2476 +
1.2477 +lemma Sup_empty_fun:
1.2478 + "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
1.2479 + by rule (auto simp add: Sup_fun_def)
1.2480 +
1.2481 +
1.2482 +subsection {* Set as lattice *}
1.2483 +
1.2484 +lemma inf_set_eq: "A \<sqinter> B = A \<inter> B"
1.2485 + apply (rule subset_antisym)
1.2486 + apply (rule Int_greatest)
1.2487 + apply (rule inf_le1)
1.2488 + apply (rule inf_le2)
1.2489 + apply (rule inf_greatest)
1.2490 + apply (rule Int_lower1)
1.2491 + apply (rule Int_lower2)
1.2492 + done
1.2493 +
1.2494 +lemma sup_set_eq: "A \<squnion> B = A \<union> B"
1.2495 + apply (rule subset_antisym)
1.2496 + apply (rule sup_least)
1.2497 + apply (rule Un_upper1)
1.2498 + apply (rule Un_upper2)
1.2499 + apply (rule Un_least)
1.2500 + apply (rule sup_ge1)
1.2501 + apply (rule sup_ge2)
1.2502 + done
1.2503 +
1.2504 +lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
1.2505 + apply (fold inf_set_eq sup_set_eq)
1.2506 + apply (erule mono_inf)
1.2507 + done
1.2508 +
1.2509 +lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
1.2510 + apply (fold inf_set_eq sup_set_eq)
1.2511 + apply (erule mono_sup)
1.2512 + done
1.2513 +
1.2514 +lemma Inf_set_eq: "\<Sqinter>S = \<Inter>S"
1.2515 + apply (rule subset_antisym)
1.2516 + apply (rule Inter_greatest)
1.2517 + apply (erule Inf_lower)
1.2518 + apply (rule Inf_greatest)
1.2519 + apply (erule Inter_lower)
1.2520 + done
1.2521 +
1.2522 +lemma Sup_set_eq: "\<Squnion>S = \<Union>S"
1.2523 + apply (rule subset_antisym)
1.2524 + apply (rule Sup_least)
1.2525 + apply (erule Union_upper)
1.2526 + apply (rule Union_least)
1.2527 + apply (erule Sup_upper)
1.2528 + done
1.2529 +
1.2530 +lemma top_set_eq: "top = UNIV"
1.2531 + by (iprover intro!: subset_antisym subset_UNIV top_greatest)
1.2532 +
1.2533 +lemma bot_set_eq: "bot = {}"
1.2534 + by (iprover intro!: subset_antisym empty_subsetI bot_least)
1.2535 +
1.2536 +no_notation
1.2537 + less_eq (infix "\<sqsubseteq>" 50) and
1.2538 + less (infix "\<sqsubset>" 50) and
1.2539 + inf (infixl "\<sqinter>" 70) and
1.2540 + sup (infixl "\<squnion>" 65) and
1.2541 + Inf ("\<Sqinter>_" [900] 900) and
1.2542 + Sup ("\<Squnion>_" [900] 900)
1.2543 +
1.2544 +
1.2545 +subsection {* Basic ML bindings *}
1.2546
1.2547 ML {*
1.2548 val Ball_def = @{thm Ball_def}