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