src/HOL/Library/Relational.thy

 next
   case (Cons x xs)
   from Cons(2) obtain h1 y ys where crel_f: "crel (f x) h h1 y"
     and crel_mapM: "crel (mapM f xs) h1 h' ys"
     and r_def: "r = y#ys"
-    unfolding mapM.simps run_drop
+    unfolding mapM.simps
     by (auto elim!: crelE crel_return)
   from Cons(1)[OF crel_mapM] crel_mapM crel_f assms(3) r_def
   show ?case by auto
 qed
 

 
 lemma crel_nth[consumes 1]:
   assumes "crel (nth a i) h h' r"
   obtains "r = (get_array a h) ! i" "h = h'" "i < Heap.length a h"
   using assms
-  unfolding nth_def run_drop
+  unfolding nth_def
   by (auto elim!: crelE crel_if crel_raise crel_length crel_heap)
 
 lemma crel_upd[consumes 1]:
   assumes "crel (upd i v a) h h' r"
   obtains "r = a" "h' = Heap.upd a i v h"
   using assms
-  unfolding upd_def run_drop
+  unfolding upd_def
   by (elim crelE crel_if crel_return crel_raise
     crel_length crel_heap) auto
 
 (* Strong version of the lemma for this operation is missing *)
 lemma crel_of_list_weak:

 
 lemma crel_map_entry:
   assumes "crel (Array.map_entry i f a) h h' r"
   obtains "r = a" "h' = Heap.upd a i (f (get_array a h ! i)) h"
   using assms
-  unfolding Array.map_entry_def run_drop
+  unfolding Array.map_entry_def
   by (elim crelE crel_upd crel_nth) auto
 
 lemma crel_swap:
   assumes "crel (Array.swap i x a) h h' r"
   obtains "r = get_array a h ! i" "h' = Heap.upd a i x h"
   using assms
-  unfolding Array.swap_def run_drop
+  unfolding Array.swap_def
   by (elim crelE crel_upd crel_nth crel_return) auto
 
 (* Strong version of the lemma for this operation is missing *)
 lemma crel_make_weak:
   assumes "crel (Array.make n f) h h' r"

   from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
     by (simp add: upt_conv_Cons')
   with Suc(2) obtain r where
     crel_mapM: "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' r"
     and xs_def: "xs = get_array a h ! (Heap.length a h - Suc n) # r"
-    by (auto simp add: run_drop elim!: crelE crel_nth crel_return)
+    by (auto elim!: crelE crel_nth crel_return)
   from Suc(3) have "Heap.length a h - n = Suc (Heap.length a h - Suc n)" 
     by arith
   with Suc.hyps[OF crel_mapM] xs_def show ?case
     unfolding Heap.length_def
     by (auto simp add: nth_drop')

 lemma crel_freeze:
   assumes "crel (Array.freeze a) h h' xs"
   obtains "h = h'" "xs = get_array a h"
 proof 
   from assms have "crel (mapM (Array.nth a) [0..<Heap.length a h]) h h' xs"
-    unfolding freeze_def run_drop
+    unfolding freeze_def
     by (auto elim: crelE crel_length)
   hence "crel (mapM (Array.nth a) [(Heap.length a h - Heap.length a h)..<Heap.length a h]) h h' xs"
     by simp
   from crel_mapM_nth[OF this] show "h = h'" and "xs = get_array a h" by auto
 qed

   let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
   from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
     by (simp add: upt_conv_Cons')
   from Suc(2) this obtain r where
     crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
-    by (auto simp add: run_drop elim!: crelE crel_map_entry crel_return)
+    by (auto simp add: elim!: crelE crel_map_entry crel_return)
   have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
   from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
     by simp
   from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
 qed

   let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
   from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
     by (simp add: upt_conv_Cons')
   from Suc(2) this obtain r where
     crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
-    by (auto simp add: run_drop elim!: crelE crel_map_entry crel_return)
+    by (auto simp add: elim!: crelE crel_map_entry crel_return)
   have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
   from Suc(3) have less: "Heap.length a h - Suc n < Heap.length a h - n" by arith
   from Suc(3) have less2: "Heap.length a h - Suc n < Heap.length a h" by arith
   from Suc(4) length_remains have cases: "i = Heap.length a ?h1 - Suc n \<or> i \<ge> Heap.length a ?h1 - n" by arith
   from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"

   let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
   from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
     by (simp add: upt_conv_Cons')
   from Suc(2) this obtain r where 
     crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
-    by (auto simp add: run_drop elim!: crelE crel_map_entry crel_return)
+    by (auto elim!: crelE crel_map_entry crel_return)
   have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
   from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
     by simp
   from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
 qed

 lemma crel_map_weak:
   assumes crel_map: "crel (Array.map f a) h h' r"
   obtains "r = a" "get_array a h' = List.map f (get_array a h)"
 proof
   from assms crel_mapM_map_entry show  "get_array a h' = List.map f (get_array a h)"
-    unfolding Array.map_def run_drop
+    unfolding Array.map_def
     by (fastsimp elim!: crelE crel_length crel_return)
   from assms show "r = a"
-    unfolding Array.map_def run_drop
+    unfolding Array.map_def
     by (elim crelE crel_return)
 qed
 
 subsection {* Elimination rules for reference commands *}
 

 
 lemma crel_change:
   assumes "crel (Ref.change f ref) h h' r"
   obtains "h' = set_ref ref (f (get_ref ref h)) h" "r = f (get_ref ref h)"
 using assms
-unfolding Ref.change_def run_drop Let_def
+unfolding Ref.change_def Let_def
 by (auto elim!: crelE crel_lookup crel_update crel_return)
 
 subsection {* Elimination rules for the assert command *}
 
 lemma crel_assert[consumes 1]:

 
 lemma crel_nthI:
   assumes "i < Heap.length a h"
   shows "crel (nth a i) h h ((get_array a h) ! i)"
   using assms
-  unfolding nth_def run_drop
+  unfolding nth_def
   by (auto intro!: crelI crel_ifI crel_raiseI crel_lengthI crel_heapI')
 
 lemma crel_updI:
   assumes "i < Heap.length a h"
   shows "crel (upd i v a) h (Heap.upd a i v h) a"
   using assms
-  unfolding upd_def run_drop
+  unfolding upd_def
   by (auto intro!: crelI crel_ifI crel_returnI crel_raiseI
     crel_lengthI crel_heapI')
 
 (* thm crel_of_listI is missing *)
 

   shows "crel (ref := v) h (set_ref ref v h) ()"
   unfolding update_def by (auto intro!: crel_heapI')
 
 lemma crel_changeI: 
   shows "crel (Ref.change f ref) h (set_ref ref (f (get_ref ref h)) h) (f (get_ref ref h))"
-unfolding change_def Let_def run_drop by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
+unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
 
 subsection {* Introduction rules for the assert command *}
 
 lemma crel_assertI:
   assumes "P x"

   thus ?case
     unfolding mapM.simps by (intro noError_return)
 next
   case (Cons x xs)
   thus ?case
-    unfolding mapM.simps run_drop
+    unfolding mapM.simps
     by (auto intro: noErrorI2[of "f x"] noErrorI noError_return)
 qed
 
 lemma noError_heap:
   shows "noError (Heap_Monad.heap f) h"

 
 lemma noError_upd:
   assumes "i < Heap.length a h"
   shows "noError (Array.upd i v a) h"
   using assms
-  unfolding upd_def run_drop
+  unfolding upd_def
   by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
 
 lemma noError_nth:
 assumes "i < Heap.length a h"
   shows "noError (Array.nth a i) h"
   using assms
-  unfolding nth_def run_drop
+  unfolding nth_def
   by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
 
 lemma noError_of_list:
   shows "noError (of_list ls) h"
   unfolding of_list_def by (rule noError_heap)
 
 lemma noError_map_entry:
   assumes "i < Heap.length a h"
   shows "noError (map_entry i f a) h"
   using assms
-  unfolding map_entry_def run_drop
+  unfolding map_entry_def
   by (auto elim: crel_nth intro!: noErrorI noError_nth noError_upd)
 
 lemma noError_swap:
   assumes "i < Heap.length a h"
   shows "noError (swap i x a) h"
   using assms
-  unfolding swap_def run_drop
+  unfolding swap_def
   by (auto elim: crel_nth intro!: noErrorI noError_return noError_nth noError_upd)
 
 lemma noError_make:
   shows "noError (make n f) h"
   unfolding make_def

   "mapM f (xs @ ys) = mapM f xs \<guillemotright>= (\<lambda>xs. mapM f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
   by (induct xs) (simp_all add: monad_simp)
 
 lemma noError_freeze:
   shows "noError (freeze a) h"
-unfolding freeze_def run_drop
+unfolding freeze_def
 by (auto intro!: noErrorI noError_length noError_mapM[of _ _ _ "\<lambda>x. get_array a h ! x"]
   noError_nth crel_nthI elim: crel_length)
 
 lemma noError_mapM_map_entry:
   assumes "n \<le> Heap.length a h"

 next
   case (Suc n)
   from Suc.prems have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
     by (simp add: upt_conv_Cons')
   with Suc.hyps[of "(Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h)"] Suc.prems show ?case
-    by (auto simp add: run_drop intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
+    by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
 qed
 
 lemma noError_map:
   shows "noError (Array.map f a) h"
 using noError_mapM_map_entry[of "Heap.length a h" a h]
-unfolding Array.map_def run_drop
+unfolding Array.map_def
 by (auto intro: noErrorI noError_length noError_return elim!: crel_length)
 
 subsection {* Introduction rules for the reference commands *}
 
 lemma noError_Ref_new:

   shows "noError (ref := v) h"
   unfolding update_def by (intro noError_heap)
 
 lemma noError_change:
   shows "noError (Ref.change f ref) h"
-  unfolding Ref.change_def run_drop Let_def by (intro noErrorI noError_lookup noError_update noError_return)
+  unfolding Ref.change_def Let_def by (intro noErrorI noError_lookup noError_update noError_return)
 
 subsection {* Introduction rules for the assert command *}
 
 lemma noError_assert:
   assumes "P x"