src/HOL/Set.thy
 changeset 26800 dcf1dfc915a7 parent 26732 6ea9de67e576 child 27106 ff27dc6e7d05
```     1.1 --- a/src/HOL/Set.thy	Wed May 07 10:56:41 2008 +0200
1.2 +++ b/src/HOL/Set.thy	Wed May 07 10:56:43 2008 +0200
1.3 @@ -6,7 +6,7 @@
1.4  header {* Set theory for higher-order logic *}
1.5
1.6  theory Set
1.7 -imports Code_Setup
1.8 +imports Orderings
1.9  begin
1.10
1.11  text {* A set in HOL is simply a predicate. *}
1.12 @@ -16,7 +16,7 @@
1.13
1.14  global
1.15
1.16 -typedecl 'a set
1.17 +types 'a set = "'a => bool"
1.18
1.19  consts
1.20    "{}"          :: "'a set"                             ("{}")
1.21 @@ -143,19 +143,6 @@
1.22    union/intersection symbol because this leads to problems with nested
1.23    subscripts in Proof General. *}
1.24
1.25 -instantiation set :: (type) ord
1.26 -begin
1.27 -
1.28 -definition
1.29 -  subset_def [code func del]: "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
1.30 -
1.31 -definition
1.32 -  psubset_def [code func del]: "(A\<Colon>'a set) < B \<equiv> A \<le> B \<and> A \<noteq> B"
1.33 -
1.34 -instance ..
1.35 -
1.36 -end
1.37 -
1.38  abbreviation
1.39    subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
1.40    "subset \<equiv> less"
1.41 @@ -336,33 +323,50 @@
1.42
1.43  text {* Isomorphisms between predicates and sets. *}
1.44
1.45 -axioms
1.46 -  mem_Collect_eq: "(a : {x. P(x)}) = P(a)"
1.47 -  Collect_mem_eq: "{x. x:A} = A"
1.48 -finalconsts
1.49 -  Collect
1.50 -  "op :"
1.51 +defs
1.52 +  mem_def: "x : S == S x"
1.53 +  Collect_def: "Collect P == P"
1.54
1.55  defs
1.56    Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
1.57    Bex_def:      "Bex A P        == EX x. x:A & P(x)"
1.58    Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
1.59
1.60 -instantiation set :: (type) minus
1.61 +instantiation "fun" :: (type, minus) minus
1.62  begin
1.63
1.64  definition
1.65 -  set_diff_def [code func del]: "A - B = {x. x:A & ~x:B}"
1.66 +  fun_diff_def: "A - B = (%x. A x - B x)"
1.67
1.68  instance ..
1.69
1.70  end
1.71
1.72 -instantiation set :: (type) uminus
1.73 +instantiation bool :: minus
1.74  begin
1.75
1.76  definition
1.77 -  Compl_def [code func del]:    "- A   = {x. ~x:A}"
1.78 +  bool_diff_def: "A - B = (A & ~ B)"
1.79 +
1.80 +instance ..
1.81 +
1.82 +end
1.83 +
1.84 +instantiation "fun" :: (type, uminus) uminus
1.85 +begin
1.86 +
1.87 +definition
1.88 +  fun_Compl_def: "- A = (%x. - A x)"
1.89 +
1.90 +instance ..
1.91 +
1.92 +end
1.93 +
1.94 +instantiation bool :: uminus
1.95 +begin
1.96 +
1.97 +definition
1.98 +  bool_Compl_def: "- A = (~ A)"
1.99
1.100  instance ..
1.101
1.102 @@ -386,7 +390,11 @@
1.103
1.104  subsubsection {* Relating predicates and sets *}
1.105
1.106 -declare mem_Collect_eq [iff]  Collect_mem_eq [simp]
1.107 +lemma mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"
1.108 +  by (simp add: Collect_def mem_def)
1.109 +
1.110 +lemma Collect_mem_eq [simp]: "{x. x:A} = A"
1.111 +  by (simp add: Collect_def mem_def)
1.112
1.113  lemma CollectI: "P(a) ==> a : {x. P(x)}"
1.114    by simp
1.115 @@ -519,7 +527,7 @@
1.116  subsubsection {* Subsets *}
1.117
1.118  lemma subsetI [atp,intro!]: "(!!x. x:A ==> x:B) ==> A \<subseteq> B"
1.119 -  by (simp add: subset_def)
1.120 +  by (auto simp add: mem_def intro: predicate1I)
1.121
1.122  text {*
1.123    \medskip Map the type @{text "'a set => anything"} to just @{typ
1.124 @@ -529,7 +537,7 @@
1.125
1.126  lemma subsetD [elim]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
1.127    -- {* Rule in Modus Ponens style. *}
1.128 -  by (unfold subset_def) blast
1.129 +  by (unfold mem_def) blast
1.130
1.131  declare subsetD [intro?] -- FIXME
1.132
1.133 @@ -550,7 +558,9 @@
1.134
1.135  lemma subsetCE [elim]: "A \<subseteq>  B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
1.136    -- {* Classical elimination rule. *}
1.137 -  by (unfold subset_def) blast
1.138 +  by (unfold mem_def) blast
1.139 +
1.140 +lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
1.141
1.142  text {*
1.143    \medskip Takes assumptions @{prop "A \<subseteq> B"}; @{prop "c \<in> A"} and
1.144 @@ -699,10 +709,10 @@
1.145  subsubsection {* Set complement *}
1.146
1.147  lemma Compl_iff [simp]: "(c \<in> -A) = (c \<notin> A)"
1.148 -  by (unfold Compl_def) blast
1.149 +  by (simp add: mem_def fun_Compl_def bool_Compl_def)
1.150
1.151  lemma ComplI [intro!]: "(c \<in> A ==> False) ==> c \<in> -A"
1.152 -  by (unfold Compl_def) blast
1.153 +  by (unfold mem_def fun_Compl_def bool_Compl_def) blast
1.154
1.155  text {*
1.156    \medskip This form, with negated conclusion, works well with the
1.157 @@ -710,10 +720,12 @@
1.158    right side of the notional turnstile ... *}
1.159
1.160  lemma ComplD [dest!]: "c : -A ==> c~:A"
1.161 -  by (unfold Compl_def) blast
1.162 +  by (simp add: mem_def fun_Compl_def bool_Compl_def)
1.163
1.164  lemmas ComplE = ComplD [elim_format]
1.165
1.166 +lemma Compl_eq: "- A = {x. ~ x : A}" by blast
1.167 +
1.168
1.169  subsubsection {* Binary union -- Un *}
1.170
1.171 @@ -759,7 +771,7 @@
1.172  subsubsection {* Set difference *}
1.173
1.174  lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
1.175 -  by (unfold set_diff_def) blast
1.176 +  by (simp add: mem_def fun_diff_def bool_diff_def)
1.177
1.178  lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"
1.179    by simp
1.180 @@ -773,6 +785,8 @@
1.181  lemma DiffE [elim!]: "c : A - B ==> (c:A ==> c~:B ==> P) ==> P"
1.182    by simp
1.183
1.184 +lemma set_diff_eq: "A - B = {x. x : A & ~ x : B}" by blast
1.185 +
1.186
1.187  subsubsection {* Augmenting a set -- insert *}
1.188
1.189 @@ -1013,7 +1027,7 @@
1.190    by (rule split_if)
1.191
1.192  lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))"
1.193 -  by (rule split_if)
1.194 +  by (rule split_if [where P="%S. a : S"])
1.195
1.196  lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
1.197
1.198 @@ -1042,29 +1056,29 @@
1.199  subsubsection {* The ``proper subset'' relation *}
1.200
1.201  lemma psubsetI [intro!,noatp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
1.202 -  by (unfold psubset_def) blast
1.203 +  by (unfold less_le) blast
1.204
1.205  lemma psubsetE [elim!,noatp]:
1.206      "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
1.207 -  by (unfold psubset_def) blast
1.208 +  by (unfold less_le) blast
1.209
1.210  lemma psubset_insert_iff:
1.211    "(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.212 -  by (auto simp add: psubset_def subset_insert_iff)
1.213 +  by (auto simp add: less_le subset_insert_iff)
1.214
1.215  lemma psubset_eq: "(A \<subset> B) = (A \<subseteq> B & A \<noteq> B)"
1.216 -  by (simp only: psubset_def)
1.217 +  by (simp only: less_le)
1.218
1.219  lemma psubset_imp_subset: "A \<subset> B ==> A \<subseteq> B"
1.221
1.222  lemma psubset_trans: "[| A \<subset> B; B \<subset> C |] ==> A \<subset> C"
1.223 -apply (unfold psubset_def)
1.224 +apply (unfold less_le)
1.225  apply (auto dest: subset_antisym)
1.226  done
1.227
1.228  lemma psubsetD: "[| A \<subset> B; c \<in> A |] ==> c \<in> B"
1.229 -apply (unfold psubset_def)
1.230 +apply (unfold less_le)
1.231  apply (auto dest: subsetD)
1.232  done
1.233
1.234 @@ -1075,7 +1089,7 @@
1.235    by (auto simp add: psubset_eq)
1.236
1.237  lemma psubset_imp_ex_mem: "A \<subset> B ==> \<exists>b. b \<in> (B - A)"
1.238 -  by (unfold psubset_def) blast
1.239 +  by (unfold less_le) blast
1.240
1.241  lemma atomize_ball:
1.242      "(!!x. x \<in> A ==> P x) == Trueprop (\<forall>x\<in>A. P x)"
1.243 @@ -1183,7 +1197,7 @@
1.244    by blast
1.245
1.246  lemma not_psubset_empty [iff]: "\<not> (A < {})"
1.247 -  by (unfold psubset_def) blast
1.248 +  by (unfold less_le) blast
1.249
1.250  lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\<forall>x. \<not> P x)"
1.251  by blast
1.252 @@ -1854,7 +1868,7 @@
1.253    by blast
1.254
1.255  lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
1.256 -  by (unfold psubset_def) blast
1.257 +  by (unfold less_le) blast
1.258
1.259  lemma all_not_in_conv [simp]: "(\<forall>x. x \<notin> A) = (A = {})"
1.260    by blast
1.261 @@ -2142,7 +2156,7 @@
1.262  definition
1.263    contents :: "'a set \<Rightarrow> 'a"
1.264  where
1.265 -  [code func del]: "contents X = (THE x. X = {x})"
1.266 +  "contents X = (THE x. X = {x})"
1.267
1.268  lemma contents_eq [simp]: "contents {x} = x"
1.270 @@ -2156,156 +2170,45 @@
1.271  lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
1.272    by (rule subsetD)
1.273
1.274 -
1.275 -subsection {* Code generation for finite sets *}
1.276 -
1.277 -code_datatype "{}" insert
1.278 -
1.279 -
1.280 -subsubsection {* Primitive predicates *}
1.281 -
1.282 -definition
1.283 -  is_empty :: "'a set \<Rightarrow> bool"
1.284 -where
1.285 -  [code func del, code post]: "is_empty A \<longleftrightarrow> A = {}"
1.286 -lemmas [code inline] = is_empty_def [symmetric]
1.287 -
1.288 -lemma is_empty_insert [code func]:
1.289 -  "is_empty (insert a A) \<longleftrightarrow> False"
1.290 -  by (simp add: is_empty_def)
1.291 -
1.292 -lemma is_empty_empty [code func]:
1.293 -  "is_empty {} \<longleftrightarrow> True"
1.294 -  by (simp add: is_empty_def)
1.295 -
1.296 -lemma Ball_insert [code func]:
1.297 -  "Ball (insert a A) P \<longleftrightarrow> P a \<and> Ball A P"
1.298 -  by simp
1.299 -
1.300 -lemma Ball_empty [code func]:
1.301 -  "Ball {} P \<longleftrightarrow> True"
1.302 -  by simp
1.303 -
1.304 -lemma Bex_insert [code func]:
1.305 -  "Bex (insert a A) P \<longleftrightarrow> P a \<or> Bex A P"
1.306 -  by simp
1.307 -
1.308 -lemma Bex_empty [code func]:
1.309 -  "Bex {} P \<longleftrightarrow> False"
1.310 -  by simp
1.311 -
1.312 -
1.313 -subsubsection {* Primitive operations *}
1.314 -
1.315 -lemma minus_insert [code func]:
1.316 -  "insert (a\<Colon>'a\<Colon>eq) A - B = (let C = A - B in if a \<in> B then C else insert a C)"
1.317 -  by (auto simp add: Let_def)
1.318 -
1.319 -lemma minus_empty1 [code func]:
1.320 -  "{} - A = {}"
1.321 -  by simp
1.322 -
1.323 -lemma minus_empty2 [code func]:
1.324 -  "A - {} = A"
1.325 -  by simp
1.326 -
1.327 -lemma inter_insert [code func]:
1.328 -  "insert a A \<inter> B = (let C = A \<inter> B in if a \<in> B then insert a C else C)"
1.329 -  by (auto simp add: Let_def)
1.330 -
1.331 -lemma inter_empty1 [code func]:
1.332 -  "{} \<inter> A = {}"
1.333 -  by simp
1.334 -
1.335 -lemma inter_empty2 [code func]:
1.336 -  "A \<inter> {} = {}"
1.337 -  by simp
1.338 -
1.339 -lemma union_insert [code func]:
1.340 -  "insert a A \<union> B = (let C = A \<union> B in if a \<in> B then C else insert a C)"
1.341 -  by (auto simp add: Let_def)
1.342 -
1.343 -lemma union_empty1 [code func]:
1.344 -  "{} \<union> A = A"
1.345 -  by simp
1.346 -
1.347 -lemma union_empty2 [code func]:
1.348 -  "A \<union> {} = A"
1.349 -  by simp
1.350 -
1.351 -lemma INTER_insert [code func]:
1.352 -  "INTER (insert a A) f = f a \<inter> INTER A f"
1.353 -  by auto
1.354 -
1.355 -lemma INTER_singleton [code func]:
1.356 -  "INTER {a} f = f a"
1.357 -  by auto
1.358 -
1.359 -lemma UNION_insert [code func]:
1.360 -  "UNION (insert a A) f = f a \<union> UNION A f"
1.361 -  by auto
1.362 -
1.363 -lemma UNION_empty [code func]:
1.364 -  "UNION {} f = {}"
1.365 -  by auto
1.366 -
1.367 -lemma contents_insert [code func]:
1.368 -  "contents (insert a A) = contents (insert a (A - {a}))"
1.369 -  by auto
1.370 -declare contents_eq [code func]
1.371 -
1.372 -
1.373 -subsubsection {* Derived predicates *}
1.374 -
1.375 -lemma in_code [code func]:
1.376 -  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
1.377 -  by simp
1.378 -
1.379 -lemma subset_eq_code [code func]:
1.380 -  fixes A B :: "'a\<Colon>eq set"
1.381 -  shows "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
1.382 -  by auto
1.383 -
1.384 -lemma subset_code [code func]:
1.385 -  fixes A B :: "'a\<Colon>eq set"
1.386 -  shows "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
1.387 -  by auto
1.388 -
1.389 -instantiation set :: (eq) eq
1.390 +lemmas basic_trans_rules [trans] =
1.391 +  order_trans_rules set_rev_mp set_mp
1.392 +
1.393 +
1.394 +subsection {* Dense orders *}
1.395 +
1.396 +class dense_linear_order = linorder +
1.397 +  assumes gt_ex: "\<exists>y. x < y"
1.398 +  and lt_ex: "\<exists>y. y < x"
1.399 +  and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
1.400 +  (*see further theory Dense_Linear_Order*)
1.401  begin
1.402
1.403 -definition
1.404 -  "eq_class.eq A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
1.405 -
1.406 -instance by default (auto simp add: eq_set_def)
1.407 +lemma interval_empty_iff:
1.408 +  "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
1.409 +  by (auto dest: dense)
1.410
1.411  end
1.412
1.413
1.414 -subsubsection {* Derived operations *}
1.415 -
1.416 -lemma image_code [code func]:
1.417 -  "image f A = UNION A (\<lambda>x. {f x})" by auto
1.418 -
1.419 -definition
1.420 -  project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
1.421 -  [code func del, code post]: "project P A = {a\<in>A. P a}"
1.422 -
1.423 -lemmas [symmetric, code inline] = project_def
1.424 -
1.425 -lemma project_code [code func]:
1.426 -  "project P A = UNION A (\<lambda>a. if P a then {a} else {})"
1.427 -  by (auto simp add: project_def split: if_splits)
1.428 -
1.429 -lemma Inter_code [code func]:
1.430 -  "Inter A = INTER A (\<lambda>x. x)"
1.431 -  by auto
1.432 -
1.433 -lemma Union_code [code func]:
1.434 -  "Union A = UNION A (\<lambda>x. x)"
1.435 -  by auto
1.436 -
1.437 -code_reserved SML union inter -- {* avoid clashes with ML infixes *}
1.438 +subsection {* Least value operator *}
1.439 +
1.440 +lemma Least_mono:
1.441 +  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
1.442 +    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
1.443 +    -- {* Courtesy of Stephan Merz *}
1.444 +  apply clarify
1.445 +  apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
1.446 +  apply (rule LeastI2_order)
1.447 +  apply (auto elim: monoD intro!: order_antisym)
1.448 +  done
1.449 +
1.450 +lemma Least_equality:
1.451 +  "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"