--- a/src/HOL/Product_Type.thy Sun Jan 01 11:28:45 2012 +0100
+++ b/src/HOL/Product_Type.thy Sun Jan 01 15:44:15 2012 +0100
@@ -893,11 +893,6 @@
hide_const (open) Times
-definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
- [code_abbrev]: "product A B = Sigma A (\<lambda>_. B)"
-
-hide_const (open) product
-
syntax
"_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
translations
@@ -1044,12 +1039,21 @@
lemma image_split_eq_Sigma:
"(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
-proof (safe intro!: imageI vimageI)
+proof (safe intro!: imageI)
fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b"
show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A"
using * eq[symmetric] by auto
qed simp_all
+definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
+ [code_abbrev]: "product A B = A \<times> B"
+
+hide_const (open) product
+
+lemma member_product:
+ "x \<in> Product_Type.product A B \<longleftrightarrow> x \<in> A \<times> B"
+ by (simp add: product_def)
+
text {* The following @{const map_pair} lemmas are due to Joachim Breitner: *}
lemma map_pair_inj_on:
--- a/src/HOL/Set.thy Sun Jan 01 11:28:45 2012 +0100
+++ b/src/HOL/Set.thy Sun Jan 01 15:44:15 2012 +0100
@@ -833,7 +833,7 @@
thus ?R using `a\<noteq>b` by auto
qed
next
- assume ?R thus ?L by(auto split: if_splits)
+ assume ?R thus ?L by (auto split: if_splits)
qed
subsubsection {* Singletons, using insert *}
@@ -1796,7 +1796,7 @@
by (auto simp add: bind_def)
lemma empty_bind [simp]:
- "Set.bind {} B = {}"
+ "Set.bind {} f = {}"
by (simp add: bind_def)
lemma nonempty_bind_const:
@@ -1819,11 +1819,19 @@
hide_const (open) remove
+lemma member_remove [simp]:
+ "x \<in> Set.remove y A \<longleftrightarrow> x \<in> A \<and> x \<noteq> y"
+ by (simp add: remove_def)
+
definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
[code_abbrev]: "project P A = {a \<in> A. P a}"
hide_const (open) project
+lemma member_project [simp]:
+ "x \<in> Set.project P A \<longleftrightarrow> x \<in> A \<and> P x"
+ by (simp add: project_def)
+
instantiation set :: (equal) equal
begin