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