src/HOL/Product_Type.thy
changeset 14101 d25c23e46173
parent 13480 bb72bd43c6c3
child 14189 de58f4d939e1
     1.1 --- a/src/HOL/Product_Type.thy	Fri Jul 11 14:12:06 2003 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Jul 11 14:12:41 2003 +0200
     1.3 @@ -478,6 +478,10 @@
     1.4    apply blast
     1.5    done
     1.6  
     1.7 +lemma split_comp_eq [simp]: 
     1.8 +"(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
     1.9 +by (rule ext, auto)
    1.10 +
    1.11  lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)"
    1.12    by blast
    1.13  
    1.14 @@ -541,6 +545,19 @@
    1.15  qed
    1.16  
    1.17  
    1.18 +constdefs
    1.19 +  upd_fst :: "('a => 'c) => 'a * 'b => 'c * 'b"
    1.20 + "upd_fst f == prod_fun f id"
    1.21 +
    1.22 +  upd_snd :: "('b => 'c) => 'a * 'b => 'a * 'c"
    1.23 + "upd_snd f == prod_fun id f"
    1.24 +
    1.25 +lemma upd_fst_conv [simp]: "upd_fst f (x,y) = (f x,y)" 
    1.26 +by (simp add: upd_fst_def)
    1.27 +
    1.28 +lemma upd_snd_conv [simp]: "upd_snd f (x,y) = (x,f y)" 
    1.29 +by (simp add: upd_snd_def)
    1.30 +
    1.31  text {*
    1.32    \bigskip Disjoint union of a family of sets -- Sigma.
    1.33  *}