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--
modernized header uniformly as section;
     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