1.1 --- a/src/HOL/Library/Ref.thy	Thu Jan 08 10:53:48 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,91 +0,0 @@
     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 -
    1.36 -subsection {* Derivates *}
    1.37 -
    1.38 -definition
    1.39 -  change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap"
    1.40 -where
    1.41 -  "change f r = (do x \<leftarrow> ! r;
    1.42 -                    let y = f x;
    1.43 -                    r := y;
    1.44 -                    return y
    1.45 -                 done)"
    1.46 -
    1.47 -hide (open) const new lookup update change
    1.48 -
    1.49 -
    1.50 -subsection {* Properties *}
    1.51 -
    1.52 -lemma lookup_chain:
    1.53 -  "(!r \<guillemotright> f) = f"
    1.54 -  by (cases f)
    1.55 -    (auto simp add: Let_def bindM_def lookup_def expand_fun_eq)
    1.56 -
    1.57 -lemma update_change [code]:
    1.58 -  "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()"
    1.59 -  by (auto simp add: monad_simp change_def lookup_chain)
    1.60 -
    1.61 -
    1.62 -subsection {* Code generator setup *}
    1.63 -
    1.64 -subsubsection {* SML *}
    1.65 -
    1.66 -code_type ref (SML "_/ ref")
    1.67 -code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
    1.68 -code_const Ref.new (SML "(fn/ ()/ =>/ ref/ _)")
    1.69 -code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
    1.70 -code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
    1.71 -
    1.72 -code_reserved SML ref
    1.73 -
    1.74 -
    1.75 -subsubsection {* OCaml *}
    1.76 -
    1.77 -code_type ref (OCaml "_/ ref")
    1.78 -code_const Ref (OCaml "failwith/ \"bare Ref\")")
    1.79 -code_const Ref.new (OCaml "(fn/ ()/ =>/ ref/ _)")
    1.80 -code_const Ref.lookup (OCaml "(fn/ ()/ =>/ !/ _)")
    1.81 -code_const Ref.update (OCaml "(fn/ ()/ =>/ _/ :=/ _)")
    1.82 -
    1.83 -code_reserved OCaml ref
    1.84 -
    1.85 -
    1.86 -subsubsection {* Haskell *}
    1.87 -
    1.88 -code_type ref (Haskell "STRef/ RealWorld/ _")
    1.89 -code_const Ref (Haskell "error/ \"bare Ref\"")
    1.90 -code_const Ref.new (Haskell "newSTRef")
    1.91 -code_const Ref.lookup (Haskell "readSTRef")
    1.92 -code_const Ref.update (Haskell "writeSTRef")
    1.93 -
    1.94 -end
    1.95 \ No newline at end of file