src/HOL/Set.thy
changeset 45959 184d36538e51
parent 45909 6fe61da4c467
child 45986 c9e50153e5ae
     1.1 --- a/src/HOL/Set.thy	Fri Dec 23 16:37:27 2011 +0100
     1.2 +++ b/src/HOL/Set.thy	Sat Dec 24 15:53:07 2011 +0100
     1.3 @@ -8,13 +8,13 @@
     1.4  
     1.5  subsection {* Sets as predicates *}
     1.6  
     1.7 -type_synonym 'a set = "'a \<Rightarrow> bool"
     1.8 +typedecl 'a set
     1.9  
    1.10 -definition Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" where -- "comprehension"
    1.11 -  "Collect P = P"
    1.12 -
    1.13 -definition member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" where -- "membership"
    1.14 -  mem_def: "member x A = A x"
    1.15 +axiomatization Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" -- "comprehension"
    1.16 +  and member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" -- "membership"
    1.17 +where
    1.18 +  mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
    1.19 +  and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
    1.20  
    1.21  notation
    1.22    member  ("op :") and
    1.23 @@ -40,7 +40,6 @@
    1.24    not_member  ("(_/ \<notin> _)" [50, 51] 50)
    1.25  
    1.26  
    1.27 -
    1.28  text {* Set comprehensions *}
    1.29  
    1.30  syntax
    1.31 @@ -55,12 +54,6 @@
    1.32  translations
    1.33    "{x:A. P}" => "{x. x:A & P}"
    1.34  
    1.35 -lemma mem_Collect_eq [iff]: "a \<in> {x. P x} = P a"
    1.36 -  by (simp add: Collect_def mem_def)
    1.37 -
    1.38 -lemma Collect_mem_eq [simp]: "{x. x \<in> A} = A"
    1.39 -  by (simp add: Collect_def mem_def)
    1.40 -
    1.41  lemma CollectI: "P a \<Longrightarrow> a \<in> {x. P x}"
    1.42    by simp
    1.43  
    1.44 @@ -98,6 +91,43 @@
    1.45    "A = B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)"
    1.46    by (auto intro:set_eqI)
    1.47  
    1.48 +text {* Lifting of predicate class instances *}
    1.49 +
    1.50 +instantiation set :: (type) boolean_algebra
    1.51 +begin
    1.52 +
    1.53 +definition less_eq_set where
    1.54 +  "less_eq_set A B = less_eq (\<lambda>x. member x A) (\<lambda>x. member x B)"
    1.55 +
    1.56 +definition less_set where
    1.57 +  "less_set A B = less (\<lambda>x. member x A) (\<lambda>x. member x B)"
    1.58 +
    1.59 +definition inf_set where
    1.60 +  "inf_set A B = Collect (inf (\<lambda>x. member x A) (\<lambda>x. member x B))"
    1.61 +
    1.62 +definition sup_set where
    1.63 +  "sup_set A B = Collect (sup (\<lambda>x. member x A) (\<lambda>x. member x B))"
    1.64 +
    1.65 +definition bot_set where
    1.66 +  "bot = Collect bot"
    1.67 +
    1.68 +definition top_set where
    1.69 +  "top = Collect top"
    1.70 +
    1.71 +definition uminus_set where
    1.72 +  "uminus A = Collect (uminus (\<lambda>x. member x A))"
    1.73 +
    1.74 +definition minus_set where
    1.75 +  "minus_set A B = Collect (minus (\<lambda>x. member x A) (\<lambda>x. member x B))"
    1.76 +
    1.77 +instance proof
    1.78 +qed (simp_all add: less_eq_set_def less_set_def inf_set_def sup_set_def
    1.79 +  bot_set_def top_set_def uminus_set_def minus_set_def
    1.80 +  less_le_not_le inf_compl_bot sup_compl_top sup_inf_distrib1 diff_eq
    1.81 +  set_eqI fun_eq_iff)
    1.82 +
    1.83 +end
    1.84 +
    1.85  text {* Set enumerations *}
    1.86  
    1.87  abbreviation empty :: "'a set" ("{}") where
    1.88 @@ -453,7 +483,7 @@
    1.89  subsubsection {* Subsets *}
    1.90  
    1.91  lemma subsetI [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B) \<Longrightarrow> A \<subseteq> B"
    1.92 -  unfolding mem_def by (rule le_funI, rule le_boolI)
    1.93 +  by (simp add: less_eq_set_def le_fun_def)
    1.94  
    1.95  text {*
    1.96    \medskip Map the type @{text "'a set => anything"} to just @{typ
    1.97 @@ -462,7 +492,7 @@
    1.98  *}
    1.99  
   1.100  lemma subsetD [elim, intro?]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
   1.101 -  unfolding mem_def by (erule le_funE, erule le_boolE)
   1.102 +  by (simp add: less_eq_set_def le_fun_def)
   1.103    -- {* Rule in Modus Ponens style. *}
   1.104  
   1.105  lemma rev_subsetD [no_atp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
   1.106 @@ -476,7 +506,7 @@
   1.107  
   1.108  lemma subsetCE [no_atp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
   1.109    -- {* Classical elimination rule. *}
   1.110 -  unfolding mem_def by (blast dest: le_funE le_boolE)
   1.111 +  by (auto simp add: less_eq_set_def le_fun_def)
   1.112  
   1.113  lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
   1.114  
   1.115 @@ -543,7 +573,7 @@
   1.116  
   1.117  lemma empty_def:
   1.118    "{} = {x. False}"
   1.119 -  by (simp add: bot_fun_def Collect_def)
   1.120 +  by (simp add: bot_set_def bot_fun_def)
   1.121  
   1.122  lemma empty_iff [simp]: "(c : {}) = False"
   1.123    by (simp add: empty_def)
   1.124 @@ -576,7 +606,7 @@
   1.125  
   1.126  lemma UNIV_def:
   1.127    "UNIV = {x. True}"
   1.128 -  by (simp add: top_fun_def Collect_def)
   1.129 +  by (simp add: top_set_def top_fun_def)
   1.130  
   1.131  lemma UNIV_I [simp]: "x : UNIV"
   1.132    by (simp add: UNIV_def)
   1.133 @@ -635,10 +665,10 @@
   1.134  subsubsection {* Set complement *}
   1.135  
   1.136  lemma Compl_iff [simp]: "(c \<in> -A) = (c \<notin> A)"
   1.137 -  by (simp add: mem_def fun_Compl_def)
   1.138 +  by (simp add: fun_Compl_def uminus_set_def)
   1.139  
   1.140  lemma ComplI [intro!]: "(c \<in> A ==> False) ==> c \<in> -A"
   1.141 -  by (unfold mem_def fun_Compl_def bool_Compl_def) blast
   1.142 +  by (simp add: fun_Compl_def uminus_set_def) blast
   1.143  
   1.144  text {*
   1.145    \medskip This form, with negated conclusion, works well with the
   1.146 @@ -646,11 +676,12 @@
   1.147    right side of the notional turnstile ... *}
   1.148  
   1.149  lemma ComplD [dest!]: "c : -A ==> c~:A"
   1.150 -  by (simp add: mem_def fun_Compl_def)
   1.151 +  by simp
   1.152  
   1.153  lemmas ComplE = ComplD [elim_format]
   1.154  
   1.155 -lemma Compl_eq: "- A = {x. ~ x : A}" by blast
   1.156 +lemma Compl_eq: "- A = {x. ~ x : A}"
   1.157 +  by blast
   1.158  
   1.159  
   1.160  subsubsection {* Binary intersection *}
   1.161 @@ -666,7 +697,7 @@
   1.162  
   1.163  lemma Int_def:
   1.164    "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
   1.165 -  by (simp add: inf_fun_def Collect_def mem_def)
   1.166 +  by (simp add: inf_set_def inf_fun_def)
   1.167  
   1.168  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
   1.169    by (unfold Int_def) blast
   1.170 @@ -700,7 +731,7 @@
   1.171  
   1.172  lemma Un_def:
   1.173    "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
   1.174 -  by (simp add: sup_fun_def Collect_def mem_def)
   1.175 +  by (simp add: sup_set_def sup_fun_def)
   1.176  
   1.177  lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
   1.178    by (unfold Un_def) blast
   1.179 @@ -723,7 +754,7 @@
   1.180    by (unfold Un_def) blast
   1.181  
   1.182  lemma insert_def: "insert a B = {x. x = a} \<union> B"
   1.183 -  by (simp add: Collect_def mem_def insert_compr Un_def)
   1.184 +  by (simp add: insert_compr Un_def)
   1.185  
   1.186  lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
   1.187    by (fact mono_sup)
   1.188 @@ -732,7 +763,7 @@
   1.189  subsubsection {* Set difference *}
   1.190  
   1.191  lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
   1.192 -  by (simp add: mem_def fun_diff_def)
   1.193 +  by (simp add: minus_set_def fun_diff_def)
   1.194  
   1.195  lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"
   1.196    by simp
   1.197 @@ -1751,20 +1782,19 @@
   1.198    apply (auto elim: monoD intro!: order_antisym)
   1.199    done
   1.200  
   1.201 -subsection {* Misc *}
   1.202  
   1.203 -text {* Rudimentary code generation *}
   1.204 +subsubsection {* Monad operation *}
   1.205  
   1.206 -lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
   1.207 -  by (auto simp add: insert_compr Collect_def mem_def)
   1.208 +definition bind :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   1.209 +  "bind A f = {x. \<exists>B \<in> f`A. x \<in> B}"
   1.210  
   1.211 -lemma vimage_code [code]: "(f -` A) x = A (f x)"
   1.212 -  by (simp add: vimage_def Collect_def mem_def)
   1.213 +hide_const (open) bind
   1.214 +
   1.215 +
   1.216 +text {* Misc *}
   1.217  
   1.218  hide_const (open) member not_member
   1.219  
   1.220 -text {* Misc theorem and ML bindings *}
   1.221 -
   1.222  lemmas equalityI = subset_antisym
   1.223  
   1.224  ML {*