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