src/HOL/Hoare/Heap.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (2017-10-10)
changeset 66831 29ea2b900a05
parent 62042 6c6ccf573479
child 67613 ce654b0e6d69
permissions -rw-r--r--
tuned: each session has at most one defining entry;
nipkow@13875
     1
(*  Title:      HOL/Hoare/Heap.thy
nipkow@13875
     2
    Author:     Tobias Nipkow
nipkow@13875
     3
    Copyright   2002 TUM
nipkow@13875
     4
nipkow@13875
     5
Pointers, heaps and heap abstractions.
nipkow@13875
     6
See the paper by Mehta and Nipkow.
nipkow@13875
     7
*)
nipkow@13875
     8
haftmann@16417
     9
theory Heap imports Main begin
nipkow@13875
    10
nipkow@13875
    11
subsection "References"
nipkow@13875
    12
blanchet@58310
    13
datatype 'a ref = Null | Ref 'a
nipkow@13875
    14
nipkow@13875
    15
lemma not_Null_eq [iff]: "(x ~= Null) = (EX y. x = Ref y)"
nipkow@13875
    16
  by (induct x) auto
nipkow@13875
    17
nipkow@13875
    18
lemma not_Ref_eq [iff]: "(ALL y. x ~= Ref y) = (x = Null)"
nipkow@13875
    19
  by (induct x) auto
nipkow@13875
    20
haftmann@35416
    21
primrec addr :: "'a ref \<Rightarrow> 'a" where
haftmann@35416
    22
  "addr (Ref a) = a"
nipkow@13875
    23
nipkow@13875
    24
nipkow@13875
    25
section "The heap"
nipkow@13875
    26
nipkow@13875
    27
subsection "Paths in the heap"
nipkow@13875
    28
haftmann@35416
    29
primrec Path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool" where
haftmann@35416
    30
  "Path h x [] y \<longleftrightarrow> x = y"
haftmann@35416
    31
| "Path h x (a#as) y \<longleftrightarrow> x = Ref a \<and> Path h (h a) as y"
nipkow@13875
    32
nipkow@13875
    33
lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
nipkow@13875
    34
apply(case_tac xs)
nipkow@44890
    35
apply fastforce
nipkow@44890
    36
apply fastforce
nipkow@13875
    37
done
nipkow@13875
    38
nipkow@13875
    39
lemma [simp]: "Path h (Ref a) as z =
nipkow@13875
    40
 (as = [] \<and> z = Ref a  \<or>  (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))"
nipkow@13875
    41
apply(case_tac as)
nipkow@44890
    42
apply fastforce
nipkow@44890
    43
apply fastforce
nipkow@13875
    44
done
nipkow@13875
    45
nipkow@13875
    46
lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
nipkow@13875
    47
by(induct as, simp+)
nipkow@13875
    48
nipkow@13875
    49
lemma Path_upd[simp]:
nipkow@13875
    50
 "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
nipkow@13875
    51
by(induct as, simp, simp add:eq_sym_conv)
nipkow@13875
    52
nipkow@13875
    53
lemma Path_snoc:
nipkow@13875
    54
 "Path (f(a := q)) p as (Ref a) \<Longrightarrow> Path (f(a := q)) p (as @ [a]) q"
nipkow@13875
    55
by simp
nipkow@13875
    56
nipkow@13875
    57
nipkow@19399
    58
subsection "Non-repeating paths"
nipkow@19399
    59
wenzelm@38353
    60
definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
wenzelm@38353
    61
  where "distPath h x as y \<longleftrightarrow> Path h x as y \<and> distinct as"
nipkow@19399
    62
wenzelm@62042
    63
text\<open>The term @{term"distPath h x as y"} expresses the fact that a
nipkow@19399
    64
non-repeating path @{term as} connects location @{term x} to location
wenzelm@62042
    65
@{term y} by means of the @{term h} field. In the case where \<open>x
wenzelm@62042
    66
= y\<close>, and there is a cycle from @{term x} to itself, @{term as} can
nipkow@19399
    67
be both @{term "[]"} and the non-repeating list of nodes in the
wenzelm@62042
    68
cycle.\<close>
nipkow@19399
    69
nipkow@19399
    70
lemma neq_dP: "p \<noteq> q \<Longrightarrow> Path h p Ps q \<Longrightarrow> distinct Ps \<Longrightarrow>
nipkow@19399
    71
 EX a Qs. p = Ref a & Ps = a#Qs & a \<notin> set Qs"
nipkow@19399
    72
by (case_tac Ps, auto)
nipkow@19399
    73
nipkow@19399
    74
nipkow@19399
    75
lemma neq_dP_disp: "\<lbrakk> p \<noteq> q; distPath h p Ps q \<rbrakk> \<Longrightarrow>
nipkow@19399
    76
 EX a Qs. p = Ref a \<and> Ps = a#Qs \<and> a \<notin> set Qs"
nipkow@19399
    77
apply (simp only:distPath_def)
nipkow@19399
    78
by (case_tac Ps, auto)
nipkow@19399
    79
nipkow@19399
    80
nipkow@13875
    81
subsection "Lists on the heap"
nipkow@13875
    82
nipkow@13875
    83
subsubsection "Relational abstraction"
nipkow@13875
    84
wenzelm@38353
    85
definition List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
wenzelm@38353
    86
  where "List h x as = Path h x as Null"
nipkow@13875
    87
nipkow@13875
    88
lemma [simp]: "List h x [] = (x = Null)"
nipkow@13875
    89
by(simp add:List_def)
nipkow@13875
    90
nipkow@13875
    91
lemma [simp]: "List h x (a#as) = (x = Ref a \<and> List h (h a) as)"
nipkow@13875
    92
by(simp add:List_def)
nipkow@13875
    93
nipkow@13875
    94
lemma [simp]: "List h Null as = (as = [])"
nipkow@13875
    95
by(case_tac as, simp_all)
nipkow@13875
    96
nipkow@13875
    97
lemma List_Ref[simp]: "List h (Ref a) as = (\<exists>bs. as = a#bs \<and> List h (h a) bs)"
nipkow@13875
    98
by(case_tac as, simp_all, fast)
nipkow@13875
    99
nipkow@13875
   100
theorem notin_List_update[simp]:
nipkow@13875
   101
 "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
nipkow@13875
   102
apply(induct as)
nipkow@13875
   103
apply simp
nipkow@13875
   104
apply(clarsimp simp add:fun_upd_apply)
nipkow@13875
   105
done
nipkow@13875
   106
nipkow@13875
   107
lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
nipkow@13875
   108
by(induct as, simp, clarsimp)
nipkow@13875
   109
nipkow@13875
   110
lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
nipkow@13875
   111
by(blast intro:List_unique)
nipkow@13875
   112
nipkow@13875
   113
lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
nipkow@13875
   114
by(induct as, simp, clarsimp)
nipkow@13875
   115
nipkow@13875
   116
lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as"
nipkow@13875
   117
apply (clarsimp simp add:in_set_conv_decomp)
nipkow@13875
   118
apply(frule List_app[THEN iffD1])
nipkow@44890
   119
apply(fastforce dest: List_unique)
nipkow@13875
   120
done
nipkow@13875
   121
nipkow@13875
   122
lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
nipkow@13875
   123
apply(induct as, simp)
nipkow@44890
   124
apply(fastforce dest:List_hd_not_in_tl)
nipkow@13875
   125
done
nipkow@13875
   126
nipkow@19399
   127
lemma Path_is_List:
nipkow@19399
   128
  "\<lbrakk>Path h b Ps (Ref a); a \<notin> set Ps\<rbrakk> \<Longrightarrow> List (h(a := Null)) b (Ps @ [a])"
wenzelm@20503
   129
apply (induct Ps arbitrary: b)
nipkow@19399
   130
apply (auto simp add:fun_upd_apply)
nipkow@19399
   131
done
nipkow@19399
   132
nipkow@19399
   133
nipkow@13875
   134
subsection "Functional abstraction"
nipkow@13875
   135
wenzelm@38353
   136
definition islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
wenzelm@38353
   137
  where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
haftmann@35416
   138
wenzelm@38353
   139
definition list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list"
wenzelm@38353
   140
  where "list h p = (SOME as. List h p as)"
nipkow@13875
   141
nipkow@13875
   142
lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
nipkow@13875
   143
apply(simp add:islist_def list_def)
nipkow@13875
   144
apply(rule iffI)
nipkow@13875
   145
apply(rule conjI)
nipkow@13875
   146
apply blast
nipkow@13875
   147
apply(subst some1_equality)
nipkow@13875
   148
  apply(erule List_unique1)
nipkow@13875
   149
 apply assumption
nipkow@13875
   150
apply(rule refl)
nipkow@13875
   151
apply simp
nipkow@13875
   152
apply(rule someI_ex)
nipkow@13875
   153
apply fast
nipkow@13875
   154
done
nipkow@13875
   155
nipkow@13875
   156
lemma [simp]: "islist h Null"
nipkow@13875
   157
by(simp add:islist_def)
nipkow@13875
   158
nipkow@13875
   159
lemma [simp]: "islist h (Ref a) = islist h (h a)"
nipkow@13875
   160
by(simp add:islist_def)
nipkow@13875
   161
nipkow@13875
   162
lemma [simp]: "list h Null = []"
nipkow@13875
   163
by(simp add:list_def)
nipkow@13875
   164
nipkow@13875
   165
lemma list_Ref_conv[simp]:
nipkow@13875
   166
 "islist h (h a) \<Longrightarrow> list h (Ref a) = a # list h (h a)"
nipkow@13875
   167
apply(insert List_Ref[of h])
nipkow@44890
   168
apply(fastforce simp:List_conv_islist_list)
nipkow@13875
   169
done
nipkow@13875
   170
nipkow@13875
   171
lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))"
nipkow@13875
   172
apply(insert List_hd_not_in_tl[of h])
nipkow@13875
   173
apply(simp add:List_conv_islist_list)
nipkow@13875
   174
done
nipkow@13875
   175
nipkow@13875
   176
lemma list_upd_conv[simp]:
nipkow@13875
   177
 "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> list (h(y := q)) p = list h p"
nipkow@13875
   178
apply(drule notin_List_update[of _ _ h q p])
nipkow@13875
   179
apply(simp add:List_conv_islist_list)
nipkow@13875
   180
done
nipkow@13875
   181
nipkow@13875
   182
lemma islist_upd[simp]:
nipkow@13875
   183
 "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> islist (h(y := q)) p"
nipkow@13875
   184
apply(frule notin_List_update[of _ _ h q p])
nipkow@13875
   185
apply(simp add:List_conv_islist_list)
nipkow@13875
   186
done
nipkow@13875
   187
nipkow@13875
   188
end