src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
 changeset 37802 f2e9c104cebd parent 37798 0b0570445a2a child 37805 0f797d586ce5
```     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 11:23:21 2010 +0100
1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 15:34:02 2010 +0200
1.3 @@ -64,7 +64,7 @@
1.4
1.5  lemma rev_length:
1.6    assumes "crel (rev a i j) h h' r"
1.7 -  shows "Array.length a h = Array.length a h'"
1.8 +  shows "Array.length h a = Array.length h' a"
1.9  using assms
1.10  proof (induct a i j arbitrary: h h' rule: rev.induct)
1.11    case (1 a i j h h'')
1.12 @@ -88,7 +88,7 @@
1.13  qed
1.14
1.15  lemma rev2_rev': assumes "crel (rev a i j) h h' u"
1.16 -  assumes "j < Array.length a h"
1.17 +  assumes "j < Array.length h a"
1.18    shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
1.19  proof -
1.20    {
1.21 @@ -103,10 +103,10 @@
1.22  qed
1.23
1.24  lemma rev2_rev:
1.25 -  assumes "crel (rev a 0 (Array.length a h - 1)) h h' u"
1.26 +  assumes "crel (rev a 0 (Array.length h a - 1)) h h' u"
1.27    shows "get_array a h' = List.rev (get_array a h)"
1.28    using rev2_rev'[OF assms] rev_length[OF assms] assms
1.29 -    by (cases "Array.length a h = 0", auto simp add: Array.length_def
1.30 +    by (cases "Array.length h a = 0", auto simp add: Array.length_def
1.31        subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
1.32    (drule sym[of "List.length (get_array a h)"], simp)
1.33
```