src/HOL/Product_Type.thy
changeset 60057 86fa63ce8156
parent 59880 30687c3f2b10
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Product_Type.thy	Mon Apr 13 13:03:41 2015 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Apr 14 11:32:01 2015 +0200
     1.3 @@ -1224,6 +1224,18 @@
     1.4      using * eq[symmetric] by auto
     1.5  qed simp_all
     1.6  
     1.7 +lemma inj_on_apfst [simp]: "inj_on (apfst f) (A \<times> UNIV) \<longleftrightarrow> inj_on f A"
     1.8 +by(auto simp add: inj_on_def)
     1.9 +
    1.10 +lemma inj_apfst [simp]: "inj (apfst f) \<longleftrightarrow> inj f"
    1.11 +using inj_on_apfst[of f UNIV] by simp
    1.12 +
    1.13 +lemma inj_on_apsnd [simp]: "inj_on (apsnd f) (UNIV \<times> A) \<longleftrightarrow> inj_on f A"
    1.14 +by(auto simp add: inj_on_def)
    1.15 +
    1.16 +lemma inj_apsnd [simp]: "inj (apsnd f) \<longleftrightarrow> inj f"
    1.17 +using inj_on_apsnd[of f UNIV] by simp
    1.18 +
    1.19  definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
    1.20    [code_abbrev]: "product A B = A \<times> B"
    1.21