src/HOL/Library/Relational.thy
author wenzelm
Thu Oct 16 22:44:24 2008 +0200 (2008-10-16)
changeset 28615 4c8fa015ec7f
parent 28145 af3923ed4786
child 28744 9257bb7bcd2d
permissions -rw-r--r--
explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;
bulwahn@27656
     1
theory Relational 
bulwahn@27656
     2
imports Array Ref Assert
bulwahn@27656
     3
begin
bulwahn@27656
     4
bulwahn@27656
     5
section{* Definition of the Relational framework *}
bulwahn@27656
     6
bulwahn@27656
     7
text {* The crel predicate states that when a computation c runs with the heap h
bulwahn@27656
     8
  will result in return value r and a heap h' (if no exception occurs). *}  
bulwahn@27656
     9
bulwahn@27656
    10
definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@27656
    11
where
bulwahn@27656
    12
  crel_def': "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = (Inl r, h')"
bulwahn@27656
    13
bulwahn@27656
    14
lemma crel_def: -- FIXME
bulwahn@27656
    15
  "crel c h h' r \<longleftrightarrow> (Inl r, h') = Heap_Monad.execute c h"
bulwahn@27656
    16
  unfolding crel_def' by auto
bulwahn@27656
    17
bulwahn@27656
    18
lemma crel_deterministic: "\<lbrakk> crel f h h' a; crel f h h'' b \<rbrakk> \<Longrightarrow> (a = b) \<and> (h' = h'')"
bulwahn@27656
    19
unfolding crel_def' by auto
bulwahn@27656
    20
bulwahn@27656
    21
section {* Elimination rules *}
bulwahn@27656
    22
bulwahn@27656
    23
text {* For all commands, we define simple elimination rules. *}
bulwahn@27656
    24
(* FIXME: consumes 1 necessary ?? *)
bulwahn@27656
    25
bulwahn@27656
    26
subsection {* Elimination rules for basic monadic commands *}
bulwahn@27656
    27
bulwahn@27656
    28
lemma crelE[consumes 1]:
bulwahn@27656
    29
  assumes "crel (f >>= g) h h'' r'"
bulwahn@27656
    30
  obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
bulwahn@27656
    31
  using assms
bulwahn@27656
    32
  by (auto simp add: crel_def bindM_def Let_def prod_case_beta split_def Pair_fst_snd_eq split add: sum.split_asm)
bulwahn@27656
    33
bulwahn@27656
    34
lemma crelE'[consumes 1]:
bulwahn@27656
    35
  assumes "crel (f >> g) h h'' r'"
bulwahn@27656
    36
  obtains h' r where "crel f h h' r" "crel g h' h'' r'"
bulwahn@27656
    37
  using assms
bulwahn@27656
    38
  by (elim crelE) auto
bulwahn@27656
    39
bulwahn@27656
    40
lemma crel_return[consumes 1]:
bulwahn@27656
    41
  assumes "crel (return x) h h' r"
bulwahn@27656
    42
  obtains "r = x" "h = h'"
bulwahn@27656
    43
  using assms
bulwahn@27656
    44
  unfolding crel_def return_def by simp
bulwahn@27656
    45
bulwahn@27656
    46
lemma crel_raise[consumes 1]:
bulwahn@27656
    47
  assumes "crel (raise x) h h' r"
bulwahn@27656
    48
  obtains "False"
bulwahn@27656
    49
  using assms
bulwahn@27656
    50
  unfolding crel_def raise_def by simp
bulwahn@27656
    51
bulwahn@27656
    52
lemma crel_if:
bulwahn@27656
    53
  assumes "crel (if c then t else e) h h' r"
bulwahn@27656
    54
  obtains "c" "crel t h h' r"
bulwahn@27656
    55
        | "\<not>c" "crel e h h' r"
bulwahn@27656
    56
  using assms
bulwahn@27656
    57
  unfolding crel_def by auto
bulwahn@27656
    58
bulwahn@27656
    59
lemma crel_option_case:
bulwahn@27656
    60
  assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
bulwahn@27656
    61
  obtains "x = None" "crel n h h' r"
bulwahn@27656
    62
        | y where "x = Some y" "crel (s y) h h' r" 
bulwahn@27656
    63
  using assms
bulwahn@27656
    64
  unfolding crel_def by auto
bulwahn@27656
    65
bulwahn@27656
    66
lemma crel_mapM:
bulwahn@27656
    67
  assumes "crel (mapM f xs) h h' r"
bulwahn@27656
    68
  assumes "\<And>h h'. P f [] h h' []"
bulwahn@27656
    69
  assumes "\<And>h h1 h' x xs y ys. \<lbrakk> crel (f x) h h1 y; crel (mapM f xs) h1 h' ys; P f xs h1 h' ys \<rbrakk> \<Longrightarrow> P f (x#xs) h h' (y#ys)"
bulwahn@27656
    70
  shows "P f xs h h' r"
bulwahn@27656
    71
using assms(1)
bulwahn@27656
    72
proof (induct xs arbitrary: h h' r)
bulwahn@27656
    73
  case Nil  with assms(2) show ?case
bulwahn@27656
    74
    by (auto elim: crel_return)
bulwahn@27656
    75
next
bulwahn@27656
    76
  case (Cons x xs)
bulwahn@27656
    77
  from Cons(2) obtain h1 y ys where crel_f: "crel (f x) h h1 y"
bulwahn@27656
    78
    and crel_mapM: "crel (mapM f xs) h1 h' ys"
bulwahn@27656
    79
    and r_def: "r = y#ys"
haftmann@28145
    80
    unfolding mapM.simps
bulwahn@27656
    81
    by (auto elim!: crelE crel_return)
bulwahn@27656
    82
  from Cons(1)[OF crel_mapM] crel_mapM crel_f assms(3) r_def
bulwahn@27656
    83
  show ?case by auto
bulwahn@27656
    84
qed
bulwahn@27656
    85
bulwahn@27656
    86
lemma crel_heap:
bulwahn@27656
    87
  assumes "crel (Heap_Monad.heap f) h h' r"
bulwahn@27656
    88
  obtains "h' = snd (f h)" "r = fst (f h)"
bulwahn@27656
    89
  using assms
bulwahn@27656
    90
  unfolding heap_def crel_def apfst_def split_def prod_fun_def by simp_all
bulwahn@27656
    91
bulwahn@27656
    92
subsection {* Elimination rules for array commands *}
bulwahn@27656
    93
bulwahn@27656
    94
lemma crel_length:
bulwahn@27656
    95
  assumes "crel (length a) h h' r"
bulwahn@27656
    96
  obtains "h = h'" "r = Heap.length a h'"
bulwahn@27656
    97
  using assms
bulwahn@27656
    98
  unfolding length_def
bulwahn@27656
    99
  by (elim crel_heap) simp
bulwahn@27656
   100
bulwahn@27656
   101
(* Strong version of the lemma for this operation is missing *) 
bulwahn@27656
   102
lemma crel_new_weak:
bulwahn@27656
   103
  assumes "crel (Array.new n v) h h' r"
bulwahn@27656
   104
  obtains "get_array r h' = List.replicate n v"
bulwahn@27656
   105
  using assms unfolding  Array.new_def
bulwahn@27656
   106
  by (elim crel_heap) (auto simp:Heap.array_def Let_def split_def)
bulwahn@27656
   107
bulwahn@27656
   108
lemma crel_nth[consumes 1]:
bulwahn@27656
   109
  assumes "crel (nth a i) h h' r"
bulwahn@27656
   110
  obtains "r = (get_array a h) ! i" "h = h'" "i < Heap.length a h"
bulwahn@27656
   111
  using assms
haftmann@28145
   112
  unfolding nth_def
bulwahn@27656
   113
  by (auto elim!: crelE crel_if crel_raise crel_length crel_heap)
bulwahn@27656
   114
bulwahn@27656
   115
lemma crel_upd[consumes 1]:
bulwahn@27656
   116
  assumes "crel (upd i v a) h h' r"
bulwahn@27656
   117
  obtains "r = a" "h' = Heap.upd a i v h"
bulwahn@27656
   118
  using assms
haftmann@28145
   119
  unfolding upd_def
bulwahn@27656
   120
  by (elim crelE crel_if crel_return crel_raise
bulwahn@27656
   121
    crel_length crel_heap) auto
bulwahn@27656
   122
bulwahn@27656
   123
(* Strong version of the lemma for this operation is missing *)
bulwahn@27656
   124
lemma crel_of_list_weak:
bulwahn@27656
   125
  assumes "crel (Array.of_list xs) h h' r"
bulwahn@27656
   126
  obtains "get_array r h' = xs"
bulwahn@27656
   127
  using assms
bulwahn@27656
   128
  unfolding of_list_def 
bulwahn@27656
   129
  by (elim crel_heap) (simp add:get_array_init_array_list)
bulwahn@27656
   130
bulwahn@27656
   131
lemma crel_map_entry:
bulwahn@27656
   132
  assumes "crel (Array.map_entry i f a) h h' r"
bulwahn@27656
   133
  obtains "r = a" "h' = Heap.upd a i (f (get_array a h ! i)) h"
bulwahn@27656
   134
  using assms
haftmann@28145
   135
  unfolding Array.map_entry_def
bulwahn@27656
   136
  by (elim crelE crel_upd crel_nth) auto
bulwahn@27656
   137
bulwahn@27656
   138
lemma crel_swap:
bulwahn@27656
   139
  assumes "crel (Array.swap i x a) h h' r"
bulwahn@27656
   140
  obtains "r = get_array a h ! i" "h' = Heap.upd a i x h"
bulwahn@27656
   141
  using assms
haftmann@28145
   142
  unfolding Array.swap_def
bulwahn@27656
   143
  by (elim crelE crel_upd crel_nth crel_return) auto
bulwahn@27656
   144
bulwahn@27656
   145
(* Strong version of the lemma for this operation is missing *)
bulwahn@27656
   146
lemma crel_make_weak:
bulwahn@27656
   147
  assumes "crel (Array.make n f) h h' r"
bulwahn@27656
   148
  obtains "i < n \<Longrightarrow> get_array r h' ! i = f i"
bulwahn@27656
   149
  using assms
bulwahn@27656
   150
  unfolding Array.make_def
bulwahn@27656
   151
  by (elim crel_of_list_weak) auto
bulwahn@27656
   152
bulwahn@27656
   153
lemma upt_conv_Cons':
bulwahn@27656
   154
  assumes "Suc a \<le> b"
bulwahn@27656
   155
  shows "[b - Suc a..<b] = (b - Suc a)#[b - a..<b]"
bulwahn@27656
   156
proof -
bulwahn@27656
   157
  from assms have l: "b - Suc a < b" by arith
bulwahn@27656
   158
  from assms have "Suc (b - Suc a) = b - a" by arith
bulwahn@27656
   159
  with l show ?thesis by (simp add: upt_conv_Cons)
bulwahn@27656
   160
qed
bulwahn@27656
   161
bulwahn@27656
   162
lemma crel_mapM_nth:
bulwahn@27656
   163
  assumes
bulwahn@27656
   164
  "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' xs"
bulwahn@27656
   165
  assumes "n \<le> Heap.length a h"
bulwahn@27656
   166
  shows "h = h' \<and> xs = drop (Heap.length a h - n) (get_array a h)"
bulwahn@27656
   167
using assms
bulwahn@27656
   168
proof (induct n arbitrary: xs h h')
bulwahn@27656
   169
  case 0 thus ?case
bulwahn@27656
   170
    by (auto elim!: crel_return simp add: Heap.length_def)
bulwahn@27656
   171
next
bulwahn@27656
   172
  case (Suc n)
bulwahn@27656
   173
  from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
bulwahn@27656
   174
    by (simp add: upt_conv_Cons')
bulwahn@27656
   175
  with Suc(2) obtain r where
bulwahn@27656
   176
    crel_mapM: "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' r"
bulwahn@27656
   177
    and xs_def: "xs = get_array a h ! (Heap.length a h - Suc n) # r"
haftmann@28145
   178
    by (auto elim!: crelE crel_nth crel_return)
bulwahn@27656
   179
  from Suc(3) have "Heap.length a h - n = Suc (Heap.length a h - Suc n)" 
bulwahn@27656
   180
    by arith
bulwahn@27656
   181
  with Suc.hyps[OF crel_mapM] xs_def show ?case
bulwahn@27656
   182
    unfolding Heap.length_def
bulwahn@27656
   183
    by (auto simp add: nth_drop')
bulwahn@27656
   184
qed
bulwahn@27656
   185
bulwahn@27656
   186
lemma crel_freeze:
bulwahn@27656
   187
  assumes "crel (Array.freeze a) h h' xs"
bulwahn@27656
   188
  obtains "h = h'" "xs = get_array a h"
bulwahn@27656
   189
proof 
bulwahn@27656
   190
  from assms have "crel (mapM (Array.nth a) [0..<Heap.length a h]) h h' xs"
haftmann@28145
   191
    unfolding freeze_def
bulwahn@27656
   192
    by (auto elim: crelE crel_length)
bulwahn@27656
   193
  hence "crel (mapM (Array.nth a) [(Heap.length a h - Heap.length a h)..<Heap.length a h]) h h' xs"
bulwahn@27656
   194
    by simp
bulwahn@27656
   195
  from crel_mapM_nth[OF this] show "h = h'" and "xs = get_array a h" by auto
bulwahn@27656
   196
qed
bulwahn@27656
   197
bulwahn@27656
   198
lemma crel_mapM_map_entry_remains:
bulwahn@27656
   199
  assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
bulwahn@27656
   200
  assumes "i < Heap.length a h - n"
bulwahn@27656
   201
  shows "get_array a h ! i = get_array a h' ! i"
bulwahn@27656
   202
using assms
bulwahn@27656
   203
proof (induct n arbitrary: h h' r)
bulwahn@27656
   204
  case 0
bulwahn@27656
   205
  thus ?case
bulwahn@27656
   206
    by (auto elim: crel_return)
bulwahn@27656
   207
next
bulwahn@27656
   208
  case (Suc n)
bulwahn@27656
   209
  let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
bulwahn@27656
   210
  from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
bulwahn@27656
   211
    by (simp add: upt_conv_Cons')
bulwahn@27656
   212
  from Suc(2) this obtain r where
bulwahn@27656
   213
    crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
haftmann@28145
   214
    by (auto simp add: elim!: crelE crel_map_entry crel_return)
bulwahn@27656
   215
  have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
bulwahn@27656
   216
  from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
bulwahn@27656
   217
    by simp
bulwahn@27656
   218
  from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
bulwahn@27656
   219
qed
bulwahn@27656
   220
bulwahn@27656
   221
lemma crel_mapM_map_entry_changes:
bulwahn@27656
   222
  assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
bulwahn@27656
   223
  assumes "n \<le> Heap.length a h"  
bulwahn@27656
   224
  assumes "i \<ge> Heap.length a h - n"
bulwahn@27656
   225
  assumes "i < Heap.length a h"
bulwahn@27656
   226
  shows "get_array a h' ! i = f (get_array a h ! i)"
bulwahn@27656
   227
using assms
bulwahn@27656
   228
proof (induct n arbitrary: h h' r)
bulwahn@27656
   229
  case 0
bulwahn@27656
   230
  thus ?case
bulwahn@27656
   231
    by (auto elim!: crel_return)
bulwahn@27656
   232
next
bulwahn@27656
   233
  case (Suc n)
bulwahn@27656
   234
  let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
bulwahn@27656
   235
  from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
bulwahn@27656
   236
    by (simp add: upt_conv_Cons')
bulwahn@27656
   237
  from Suc(2) this obtain r where
bulwahn@27656
   238
    crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
haftmann@28145
   239
    by (auto simp add: elim!: crelE crel_map_entry crel_return)
bulwahn@27656
   240
  have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
bulwahn@27656
   241
  from Suc(3) have less: "Heap.length a h - Suc n < Heap.length a h - n" by arith
bulwahn@27656
   242
  from Suc(3) have less2: "Heap.length a h - Suc n < Heap.length a h" by arith
bulwahn@27656
   243
  from Suc(4) length_remains have cases: "i = Heap.length a ?h1 - Suc n \<or> i \<ge> Heap.length a ?h1 - n" by arith
bulwahn@27656
   244
  from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
bulwahn@27656
   245
    by simp
bulwahn@27656
   246
  from Suc(1)[OF this] cases Suc(3) Suc(5) length_remains
bulwahn@27656
   247
    crel_mapM_map_entry_remains[OF this, of "Heap.length a h - Suc n", symmetric] less less2
bulwahn@27656
   248
  show ?case
bulwahn@27656
   249
    by (auto simp add: nth_list_update_eq Heap.length_def)
bulwahn@27656
   250
qed
bulwahn@27656
   251
bulwahn@27656
   252
lemma crel_mapM_map_entry_length:
bulwahn@27656
   253
  assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
bulwahn@27656
   254
  assumes "n \<le> Heap.length a h"
bulwahn@27656
   255
  shows "Heap.length a h' = Heap.length a h"
bulwahn@27656
   256
using assms
bulwahn@27656
   257
proof (induct n arbitrary: h h' r)
bulwahn@27656
   258
  case 0
bulwahn@27656
   259
  thus ?case by (auto elim!: crel_return)
bulwahn@27656
   260
next
bulwahn@27656
   261
  case (Suc n)
bulwahn@27656
   262
  let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
bulwahn@27656
   263
  from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
bulwahn@27656
   264
    by (simp add: upt_conv_Cons')
bulwahn@27656
   265
  from Suc(2) this obtain r where 
bulwahn@27656
   266
    crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
haftmann@28145
   267
    by (auto elim!: crelE crel_map_entry crel_return)
bulwahn@27656
   268
  have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
bulwahn@27656
   269
  from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
bulwahn@27656
   270
    by simp
bulwahn@27656
   271
  from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
bulwahn@27656
   272
qed
bulwahn@27656
   273
bulwahn@27656
   274
lemma crel_mapM_map_entry:
bulwahn@27656
   275
assumes "crel (mapM (\<lambda>n. map_entry n f a) [0..<Heap.length a h]) h h' r"
bulwahn@27656
   276
  shows "get_array a h' = List.map f (get_array a h)"
bulwahn@27656
   277
proof -
bulwahn@27656
   278
  from assms have "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - Heap.length a h..<Heap.length a h]) h h' r" by simp
bulwahn@27656
   279
  from crel_mapM_map_entry_length[OF this]
bulwahn@27656
   280
  crel_mapM_map_entry_changes[OF this] show ?thesis
bulwahn@27656
   281
    unfolding Heap.length_def
bulwahn@27656
   282
    by (auto intro: nth_equalityI)
bulwahn@27656
   283
qed
bulwahn@27656
   284
bulwahn@27656
   285
lemma crel_map_weak:
bulwahn@27656
   286
  assumes crel_map: "crel (Array.map f a) h h' r"
bulwahn@27656
   287
  obtains "r = a" "get_array a h' = List.map f (get_array a h)"
bulwahn@27656
   288
proof
bulwahn@27656
   289
  from assms crel_mapM_map_entry show  "get_array a h' = List.map f (get_array a h)"
haftmann@28145
   290
    unfolding Array.map_def
bulwahn@27656
   291
    by (fastsimp elim!: crelE crel_length crel_return)
bulwahn@27656
   292
  from assms show "r = a"
haftmann@28145
   293
    unfolding Array.map_def
bulwahn@27656
   294
    by (elim crelE crel_return)
bulwahn@27656
   295
qed
bulwahn@27656
   296
bulwahn@27656
   297
subsection {* Elimination rules for reference commands *}
bulwahn@27656
   298
bulwahn@27656
   299
(* TODO:
bulwahn@27656
   300
maybe introduce a new predicate "extends h' h x"
bulwahn@27656
   301
which means h' extends h with a new reference x.
bulwahn@27656
   302
Then crel_new: would be
bulwahn@27656
   303
assumes "crel (Ref.new v) h h' x"
bulwahn@27656
   304
obtains "get_ref x h' = v"
bulwahn@27656
   305
and "extends h' h x"
bulwahn@27656
   306
bulwahn@27656
   307
and we would need further rules for extends:
bulwahn@27656
   308
extends h' h x \<Longrightarrow> \<not> ref_present x h
bulwahn@27656
   309
extends h' h x \<Longrightarrow>  ref_present x h'
bulwahn@27656
   310
extends h' h x \<Longrightarrow> ref_present y h \<Longrightarrow> ref_present y h'
bulwahn@27656
   311
extends h' h x \<Longrightarrow> ref_present y h \<Longrightarrow> get_ref y h = get_ref y h'
bulwahn@27656
   312
extends h' h x \<Longrightarrow> lim h' = Suc (lim h)
bulwahn@27656
   313
*)
bulwahn@27656
   314
bulwahn@27656
   315
lemma crel_Ref_new:
bulwahn@27656
   316
  assumes "crel (Ref.new v) h h' x"
bulwahn@27656
   317
  obtains "get_ref x h' = v"
bulwahn@27656
   318
  and "\<not> ref_present x h"
bulwahn@27656
   319
  and "ref_present x h'"
bulwahn@27656
   320
  and "\<forall>y. ref_present y h \<longrightarrow> get_ref y h = get_ref y h'"
bulwahn@27656
   321
 (* and "lim h' = Suc (lim h)" *)
bulwahn@27656
   322
  and "\<forall>y. ref_present y h \<longrightarrow> ref_present y h'"
bulwahn@27656
   323
  using assms
bulwahn@27656
   324
  unfolding Ref.new_def
bulwahn@27656
   325
  apply (elim crel_heap)
bulwahn@27656
   326
  unfolding Heap.ref_def
bulwahn@27656
   327
  apply (simp add: Let_def)
bulwahn@27656
   328
  unfolding Heap.new_ref_def
bulwahn@27656
   329
  apply (simp add: Let_def)
bulwahn@27656
   330
  unfolding ref_present_def
bulwahn@27656
   331
  apply auto
bulwahn@27656
   332
  unfolding get_ref_def set_ref_def
bulwahn@27656
   333
  apply auto
bulwahn@27656
   334
  done
bulwahn@27656
   335
bulwahn@27656
   336
lemma crel_lookup:
bulwahn@27656
   337
  assumes "crel (!ref) h h' r"
bulwahn@27656
   338
  obtains "h = h'" "r = get_ref ref h"
bulwahn@27656
   339
using assms
bulwahn@27656
   340
unfolding Ref.lookup_def
bulwahn@27656
   341
by (auto elim: crel_heap)
bulwahn@27656
   342
bulwahn@27656
   343
lemma crel_update:
bulwahn@27656
   344
  assumes "crel (ref := v) h h' r"
bulwahn@27656
   345
  obtains "h' = set_ref ref v h" "r = ()"
bulwahn@27656
   346
using assms
bulwahn@27656
   347
unfolding Ref.update_def
bulwahn@27656
   348
by (auto elim: crel_heap)
bulwahn@27656
   349
bulwahn@27656
   350
lemma crel_change:
bulwahn@27656
   351
  assumes "crel (Ref.change f ref) h h' r"
bulwahn@27656
   352
  obtains "h' = set_ref ref (f (get_ref ref h)) h" "r = f (get_ref ref h)"
bulwahn@27656
   353
using assms
haftmann@28145
   354
unfolding Ref.change_def Let_def
bulwahn@27656
   355
by (auto elim!: crelE crel_lookup crel_update crel_return)
bulwahn@27656
   356
bulwahn@27656
   357
subsection {* Elimination rules for the assert command *}
bulwahn@27656
   358
bulwahn@27656
   359
lemma crel_assert[consumes 1]:
bulwahn@27656
   360
  assumes "crel (assert P x) h h' r"
bulwahn@27656
   361
  obtains "P x" "r = x" "h = h'"
bulwahn@27656
   362
  using assms
bulwahn@27656
   363
  unfolding assert_def
bulwahn@27656
   364
  by (elim crel_if crel_return crel_raise) auto
bulwahn@27656
   365
bulwahn@27656
   366
lemma crel_assert_eq: "(\<And>h h' r. crel f h h' r \<Longrightarrow> P r) \<Longrightarrow> f \<guillemotright>= assert P = f"
bulwahn@27656
   367
unfolding crel_def bindM_def Let_def assert_def
bulwahn@27656
   368
  raise_def return_def prod_case_beta
bulwahn@27656
   369
apply (cases f)
bulwahn@27656
   370
apply simp
bulwahn@27656
   371
apply (simp add: expand_fun_eq split_def)
bulwahn@27656
   372
apply auto
bulwahn@27656
   373
apply (case_tac "fst (fun x)")
bulwahn@27656
   374
apply (simp_all add: Pair_fst_snd_eq)
bulwahn@27656
   375
apply (erule_tac x="x" in meta_allE)
bulwahn@27656
   376
apply fastsimp
bulwahn@27656
   377
done
bulwahn@27656
   378
bulwahn@27656
   379
section {* Introduction rules *}
bulwahn@27656
   380
bulwahn@27656
   381
subsection {* Introduction rules for basic monadic commands *}
bulwahn@27656
   382
bulwahn@27656
   383
lemma crelI:
bulwahn@27656
   384
  assumes "crel f h h' r" "crel (g r) h' h'' r'"
bulwahn@27656
   385
  shows "crel (f >>= g) h h'' r'"
bulwahn@27656
   386
  using assms by (simp add: crel_def' bindM_def)
bulwahn@27656
   387
bulwahn@27656
   388
lemma crelI':
bulwahn@27656
   389
  assumes "crel f h h' r" "crel g h' h'' r'"
bulwahn@27656
   390
  shows "crel (f >> g) h h'' r'"
bulwahn@27656
   391
  using assms by (intro crelI) auto
bulwahn@27656
   392
bulwahn@27656
   393
lemma crel_returnI:
bulwahn@27656
   394
  shows "crel (return x) h h x"
bulwahn@27656
   395
  unfolding crel_def return_def by simp
bulwahn@27656
   396
bulwahn@27656
   397
lemma crel_raiseI:
bulwahn@27656
   398
  shows "\<not> (crel (raise x) h h' r)"
bulwahn@27656
   399
  unfolding crel_def raise_def by simp
bulwahn@27656
   400
bulwahn@27656
   401
lemma crel_ifI:
bulwahn@27656
   402
  assumes "c \<longrightarrow> crel t h h' r"
bulwahn@27656
   403
  "\<not>c \<longrightarrow> crel e h h' r"
bulwahn@27656
   404
  shows "crel (if c then t else e) h h' r"
bulwahn@27656
   405
  using assms
bulwahn@27656
   406
  unfolding crel_def by auto
bulwahn@27656
   407
bulwahn@27656
   408
lemma crel_option_caseI:
bulwahn@27656
   409
  assumes "\<And>y. x = Some y \<Longrightarrow> crel (s y) h h' r"
bulwahn@27656
   410
  assumes "x = None \<Longrightarrow> crel n h h' r"
bulwahn@27656
   411
  shows "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
bulwahn@27656
   412
using assms
bulwahn@27656
   413
by (auto split: option.split)
bulwahn@27656
   414
bulwahn@27656
   415
lemma crel_heapI:
bulwahn@27656
   416
  shows "crel (Heap_Monad.heap f) h (snd (f h)) (fst (f h))"
bulwahn@27656
   417
  by (simp add: crel_def apfst_def split_def prod_fun_def)
bulwahn@27656
   418
bulwahn@27656
   419
lemma crel_heapI':
bulwahn@27656
   420
  assumes "h' = snd (f h)" "r = fst (f h)"
bulwahn@27656
   421
  shows "crel (Heap_Monad.heap f) h h' r"
bulwahn@27656
   422
  using assms
bulwahn@27656
   423
  by (simp add: crel_def split_def apfst_def prod_fun_def)
bulwahn@27656
   424
bulwahn@27656
   425
lemma crelI2:
bulwahn@27656
   426
  assumes "\<exists>h' rs'. crel f h h' rs' \<and> (\<exists>h'' rs. crel (g rs') h' h'' rs)"
bulwahn@27656
   427
  shows "\<exists>h'' rs. crel (f\<guillemotright>= g) h h'' rs"
bulwahn@27656
   428
  oops
bulwahn@27656
   429
bulwahn@27656
   430
lemma crel_ifI2:
bulwahn@27656
   431
  assumes "c \<Longrightarrow> \<exists>h' r. crel t h h' r"
bulwahn@27656
   432
  "\<not> c \<Longrightarrow> \<exists>h' r. crel e h h' r"
bulwahn@27656
   433
  shows "\<exists> h' r. crel (if c then t else e) h h' r"
bulwahn@27656
   434
  oops
bulwahn@27656
   435
bulwahn@27656
   436
subsection {* Introduction rules for array commands *}
bulwahn@27656
   437
bulwahn@27656
   438
lemma crel_lengthI:
bulwahn@27656
   439
  shows "crel (length a) h h (Heap.length a h)"
bulwahn@27656
   440
  unfolding length_def
bulwahn@27656
   441
  by (rule crel_heapI') auto
bulwahn@27656
   442
bulwahn@27656
   443
(* thm crel_newI for Array.new is missing *)
bulwahn@27656
   444
bulwahn@27656
   445
lemma crel_nthI:
bulwahn@27656
   446
  assumes "i < Heap.length a h"
bulwahn@27656
   447
  shows "crel (nth a i) h h ((get_array a h) ! i)"
bulwahn@27656
   448
  using assms
haftmann@28145
   449
  unfolding nth_def
bulwahn@27656
   450
  by (auto intro!: crelI crel_ifI crel_raiseI crel_lengthI crel_heapI')
bulwahn@27656
   451
bulwahn@27656
   452
lemma crel_updI:
bulwahn@27656
   453
  assumes "i < Heap.length a h"
bulwahn@27656
   454
  shows "crel (upd i v a) h (Heap.upd a i v h) a"
bulwahn@27656
   455
  using assms
haftmann@28145
   456
  unfolding upd_def
bulwahn@27656
   457
  by (auto intro!: crelI crel_ifI crel_returnI crel_raiseI
bulwahn@27656
   458
    crel_lengthI crel_heapI')
bulwahn@27656
   459
bulwahn@27656
   460
(* thm crel_of_listI is missing *)
bulwahn@27656
   461
bulwahn@27656
   462
(* thm crel_map_entryI is missing *)
bulwahn@27656
   463
bulwahn@27656
   464
(* thm crel_swapI is missing *)
bulwahn@27656
   465
bulwahn@27656
   466
(* thm crel_makeI is missing *)
bulwahn@27656
   467
bulwahn@27656
   468
(* thm crel_freezeI is missing *)
bulwahn@27656
   469
bulwahn@27656
   470
(* thm crel_mapI is missing *)
bulwahn@27656
   471
bulwahn@27656
   472
subsection {* Introduction rules for reference commands *}
bulwahn@27656
   473
bulwahn@27656
   474
lemma crel_lookupI:
bulwahn@27656
   475
  shows "crel (!ref) h h (get_ref ref h)"
bulwahn@27656
   476
  unfolding lookup_def by (auto intro!: crel_heapI')
bulwahn@27656
   477
bulwahn@27656
   478
lemma crel_updateI:
bulwahn@27656
   479
  shows "crel (ref := v) h (set_ref ref v h) ()"
bulwahn@27656
   480
  unfolding update_def by (auto intro!: crel_heapI')
bulwahn@27656
   481
bulwahn@27656
   482
lemma crel_changeI: 
bulwahn@27656
   483
  shows "crel (Ref.change f ref) h (set_ref ref (f (get_ref ref h)) h) (f (get_ref ref h))"
haftmann@28145
   484
unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
bulwahn@27656
   485
bulwahn@27656
   486
subsection {* Introduction rules for the assert command *}
bulwahn@27656
   487
bulwahn@27656
   488
lemma crel_assertI:
bulwahn@27656
   489
  assumes "P x"
bulwahn@27656
   490
  shows "crel (assert P x) h h x"
bulwahn@27656
   491
  using assms
bulwahn@27656
   492
  unfolding assert_def
bulwahn@27656
   493
  by (auto intro!: crel_ifI crel_returnI crel_raiseI)
bulwahn@27656
   494
 
bulwahn@27656
   495
section {* Defintion of the noError predicate *}
bulwahn@27656
   496
bulwahn@27656
   497
text {* We add a simple definitional setting for crel intro rules
bulwahn@27656
   498
  where we only would like to show that the computation does not result in a exception for heap h,
bulwahn@27656
   499
  but we do not care about statements about the resulting heap and return value.*}
bulwahn@27656
   500
bulwahn@27656
   501
definition noError :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool"
bulwahn@27656
   502
where
bulwahn@27656
   503
  "noError c h \<longleftrightarrow> (\<exists>r h'. (Inl r, h') = Heap_Monad.execute c h)"
bulwahn@27656
   504
bulwahn@27656
   505
lemma noError_def': -- FIXME
bulwahn@27656
   506
  "noError c h \<longleftrightarrow> (\<exists>r h'. Heap_Monad.execute c h = (Inl r, h'))"
bulwahn@27656
   507
  unfolding noError_def apply auto proof -
bulwahn@27656
   508
  fix r h'
bulwahn@27656
   509
  assume "(Inl r, h') = Heap_Monad.execute c h"
bulwahn@27656
   510
  then have "Heap_Monad.execute c h = (Inl r, h')" ..
bulwahn@27656
   511
  then show "\<exists>r h'. Heap_Monad.execute c h = (Inl r, h')" by blast
bulwahn@27656
   512
qed
bulwahn@27656
   513
bulwahn@27656
   514
subsection {* Introduction rules for basic monadic commands *}
bulwahn@27656
   515
bulwahn@27656
   516
lemma noErrorI:
bulwahn@27656
   517
  assumes "noError f h"
bulwahn@27656
   518
  assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError (g r) h'"
bulwahn@27656
   519
  shows "noError (f \<guillemotright>= g) h"
bulwahn@27656
   520
  using assms
bulwahn@27656
   521
  by (auto simp add: noError_def' crel_def' bindM_def)
bulwahn@27656
   522
bulwahn@27656
   523
lemma noErrorI':
bulwahn@27656
   524
  assumes "noError f h"
bulwahn@27656
   525
  assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError g h'"
bulwahn@27656
   526
  shows "noError (f \<guillemotright> g) h"
bulwahn@27656
   527
  using assms
bulwahn@27656
   528
  by (auto simp add: noError_def' crel_def' bindM_def)
bulwahn@27656
   529
bulwahn@27656
   530
lemma noErrorI2:
bulwahn@27656
   531
"\<lbrakk>crel f h h' r ; noError f h; noError (g r) h'\<rbrakk>
bulwahn@27656
   532
\<Longrightarrow> noError (f \<guillemotright>= g) h"
bulwahn@27656
   533
by (auto simp add: noError_def' crel_def' bindM_def)
bulwahn@27656
   534
bulwahn@27656
   535
lemma noError_return: 
bulwahn@27656
   536
  shows "noError (return x) h"
bulwahn@27656
   537
  unfolding noError_def return_def
bulwahn@27656
   538
  by auto
bulwahn@27656
   539
bulwahn@27656
   540
lemma noError_if:
bulwahn@27656
   541
  assumes "c \<Longrightarrow> noError t h" "\<not> c \<Longrightarrow> noError e h"
bulwahn@27656
   542
  shows "noError (if c then t else e) h"
bulwahn@27656
   543
  using assms
bulwahn@27656
   544
  unfolding noError_def
bulwahn@27656
   545
  by auto
bulwahn@27656
   546
bulwahn@27656
   547
lemma noError_option_case:
bulwahn@27656
   548
  assumes "\<And>y. x = Some y \<Longrightarrow> noError (s y) h"
bulwahn@27656
   549
  assumes "noError n h"
bulwahn@27656
   550
  shows "noError (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h"
bulwahn@27656
   551
using assms
bulwahn@27656
   552
by (auto split: option.split)
bulwahn@27656
   553
bulwahn@27656
   554
lemma noError_mapM: 
bulwahn@27656
   555
assumes "\<forall>x \<in> set xs. noError (f x) h \<and> crel (f x) h h (r x)" 
bulwahn@27656
   556
shows "noError (mapM f xs) h"
bulwahn@27656
   557
using assms
bulwahn@27656
   558
proof (induct xs)
bulwahn@27656
   559
  case Nil
bulwahn@27656
   560
  thus ?case
bulwahn@27656
   561
    unfolding mapM.simps by (intro noError_return)
bulwahn@27656
   562
next
bulwahn@27656
   563
  case (Cons x xs)
bulwahn@27656
   564
  thus ?case
haftmann@28145
   565
    unfolding mapM.simps
bulwahn@27656
   566
    by (auto intro: noErrorI2[of "f x"] noErrorI noError_return)
bulwahn@27656
   567
qed
bulwahn@27656
   568
bulwahn@27656
   569
lemma noError_heap:
bulwahn@27656
   570
  shows "noError (Heap_Monad.heap f) h"
bulwahn@27656
   571
  by (simp add: noError_def' apfst_def prod_fun_def split_def)
bulwahn@27656
   572
bulwahn@27656
   573
subsection {* Introduction rules for array commands *}
bulwahn@27656
   574
bulwahn@27656
   575
lemma noError_length:
bulwahn@27656
   576
  shows "noError (Array.length a) h"
bulwahn@27656
   577
  unfolding length_def
bulwahn@27656
   578
  by (intro noError_heap)
bulwahn@27656
   579
bulwahn@27656
   580
lemma noError_new:
bulwahn@27656
   581
  shows "noError (Array.new n v) h"
bulwahn@27656
   582
unfolding Array.new_def by (intro noError_heap)
bulwahn@27656
   583
bulwahn@27656
   584
lemma noError_upd:
bulwahn@27656
   585
  assumes "i < Heap.length a h"
bulwahn@27656
   586
  shows "noError (Array.upd i v a) h"
bulwahn@27656
   587
  using assms
haftmann@28145
   588
  unfolding upd_def
bulwahn@27656
   589
  by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
bulwahn@27656
   590
bulwahn@27656
   591
lemma noError_nth:
bulwahn@27656
   592
assumes "i < Heap.length a h"
bulwahn@27656
   593
  shows "noError (Array.nth a i) h"
bulwahn@27656
   594
  using assms
haftmann@28145
   595
  unfolding nth_def
bulwahn@27656
   596
  by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
bulwahn@27656
   597
bulwahn@27656
   598
lemma noError_of_list:
bulwahn@27656
   599
  shows "noError (of_list ls) h"
bulwahn@27656
   600
  unfolding of_list_def by (rule noError_heap)
bulwahn@27656
   601
bulwahn@27656
   602
lemma noError_map_entry:
bulwahn@27656
   603
  assumes "i < Heap.length a h"
bulwahn@27656
   604
  shows "noError (map_entry i f a) h"
bulwahn@27656
   605
  using assms
haftmann@28145
   606
  unfolding map_entry_def
bulwahn@27656
   607
  by (auto elim: crel_nth intro!: noErrorI noError_nth noError_upd)
bulwahn@27656
   608
bulwahn@27656
   609
lemma noError_swap:
bulwahn@27656
   610
  assumes "i < Heap.length a h"
bulwahn@27656
   611
  shows "noError (swap i x a) h"
bulwahn@27656
   612
  using assms
haftmann@28145
   613
  unfolding swap_def
bulwahn@27656
   614
  by (auto elim: crel_nth intro!: noErrorI noError_return noError_nth noError_upd)
bulwahn@27656
   615
bulwahn@27656
   616
lemma noError_make:
bulwahn@27656
   617
  shows "noError (make n f) h"
bulwahn@27656
   618
  unfolding make_def
bulwahn@27656
   619
  by (auto intro: noError_of_list)
bulwahn@27656
   620
bulwahn@27656
   621
(*TODO: move to HeapMonad *)
bulwahn@27656
   622
lemma mapM_append:
bulwahn@27656
   623
  "mapM f (xs @ ys) = mapM f xs \<guillemotright>= (\<lambda>xs. mapM f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
bulwahn@27656
   624
  by (induct xs) (simp_all add: monad_simp)
bulwahn@27656
   625
bulwahn@27656
   626
lemma noError_freeze:
bulwahn@27656
   627
  shows "noError (freeze a) h"
haftmann@28145
   628
unfolding freeze_def
bulwahn@27656
   629
by (auto intro!: noErrorI noError_length noError_mapM[of _ _ _ "\<lambda>x. get_array a h ! x"]
bulwahn@27656
   630
  noError_nth crel_nthI elim: crel_length)
bulwahn@27656
   631
bulwahn@27656
   632
lemma noError_mapM_map_entry:
bulwahn@27656
   633
  assumes "n \<le> Heap.length a h"
bulwahn@27656
   634
  shows "noError (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h"
bulwahn@27656
   635
using assms
bulwahn@27656
   636
proof (induct n arbitrary: h)
bulwahn@27656
   637
  case 0
bulwahn@27656
   638
  thus ?case by (auto intro: noError_return)
bulwahn@27656
   639
next
bulwahn@27656
   640
  case (Suc n)
bulwahn@27656
   641
  from Suc.prems have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
bulwahn@27656
   642
    by (simp add: upt_conv_Cons')
bulwahn@27656
   643
  with Suc.hyps[of "(Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h)"] Suc.prems show ?case
haftmann@28145
   644
    by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
bulwahn@27656
   645
qed
bulwahn@27656
   646
bulwahn@27656
   647
lemma noError_map:
bulwahn@27656
   648
  shows "noError (Array.map f a) h"
bulwahn@27656
   649
using noError_mapM_map_entry[of "Heap.length a h" a h]
haftmann@28145
   650
unfolding Array.map_def
bulwahn@27656
   651
by (auto intro: noErrorI noError_length noError_return elim!: crel_length)
bulwahn@27656
   652
bulwahn@27656
   653
subsection {* Introduction rules for the reference commands *}
bulwahn@27656
   654
bulwahn@27656
   655
lemma noError_Ref_new:
bulwahn@27656
   656
  shows "noError (Ref.new v) h"
bulwahn@27656
   657
unfolding Ref.new_def by (intro noError_heap)
bulwahn@27656
   658
bulwahn@27656
   659
lemma noError_lookup:
bulwahn@27656
   660
  shows "noError (!ref) h"
bulwahn@27656
   661
  unfolding lookup_def by (intro noError_heap)
bulwahn@27656
   662
bulwahn@27656
   663
lemma noError_update:
bulwahn@27656
   664
  shows "noError (ref := v) h"
bulwahn@27656
   665
  unfolding update_def by (intro noError_heap)
bulwahn@27656
   666
bulwahn@27656
   667
lemma noError_change:
bulwahn@27656
   668
  shows "noError (Ref.change f ref) h"
haftmann@28145
   669
  unfolding Ref.change_def Let_def by (intro noErrorI noError_lookup noError_update noError_return)
bulwahn@27656
   670
bulwahn@27656
   671
subsection {* Introduction rules for the assert command *}
bulwahn@27656
   672
bulwahn@27656
   673
lemma noError_assert:
bulwahn@27656
   674
  assumes "P x"
bulwahn@27656
   675
  shows "noError (assert P x) h"
bulwahn@27656
   676
  using assms
bulwahn@27656
   677
  unfolding assert_def
bulwahn@27656
   678
  by (auto intro: noError_if noError_return)
bulwahn@27656
   679
bulwahn@27656
   680
section {* Cumulative lemmas *}
bulwahn@27656
   681
bulwahn@27656
   682
lemmas crel_elim_all =
bulwahn@27656
   683
  crelE crelE' crel_return crel_raise crel_if crel_option_case
bulwahn@27656
   684
  crel_length crel_new_weak crel_nth crel_upd crel_of_list_weak crel_map_entry crel_swap crel_make_weak crel_freeze crel_map_weak
bulwahn@27656
   685
  crel_Ref_new crel_lookup crel_update crel_change
bulwahn@27656
   686
  crel_assert
bulwahn@27656
   687
bulwahn@27656
   688
lemmas crel_intro_all =
bulwahn@27656
   689
  crelI crelI' crel_returnI crel_raiseI crel_ifI crel_option_caseI
bulwahn@27656
   690
  crel_lengthI (* crel_newI *) crel_nthI crel_updI (* crel_of_listI crel_map_entryI crel_swapI crel_makeI crel_freezeI crel_mapI *)
bulwahn@27656
   691
  (* crel_Ref_newI *) crel_lookupI crel_updateI crel_changeI
bulwahn@27656
   692
  crel_assert
bulwahn@27656
   693
bulwahn@27656
   694
lemmas noError_intro_all = 
bulwahn@27656
   695
  noErrorI noErrorI' noError_return noError_if noError_option_case
bulwahn@27656
   696
  noError_length noError_new noError_nth noError_upd noError_of_list noError_map_entry noError_swap noError_make noError_freeze noError_map
bulwahn@27656
   697
  noError_Ref_new noError_lookup noError_update noError_change
bulwahn@27656
   698
  noError_assert
bulwahn@27656
   699
bulwahn@27656
   700
end