# HG changeset patch
# User paulson
# Date 1046366502 -3600
# Node ID 6d0392fc6dc5d2902dde1fb68bf54541d7b6f209
# Parent  12b2ffbe543a0b2035d9d305bd2d9b63cf9d677a
restored some deleted lemmas

diff -r 12b2ffbe543a -r 6d0392fc6dc5 src/HOL/UNITY/ELT.thy
--- a/src/HOL/UNITY/ELT.thy	Thu Feb 27 15:12:29 2003 +0100
+++ b/src/HOL/UNITY/ELT.thy	Thu Feb 27 18:21:42 2003 +0100
@@ -471,7 +471,7 @@
 apply (erule LeadsETo_subset_LeadsTo [THEN subsetD])
 (*right-to-left case*)
 apply (unfold LeadsETo_def LeadsTo_def)
-apply (fast elim: lel_lemma [THEN leadsETo_weaken])
+apply (blast intro: lel_lemma [THEN leadsETo_weaken])
 done
 
 
@@ -479,17 +479,17 @@
 
 lemma (in Extend) givenBy_o_eq_extend_set:
      "givenBy (v o f) = extend_set h ` (givenBy v)"
-by (simp add: givenBy_eq_Collect, best)
+apply (simp add: givenBy_eq_Collect)
+apply (rule equalityI, best)
+apply blast 
+done
 
 lemma (in Extend) givenBy_eq_extend_set: "givenBy f = range (extend_set h)"
-apply (simp (no_asm) add: givenBy_eq_Collect)
-apply best
-done
+by (simp add: givenBy_eq_Collect, best)
 
 lemma (in Extend) extend_set_givenBy_I:
      "D : givenBy v ==> extend_set h D : givenBy (v o f)"
-apply (simp (no_asm_use) add: givenBy_eq_all)
-apply blast
+apply (simp (no_asm_use) add: givenBy_eq_all, blast)
 done
 
 lemma (in Extend) leadsETo_imp_extend_leadsETo:
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}*}