src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
changeset 37719 271ecd4fb9f9
parent 36176 3fe7e97ccca8
child 37771 1bec64044b5e
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Jul 05 15:36:37 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Jul 05 16:46:23 2010 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4        else get_array a h ! k)"
     1.5  using assms unfolding swap.simps
     1.6  by (elim crel_elim_all)
     1.7 - (auto simp: Heap.length_def)
     1.8 + (auto simp: length_def)
     1.9  
    1.10  lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
    1.11    shows "get_array a h' ! k = (if k < i then get_array a h ! k
    1.12 @@ -69,7 +69,7 @@
    1.13  
    1.14  lemma rev_length:
    1.15    assumes "crel (rev a i j) h h' r"
    1.16 -  shows "Heap.length a h = Heap.length a h'"
    1.17 +  shows "Array.length a h = Array.length a h'"
    1.18  using assms
    1.19  proof (induct a i j arbitrary: h h' rule: rev.induct)
    1.20    case (1 a i j h h'')
    1.21 @@ -93,7 +93,7 @@
    1.22  qed
    1.23  
    1.24  lemma rev2_rev': assumes "crel (rev a i j) h h' u"
    1.25 -  assumes "j < Heap.length a h"
    1.26 +  assumes "j < Array.length a h"
    1.27    shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
    1.28  proof - 
    1.29    {
    1.30 @@ -103,15 +103,15 @@
    1.31        by auto
    1.32    } 
    1.33    with assms(2) rev_length[OF assms(1)] show ?thesis
    1.34 -  unfolding subarray_def Heap.length_def
    1.35 +  unfolding subarray_def Array.length_def
    1.36    by (auto simp add: length_sublist' rev_nth min_def nth_sublist' intro!: nth_equalityI)
    1.37  qed
    1.38  
    1.39  lemma rev2_rev: 
    1.40 -  assumes "crel (rev a 0 (Heap.length a h - 1)) h h' u"
    1.41 +  assumes "crel (rev a 0 (Array.length a h - 1)) h h' u"
    1.42    shows "get_array a h' = List.rev (get_array a h)"
    1.43    using rev2_rev'[OF assms] rev_length[OF assms] assms
    1.44 -    by (cases "Heap.length a h = 0", auto simp add: Heap.length_def
    1.45 +    by (cases "Array.length a h = 0", auto simp add: Array.length_def
    1.46        subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elim_all)
    1.47    (drule sym[of "List.length (get_array a h)"], simp)
    1.48