1.1 --- a/src/HOL/Product_Type.thy	Sun Jan 01 11:28:45 2012 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Sun Jan 01 15:44:15 2012 +0100
     1.3 @@ -893,11 +893,6 @@
     1.4  
     1.5  hide_const (open) Times
     1.6  
     1.7 -definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
     1.8 -  [code_abbrev]: "product A B = Sigma A (\<lambda>_. B)"
     1.9 -
    1.10 -hide_const (open) product
    1.11 -
    1.12  syntax
    1.13    "_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
    1.14  translations
    1.15 @@ -1044,12 +1039,21 @@
    1.16  
    1.17  lemma image_split_eq_Sigma:
    1.18    "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
    1.19 -proof (safe intro!: imageI vimageI)
    1.20 +proof (safe intro!: imageI)
    1.21    fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b"
    1.22    show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A"
    1.23      using * eq[symmetric] by auto
    1.24  qed simp_all
    1.25  
    1.26 +definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
    1.27 +  [code_abbrev]: "product A B = A \<times> B"
    1.28 +
    1.29 +hide_const (open) product
    1.30 +
    1.31 +lemma member_product:
    1.32 +  "x \<in> Product_Type.product A B \<longleftrightarrow> x \<in> A \<times> B"
    1.33 +  by (simp add: product_def)
    1.34 +
    1.35  text {* The following @{const map_pair} lemmas are due to Joachim Breitner: *}
    1.36  
    1.37  lemma map_pair_inj_on:

     2.1 --- a/src/HOL/Set.thy	Sun Jan 01 11:28:45 2012 +0100
     2.2 +++ b/src/HOL/Set.thy	Sun Jan 01 15:44:15 2012 +0100
     2.3 @@ -833,7 +833,7 @@
     2.4      thus ?R using `a\<noteq>b` by auto
     2.5    qed
     2.6  next
     2.7 -  assume ?R thus ?L by(auto split: if_splits)
     2.8 +  assume ?R thus ?L by (auto split: if_splits)
     2.9  qed
    2.10  
    2.11  subsubsection {* Singletons, using insert *}
    2.12 @@ -1796,7 +1796,7 @@
    2.13    by (auto simp add: bind_def)
    2.14  
    2.15  lemma empty_bind [simp]:
    2.16 -  "Set.bind {} B = {}"
    2.17 +  "Set.bind {} f = {}"
    2.18    by (simp add: bind_def)
    2.19  
    2.20  lemma nonempty_bind_const:
    2.21 @@ -1819,11 +1819,19 @@
    2.22  
    2.23  hide_const (open) remove
    2.24  
    2.25 +lemma member_remove [simp]:
    2.26 +  "x \<in> Set.remove y A \<longleftrightarrow> x \<in> A \<and> x \<noteq> y"
    2.27 +  by (simp add: remove_def)
    2.28 +
    2.29  definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    2.30    [code_abbrev]: "project P A = {a \<in> A. P a}"
    2.31  
    2.32  hide_const (open) project
    2.33  
    2.34 +lemma member_project [simp]:
    2.35 +  "x \<in> Set.project P A \<longleftrightarrow> x \<in> A \<and> P x"
    2.36 +  by (simp add: project_def)
    2.37 +
    2.38  instantiation set :: (equal) equal
    2.39  begin
    2.40