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 {*