src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
 author bulwahn Thu Apr 08 08:17:27 2010 +0200 (2010-04-08 ago) changeset 36098 53992c639da5 parent 34051 1a82e2e29d67 child 36176 3fe7e97ccca8 permissions -rw-r--r--
```     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 (open) const 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: Heap.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 "Heap.length a h = Heap.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 < Heap.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 Heap.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 (Heap.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 "Heap.length a h = 0", auto simp add: Heap.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
```