src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
changeset 37805 0f797d586ce5
parent 37802 f2e9c104cebd
child 37806 a7679be14442
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 16:00:56 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 16:12:40 2010 +0200
     1.3 @@ -27,17 +27,17 @@
     1.4  declare swap.simps [simp del] rev.simps [simp del]
     1.5  
     1.6  lemma swap_pointwise: assumes "crel (swap a i j) h h' r"
     1.7 -  shows "get_array a h' ! k = (if k = i then get_array a h ! j
     1.8 -      else if k = j then get_array a h ! i
     1.9 -      else get_array a h ! k)"
    1.10 +  shows "get_array h' a ! k = (if k = i then get_array h a ! j
    1.11 +      else if k = j then get_array h a ! i
    1.12 +      else get_array h a ! k)"
    1.13  using assms unfolding swap.simps
    1.14  by (elim crel_elims)
    1.15   (auto simp: length_def)
    1.16  
    1.17  lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
    1.18 -  shows "get_array a h' ! k = (if k < i then get_array a h ! k
    1.19 -      else if j < k then get_array a h ! k
    1.20 -      else get_array a h ! (j - (k - i)))" (is "?P a i j h h'")
    1.21 +  shows "get_array h' a ! k = (if k < i then get_array h a ! k
    1.22 +      else if j < k then get_array h a ! k
    1.23 +      else get_array h a ! (j - (k - i)))" (is "?P a i j h h'")
    1.24  using assms proof (induct a i j arbitrary: h h' rule: rev.induct)
    1.25    case (1 a i j h h'')
    1.26    thus ?case
    1.27 @@ -94,7 +94,7 @@
    1.28    {
    1.29      fix k
    1.30      assume "k < Suc j - i"
    1.31 -    with rev_pointwise[OF assms(1)] have "get_array a h' ! (i + k) = get_array a h ! (j - k)"
    1.32 +    with rev_pointwise[OF assms(1)] have "get_array h' a ! (i + k) = get_array h a ! (j - k)"
    1.33        by auto
    1.34    } 
    1.35    with assms(2) rev_length[OF assms(1)] show ?thesis
    1.36 @@ -104,10 +104,10 @@
    1.37  
    1.38  lemma rev2_rev: 
    1.39    assumes "crel (rev a 0 (Array.length h a - 1)) h h' u"
    1.40 -  shows "get_array a h' = List.rev (get_array a h)"
    1.41 +  shows "get_array h' a = List.rev (get_array h a)"
    1.42    using rev2_rev'[OF assms] rev_length[OF assms] assms
    1.43      by (cases "Array.length h a = 0", auto simp add: Array.length_def
    1.44        subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
    1.45 -  (drule sym[of "List.length (get_array a h)"], simp)
    1.46 +  (drule sym[of "List.length (get_array h a)"], simp)
    1.47  
    1.48  end