diff -r 12b2ffbe543a -r 6d0392fc6dc5 src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Thu Feb 27 15:12:29 2003 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Thu Feb 27 18:21:42 2003 +0100
@@ -114,6 +114,34 @@
 lemma all_total_lift: "all_total F ==> all_total (lift i F)"
 by (simp add: lift_def rename_def Extend.all_total_extend)
 
+lemma insert_map_upd_same: "(insert_map i t f)(i := s) = insert_map i s f"
+by (rule ext, auto)
+
+lemma insert_map_upd:
+     "(insert_map j t f)(i := s) =  
+      (if i=j then insert_map i s f  
+       else if i<j then insert_map j t (f(i:=s))  
+       else insert_map j t (f(i - Suc 0 := s)))"
+apply (rule ext) 
+apply (simp split add: nat_diff_split) 
+ txt{*This simplification is VERY slow*}
+done
+
+lemma insert_map_eq_diff:
+     "[| insert_map i s f = insert_map j t g;  i\<noteq>j |]  
+      ==> \<exists>g'. insert_map i s' f = insert_map j t g'"
+apply (subst insert_map_upd_same [symmetric])
+apply (erule ssubst)
+apply (simp only: insert_map_upd if_False split: split_if, blast)
+done
+
+lemma lift_map_eq_diff: 
+     "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv));  i\<noteq>j |]  
+      ==> \<exists>g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))"
+apply (unfold lift_map_def, auto)
+apply (blast dest: insert_map_eq_diff)
+done
+
 
 subsection{*The Operator @{term lift_set}*}