src/HOL/Product_Type.thy
changeset 36664 6302f9ad7047
parent 36622 e393a91f86df
child 37136 e0c9d3e49e15
equal deleted inserted replaced
36663:f75b13ed4898 36664:6302f9ad7047
   414 
   414 
   415 lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
   415 lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
   416   by (simp add: split_def id_def)
   416   by (simp add: split_def id_def)
   417 
   417 
   418 lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
   418 lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
   419   -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity Datatype. *}
   419   -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
   420   by (rule ext) auto
   420   by (rule ext) auto
   421 
   421 
   422 lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
   422 lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
   423   by (cases x) simp
   423   by (cases x) simp
   424 
   424 
   750 no_notation scomp (infixl "o\<rightarrow>" 60)
   750 no_notation scomp (infixl "o\<rightarrow>" 60)
   751 
   751 
   752 
   752 
   753 text {*
   753 text {*
   754   @{term prod_fun} --- action of the product functor upon
   754   @{term prod_fun} --- action of the product functor upon
   755   Datatypes.
   755   functions.
   756 *}
   756 *}
   757 
   757 
   758 definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
   758 definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
   759   [code del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
   759   [code del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
   760 
   760