src/HOL/Library/Ref.thy
author haftmann
Wed Feb 27 21:41:08 2008 +0100 (2008-02-27)
changeset 26170 66e6b967ccf1
child 26182 8262ec0e8782
permissions -rw-r--r--
added theories for imperative HOL
haftmann@26170
     1
(*  Title:      HOL/Library/Ref.thy
haftmann@26170
     2
    ID:         $Id$
haftmann@26170
     3
    Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
haftmann@26170
     4
*)
haftmann@26170
     5
haftmann@26170
     6
header {* Monadic references *}
haftmann@26170
     7
haftmann@26170
     8
theory Ref
haftmann@26170
     9
imports Heap_Monad
haftmann@26170
    10
begin
haftmann@26170
    11
haftmann@26170
    12
text {*
haftmann@26170
    13
  Imperative reference operations; modeled after their ML counterparts.
haftmann@26170
    14
  See http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html
haftmann@26170
    15
  and http://www.smlnj.org/doc/Conversion/top-level-comparison.html
haftmann@26170
    16
*}
haftmann@26170
    17
haftmann@26170
    18
subsection {* Primitives *}
haftmann@26170
    19
haftmann@26170
    20
definition
haftmann@26170
    21
  new :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where
haftmann@26170
    22
  [code del]: "new v = Heap_Monad.heap (Heap.ref v)"
haftmann@26170
    23
haftmann@26170
    24
definition
haftmann@26170
    25
  lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where
haftmann@26170
    26
  [code del]: "lookup r = Heap_Monad.heap (\<lambda>h. (get_ref r h, h))"
haftmann@26170
    27
haftmann@26170
    28
definition
haftmann@26170
    29
  update :: "'a ref \<Rightarrow> ('a\<Colon>heap) \<Rightarrow> unit Heap" ("_ := _" 62) where
haftmann@26170
    30
  [code del]: "update r e = Heap_Monad.heap (\<lambda>h. ((), set_ref r e h))"
haftmann@26170
    31
haftmann@26170
    32
subsection {* Derivates *}
haftmann@26170
    33
haftmann@26170
    34
definition
haftmann@26170
    35
  change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap"
haftmann@26170
    36
where
haftmann@26170
    37
  "change f r = (do x \<leftarrow> ! r;
haftmann@26170
    38
                    let y = f x;
haftmann@26170
    39
                    r := y;
haftmann@26170
    40
                    return y
haftmann@26170
    41
                 done)"
haftmann@26170
    42
haftmann@26170
    43
hide (open) const new lookup update change
haftmann@26170
    44
haftmann@26170
    45
subsection {* Properties *}
haftmann@26170
    46
haftmann@26170
    47
lemma lookup_chain:
haftmann@26170
    48
  "(!r \<guillemotright> f) = f"
haftmann@26170
    49
  by (cases f)
haftmann@26170
    50
    (auto simp add: Let_def bindM_def lookup_def expand_fun_eq)
haftmann@26170
    51
haftmann@26170
    52
lemma update_change [code func]:
haftmann@26170
    53
  "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()"
haftmann@26170
    54
  by (auto simp add: monad_simp change_def lookup_chain)
haftmann@26170
    55
haftmann@26170
    56
end