src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy

   shows "get_array a h' ! k = (if k = i then get_array a h ! j
       else if k = j then get_array a h ! i
       else get_array a h ! k)"
 using assms unfolding swap.simps
 by (elim crel_elim_all)
- (auto simp: Heap.length_def)
+ (auto simp: length_def)
 
 lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
   shows "get_array a h' ! k = (if k < i then get_array a h ! k
       else if j < k then get_array a h ! k
       else get_array a h ! (j - (k - i)))" (is "?P a i j h h'")

   qed
 qed
 
 lemma rev_length:
   assumes "crel (rev a i j) h h' r"
-  shows "Heap.length a h = Heap.length a h'"
+  shows "Array.length a h = Array.length a h'"
 using assms
 proof (induct a i j arbitrary: h h' rule: rev.induct)
   case (1 a i j h h'')
   thus ?case
   proof (cases "i < j")

       by (auto elim: crel_elim_all)
   qed
 qed
 
 lemma rev2_rev': assumes "crel (rev a i j) h h' u"
-  assumes "j < Heap.length a h"
+  assumes "j < Array.length a h"
   shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
 proof - 
   {
     fix k
     assume "k < Suc j - i"
     with rev_pointwise[OF assms(1)] have "get_array a h' ! (i + k) = get_array a h ! (j - k)"
       by auto
   } 
   with assms(2) rev_length[OF assms(1)] show ?thesis
-  unfolding subarray_def Heap.length_def
+  unfolding subarray_def Array.length_def
   by (auto simp add: length_sublist' rev_nth min_def nth_sublist' intro!: nth_equalityI)
 qed
 
 lemma rev2_rev: 
-  assumes "crel (rev a 0 (Heap.length a h - 1)) h h' u"
+  assumes "crel (rev a 0 (Array.length a h - 1)) h h' u"
   shows "get_array a h' = List.rev (get_array a h)"
   using rev2_rev'[OF assms] rev_length[OF assms] assms
-    by (cases "Heap.length a h = 0", auto simp add: Heap.length_def
+    by (cases "Array.length a h = 0", auto simp add: Array.length_def
       subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elim_all)
   (drule sym[of "List.length (get_array a h)"], simp)
 
 end