src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
author huffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 47255 30a1692557b0
parent 47108 2a1953f0d20d
child 50630 1ea90e8046dc
permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
bulwahn@36098
     1
(*  Title:      HOL/Imperative_HOL/ex/Imperative_Reverse.thy
bulwahn@36098
     2
    Author:     Lukas Bulwahn, TU Muenchen
bulwahn@36098
     3
*)
bulwahn@36098
     4
bulwahn@36098
     5
header {* An imperative in-place reversal on arrays *}
bulwahn@36098
     6
bulwahn@34051
     7
theory Imperative_Reverse
huffman@47108
     8
imports Subarray "~~/src/HOL/Imperative_HOL/Imperative_HOL"
bulwahn@34051
     9
begin
bulwahn@34051
    10
bulwahn@34051
    11
fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
krauss@37792
    12
  "swap a i j = do {
haftmann@37798
    13
     x \<leftarrow> Array.nth a i;
haftmann@37798
    14
     y \<leftarrow> Array.nth a j;
haftmann@37798
    15
     Array.upd i y a;
haftmann@37798
    16
     Array.upd j x a;
bulwahn@34051
    17
     return ()
krauss@37792
    18
   }"
bulwahn@34051
    19
bulwahn@34051
    20
fun rev :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
krauss@37792
    21
  "rev a i j = (if (i < j) then do {
bulwahn@34051
    22
     swap a i j;
bulwahn@34051
    23
     rev a (i + 1) (j - 1)
krauss@37792
    24
   }
bulwahn@34051
    25
   else return ())"
bulwahn@34051
    26
bulwahn@34051
    27
declare swap.simps [simp del] rev.simps [simp del]
bulwahn@34051
    28
haftmann@40671
    29
lemma swap_pointwise: assumes "effect (swap a i j) h h' r"
haftmann@37806
    30
  shows "Array.get h' a ! k = (if k = i then Array.get h a ! j
haftmann@37806
    31
      else if k = j then Array.get h a ! i
haftmann@37806
    32
      else Array.get h a ! k)"
bulwahn@34051
    33
using assms unfolding swap.simps
haftmann@40671
    34
by (elim effect_elims)
haftmann@37719
    35
 (auto simp: length_def)
bulwahn@34051
    36
haftmann@40671
    37
lemma rev_pointwise: assumes "effect (rev a i j) h h' r"
haftmann@37806
    38
  shows "Array.get h' a ! k = (if k < i then Array.get h a ! k
haftmann@37806
    39
      else if j < k then Array.get h a ! k
haftmann@37806
    40
      else Array.get h a ! (j - (k - i)))" (is "?P a i j h h'")
bulwahn@34051
    41
using assms proof (induct a i j arbitrary: h h' rule: rev.induct)
bulwahn@34051
    42
  case (1 a i j h h'')
bulwahn@34051
    43
  thus ?case
bulwahn@34051
    44
  proof (cases "i < j")
bulwahn@34051
    45
    case True
bulwahn@34051
    46
    with 1[unfolded rev.simps[of a i j]]
bulwahn@34051
    47
    obtain h' where
haftmann@40671
    48
      swp: "effect (swap a i j) h h' ()"
haftmann@40671
    49
      and rev: "effect (rev a (i + 1) (j - 1)) h' h'' ()"
haftmann@40671
    50
      by (auto elim: effect_elims)
bulwahn@34051
    51
    from rev 1 True
bulwahn@34051
    52
    have eq: "?P a (i + 1) (j - 1) h' h''" by auto
bulwahn@34051
    53
bulwahn@34051
    54
    have "k < i \<or> i = k \<or> (i < k \<and> k < j) \<or> j = k \<or> j < k" by arith
bulwahn@34051
    55
    with True show ?thesis
bulwahn@34051
    56
      by (elim disjE) (auto simp: eq swap_pointwise[OF swp])
bulwahn@34051
    57
  next
bulwahn@34051
    58
    case False
bulwahn@34051
    59
    with 1[unfolded rev.simps[of a i j]]
bulwahn@34051
    60
    show ?thesis
haftmann@40671
    61
      by (cases "k = j") (auto elim: effect_elims)
bulwahn@34051
    62
  qed
bulwahn@34051
    63
qed
bulwahn@34051
    64
bulwahn@34051
    65
lemma rev_length:
haftmann@40671
    66
  assumes "effect (rev a i j) h h' r"
haftmann@37802
    67
  shows "Array.length h a = Array.length h' a"
bulwahn@34051
    68
using assms
bulwahn@34051
    69
proof (induct a i j arbitrary: h h' rule: rev.induct)
bulwahn@34051
    70
  case (1 a i j h h'')
bulwahn@34051
    71
  thus ?case
bulwahn@34051
    72
  proof (cases "i < j")
bulwahn@34051
    73
    case True
bulwahn@34051
    74
    with 1[unfolded rev.simps[of a i j]]
bulwahn@34051
    75
    obtain h' where
haftmann@40671
    76
      swp: "effect (swap a i j) h h' ()"
haftmann@40671
    77
      and rev: "effect (rev a (i + 1) (j - 1)) h' h'' ()"
haftmann@40671
    78
      by (auto elim: effect_elims)
bulwahn@34051
    79
    from swp rev 1 True show ?thesis
bulwahn@34051
    80
      unfolding swap.simps
nipkow@44890
    81
      by (elim effect_elims) fastforce
bulwahn@34051
    82
  next
bulwahn@34051
    83
    case False
bulwahn@34051
    84
    with 1[unfolded rev.simps[of a i j]]
bulwahn@34051
    85
    show ?thesis
haftmann@40671
    86
      by (auto elim: effect_elims)
bulwahn@34051
    87
  qed
bulwahn@34051
    88
qed
bulwahn@34051
    89
haftmann@40671
    90
lemma rev2_rev': assumes "effect (rev a i j) h h' u"
haftmann@37802
    91
  assumes "j < Array.length h a"
bulwahn@34051
    92
  shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
bulwahn@34051
    93
proof - 
bulwahn@34051
    94
  {
bulwahn@34051
    95
    fix k
bulwahn@34051
    96
    assume "k < Suc j - i"
haftmann@37806
    97
    with rev_pointwise[OF assms(1)] have "Array.get h' a ! (i + k) = Array.get h a ! (j - k)"
bulwahn@34051
    98
      by auto
bulwahn@34051
    99
  } 
bulwahn@34051
   100
  with assms(2) rev_length[OF assms(1)] show ?thesis
haftmann@37719
   101
  unfolding subarray_def Array.length_def
bulwahn@34051
   102
  by (auto simp add: length_sublist' rev_nth min_def nth_sublist' intro!: nth_equalityI)
bulwahn@34051
   103
qed
bulwahn@34051
   104
bulwahn@34051
   105
lemma rev2_rev: 
haftmann@40671
   106
  assumes "effect (rev a 0 (Array.length h a - 1)) h h' u"
haftmann@37806
   107
  shows "Array.get h' a = List.rev (Array.get h a)"
bulwahn@34051
   108
  using rev2_rev'[OF assms] rev_length[OF assms] assms
haftmann@37802
   109
    by (cases "Array.length h a = 0", auto simp add: Array.length_def
huffman@47108
   110
      subarray_def rev.simps[where j=0] elim!: effect_elims)
haftmann@37806
   111
  (drule sym[of "List.length (Array.get h a)"], simp)
bulwahn@34051
   112
haftmann@38069
   113
definition "example = (Array.make 10 id \<guillemotright>= (\<lambda>a. rev a 0 9))"
haftmann@38058
   114
haftmann@38058
   115
export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
haftmann@37826
   116
bulwahn@34051
   117
end
huffman@47108
   118