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