Quelle Ref.thy Sprache: Isabelle

(*  Title:      HOL/Imperative_HOL/Ref.thy
    Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)

section \<open>Monadic references\<close>

theory Ref
imports Array
begin

text \<open>
  Imperative reference operations; modeled after their ML counterparts.
  See \<^url>\<open>https://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html\<close>
  and \<^url>\<open>https://www.smlnj.org/doc/Conversion/top-level-comparison.html\<close>.
\<close>

subsection \<open>Primitives\<close>

definition present :: "heap \ 'a::heap ref \ bool" where
  "present h r \ addr_of_ref r < lim h"

definition get :: "heap \ 'a::heap ref \ 'a" where
  "get h = from_nat \ refs h TYPEREP('a) \ addr_of_ref"

definition set :: "'a::heap ref \ 'a \ heap \ heap" where
  "set r x = refs_update
    (\<lambda>h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r := to_nat x))))"

definition alloc :: "'a \ heap \ 'a::heap ref \ heap" where
  "alloc x h = (let
     l = lim h;
     r = Ref l
   in (r, set r x (h\<lparr>lim := l + 1\<rparr>)))"

definition noteq :: "'a::heap ref \ 'b::heap ref \ bool" (infix \=!=\ 70) where
  "r =!= s \ TYPEREP('a) \ TYPEREP('b) \ addr_of_ref r \ addr_of_ref s"

subsection \<open>Monad operations\<close>

definition ref :: "'a::heap \ 'a ref Heap" where
  [code del]: "ref v = Heap_Monad.heap (alloc v)"

definition lookup :: "'a::heap ref \ 'a Heap" (\!_\ 61) where
  [code del]: "lookup r = Heap_Monad.tap (\h. get h r)"

definition update :: "'a ref \ 'a::heap \ unit Heap" (\_ := _\ 62) where
  [code del]: "update r v = Heap_Monad.heap (\h. ((), set r v h))"

definition change :: "('a::heap \ 'a) \ 'a ref \ 'a Heap" where
  "change f r = do {
     x \<leftarrow> ! r;
     let y = f x;
     r := y;
     return y
   }"

subsection \<open>Properties\<close>

text \<open>Primitives\<close>

lemma noteq_sym: "r =!= s \ s =!= r"
  and unequal [simp]: "r \ r' \ r =!= r'" \ \same types!\
  by (auto simp add: noteq_def)

lemma noteq_irrefl: "r =!= r \ False"
  by (auto simp add: noteq_def)

lemma present_alloc_neq: "present h r \ r =!= fst (alloc v h)"
  by (simp add: present_def alloc_def noteq_def Let_def)

lemma next_fresh [simp]:
  assumes "(r, h') = alloc x h"
  shows "\ present h r"
  using assms by (cases h) (auto simp add: alloc_def present_def Let_def)

lemma next_present [simp]:
  assumes "(r, h') = alloc x h"
  shows "present h' r"
  using assms by (cases h) (auto simp add: alloc_def set_def present_def Let_def)

lemma get_set_eq [simp]:
  "get (set r x h) r = x"
  by (simp add: get_def set_def)

lemma get_set_neq [simp]:
  "r =!= s \ get (set s x h) r = get h r"
  by (simp add: noteq_def get_def set_def)

lemma set_same [simp]:
  "set r x (set r y h) = set r x h"
  by (simp add: set_def)

lemma not_present_alloc [simp]:
  "\ present h (fst (alloc v h))"
  by (simp add: present_def alloc_def Let_def)

lemma set_set_swap:
  "r =!= r' \ set r x (set r' x' h) = set r' x' (set r x h)"
  by (simp add: noteq_def set_def fun_eq_iff)

lemma alloc_set:
  "fst (alloc x (set r x' h)) = fst (alloc x h)"
  by (simp add: alloc_def set_def Let_def)

lemma get_alloc [simp]:
  "get (snd (alloc x h)) (fst (alloc x' h)) = x"
  by (simp add: alloc_def Let_def)

lemma set_alloc [simp]:
  "set (fst (alloc v h)) v' (snd (alloc v h)) = snd (alloc v' h)"
  by (simp add: alloc_def Let_def)

lemma get_alloc_neq: "r =!= fst (alloc v h) \
  get (snd (alloc v h)) r  = get h r"
  by (simp add: get_def set_def alloc_def Let_def noteq_def)

lemma lim_set [simp]:
  "lim (set r v h) = lim h"
  by (simp add: set_def)

lemma present_alloc [simp]:
  "present h r \ present (snd (alloc v h)) r"
  by (simp add: present_def alloc_def Let_def)

lemma present_set [simp]:
  "present (set r v h) = present h"
  by (simp add: present_def fun_eq_iff)

lemma noteq_I:
  "present h r \ \ present h r' \ r =!= r'"
  by (auto simp add: noteq_def present_def)

text \<open>Monad operations\<close>

lemma execute_ref [execute_simps]:
  "execute (ref v) h = Some (alloc v h)"
  by (simp add: ref_def execute_simps)

lemma success_refI [success_intros]:
  "success (ref v) h"
  by (auto intro: success_intros simp add: ref_def)

lemma effect_refI [effect_intros]:
  assumes "(r, h') = alloc v h"
  shows "effect (ref v) h h' r"
  by (rule effectI) (insert assms, simp add: execute_simps)

lemma effect_refE [effect_elims]:
  assumes "effect (ref v) h h' r"
  obtains "get h' r = v" and "present h' r" and "\ present h r"
  using assms by (rule effectE) (simp add: execute_simps)

lemma execute_lookup [execute_simps]:
  "Heap_Monad.execute (lookup r) h = Some (get h r, h)"
  by (simp add: lookup_def execute_simps)

lemma success_lookupI [success_intros]:
  "success (lookup r) h"
  by (auto intro: success_intros  simp add: lookup_def)

lemma effect_lookupI [effect_intros]:
  assumes "h' = h" "x = get h r"
  shows "effect (!r) h h' x"
  by (rule effectI) (insert assms, simp add: execute_simps)

lemma effect_lookupE [effect_elims]:
  assumes "effect (!r) h h' x"
  obtains "h' = h" "x = get h r"
  using assms by (rule effectE) (simp add: execute_simps)

lemma execute_update [execute_simps]:
  "Heap_Monad.execute (update r v) h = Some ((), set r v h)"
  by (simp add: update_def execute_simps)

lemma success_updateI [success_intros]:
  "success (update r v) h"
  by (auto intro: success_intros  simp add: update_def)

lemma effect_updateI [effect_intros]:
  assumes "h' = set r v h"
  shows "effect (r := v) h h' x"
  by (rule effectI) (insert assms, simp add: execute_simps)

lemma effect_updateE [effect_elims]:
  assumes "effect (r' := v) h h' r"
  obtains "h' = set r' v h"
  using assms by (rule effectE) (simp add: execute_simps)

lemma execute_change [execute_simps]:
  "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)"
  by (simp add: change_def bind_def Let_def execute_simps)

lemma success_changeI [success_intros]:
  "success (change f r) h"
  by (auto intro!: success_intros effect_intros simp add: change_def)

lemma effect_changeI [effect_intros]:
  assumes "h' = set r (f (get h r)) h" "x = f (get h r)"
  shows "effect (change f r) h h' x"
  by (rule effectI) (insert assms, simp add: execute_simps)

lemma effect_changeE [effect_elims]:
  assumes "effect (change f r') h h' r"
  obtains "h' = set r' (f (get h r')) h" "r = f (get h r')"
  using assms by (rule effectE) (simp add: execute_simps)

lemma lookup_chain:
  "(!r \ f) = f"
  by (rule Heap_eqI) (auto simp add: lookup_def execute_simps intro: execute_bind)

lemma update_change [code]:
  "r := e = change (\_. e) r \ return ()"
  by (rule Heap_eqI) (simp add: change_def lookup_chain)

text \<open>Non-interaction between imperative arrays and imperative references\<close>

lemma array_get_set [simp]:
  "Array.get (set r v h) = Array.get h"
  by (simp add: Array.get_def set_def fun_eq_iff)

lemma get_update [simp]:
  "get (Array.update a i v h) r = get h r"
  by (simp add: get_def Array.update_def Array.set_def)

lemma alloc_update:
  "fst (alloc v (Array.update a i v' h)) = fst (alloc v h)"
  by (simp add: Array.update_def Array.get_def Array.set_def alloc_def Let_def)

lemma update_set_swap:
  "Array.update a i v (set r v' h) = set r v' (Array.update a i v h)"
  by (simp add: Array.update_def Array.get_def Array.set_def set_def)

lemma length_alloc [simp]:
  "Array.length (snd (alloc v h)) a = Array.length h a"
  by (simp add: Array.length_def Array.get_def alloc_def set_def Let_def)

lemma array_get_alloc [simp]:
  "Array.get (snd (alloc v h)) = Array.get h"
  by (simp add: Array.get_def alloc_def set_def Let_def fun_eq_iff)

lemma present_update [simp]:
  "present (Array.update a i v h) = present h"
  by (simp add: Array.update_def Array.set_def fun_eq_iff present_def)

lemma array_present_set [simp]:
  "Array.present (set r v h) = Array.present h"
  by (simp add: Array.present_def set_def fun_eq_iff)

lemma array_present_alloc [simp]:
  "Array.present h a \ Array.present (snd (alloc v h)) a"
  by (simp add: Array.present_def alloc_def Let_def)

lemma set_array_set_swap:
  "Array.set a xs (set r x' h) = set r x' (Array.set a xs h)"
  by (simp add: Array.set_def set_def)

hide_const (open) present get set alloc noteq lookup update change

subsection \<open>Code generator setup\<close>

text \<open>Intermediate operation avoids invariance problem in \<open>Scala\<close> (similar to value restriction)\<close>

definition ref' where
  [code del]: "ref' = ref"

lemma [code]:
  "ref x = ref' x"
  by (simp add: ref'_def)

text \<open>SML / Eval\<close>

code_printing type_constructor ref \<rightharpoonup> (SML) "_/ ref"
code_printing type_constructor ref \<rightharpoonup> (Eval) "_/ Unsynchronized.ref"
code_printing constant Ref \<rightharpoonup> (SML) "raise/ (Fail/ \"bare Ref\")"
code_printing constant ref' \ (SML) "(fn/ ()/ =>/ ref/ _)"
code_printing constant ref' \ (Eval) "(fn/ ()/ =>/ Unsynchronized.ref/ _)"
code_printing constant Ref.lookup \<rightharpoonup> (SML) "(fn/ ()/ =>/ !/ _)"
code_printing constant Ref.update \<rightharpoonup> (SML) "(fn/ ()/ =>/ _/ :=/ _)"
code_printing constant "HOL.equal :: 'a ref \ 'a ref \ bool" \ (SML) infixl 6 "="

code_reserved (Eval) Unsynchronized

text \<open>OCaml\<close>

code_printing type_constructor ref \<rightharpoonup> (OCaml) "_/ ref"
code_printing constant Ref \<rightharpoonup> (OCaml) "failwith/ \"bare Ref\""
code_printing constant ref' \ (OCaml) "(fun/ ()/ ->/ ref/ _)"
code_printing constant Ref.lookup \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ !/ _)"
code_printing constant Ref.update \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ _/ :=/ _)"
code_printing constant "HOL.equal :: 'a ref \ 'a ref \ bool" \ (OCaml) infixl 4 "="

code_reserved (OCaml) ref

text \<open>Haskell\<close>

code_printing type_constructor ref \<rightharpoonup> (Haskell) "Heap.STRef/ Heap.RealWorld/ _"
code_printing constant Ref \<rightharpoonup> (Haskell) "error/ \"bare Ref\""
code_printing constant ref' \ (Haskell) "Heap.newSTRef"
code_printing constant Ref.lookup \<rightharpoonup> (Haskell) "Heap.readSTRef"
code_printing constant Ref.update \<rightharpoonup> (Haskell) "Heap.writeSTRef"
code_printing constant "HOL.equal :: 'a ref \ 'a ref \ bool" \ (Haskell) infix 4 "=="
code_printing class_instance ref :: HOL.equal \<rightharpoonup> (Haskell) -

text \<open>Scala\<close>

code_printing type_constructor ref \<rightharpoonup> (Scala) "!Ref[_]"
code_printing constant Ref \<rightharpoonup> (Scala) "!sys.error(\"bare Ref\")"
code_printing constant ref' \ (Scala) "('_: Unit)/ =>/ Ref((_))"
code_printing constant Ref.lookup \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Ref.lookup((_))"
code_printing constant Ref.update \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Ref.update((_), (_))"
code_printing constant "HOL.equal :: 'a ref \ 'a ref \ bool" \ (Scala) infixl 5 "=="

end

quality98%

¤ Dauer der Verarbeitung: 0.34 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.