src/HOL/Imperative_HOL/Ref.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 63680 6e1e8b5abbfa
child 67443 3abf6a722518
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
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
wenzelm@63167
     5
section \<open>Monadic references\<close>
haftmann@26170
     6
haftmann@26170
     7
theory Ref
haftmann@37719
     8
imports Array
haftmann@26170
     9
begin
haftmann@26170
    10
wenzelm@63167
    11
text \<open>
haftmann@26170
    12
  Imperative reference operations; modeled after their ML counterparts.
wenzelm@63680
    13
  See \<^url>\<open>http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html\<close>
wenzelm@63680
    14
  and \<^url>\<open>http://www.smlnj.org/doc/Conversion/top-level-comparison.html\<close>.
wenzelm@63167
    15
\<close>
haftmann@26170
    16
wenzelm@63167
    17
subsection \<open>Primitives\<close>
haftmann@37719
    18
wenzelm@61076
    19
definition present :: "heap \<Rightarrow> 'a::heap ref \<Rightarrow> bool" where
haftmann@37725
    20
  "present h r \<longleftrightarrow> addr_of_ref r < lim h"
haftmann@37719
    21
wenzelm@61076
    22
definition get :: "heap \<Rightarrow> 'a::heap ref \<Rightarrow> 'a" where
haftmann@37725
    23
  "get h = from_nat \<circ> refs h TYPEREP('a) \<circ> addr_of_ref"
haftmann@37719
    24
wenzelm@61076
    25
definition set :: "'a::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
wenzelm@61076
    29
definition alloc :: "'a \<Rightarrow> heap \<Rightarrow> 'a::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
wenzelm@61076
    35
definition noteq :: "'a::heap ref \<Rightarrow> 'b::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
wenzelm@63167
    39
subsection \<open>Monad operations\<close>
haftmann@37753
    40
wenzelm@61076
    41
definition ref :: "'a::heap \<Rightarrow> 'a ref Heap" where
haftmann@37753
    42
  [code del]: "ref v = Heap_Monad.heap (alloc v)"
haftmann@37753
    43
wenzelm@61076
    44
definition lookup :: "'a::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
wenzelm@61076
    47
definition update :: "'a ref \<Rightarrow> 'a::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
wenzelm@61076
    50
definition change :: "('a::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
wenzelm@63167
    59
subsection \<open>Properties\<close>
haftmann@37753
    60
wenzelm@63167
    61
text \<open>Primitives\<close>
haftmann@37758
    62
haftmann@37725
    63
lemma noteq_sym: "r =!= s \<Longrightarrow> s =!= r"
wenzelm@63167
    64
  and unequal [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" \<comment> "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)"
nipkow@39302
   101
  by (simp add: noteq_def set_def fun_eq_iff)
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"
nipkow@39302
   129
  by (simp add: present_def fun_eq_iff)
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
wenzelm@63167
   136
text \<open>Monad operations\<close>
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@40671
   146
lemma effect_refI [effect_intros]:
haftmann@37771
   147
  assumes "(r, h') = alloc v h"
haftmann@40671
   148
  shows "effect (ref v) h h' r"
haftmann@40671
   149
  by (rule effectI) (insert assms, simp add: execute_simps)
haftmann@37771
   150
haftmann@40671
   151
lemma effect_refE [effect_elims]:
haftmann@40671
   152
  assumes "effect (ref v) h h' r"
haftmann@37796
   153
  obtains "get h' r = v" and "present h' r" and "\<not> present h r"
haftmann@40671
   154
  using assms by (rule effectE) (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@40671
   164
lemma effect_lookupI [effect_intros]:
haftmann@37796
   165
  assumes "h' = h" "x = get h r"
haftmann@40671
   166
  shows "effect (!r) h h' x"
haftmann@40671
   167
  by (rule effectI) (insert assms, simp add: execute_simps)
haftmann@37771
   168
haftmann@40671
   169
lemma effect_lookupE [effect_elims]:
haftmann@40671
   170
  assumes "effect (!r) h h' x"
haftmann@37796
   171
  obtains "h' = h" "x = get h r"
haftmann@40671
   172
  using assms by (rule effectE) (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@40671
   182
lemma effect_updateI [effect_intros]:
haftmann@37796
   183
  assumes "h' = set r v h"
haftmann@40671
   184
  shows "effect (r := v) h h' x"
haftmann@40671
   185
  by (rule effectI) (insert assms, simp add: execute_simps)
haftmann@37771
   186
haftmann@40671
   187
lemma effect_updateE [effect_elims]:
haftmann@40671
   188
  assumes "effect (r' := v) h h' r"
haftmann@37796
   189
  obtains "h' = set r' v h"
haftmann@40671
   190
  using assms by (rule effectE) (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@40671
   198
  by (auto intro!: success_intros effect_intros simp add: change_def)
haftmann@37771
   199
haftmann@40671
   200
lemma effect_changeI [effect_intros]: 
haftmann@37796
   201
  assumes "h' = set r (f (get h r)) h" "x = f (get h r)"
haftmann@40671
   202
  shows "effect (change f r) h h' x"
haftmann@40671
   203
  by (rule effectI) (insert assms, simp add: execute_simps)  
haftmann@37771
   204
haftmann@40671
   205
lemma effect_changeE [effect_elims]:
haftmann@40671
   206
  assumes "effect (change f r') h h' r"
haftmann@37796
   207
  obtains "h' = set r' (f (get h r')) h" "r = f (get h r')"
haftmann@40671
   208
  using assms by (rule effectE) (simp add: execute_simps)
haftmann@26170
   209
haftmann@26170
   210
lemma lookup_chain:
wenzelm@62026
   211
  "(!r \<then> 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]:
wenzelm@62026
   215
  "r := e = change (\<lambda>_. e) r \<then> return ()"
haftmann@37725
   216
  by (rule Heap_eqI) (simp add: change_def lookup_chain)
haftmann@26170
   217
haftmann@26182
   218
wenzelm@63167
   219
text \<open>Non-interaction between imperative arrays and imperative references\<close>
haftmann@37719
   220
haftmann@37806
   221
lemma array_get_set [simp]:
haftmann@37806
   222
  "Array.get (set r v h) = Array.get h"
nipkow@39302
   223
  by (simp add: Array.get_def set_def fun_eq_iff)
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"
nipkow@39302
   243
  by (simp add: Array.get_def alloc_def set_def Let_def fun_eq_iff)
haftmann@37719
   244
haftmann@37796
   245
lemma present_update [simp]: 
haftmann@37796
   246
  "present (Array.update a i v h) = present h"
nipkow@39302
   247
  by (simp add: Array.update_def Array.set_def fun_eq_iff 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"
nipkow@39302
   251
  by (simp add: Array.present_def set_def fun_eq_iff)
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
wenzelm@63167
   264
subsection \<open>Code generator setup\<close>
haftmann@26182
   265
wenzelm@63167
   266
text \<open>Intermediate operation avoids invariance problem in \<open>Scala\<close> (similar to value restriction)\<close>
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
wenzelm@63167
   276
text \<open>SML / Eval\<close>
haftmann@26182
   277
haftmann@52435
   278
code_printing type_constructor ref \<rightharpoonup> (SML) "_/ ref"
haftmann@52435
   279
code_printing type_constructor ref \<rightharpoonup> (Eval) "_/ Unsynchronized.ref"
haftmann@52435
   280
code_printing constant Ref \<rightharpoonup> (SML) "raise/ (Fail/ \"bare Ref\")"
haftmann@52435
   281
code_printing constant ref' \<rightharpoonup> (SML) "(fn/ ()/ =>/ ref/ _)"
haftmann@52435
   282
code_printing constant ref' \<rightharpoonup> (Eval) "(fn/ ()/ =>/ Unsynchronized.ref/ _)"
haftmann@52435
   283
code_printing constant Ref.lookup \<rightharpoonup> (SML) "(fn/ ()/ =>/ !/ _)"
haftmann@52435
   284
code_printing constant Ref.update \<rightharpoonup> (SML) "(fn/ ()/ =>/ _/ :=/ _)"
haftmann@52435
   285
code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (SML) infixl 6 "="
haftmann@26182
   286
haftmann@39607
   287
code_reserved Eval Unsynchronized
haftmann@26182
   288
haftmann@26182
   289
wenzelm@63167
   290
text \<open>OCaml\<close>
haftmann@26182
   291
haftmann@52435
   292
code_printing type_constructor ref \<rightharpoonup> (OCaml) "_/ ref"
haftmann@52435
   293
code_printing constant Ref \<rightharpoonup> (OCaml) "failwith/ \"bare Ref\""
haftmann@52435
   294
code_printing constant ref' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ ref/ _)"
haftmann@52435
   295
code_printing constant Ref.lookup \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ !/ _)"
haftmann@52435
   296
code_printing constant Ref.update \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ _/ :=/ _)"
haftmann@52435
   297
code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (OCaml) infixl 4 "="
haftmann@26182
   298
haftmann@26182
   299
code_reserved OCaml ref
haftmann@26182
   300
haftmann@26182
   301
wenzelm@63167
   302
text \<open>Haskell\<close>
haftmann@26182
   303
haftmann@52435
   304
code_printing type_constructor ref \<rightharpoonup> (Haskell) "Heap.STRef/ Heap.RealWorld/ _"
haftmann@52435
   305
code_printing constant Ref \<rightharpoonup> (Haskell) "error/ \"bare Ref\""
haftmann@52435
   306
code_printing constant ref' \<rightharpoonup> (Haskell) "Heap.newSTRef"
haftmann@52435
   307
code_printing constant Ref.lookup \<rightharpoonup> (Haskell) "Heap.readSTRef"
haftmann@52435
   308
code_printing constant Ref.update \<rightharpoonup> (Haskell) "Heap.writeSTRef"
haftmann@52435
   309
code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "=="
haftmann@52435
   310
code_printing class_instance ref :: HOL.equal \<rightharpoonup> (Haskell) -
haftmann@26182
   311
haftmann@37842
   312
wenzelm@63167
   313
text \<open>Scala\<close>
haftmann@37842
   314
haftmann@52435
   315
code_printing type_constructor ref \<rightharpoonup> (Scala) "!Ref[_]"
haftmann@52435
   316
code_printing constant Ref \<rightharpoonup> (Scala) "!sys.error(\"bare Ref\")"
haftmann@52435
   317
code_printing constant ref' \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Ref((_))"
haftmann@52435
   318
code_printing constant Ref.lookup \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Ref.lookup((_))"
haftmann@52435
   319
code_printing constant Ref.update \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Ref.update((_), (_))"
haftmann@52435
   320
code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (Scala) infixl 5 "=="
haftmann@37842
   321
haftmann@37758
   322
end