src/HOL/Hoare/SepLogHeap.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 44890 22f665a2e91c
child 62042 6c6ccf573479
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     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{* @{text "Some"} means allocated, @{text "None"} means
    16 free. Address @{text "0"} serves as the null reference. *}
    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