src/HOL/Imperative_HOL/Ref.thy
author haftmann
Wed Sep 01 11:09:50 2010 +0200 (2010-09-01)
changeset 38968 e55deaa22fff
parent 38771 f9cd27cbe8a4
child 39198 f967a16dfcdd
permissions -rw-r--r--
do not print object frame around Scala includes -- this is in the responsibility of the user
haftmann@37787
     1
(*  Title:      HOL/Imperative_HOL/Ref.thy
haftmann@26170
     2
    Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
haftmann@26170
     3
*)
haftmann@26170
     4
haftmann@26170
     5
header {* Monadic references *}
haftmann@26170
     6
haftmann@26170
     7
theory Ref
haftmann@37719
     8
imports Array
haftmann@26170
     9
begin
haftmann@26170
    10
haftmann@26170
    11
text {*
haftmann@26170
    12
  Imperative reference operations; modeled after their ML counterparts.
haftmann@26170
    13
  See http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html
haftmann@26170
    14
  and http://www.smlnj.org/doc/Conversion/top-level-comparison.html
haftmann@26170
    15
*}
haftmann@26170
    16
haftmann@37753
    17
subsection {* Primitives *}
haftmann@37719
    18
haftmann@37725
    19
definition present :: "heap \<Rightarrow> 'a\<Colon>heap ref \<Rightarrow> bool" where
haftmann@37725
    20
  "present h r \<longleftrightarrow> addr_of_ref r < lim h"
haftmann@37719
    21
haftmann@37725
    22
definition get :: "heap \<Rightarrow> 'a\<Colon>heap ref \<Rightarrow> 'a" where
haftmann@37725
    23
  "get h = from_nat \<circ> refs h TYPEREP('a) \<circ> addr_of_ref"
haftmann@37719
    24
haftmann@37725
    25
definition set :: "'a\<Colon>heap ref \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
haftmann@37725
    26
  "set r x = refs_update
haftmann@37725
    27
    (\<lambda>h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r := to_nat x))))"
haftmann@37719
    28
haftmann@37725
    29
definition alloc :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where
haftmann@37725
    30
  "alloc x h = (let
haftmann@37719
    31
     l = lim h;
haftmann@37725
    32
     r = Ref l
haftmann@37725
    33
   in (r, set r x (h\<lparr>lim := l + 1\<rparr>)))"
haftmann@37719
    34
haftmann@37725
    35
definition noteq :: "'a\<Colon>heap ref \<Rightarrow> 'b\<Colon>heap ref \<Rightarrow> bool" (infix "=!=" 70) where
haftmann@37719
    36
  "r =!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_ref r \<noteq> addr_of_ref s"
haftmann@37719
    37
haftmann@37753
    38
haftmann@37753
    39
subsection {* Monad operations *}
haftmann@37753
    40
haftmann@37753
    41
definition ref :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where
haftmann@37753
    42
  [code del]: "ref v = Heap_Monad.heap (alloc v)"
haftmann@37753
    43
haftmann@37753
    44
definition lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where
haftmann@37758
    45
  [code del]: "lookup r = Heap_Monad.tap (\<lambda>h. get h r)"
haftmann@37753
    46
haftmann@37753
    47
definition update :: "'a ref \<Rightarrow> 'a\<Colon>heap \<Rightarrow> unit Heap" ("_ := _" 62) where
haftmann@37753
    48
  [code del]: "update r v = Heap_Monad.heap (\<lambda>h. ((), set r v h))"
haftmann@37753
    49
haftmann@37753
    50
definition change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap" where
krauss@37792
    51
  "change f r = do {
haftmann@37753
    52
     x \<leftarrow> ! r;
haftmann@37753
    53
     let y = f x;
haftmann@37753
    54
     r := y;
haftmann@37753
    55
     return y
krauss@37792
    56
   }"
haftmann@37753
    57
haftmann@37753
    58
haftmann@37753
    59
subsection {* Properties *}
haftmann@37753
    60
haftmann@37758
    61
text {* Primitives *}
haftmann@37758
    62
haftmann@37725
    63
lemma noteq_sym: "r =!= s \<Longrightarrow> s =!= r"
haftmann@37725
    64
  and unequal [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" -- "same types!"
haftmann@37725
    65
  by (auto simp add: noteq_def)
haftmann@37719
    66
haftmann@37725
    67
lemma noteq_irrefl: "r =!= r \<Longrightarrow> False"
haftmann@37725
    68
  by (auto simp add: noteq_def)
haftmann@37719
    69
haftmann@37725
    70
lemma present_alloc_neq: "present h r \<Longrightarrow> r =!= fst (alloc v h)"
haftmann@37725
    71
  by (simp add: present_def alloc_def noteq_def Let_def)
haftmann@37719
    72
haftmann@37725
    73
lemma next_fresh [simp]:
haftmann@37725
    74
  assumes "(r, h') = alloc x h"
haftmann@37725
    75
  shows "\<not> present h r"
haftmann@37725
    76
  using assms by (cases h) (auto simp add: alloc_def present_def Let_def)
haftmann@37719
    77
haftmann@37725
    78
lemma next_present [simp]:
haftmann@37725
    79
  assumes "(r, h') = alloc x h"
haftmann@37725
    80
  shows "present h' r"
haftmann@37725
    81
  using assms by (cases h) (auto simp add: alloc_def set_def present_def Let_def)
haftmann@37719
    82
haftmann@37725
    83
lemma get_set_eq [simp]:
haftmann@37725
    84
  "get (set r x h) r = x"
haftmann@37725
    85
  by (simp add: get_def set_def)
haftmann@37719
    86
haftmann@37725
    87
lemma get_set_neq [simp]:
haftmann@37725
    88
  "r =!= s \<Longrightarrow> get (set s x h) r = get h r"
haftmann@37725
    89
  by (simp add: noteq_def get_def set_def)
haftmann@37719
    90
haftmann@37725
    91
lemma set_same [simp]:
haftmann@37725
    92
  "set r x (set r y h) = set r x h"
haftmann@37725
    93
  by (simp add: set_def)
haftmann@37719
    94
haftmann@37771
    95
lemma not_present_alloc [simp]:
haftmann@37771
    96
  "\<not> present h (fst (alloc v h))"
haftmann@37771
    97
  by (simp add: present_def alloc_def Let_def)
haftmann@37771
    98
haftmann@37725
    99
lemma set_set_swap:
haftmann@37725
   100
  "r =!= r' \<Longrightarrow> set r x (set r' x' h) = set r' x' (set r x h)"
haftmann@37725
   101
  by (simp add: noteq_def set_def expand_fun_eq)
haftmann@37719
   102
haftmann@37725
   103
lemma alloc_set:
haftmann@37725
   104
  "fst (alloc x (set r x' h)) = fst (alloc x h)"
haftmann@37725
   105
  by (simp add: alloc_def set_def Let_def)
haftmann@37719
   106
haftmann@37725
   107
lemma get_alloc [simp]:
haftmann@37725
   108
  "get (snd (alloc x h)) (fst (alloc x' h)) = x"
haftmann@37725
   109
  by (simp add: alloc_def Let_def)
haftmann@37719
   110
haftmann@37725
   111
lemma set_alloc [simp]:
haftmann@37725
   112
  "set (fst (alloc v h)) v' (snd (alloc v h)) = snd (alloc v' h)"
haftmann@37725
   113
  by (simp add: alloc_def Let_def)
haftmann@37719
   114
haftmann@37725
   115
lemma get_alloc_neq: "r =!= fst (alloc v h) \<Longrightarrow> 
haftmann@37725
   116
  get (snd (alloc v h)) r  = get h r"
haftmann@37725
   117
  by (simp add: get_def set_def alloc_def Let_def noteq_def)
haftmann@37719
   118
haftmann@37725
   119
lemma lim_set [simp]:
haftmann@37725
   120
  "lim (set r v h) = lim h"
haftmann@37725
   121
  by (simp add: set_def)
haftmann@37719
   122
haftmann@37725
   123
lemma present_alloc [simp]: 
haftmann@37725
   124
  "present h r \<Longrightarrow> present (snd (alloc v h)) r"
haftmann@37725
   125
  by (simp add: present_def alloc_def Let_def)
haftmann@37719
   126
haftmann@37725
   127
lemma present_set [simp]:
haftmann@37725
   128
  "present (set r v h) = present h"
haftmann@37725
   129
  by (simp add: present_def expand_fun_eq)
haftmann@37719
   130
haftmann@37725
   131
lemma noteq_I:
haftmann@37725
   132
  "present h r \<Longrightarrow> \<not> present h r' \<Longrightarrow> r =!= r'"
haftmann@37725
   133
  by (auto simp add: noteq_def present_def)
haftmann@37719
   134
haftmann@37758
   135
haftmann@37758
   136
text {* Monad operations *}
haftmann@37758
   137
haftmann@37787
   138
lemma execute_ref [execute_simps]:
haftmann@37758
   139
  "execute (ref v) h = Some (alloc v h)"
haftmann@37787
   140
  by (simp add: ref_def execute_simps)
haftmann@26170
   141
haftmann@37787
   142
lemma success_refI [success_intros]:
haftmann@37758
   143
  "success (ref v) h"
haftmann@37787
   144
  by (auto intro: success_intros simp add: ref_def)
haftmann@37758
   145
haftmann@37771
   146
lemma crel_refI [crel_intros]:
haftmann@37771
   147
  assumes "(r, h') = alloc v h"
haftmann@37771
   148
  shows "crel (ref v) h h' r"
haftmann@37787
   149
  by (rule crelI) (insert assms, simp add: execute_simps)
haftmann@37771
   150
haftmann@37771
   151
lemma crel_refE [crel_elims]:
haftmann@37771
   152
  assumes "crel (ref v) h h' r"
haftmann@37796
   153
  obtains "get h' r = v" and "present h' r" and "\<not> present h r"
haftmann@37787
   154
  using assms by (rule crelE) (simp add: execute_simps)
haftmann@37771
   155
haftmann@37787
   156
lemma execute_lookup [execute_simps]:
haftmann@37753
   157
  "Heap_Monad.execute (lookup r) h = Some (get h r, h)"
haftmann@37787
   158
  by (simp add: lookup_def execute_simps)
haftmann@26182
   159
haftmann@37787
   160
lemma success_lookupI [success_intros]:
haftmann@37758
   161
  "success (lookup r) h"
haftmann@37787
   162
  by (auto intro: success_intros  simp add: lookup_def)
haftmann@37758
   163
haftmann@37771
   164
lemma crel_lookupI [crel_intros]:
haftmann@37796
   165
  assumes "h' = h" "x = get h r"
haftmann@37771
   166
  shows "crel (!r) h h' x"
haftmann@37787
   167
  by (rule crelI) (insert assms, simp add: execute_simps)
haftmann@37771
   168
haftmann@37771
   169
lemma crel_lookupE [crel_elims]:
haftmann@37771
   170
  assumes "crel (!r) h h' x"
haftmann@37796
   171
  obtains "h' = h" "x = get h r"
haftmann@37787
   172
  using assms by (rule crelE) (simp add: execute_simps)
haftmann@37771
   173
haftmann@37787
   174
lemma execute_update [execute_simps]:
haftmann@37753
   175
  "Heap_Monad.execute (update r v) h = Some ((), set r v h)"
haftmann@37787
   176
  by (simp add: update_def execute_simps)
haftmann@26170
   177
haftmann@37787
   178
lemma success_updateI [success_intros]:
haftmann@37758
   179
  "success (update r v) h"
haftmann@37787
   180
  by (auto intro: success_intros  simp add: update_def)
haftmann@37758
   181
haftmann@37771
   182
lemma crel_updateI [crel_intros]:
haftmann@37796
   183
  assumes "h' = set r v h"
haftmann@37771
   184
  shows "crel (r := v) h h' x"
haftmann@37787
   185
  by (rule crelI) (insert assms, simp add: execute_simps)
haftmann@37771
   186
haftmann@37771
   187
lemma crel_updateE [crel_elims]:
haftmann@37771
   188
  assumes "crel (r' := v) h h' r"
haftmann@37796
   189
  obtains "h' = set r' v h"
haftmann@37787
   190
  using assms by (rule crelE) (simp add: execute_simps)
haftmann@37771
   191
haftmann@37787
   192
lemma execute_change [execute_simps]:
haftmann@37753
   193
  "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)"
haftmann@37787
   194
  by (simp add: change_def bind_def Let_def execute_simps)
haftmann@37758
   195
haftmann@37787
   196
lemma success_changeI [success_intros]:
haftmann@37758
   197
  "success (change f r) h"
haftmann@37771
   198
  by (auto intro!: success_intros crel_intros simp add: change_def)
haftmann@37771
   199
haftmann@37771
   200
lemma crel_changeI [crel_intros]: 
haftmann@37796
   201
  assumes "h' = set r (f (get h r)) h" "x = f (get h r)"
haftmann@37796
   202
  shows "crel (change f r) h h' x"
haftmann@37787
   203
  by (rule crelI) (insert assms, simp add: execute_simps)  
haftmann@37771
   204
haftmann@37771
   205
lemma crel_changeE [crel_elims]:
haftmann@37796
   206
  assumes "crel (change f r') h h' r"
haftmann@37796
   207
  obtains "h' = set r' (f (get h r')) h" "r = f (get h r')"
haftmann@37787
   208
  using assms by (rule crelE) (simp add: execute_simps)
haftmann@26170
   209
haftmann@26170
   210
lemma lookup_chain:
haftmann@26170
   211
  "(!r \<guillemotright> f) = f"
haftmann@37771
   212
  by (rule Heap_eqI) (auto simp add: lookup_def execute_simps intro: execute_bind)
haftmann@26170
   213
haftmann@28562
   214
lemma update_change [code]:
haftmann@37725
   215
  "r := e = change (\<lambda>_. e) r \<guillemotright> return ()"
haftmann@37725
   216
  by (rule Heap_eqI) (simp add: change_def lookup_chain)
haftmann@26170
   217
haftmann@26182
   218
haftmann@37719
   219
text {* Non-interaction between imperative array and imperative references *}
haftmann@37719
   220
haftmann@37806
   221
lemma array_get_set [simp]:
haftmann@37806
   222
  "Array.get (set r v h) = Array.get h"
haftmann@37806
   223
  by (simp add: Array.get_def set_def expand_fun_eq)
haftmann@37719
   224
haftmann@37796
   225
lemma get_update [simp]:
haftmann@37805
   226
  "get (Array.update a i v h) r = get h r"
haftmann@37804
   227
  by (simp add: get_def Array.update_def Array.set_def)
haftmann@37719
   228
haftmann@37796
   229
lemma alloc_update:
haftmann@37796
   230
  "fst (alloc v (Array.update a i v' h)) = fst (alloc v h)"
haftmann@37806
   231
  by (simp add: Array.update_def Array.get_def Array.set_def alloc_def Let_def)
haftmann@37719
   232
haftmann@37796
   233
lemma update_set_swap:
haftmann@37796
   234
  "Array.update a i v (set r v' h) = set r v' (Array.update a i v h)"
haftmann@37806
   235
  by (simp add: Array.update_def Array.get_def Array.set_def set_def)
haftmann@37719
   236
haftmann@37725
   237
lemma length_alloc [simp]: 
haftmann@37802
   238
  "Array.length (snd (alloc v h)) a = Array.length h a"
haftmann@37806
   239
  by (simp add: Array.length_def Array.get_def alloc_def set_def Let_def)
haftmann@37719
   240
haftmann@37806
   241
lemma array_get_alloc [simp]: 
haftmann@37806
   242
  "Array.get (snd (alloc v h)) = Array.get h"
haftmann@37806
   243
  by (simp add: Array.get_def alloc_def set_def Let_def expand_fun_eq)
haftmann@37719
   244
haftmann@37796
   245
lemma present_update [simp]: 
haftmann@37796
   246
  "present (Array.update a i v h) = present h"
haftmann@37804
   247
  by (simp add: Array.update_def Array.set_def expand_fun_eq present_def)
haftmann@37719
   248
haftmann@37725
   249
lemma array_present_set [simp]:
haftmann@37804
   250
  "Array.present (set r v h) = Array.present h"
haftmann@37804
   251
  by (simp add: Array.present_def set_def expand_fun_eq)
haftmann@37719
   252
haftmann@37725
   253
lemma array_present_alloc [simp]:
haftmann@37804
   254
  "Array.present h a \<Longrightarrow> Array.present (snd (alloc v h)) a"
haftmann@37804
   255
  by (simp add: Array.present_def alloc_def Let_def)
haftmann@37719
   256
haftmann@37725
   257
lemma set_array_set_swap:
haftmann@37804
   258
  "Array.set a xs (set r x' h) = set r x' (Array.set a xs h)"
haftmann@37804
   259
  by (simp add: Array.set_def set_def)
haftmann@37725
   260
haftmann@37796
   261
hide_const (open) present get set alloc noteq lookup update change
haftmann@37719
   262
haftmann@37719
   263
haftmann@26182
   264
subsection {* Code generator setup *}
haftmann@26182
   265
haftmann@38068
   266
text {* Intermediate operation avoids invariance problem in @{text Scala} (similiar to value restriction) *}
haftmann@38068
   267
haftmann@38068
   268
definition ref' where
haftmann@38068
   269
  [code del]: "ref' = ref"
haftmann@38068
   270
haftmann@38068
   271
lemma [code]:
haftmann@38068
   272
  "ref x = ref' x"
haftmann@38068
   273
  by (simp add: ref'_def)
haftmann@38068
   274
haftmann@38068
   275
haftmann@37753
   276
text {* SML *}
haftmann@26182
   277
bulwahn@34051
   278
code_type ref (SML "_/ Unsynchronized.ref")
haftmann@26182
   279
code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
haftmann@38068
   280
code_const ref' (SML "(fn/ ()/ =>/ Unsynchronized.ref/ _)")
haftmann@26752
   281
code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
haftmann@26752
   282
code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
haftmann@26182
   283
haftmann@38068
   284
code_reserved SML Unsynchronized
haftmann@26182
   285
haftmann@26182
   286
haftmann@37753
   287
text {* OCaml *}
haftmann@26182
   288
haftmann@26182
   289
code_type ref (OCaml "_/ ref")
haftmann@37830
   290
code_const Ref (OCaml "failwith/ \"bare Ref\"")
haftmann@38068
   291
code_const ref' (OCaml "(fun/ ()/ ->/ ref/ _)")
haftmann@37830
   292
code_const Ref.lookup (OCaml "(fun/ ()/ ->/ !/ _)")
haftmann@37830
   293
code_const Ref.update (OCaml "(fun/ ()/ ->/ _/ :=/ _)")
haftmann@26182
   294
haftmann@26182
   295
code_reserved OCaml ref
haftmann@26182
   296
haftmann@26182
   297
haftmann@37753
   298
text {* Haskell *}
haftmann@26182
   299
haftmann@29793
   300
code_type ref (Haskell "Heap.STRef/ Heap.RealWorld/ _")
haftmann@26182
   301
code_const Ref (Haskell "error/ \"bare Ref\"")
haftmann@38068
   302
code_const ref' (Haskell "Heap.newSTRef")
haftmann@29793
   303
code_const Ref.lookup (Haskell "Heap.readSTRef")
haftmann@29793
   304
code_const Ref.update (Haskell "Heap.writeSTRef")
haftmann@26182
   305
haftmann@37842
   306
haftmann@37842
   307
text {* Scala *}
haftmann@37842
   308
haftmann@38968
   309
code_type ref (Scala "!Ref[_]")
haftmann@37842
   310
code_const Ref (Scala "!error(\"bare Ref\")")
haftmann@38968
   311
code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
haftmann@38968
   312
code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
haftmann@38968
   313
code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
haftmann@37842
   314
haftmann@37758
   315
end