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.220    by (simp add: psubset_eq)
   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.269    by (simp add: contents_def)
   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"
   1.452 +apply (simp add: Least_def)
   1.453 +apply (rule the_equality)
   1.454 +apply (auto intro!: order_antisym)
   1.455 +done
   1.456 +
   1.457  
   1.458  subsection {* Basic ML bindings *}
   1.459