src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
author haftmann
Tue, 13 Jul 2010 12:05:20 +0200
changeset 37797 96551d6b1414
parent 37792 ba0bc31b90d7
parent 37796 08bd610b2583
child 37798 0b0570445a2a
permissions -rw-r--r--
merged
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
36176
3fe7e97ccca8 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents: 36098
diff changeset
    11
hide_const (open) swap rev
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
    12
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    13
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
    14
  "swap a i j = 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
    15
     x \<leftarrow> nth a i;
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    16
     y \<leftarrow> nth a 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
    17
     upd i y a;
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    18
     upd j x a;
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
     return ()
37792
ba0bc31b90d7 Heap_Monad uses Monad_Syntax
krauss
parents: 37771
diff changeset
    20
   }"
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
    21
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
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
    23
  "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
    24
     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
    25
     rev a (i + 1) (j - 1)
37792
ba0bc31b90d7 Heap_Monad uses Monad_Syntax
krauss
parents: 37771
diff changeset
    26
   }
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
    27
   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
    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
notation (output) swap ("swap")
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    30
notation (output) rev ("rev")
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    31
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    32
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
    33
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    34
lemma swap_pointwise: assumes "crel (swap a i j) h h' r"
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
    35
  shows "get_array a h' ! k = (if k = i then get_array a h ! 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
    36
      else if k = j then get_array a h ! i
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
      else get_array a h ! 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
    38
using assms unfolding swap.simps
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37719
diff changeset
    39
by (elim crel_elims)
37719
271ecd4fb9f9 moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents: 36176
diff changeset
    40
 (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
    41
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
lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
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
  shows "get_array a h' ! k = (if k < i then get_array a h ! 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
    44
      else if j < k then get_array a h ! 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
    45
      else get_array a h ! (j - (k - i)))" (is "?P 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
    46
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
    47
  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
    48
  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
    49
  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
    50
    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
    51
    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
    52
    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
    53
      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
    54
      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
    55
      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
    56
    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
    57
    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
    58
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
    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
    60
    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
    61
      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
    62
  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
    63
    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
    64
    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
    65
    show ?thesis
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37719
diff changeset
    66
      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
    67
  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
    68
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
    69
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
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
    71
  assumes "crel (rev a i j) h h' r"
37719
271ecd4fb9f9 moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents: 36176
diff changeset
    72
  shows "Array.length a h = Array.length a 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
    73
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
    74
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
    75
  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
    76
  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
    77
  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
    78
    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
    79
    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
    80
    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
    81
      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
    82
      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
    83
      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
    84
    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
    85
      unfolding swap.simps
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37719
diff changeset
    86
      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
    87
  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
    88
    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
    89
    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
    90
    show ?thesis
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37719
diff changeset
    91
      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
    92
  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
    93
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
    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
lemma rev2_rev': assumes "crel (rev a i j) h h' u"
37719
271ecd4fb9f9 moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents: 36176
diff changeset
    96
  assumes "j < Array.length a 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
    97
  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
    98
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
    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
    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
   101
    assume "k < Suc j - i"
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
    with rev_pointwise[OF assms(1)] have "get_array a h' ! (i + k) = get_array a h ! (j - 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
   103
      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
   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
  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
   106
  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
   107
  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
   108
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
   109
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
   110
lemma rev2_rev: 
37719
271ecd4fb9f9 moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents: 36176
diff changeset
   111
  assumes "crel (rev a 0 (Array.length a h - 1)) h h' u"
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
  shows "get_array a h' = List.rev (get_array 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
   113
  using rev2_rev'[OF assms] rev_length[OF assms] assms
37719
271ecd4fb9f9 moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents: 36176
diff changeset
   114
    by (cases "Array.length a h = 0", auto simp add: Array.length_def
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37719
diff changeset
   115
      subarray_def sublist'_all rev.simps[where j=0] 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
   116
  (drule sym[of "List.length (get_array a h)"], simp)
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
   117
1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff changeset
   118
end