--- a/src/HOL/Set.thy Fri Dec 23 16:37:27 2011 +0100
+++ b/src/HOL/Set.thy Sat Dec 24 15:53:07 2011 +0100
@@ -8,13 +8,13 @@
subsection {* Sets as predicates *}
-type_synonym 'a set = "'a \<Rightarrow> bool"
+typedecl 'a set
-definition Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" where -- "comprehension"
- "Collect P = P"
-
-definition member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" where -- "membership"
- mem_def: "member x A = A x"
+axiomatization Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" -- "comprehension"
+ and member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" -- "membership"
+where
+ mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
+ and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
notation
member ("op :") and
@@ -40,7 +40,6 @@
not_member ("(_/ \<notin> _)" [50, 51] 50)
-
text {* Set comprehensions *}
syntax
@@ -55,12 +54,6 @@
translations
"{x:A. P}" => "{x. x:A & P}"
-lemma mem_Collect_eq [iff]: "a \<in> {x. P x} = P a"
- by (simp add: Collect_def mem_def)
-
-lemma Collect_mem_eq [simp]: "{x. x \<in> A} = A"
- by (simp add: Collect_def mem_def)
-
lemma CollectI: "P a \<Longrightarrow> a \<in> {x. P x}"
by simp
@@ -98,6 +91,43 @@
"A = B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)"
by (auto intro:set_eqI)
+text {* Lifting of predicate class instances *}
+
+instantiation set :: (type) boolean_algebra
+begin
+
+definition less_eq_set where
+ "less_eq_set A B = less_eq (\<lambda>x. member x A) (\<lambda>x. member x B)"
+
+definition less_set where
+ "less_set A B = less (\<lambda>x. member x A) (\<lambda>x. member x B)"
+
+definition inf_set where
+ "inf_set A B = Collect (inf (\<lambda>x. member x A) (\<lambda>x. member x B))"
+
+definition sup_set where
+ "sup_set A B = Collect (sup (\<lambda>x. member x A) (\<lambda>x. member x B))"
+
+definition bot_set where
+ "bot = Collect bot"
+
+definition top_set where
+ "top = Collect top"
+
+definition uminus_set where
+ "uminus A = Collect (uminus (\<lambda>x. member x A))"
+
+definition minus_set where
+ "minus_set A B = Collect (minus (\<lambda>x. member x A) (\<lambda>x. member x B))"
+
+instance proof
+qed (simp_all add: less_eq_set_def less_set_def inf_set_def sup_set_def
+ bot_set_def top_set_def uminus_set_def minus_set_def
+ less_le_not_le inf_compl_bot sup_compl_top sup_inf_distrib1 diff_eq
+ set_eqI fun_eq_iff)
+
+end
+
text {* Set enumerations *}
abbreviation empty :: "'a set" ("{}") where
@@ -453,7 +483,7 @@
subsubsection {* Subsets *}
lemma subsetI [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B) \<Longrightarrow> A \<subseteq> B"
- unfolding mem_def by (rule le_funI, rule le_boolI)
+ by (simp add: less_eq_set_def le_fun_def)
text {*
\medskip Map the type @{text "'a set => anything"} to just @{typ
@@ -462,7 +492,7 @@
*}
lemma subsetD [elim, intro?]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
- unfolding mem_def by (erule le_funE, erule le_boolE)
+ by (simp add: less_eq_set_def le_fun_def)
-- {* Rule in Modus Ponens style. *}
lemma rev_subsetD [no_atp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
@@ -476,7 +506,7 @@
lemma subsetCE [no_atp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
-- {* Classical elimination rule. *}
- unfolding mem_def by (blast dest: le_funE le_boolE)
+ by (auto simp add: less_eq_set_def le_fun_def)
lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
@@ -543,7 +573,7 @@
lemma empty_def:
"{} = {x. False}"
- by (simp add: bot_fun_def Collect_def)
+ by (simp add: bot_set_def bot_fun_def)
lemma empty_iff [simp]: "(c : {}) = False"
by (simp add: empty_def)
@@ -576,7 +606,7 @@
lemma UNIV_def:
"UNIV = {x. True}"
- by (simp add: top_fun_def Collect_def)
+ by (simp add: top_set_def top_fun_def)
lemma UNIV_I [simp]: "x : UNIV"
by (simp add: UNIV_def)
@@ -635,10 +665,10 @@
subsubsection {* Set complement *}
lemma Compl_iff [simp]: "(c \<in> -A) = (c \<notin> A)"
- by (simp add: mem_def fun_Compl_def)
+ by (simp add: fun_Compl_def uminus_set_def)
lemma ComplI [intro!]: "(c \<in> A ==> False) ==> c \<in> -A"
- by (unfold mem_def fun_Compl_def bool_Compl_def) blast
+ by (simp add: fun_Compl_def uminus_set_def) blast
text {*
\medskip This form, with negated conclusion, works well with the
@@ -646,11 +676,12 @@
right side of the notional turnstile ... *}
lemma ComplD [dest!]: "c : -A ==> c~:A"
- by (simp add: mem_def fun_Compl_def)
+ by simp
lemmas ComplE = ComplD [elim_format]
-lemma Compl_eq: "- A = {x. ~ x : A}" by blast
+lemma Compl_eq: "- A = {x. ~ x : A}"
+ by blast
subsubsection {* Binary intersection *}
@@ -666,7 +697,7 @@
lemma Int_def:
"A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
- by (simp add: inf_fun_def Collect_def mem_def)
+ by (simp add: inf_set_def inf_fun_def)
lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
by (unfold Int_def) blast
@@ -700,7 +731,7 @@
lemma Un_def:
"A \<union> B = {x. x \<in> A \<or> x \<in> B}"
- by (simp add: sup_fun_def Collect_def mem_def)
+ by (simp add: sup_set_def sup_fun_def)
lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
by (unfold Un_def) blast
@@ -723,7 +754,7 @@
by (unfold Un_def) blast
lemma insert_def: "insert a B = {x. x = a} \<union> B"
- by (simp add: Collect_def mem_def insert_compr Un_def)
+ by (simp add: insert_compr Un_def)
lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
by (fact mono_sup)
@@ -732,7 +763,7 @@
subsubsection {* Set difference *}
lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
- by (simp add: mem_def fun_diff_def)
+ by (simp add: minus_set_def fun_diff_def)
lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"
by simp
@@ -1751,20 +1782,19 @@
apply (auto elim: monoD intro!: order_antisym)
done
-subsection {* Misc *}
-text {* Rudimentary code generation *}
+subsubsection {* Monad operation *}
-lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
- by (auto simp add: insert_compr Collect_def mem_def)
+definition bind :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
+ "bind A f = {x. \<exists>B \<in> f`A. x \<in> B}"
-lemma vimage_code [code]: "(f -` A) x = A (f x)"
- by (simp add: vimage_def Collect_def mem_def)
+hide_const (open) bind
+
+
+text {* Misc *}
hide_const (open) member not_member
-text {* Misc theorem and ML bindings *}
-
lemmas equalityI = subset_antisym
ML {*