src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
 author wenzelm Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) changeset 58889 5b7a9633cfa8 parent 50630 1ea90e8046dc child 61076 bdc1e2f0a86a permissions -rw-r--r--
```     1 (*  Title:      HOL/Imperative_HOL/ex/Imperative_Reverse.thy
```
```     2     Author:     Lukas Bulwahn, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 section {* An imperative in-place reversal on arrays *}
```
```     6
```
```     7 theory Imperative_Reverse
```
```     8 imports Subarray "~~/src/HOL/Imperative_HOL/Imperative_HOL"
```
```     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    }"
```
```    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    }
```
```    25    else return ())"
```
```    26
```
```    27 declare swap.simps [simp del] rev.simps [simp del]
```
```    28
```
```    29 lemma swap_pointwise: assumes "effect (swap a i j) h h' r"
```
```    30   shows "Array.get h' a ! k = (if k = i then Array.get h a ! j
```
```    31       else if k = j then Array.get h a ! i
```
```    32       else Array.get h a ! k)"
```
```    33 using assms unfolding swap.simps
```
```    34 by (elim effect_elims)
```
```    35  (auto simp: length_def)
```
```    36
```
```    37 lemma rev_pointwise: assumes "effect (rev a i j) h h' r"
```
```    38   shows "Array.get h' a ! k = (if k < i then Array.get h a ! k
```
```    39       else if j < k then Array.get h a ! k
```
```    40       else Array.get h a ! (j - (k - i)))" (is "?P a i j h h'")
```
```    41 using assms proof (induct a i j arbitrary: h h' rule: rev.induct)
```
```    42   case (1 a i j h h'')
```
```    43   thus ?case
```
```    44   proof (cases "i < j")
```
```    45     case True
```
```    46     with 1[unfolded rev.simps[of a i j]]
```
```    47     obtain h' where
```
```    48       swp: "effect (swap a i j) h h' ()"
```
```    49       and rev: "effect (rev a (i + 1) (j - 1)) h' h'' ()"
```
```    50       by (auto elim: effect_elims)
```
```    51     from rev 1 True
```
```    52     have eq: "?P a (i + 1) (j - 1) h' h''" by auto
```
```    53
```
```    54     have "k < i \<or> i = k \<or> (i < k \<and> k < j) \<or> j = k \<or> j < k" by arith
```
```    55     with True show ?thesis
```
```    56       by (elim disjE) (auto simp: eq swap_pointwise[OF swp])
```
```    57   next
```
```    58     case False
```
```    59     with 1[unfolded rev.simps[of a i j]]
```
```    60     show ?thesis
```
```    61       by (cases "k = j") (auto elim: effect_elims)
```
```    62   qed
```
```    63 qed
```
```    64
```
```    65 lemma rev_length:
```
```    66   assumes "effect (rev a i j) h h' r"
```
```    67   shows "Array.length h a = Array.length h' a"
```
```    68 using assms
```
```    69 proof (induct a i j arbitrary: h h' rule: rev.induct)
```
```    70   case (1 a i j h h'')
```
```    71   thus ?case
```
```    72   proof (cases "i < j")
```
```    73     case True
```
```    74     with 1[unfolded rev.simps[of a i j]]
```
```    75     obtain h' where
```
```    76       swp: "effect (swap a i j) h h' ()"
```
```    77       and rev: "effect (rev a (i + 1) (j - 1)) h' h'' ()"
```
```    78       by (auto elim: effect_elims)
```
```    79     from swp rev 1 True show ?thesis
```
```    80       unfolding swap.simps
```
```    81       by (elim effect_elims) fastforce
```
```    82   next
```
```    83     case False
```
```    84     with 1[unfolded rev.simps[of a i j]]
```
```    85     show ?thesis
```
```    86       by (auto elim: effect_elims)
```
```    87   qed
```
```    88 qed
```
```    89
```
```    90 lemma rev2_rev': assumes "effect (rev a i j) h h' u"
```
```    91   assumes "j < Array.length h a"
```
```    92   shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
```
```    93 proof -
```
```    94   {
```
```    95     fix k
```
```    96     assume "k < Suc j - i"
```
```    97     with rev_pointwise[OF assms(1)] have "Array.get h' a ! (i + k) = Array.get h a ! (j - k)"
```
```    98       by auto
```
```    99   }
```
```   100   with assms(2) rev_length[OF assms(1)] show ?thesis
```
```   101   unfolding subarray_def Array.length_def
```
```   102   by (auto simp add: length_sublist' rev_nth min_def nth_sublist' intro!: nth_equalityI)
```
```   103 qed
```
```   104
```
```   105 lemma rev2_rev:
```
```   106   assumes "effect (rev a 0 (Array.length h a - 1)) h h' u"
```
```   107   shows "Array.get h' a = List.rev (Array.get h a)"
```
```   108   using rev2_rev'[OF assms] rev_length[OF assms] assms
```
```   109     by (cases "Array.length h a = 0", auto simp add: Array.length_def
```
```   110       subarray_def rev.simps[where j=0] elim!: effect_elims)
```
```   111   (drule sym[of "List.length (Array.get h a)"], simp)
```
```   112
```
```   113 definition "example = (Array.make 10 id \<guillemotright>= (\<lambda>a. rev a 0 9))"
```
```   114
```
```   115 export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
```
```   116
```
```   117 end
```
```   118
```