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