src/HOL/Product_Type.thy
changeset 36622 e393a91f86df
parent 36176 3fe7e97ccca8
child 36664 6302f9ad7047
     1.1 --- a/src/HOL/Product_Type.thy	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Apr 20 17:58:34 2010 +0200
     1.3 @@ -990,6 +990,15 @@
     1.4  lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)"
     1.5  by blast
     1.6  
     1.7 +lemma Times_empty[simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
     1.8 +  by auto
     1.9 +
    1.10 +lemma fst_image_times[simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)"
    1.11 +  by (auto intro!: image_eqI)
    1.12 +
    1.13 +lemma snd_image_times[simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)"
    1.14 +  by (auto intro!: image_eqI)
    1.15 +
    1.16  lemma insert_times_insert[simp]:
    1.17    "insert a A \<times> insert b B =
    1.18     insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
    1.19 @@ -999,13 +1008,20 @@
    1.20    by (auto, rule_tac p = "f x" in PairE, auto)
    1.21  
    1.22  lemma swap_inj_on:
    1.23 -  "inj_on (%(i, j). (j, i)) (A \<times> B)"
    1.24 -  by (unfold inj_on_def) fast
    1.25 +  "inj_on (\<lambda>(i, j). (j, i)) A"
    1.26 +  by (auto intro!: inj_onI)
    1.27  
    1.28  lemma swap_product:
    1.29    "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
    1.30    by (simp add: split_def image_def) blast
    1.31  
    1.32 +lemma image_split_eq_Sigma:
    1.33 +  "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
    1.34 +proof (safe intro!: imageI vimageI)
    1.35 +  fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b"
    1.36 +  show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A"
    1.37 +    using * eq[symmetric] by auto
    1.38 +qed simp_all
    1.39  
    1.40  subsubsection {* Code generator setup *}
    1.41