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