src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
author haftmann
Wed, 14 Jul 2010 16:13:14 +0200
changeset 37826 4c0a5e35931a
parent 37806 a7679be14442
child 37845 b70d7a347964
permissions -rw-r--r--
avoid export_code ... file -
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents: 34051
diff changeset
     1
(*  Title:      HOL/Imperative_HOL/ex/Imperative_Reverse.thy
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents: 34051
diff changeset
     2
    Author:     Lukas Bulwahn, TU Muenchen
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents: 34051
diff changeset
     3
*)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents: 34051
diff changeset
     4
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents: 34051
diff changeset
     5
header {* An imperative in-place reversal on arrays *}
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents: 34051
diff changeset
     6
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
     7
theory Imperative_Reverse
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37719
diff changeset
     8
imports Imperative_HOL Subarray
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
     9
begin
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    10
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    11
fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
37792
ba0bc31b90d7 Heap_Monad uses Monad_Syntax
krauss
parents: 37771
diff changeset
    12
  "swap a i j = do {
37798
0b0570445a2a proper merge of operation changes and generic do-syntax
haftmann
parents: 37797
diff changeset
    13
     x \<leftarrow> Array.nth a i;
0b0570445a2a proper merge of operation changes and generic do-syntax
haftmann
parents: 37797
diff changeset
    14
     y \<leftarrow> Array.nth a j;
0b0570445a2a proper merge of operation changes and generic do-syntax
haftmann
parents: 37797
diff changeset
    15
     Array.upd i y a;
0b0570445a2a proper merge of operation changes and generic do-syntax
haftmann
parents: 37797
diff changeset
    16
     Array.upd j x a;
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    17
     return ()
37792
ba0bc31b90d7 Heap_Monad uses Monad_Syntax
krauss
parents: 37771
diff changeset
    18
   }"
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    19
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    20
fun rev :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
37792
ba0bc31b90d7 Heap_Monad uses Monad_Syntax
krauss
parents: 37771
diff changeset
    21
  "rev a i j = (if (i < j) then do {
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    22
     swap a i j;
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    23
     rev a (i + 1) (j - 1)
37792
ba0bc31b90d7 Heap_Monad uses Monad_Syntax
krauss
parents: 37771
diff changeset
    24
   }
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    25
   else return ())"
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    26
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    27
declare swap.simps [simp del] rev.simps [simp del]
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    28
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    29
lemma swap_pointwise: assumes "crel (swap a i j) h h' r"
37806
a7679be14442 qualified names for (really) all array operations
haftmann
parents: 37805
diff changeset
    30
  shows "Array.get h' a ! k = (if k = i then Array.get h a ! j
a7679be14442 qualified names for (really) all array operations
haftmann
parents: 37805
diff changeset
    31
      else if k = j then Array.get h a ! i
a7679be14442 qualified names for (really) all array operations
haftmann
parents: 37805
diff changeset
    32
      else Array.get h a ! k)"
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    33
using assms unfolding swap.simps
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37719
diff changeset
    34
by (elim crel_elims)
37719
271ecd4fb9f9 moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents: 36176
diff changeset
    35
 (auto simp: length_def)
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    36
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    37
lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
37806
a7679be14442 qualified names for (really) all array operations
haftmann
parents: 37805
diff changeset
    38
  shows "Array.get h' a ! k = (if k < i then Array.get h a ! k
a7679be14442 qualified names for (really) all array operations
haftmann
parents: 37805
diff changeset
    39
      else if j < k then Array.get h a ! k
a7679be14442 qualified names for (really) all array operations
haftmann
parents: 37805
diff changeset
    40
      else Array.get h a ! (j - (k - i)))" (is "?P a i j h h'")
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    41
using assms proof (induct a i j arbitrary: h h' rule: rev.induct)
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    42
  case (1 a i j h h'')
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    43
  thus ?case
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    44
  proof (cases "i < j")
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    45
    case True
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    46
    with 1[unfolded rev.simps[of a i j]]
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    47
    obtain h' where
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    48
      swp: "crel (swap a i j) h h' ()"
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    49
      and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()"
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37719
diff changeset
    50
      by (auto elim: crel_elims)
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    51
    from rev 1 True
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    52
    have eq: "?P a (i + 1) (j - 1) h' h''" by auto
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    53
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    54
    have "k < i \<or> i = k \<or> (i < k \<and> k < j) \<or> j = k \<or> j < k" by arith
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    55
    with True show ?thesis
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    56
      by (elim disjE) (auto simp: eq swap_pointwise[OF swp])
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    57
  next
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    58
    case False
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    59
    with 1[unfolded rev.simps[of a i j]]
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    60
    show ?thesis
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37719
diff changeset
    61
      by (cases "k = j") (auto elim: crel_elims)
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    62
  qed
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    63
qed
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    64
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    65
lemma rev_length:
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    66
  assumes "crel (rev a i j) h h' r"
37802
f2e9c104cebd canonical argument order for length
haftmann
parents: 37798
diff changeset
    67
  shows "Array.length h a = Array.length h' a"
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    68
using assms
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    69
proof (induct a i j arbitrary: h h' rule: rev.induct)
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    70
  case (1 a i j h h'')
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    71
  thus ?case
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    72
  proof (cases "i < j")
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    73
    case True
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    74
    with 1[unfolded rev.simps[of a i j]]
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    75
    obtain h' where
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    76
      swp: "crel (swap a i j) h h' ()"
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    77
      and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()"
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37719
diff changeset
    78
      by (auto elim: crel_elims)
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    79
    from swp rev 1 True show ?thesis
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    80
      unfolding swap.simps
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37719
diff changeset
    81
      by (elim crel_elims) fastsimp
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    82
  next
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    83
    case False
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    84
    with 1[unfolded rev.simps[of a i j]]
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    85
    show ?thesis
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37719
diff changeset
    86
      by (auto elim: crel_elims)
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    87
  qed
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    88
qed
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    89
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    90
lemma rev2_rev': assumes "crel (rev a i j) h h' u"
37802
f2e9c104cebd canonical argument order for length
haftmann
parents: 37798
diff changeset
    91
  assumes "j < Array.length h a"
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    92
  shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    93
proof - 
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    94
  {
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    95
    fix k
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    96
    assume "k < Suc j - i"
37806
a7679be14442 qualified names for (really) all array operations
haftmann
parents: 37805
diff changeset
    97
    with rev_pointwise[OF assms(1)] have "Array.get h' a ! (i + k) = Array.get h a ! (j - k)"
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    98
      by auto
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    99
  } 
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
   100
  with assms(2) rev_length[OF assms(1)] show ?thesis
37719
271ecd4fb9f9 moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents: 36176
diff changeset
   101
  unfolding subarray_def Array.length_def
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
   102
  by (auto simp add: length_sublist' rev_nth min_def nth_sublist' intro!: nth_equalityI)
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
   103
qed
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
   104
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
   105
lemma rev2_rev: 
37802
f2e9c104cebd canonical argument order for length
haftmann
parents: 37798
diff changeset
   106
  assumes "crel (rev a 0 (Array.length h a - 1)) h h' u"
37806
a7679be14442 qualified names for (really) all array operations
haftmann
parents: 37805
diff changeset
   107
  shows "Array.get h' a = List.rev (Array.get h a)"
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
   108
  using rev2_rev'[OF assms] rev_length[OF assms] assms
37802
f2e9c104cebd canonical argument order for length
haftmann
parents: 37798
diff changeset
   109
    by (cases "Array.length h a = 0", auto simp add: Array.length_def
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37719
diff changeset
   110
      subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
37806
a7679be14442 qualified names for (really) all array operations
haftmann
parents: 37805
diff changeset
   111
  (drule sym[of "List.length (Array.get h a)"], simp)
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
   112
37826
4c0a5e35931a avoid export_code ... file -
haftmann
parents: 37806
diff changeset
   113
export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell?
4c0a5e35931a avoid export_code ... file -
haftmann
parents: 37806
diff changeset
   114
34051
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
   115
end