src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
author haftmann
Tue Jul 13 12:01:34 2010 +0200 (2010-07-13 ago)
changeset 37796 08bd610b2583
parent 37771 1bec64044b5e
child 37797 96551d6b1414
permissions -rw-r--r--
hide_const; update replaces change
     1 (*  Title:      HOL/Imperative_HOL/ex/Imperative_Reverse.thy
     2     Author:     Lukas Bulwahn, TU Muenchen
     3 *)
     4 
     5 header {* An imperative in-place reversal on arrays *}
     6 
     7 theory Imperative_Reverse
     8 imports Imperative_HOL Subarray
     9 begin
    10 
    11 fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
    12   "swap a i j = (do
    13      x \<leftarrow> Array.nth a i;
    14      y \<leftarrow> Array.nth a j;
    15      Array.upd i y a;
    16      Array.upd j x a;
    17      return ()
    18    done)"
    19 
    20 fun rev :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
    21   "rev a i j = (if (i < j) then (do
    22      swap a i j;
    23      rev a (i + 1) (j - 1)
    24    done)
    25    else return ())"
    26 
    27 notation (output) swap ("swap")
    28 notation (output) rev ("rev")
    29 
    30 declare swap.simps [simp del] rev.simps [simp del]
    31 
    32 lemma swap_pointwise: assumes "crel (swap a i j) h h' r"
    33   shows "get_array a h' ! k = (if k = i then get_array a h ! j
    34       else if k = j then get_array a h ! i
    35       else get_array a h ! k)"
    36 using assms unfolding swap.simps
    37 by (elim crel_elims)
    38  (auto simp: length_def)
    39 
    40 lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
    41   shows "get_array a h' ! k = (if k < i then get_array a h ! k
    42       else if j < k then get_array a h ! k
    43       else get_array a h ! (j - (k - i)))" (is "?P a i j h h'")
    44 using assms proof (induct a i j arbitrary: h h' rule: rev.induct)
    45   case (1 a i j h h'')
    46   thus ?case
    47   proof (cases "i < j")
    48     case True
    49     with 1[unfolded rev.simps[of a i j]]
    50     obtain h' where
    51       swp: "crel (swap a i j) h h' ()"
    52       and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()"
    53       by (auto elim: crel_elims)
    54     from rev 1 True
    55     have eq: "?P a (i + 1) (j - 1) h' h''" by auto
    56 
    57     have "k < i \<or> i = k \<or> (i < k \<and> k < j) \<or> j = k \<or> j < k" by arith
    58     with True show ?thesis
    59       by (elim disjE) (auto simp: eq swap_pointwise[OF swp])
    60   next
    61     case False
    62     with 1[unfolded rev.simps[of a i j]]
    63     show ?thesis
    64       by (cases "k = j") (auto elim: crel_elims)
    65   qed
    66 qed
    67 
    68 lemma rev_length:
    69   assumes "crel (rev a i j) h h' r"
    70   shows "Array.length a h = Array.length a h'"
    71 using assms
    72 proof (induct a i j arbitrary: h h' rule: rev.induct)
    73   case (1 a i j h h'')
    74   thus ?case
    75   proof (cases "i < j")
    76     case True
    77     with 1[unfolded rev.simps[of a i j]]
    78     obtain h' where
    79       swp: "crel (swap a i j) h h' ()"
    80       and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()"
    81       by (auto elim: crel_elims)
    82     from swp rev 1 True show ?thesis
    83       unfolding swap.simps
    84       by (elim crel_elims) fastsimp
    85   next
    86     case False
    87     with 1[unfolded rev.simps[of a i j]]
    88     show ?thesis
    89       by (auto elim: crel_elims)
    90   qed
    91 qed
    92 
    93 lemma rev2_rev': assumes "crel (rev a i j) h h' u"
    94   assumes "j < Array.length a h"
    95   shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
    96 proof - 
    97   {
    98     fix k
    99     assume "k < Suc j - i"
   100     with rev_pointwise[OF assms(1)] have "get_array a h' ! (i + k) = get_array a h ! (j - k)"
   101       by auto
   102   } 
   103   with assms(2) rev_length[OF assms(1)] show ?thesis
   104   unfolding subarray_def Array.length_def
   105   by (auto simp add: length_sublist' rev_nth min_def nth_sublist' intro!: nth_equalityI)
   106 qed
   107 
   108 lemma rev2_rev: 
   109   assumes "crel (rev a 0 (Array.length a h - 1)) h h' u"
   110   shows "get_array a h' = List.rev (get_array a h)"
   111   using rev2_rev'[OF assms] rev_length[OF assms] assms
   112     by (cases "Array.length a h = 0", auto simp add: Array.length_def
   113       subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
   114   (drule sym[of "List.length (get_array a h)"], simp)
   115 
   116 end