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
```