src/HOL/Library/Ref.thy
changeset 26170 66e6b967ccf1
child 26182 8262ec0e8782
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Ref.thy	Wed Feb 27 21:41:08 2008 +0100
     1.3 @@ -0,0 +1,56 @@
     1.4 +(*  Title:      HOL/Library/Ref.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {* Monadic references *}
    1.10 +
    1.11 +theory Ref
    1.12 +imports Heap_Monad
    1.13 +begin
    1.14 +
    1.15 +text {*
    1.16 +  Imperative reference operations; modeled after their ML counterparts.
    1.17 +  See http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html
    1.18 +  and http://www.smlnj.org/doc/Conversion/top-level-comparison.html
    1.19 +*}
    1.20 +
    1.21 +subsection {* Primitives *}
    1.22 +
    1.23 +definition
    1.24 +  new :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where
    1.25 +  [code del]: "new v = Heap_Monad.heap (Heap.ref v)"
    1.26 +
    1.27 +definition
    1.28 +  lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where
    1.29 +  [code del]: "lookup r = Heap_Monad.heap (\<lambda>h. (get_ref r h, h))"
    1.30 +
    1.31 +definition
    1.32 +  update :: "'a ref \<Rightarrow> ('a\<Colon>heap) \<Rightarrow> unit Heap" ("_ := _" 62) where
    1.33 +  [code del]: "update r e = Heap_Monad.heap (\<lambda>h. ((), set_ref r e h))"
    1.34 +
    1.35 +subsection {* Derivates *}
    1.36 +
    1.37 +definition
    1.38 +  change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap"
    1.39 +where
    1.40 +  "change f r = (do x \<leftarrow> ! r;
    1.41 +                    let y = f x;
    1.42 +                    r := y;
    1.43 +                    return y
    1.44 +                 done)"
    1.45 +
    1.46 +hide (open) const new lookup update change
    1.47 +
    1.48 +subsection {* Properties *}
    1.49 +
    1.50 +lemma lookup_chain:
    1.51 +  "(!r \<guillemotright> f) = f"
    1.52 +  by (cases f)
    1.53 +    (auto simp add: Let_def bindM_def lookup_def expand_fun_eq)
    1.54 +
    1.55 +lemma update_change [code func]:
    1.56 +  "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()"
    1.57 +  by (auto simp add: monad_simp change_def lookup_chain)
    1.58 +
    1.59 +end
    1.60 \ No newline at end of file