# HG changeset patch
# User oheimb
# Date 1057925561 -7200
# Node ID d25c23e46173c51442f7cff966522699dac52040
# Parent  804be4c4b642fdcd4600a55a8cdc974a7310ef32
added upd_fst, upd_snd, some thms

diff -r 804be4c4b642 -r d25c23e46173 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Jul 11 14:12:06 2003 +0200
+++ b/src/HOL/Product_Type.thy	Fri Jul 11 14:12:41 2003 +0200
@@ -478,6 +478,10 @@
   apply blast
   done
 
+lemma split_comp_eq [simp]: 
+"(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
+by (rule ext, auto)
+
 lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)"
   by blast
 
@@ -541,6 +545,19 @@
 qed
 
 
+constdefs
+  upd_fst :: "('a => 'c) => 'a * 'b => 'c * 'b"
+ "upd_fst f == prod_fun f id"
+
+  upd_snd :: "('b => 'c) => 'a * 'b => 'a * 'c"
+ "upd_snd f == prod_fun id f"
+
+lemma upd_fst_conv [simp]: "upd_fst f (x,y) = (f x,y)" 
+by (simp add: upd_fst_def)
+
+lemma upd_snd_conv [simp]: "upd_snd f (x,y) = (x,f y)" 
+by (simp add: upd_snd_def)
+
 text {*
   \bigskip Disjoint union of a family of sets -- Sigma.
 *}
diff -r 804be4c4b642 -r d25c23e46173 src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Fri Jul 11 14:12:06 2003 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy	Fri Jul 11 14:12:41 2003 +0200
@@ -257,7 +257,7 @@
 lemma lift_preserves_snd_I: "F \<in> preserves snd ==> lift i F \<in> preserves snd"
 apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD])
 apply (simp add: lift_def rename_preserves)
-apply (simp add: lift_map_def o_def split_def)
+apply (simp add: lift_map_def o_def split_def del: split_comp_eq)
 done
 
 lemma delete_map_eqE':
@@ -332,7 +332,7 @@
 apply (drule subset_preserves_o [THEN subsetD])
 apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq)
 apply (auto cong del: if_weak_cong 
-            simp add: lift_map_def eq_commute split_def o_def)
+       simp add: lift_map_def eq_commute split_def o_def simp del:split_comp_eq)
 done