# HG changeset patch
# User haftmann
# Date 1325429055 -3600
# Node ID 53e7cc599f585421003ee0d22fe44b9033d65250
# Parent  af3b95160b59c7b025a6303f8c58d2ff0656bdd8
interaction of set operations for execution and membership predicate

diff -r af3b95160b59 -r 53e7cc599f58 src/HOL/Product_Type.thy
--- 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:
diff -r af3b95160b59 -r 53e7cc599f58 src/HOL/Set.thy
--- 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