# HG changeset patch
# User haftmann
# Date 1441570491 -7200
# Node ID 76cd7f1ec257710b3ae0a3be26740dab380a09e4
# Parent  e6b1236f9b3daae4e770411ee6a22c7888ec46b2
tuned notation, proofs, namespace

diff -r e6b1236f9b3d -r 76cd7f1ec257 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Product_Type.thy	Sun Sep 06 22:14:51 2015 +0200
@@ -363,23 +363,23 @@
 lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
   by (simp add: prod_eq_iff)
 
-lemma split_conv [simp, code]: "uncurry f (a, b) = f a b"
+lemma split_conv [simp, code]: "(case (a, b) of (c, d) \<Rightarrow> f c d) = f a b"
   by (fact prod.case)
 
-lemma splitI: "f a b \<Longrightarrow> uncurry f (a, b)"
+lemma splitI: "f a b \<Longrightarrow> case (a, b) of (c, d) \<Rightarrow> f c d"
   by (rule split_conv [THEN iffD2])
 
-lemma splitD: "uncurry f (a, b) \<Longrightarrow> f a b"
+lemma splitD: "(case (a, b) of (c, d) \<Rightarrow> f c d) \<Longrightarrow> f a b"
   by (rule split_conv [THEN iffD1])
 
-lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
+lemma split_Pair [simp]: "uncurry Pair = id"
   by (simp add: fun_eq_iff split: prod.split)
 
 lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
   -- \<open>Subsumes the old @{text split_Pair} when @{term f} is the identity function.\<close>
   by (simp add: fun_eq_iff split: prod.split)
 
-lemma split_comp: "uncurry (f \<circ> g) x = f (g (fst x)) (snd x)"
+lemma split_comp: "(case x of (a, b) \<Rightarrow> (f \<circ> g) a b) = f (g (fst x)) (snd x)"
   by (cases x) simp
 
 lemma split_twice: "uncurry f (uncurry g p) = uncurry (\<lambda>x y. uncurry f (g x y)) p"
@@ -535,24 +535,24 @@
   \medskip These rules are for use with @{text blast}; could instead
   call @{text simp} using @{thm [source] prod.split} as rewrite.\<close>
 
-lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> uncurry c p"
+lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> case p of (a, b) \<Rightarrow> c a b"
   apply (simp only: split_tupled_all)
   apply (simp (no_asm_simp))
   done
 
-lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> uncurry c p x"
+lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> (case p of (a, b) \<Rightarrow> c a b) x"
   apply (simp only: split_tupled_all)
   apply (simp (no_asm_simp))
   done
 
-lemma splitE: "uncurry c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
+lemma splitE: "(case p of (a, b) \<Rightarrow> c a b) ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
   by (induct p) auto
 
-lemma splitE': "uncurry c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
+lemma splitE': "(case p of (a, b) \<Rightarrow> c a b) z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
   by (induct p) auto
 
 lemma splitE2:
-  "[| Q (uncurry P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
+  "[| Q (case z of (a, b) \<Rightarrow> P a b);  !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
 proof -
   assume q: "Q (uncurry P z)"
   assume r: "!!x y. [|z = (x, y); Q (P x y)|] ==> R"
@@ -562,14 +562,17 @@
     done
 qed
 
-lemma splitD': "uncurry R (a,b) c ==> R a b c"
+lemma splitD':
+  "(case (a, b) of (c, d) \<Rightarrow> R c d) c \<Longrightarrow> R a b c"
   by simp
 
-lemma mem_splitI: "z: c a b ==> z: uncurry c (a, b)"
+lemma mem_splitI:
+  "z \<in> c a b \<Longrightarrow> z \<in> (case (a, b) of (d, e) \<Rightarrow> c d e)"
   by simp
 
-lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: uncurry c p"
-by (simp only: split_tupled_all, simp)
+lemma mem_splitI2:
+  "\<And>p. (\<And>a b. p = (a, b) \<Longrightarrow> z \<in> c a b) \<Longrightarrow> z \<in> (case p of (a, b) \<Rightarrow> c a b)"
+  by (simp only: split_tupled_all) simp
 
 lemma mem_splitE:
   assumes "z \<in> uncurry c p"
@@ -1044,44 +1047,52 @@
   by (blast elim: equalityE)
 
 lemma SetCompr_Sigma_eq:
-  "Collect (uncurry (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"
+  "{(x, y). P x \<and> Q x y} = (SIGMA x:Collect P. Collect (Q x))"
   by blast
 
-lemma Collect_split [simp]: "{(a,b). P a & Q b} = Collect P <*> Collect Q"
+lemma Collect_split [simp]:
+  "{(a, b). P a \<and> Q b} = Collect P \<times> Collect Q "
   by (fact SetCompr_Sigma_eq)
 
 lemma UN_Times_distrib:
-  "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)"
+  "(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = UNION A E \<times> UNION B F"
   -- \<open>Suggested by Pierre Chartier\<close>
   by blast
 
 lemma split_paired_Ball_Sigma [simp, no_atp]:
-    "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"
+  "(\<forall>z\<in>Sigma A B. P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B x. P (x, y))"
   by blast
 
 lemma split_paired_Bex_Sigma [simp, no_atp]:
-    "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"
+  "(\<exists>z\<in>Sigma A B. P z) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>y\<in>B x. P (x, y))"
+  by blast
+
+lemma Sigma_Un_distrib1:
+  "Sigma (I \<union> J) C = Sigma I C \<union> Sigma J C"
   by blast
 
-lemma Sigma_Un_distrib1: "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))"
+lemma Sigma_Un_distrib2:
+  "(SIGMA i:I. A i \<union> B i) = Sigma I A \<union> Sigma I B"
   by blast
 
-lemma Sigma_Un_distrib2: "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))"
+lemma Sigma_Int_distrib1:
+  "Sigma (I \<inter> J) C = Sigma I C \<inter> Sigma J C"
   by blast
 
-lemma Sigma_Int_distrib1: "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))"
-  by blast
-
-lemma Sigma_Int_distrib2: "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))"
+lemma Sigma_Int_distrib2:
+  "(SIGMA i:I. A i \<inter> B i) = Sigma I A \<inter> Sigma I B"
   by blast
 
-lemma Sigma_Diff_distrib1: "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))"
+lemma Sigma_Diff_distrib1:
+  "Sigma (I - J) C = Sigma I C - Sigma J C"
   by blast
 
-lemma Sigma_Diff_distrib2: "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))"
+lemma Sigma_Diff_distrib2:
+  "(SIGMA i:I. A i - B i) = Sigma I A - Sigma I B"
   by blast
 
-lemma Sigma_Union: "Sigma (Union X) B = (UN A:X. Sigma A B)"
+lemma Sigma_Union:
+  "Sigma (\<Union>X) B = (\<Union>A\<in>X. Sigma A B)"
   by blast
 
 text \<open>
@@ -1089,25 +1100,32 @@
   matching, especially when the rules are re-oriented.
 \<close>
 
-lemma Times_Un_distrib1: "(A Un B) <*> C = (A <*> C) Un (B <*> C)"
+lemma Times_Un_distrib1:
+  "(A \<union> B) \<times> C = A \<times> C \<union> B \<times> C "
   by (fact Sigma_Un_distrib1)
 
-lemma Times_Int_distrib1: "(A Int B) <*> C = (A <*> C) Int (B <*> C)"
+lemma Times_Int_distrib1:
+  "(A \<inter> B) \<times> C = A \<times> C \<inter> B \<times> C "
   by (fact Sigma_Int_distrib1)
 
-lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)"
+lemma Times_Diff_distrib1:
+  "(A - B) \<times> C = A \<times> C - B \<times> C "
   by (fact Sigma_Diff_distrib1)
 
-lemma Times_empty[simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
+lemma Times_empty [simp]:
+  "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
   by auto
 
-lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> ((A = {} \<or> B = {}) \<and> (C = {} \<or> D = {}))"
+lemma times_eq_iff:
+  "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> (A = {} \<or> B = {}) \<and> (C = {} \<or> D = {})"
   by auto
 
-lemma fst_image_times[simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)"
+lemma fst_image_times [simp]:
+  "fst ` (A \<times> B) = (if B = {} then {} else A)"
   by force
 
-lemma snd_image_times[simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)"
+lemma snd_image_times [simp]:
+  "snd ` (A \<times> B) = (if A = {} then {} else B)"
   by force
 
 lemma vimage_fst:
@@ -1121,15 +1139,18 @@
 lemma insert_times_insert[simp]:
   "insert a A \<times> insert b B =
    insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
-by blast
+  by blast
 
-lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
-  apply auto
-  apply (case_tac "f x")
-  apply auto
-  done
+lemma vimage_Times:
+  "f -` (A \<times> B) = (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B"
+proof (rule set_eqI)
+  fix x
+  show "x \<in> f -` (A \<times> B) \<longleftrightarrow> x \<in> (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B"
+    by (cases "f x") (auto split: prod.split)
+qed
 
-lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
+lemma times_Int_times:
+  "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
   by auto
 
 lemma product_swap:
@@ -1160,15 +1181,18 @@
 lemma inj_apsnd [simp]: "inj (apsnd f) \<longleftrightarrow> inj f"
 using inj_on_apsnd[of f UNIV] by simp
 
-definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
+context
+begin
+
+qualified 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)
+  by (simp add: Product_Type.product_def)
 
+end
+  
 text \<open>The following @{const map_prod} lemmas are due to Joachim Breitner:\<close>
 
 lemma map_prod_inj_on: