lemma swap_inj_on, swap_product
authorhaftmann
Thu Mar 18 13:56:34 2010 +0100 (2010-03-18)
changeset 3582267e4de90d2c2
parent 35821 ee34f03a7d26
child 35823 bd26885af9f4
lemma swap_inj_on, swap_product
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Product_Type.thy	Thu Mar 18 13:56:33 2010 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Mar 18 13:56:34 2010 +0100
     1.3 @@ -998,6 +998,15 @@
     1.4  lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
     1.5    by (auto, rule_tac p = "f x" in PairE, auto)
     1.6  
     1.7 +lemma swap_inj_on:
     1.8 +  "inj_on (%(i, j). (j, i)) (A \<times> B)"
     1.9 +  by (unfold inj_on_def) fast
    1.10 +
    1.11 +lemma swap_product:
    1.12 +  "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
    1.13 +  by (simp add: split_def image_def) blast
    1.14 +
    1.15 +
    1.16  subsubsection {* Code generator setup *}
    1.17  
    1.18  lemma [code]: