src/HOL/Hoare/SepLogHeap.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (2017-10-10) changeset 66831 29ea2b900a05 parent 62042 6c6ccf573479 permissions -rw-r--r--
tuned: each session has at most one defining entry;
```     1 (*  Title:      HOL/Hoare/SepLogHeap.thy
```
```     2     Author:     Tobias Nipkow
```
```     3     Copyright   2002 TUM
```
```     4
```
```     5 Heap abstractions (at the moment only Path and List)
```
```     6 for Separation Logic.
```
```     7 *)
```
```     8
```
```     9 theory SepLogHeap
```
```    10 imports Main
```
```    11 begin
```
```    12
```
```    13 type_synonym heap = "(nat \<Rightarrow> nat option)"
```
```    14
```
```    15 text\<open>\<open>Some\<close> means allocated, \<open>None\<close> means
```
```    16 free. Address \<open>0\<close> serves as the null reference.\<close>
```
```    17
```
```    18 subsection "Paths in the heap"
```
```    19
```
```    20 primrec Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
```
```    21 where
```
```    22   "Path h x [] y = (x = y)"
```
```    23 | "Path h x (a#as) y = (x\<noteq>0 \<and> a=x \<and> (\<exists>b. h x = Some b \<and> Path h b as y))"
```
```    24
```
```    25 lemma [iff]: "Path h 0 xs y = (xs = [] \<and> y = 0)"
```
```    26 by (cases xs) simp_all
```
```    27
```
```    28 lemma [simp]: "x\<noteq>0 \<Longrightarrow> Path h x as z =
```
```    29  (as = [] \<and> z = x  \<or>  (\<exists>y bs. as = x#bs \<and> h x = Some y & Path h y bs z))"
```
```    30 by (cases as) auto
```
```    31
```
```    32 lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
```
```    33 by (induct as) auto
```
```    34
```
```    35 lemma Path_upd[simp]:
```
```    36  "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
```
```    37 by (induct as) simp_all
```
```    38
```
```    39
```
```    40 subsection "Lists on the heap"
```
```    41
```
```    42 definition List :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
```
```    43   where "List h x as = Path h x as 0"
```
```    44
```
```    45 lemma [simp]: "List h x [] = (x = 0)"
```
```    46 by (simp add: List_def)
```
```    47
```
```    48 lemma [simp]:
```
```    49  "List h x (a#as) = (x\<noteq>0 \<and> a=x \<and> (\<exists>y. h x = Some y \<and> List h y as))"
```
```    50 by (simp add: List_def)
```
```    51
```
```    52 lemma [simp]: "List h 0 as = (as = [])"
```
```    53 by (cases as) simp_all
```
```    54
```
```    55 lemma List_non_null: "a\<noteq>0 \<Longrightarrow>
```
```    56  List h a as = (\<exists>b bs. as = a#bs \<and> h a = Some b \<and> List h b bs)"
```
```    57 by (cases as) simp_all
```
```    58
```
```    59 theorem notin_List_update[simp]:
```
```    60  "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
```
```    61 by (induct as) simp_all
```
```    62
```
```    63 lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
```
```    64 by (induct as) (auto simp add:List_non_null)
```
```    65
```
```    66 lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
```
```    67 by (blast intro: List_unique)
```
```    68
```
```    69 lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
```
```    70 by (induct as) auto
```
```    71
```
```    72 lemma List_hd_not_in_tl[simp]: "List h b as \<Longrightarrow> h a = Some b \<Longrightarrow> a \<notin> set as"
```
```    73 apply (clarsimp simp add:in_set_conv_decomp)
```
```    74 apply(frule List_app[THEN iffD1])
```
```    75 apply(fastforce dest: List_unique)
```
```    76 done
```
```    77
```
```    78 lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
```
```    79 by (induct as) (auto dest:List_hd_not_in_tl)
```
```    80
```
```    81 lemma list_in_heap: "\<And>p. List h p ps \<Longrightarrow> set ps \<subseteq> dom h"
```
```    82 by (induct ps) auto
```
```    83
```
```    84 lemma list_ortho_sum1[simp]:
```
```    85  "\<And>p. \<lbrakk> List h1 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
```
```    86 by (induct ps) (auto simp add:map_add_def split:option.split)
```
```    87
```
```    88
```
```    89 lemma list_ortho_sum2[simp]:
```
```    90  "\<And>p. \<lbrakk> List h2 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
```
```    91 by (induct ps) (auto simp add:map_add_def split:option.split)
```
```    92
```
```    93 end
```