src/HOL/Hoare/SepLogHeap.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 14074 93dfce3b6f86
child 16972 d3f9abe00712
permissions -rw-r--r--
migrated theory headers to new format
     1 (*  Title:      HOL/Hoare/Heap.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   2002 TUM
     5 
     6 Heap abstractions (at the moment only Path and List)
     7 for Separation Logic.
     8 *)
     9 
    10 theory SepLogHeap imports Main begin
    11 
    12 types heap = "(nat \<Rightarrow> nat option)"
    13 
    14 text{* Some means allocated, none means free. Address 0 serves as the
    15 null reference. *}
    16 
    17 subsection "Paths in the heap"
    18 
    19 consts
    20  Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
    21 primrec
    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 apply(case_tac xs)
    27 apply fastsimp
    28 apply fastsimp
    29 done
    30 
    31 lemma [simp]: "x\<noteq>0 \<Longrightarrow> Path h x as z =
    32  (as = [] \<and> z = x  \<or>  (\<exists>y bs. as = x#bs \<and> h x = Some y & Path h y bs z))"
    33 apply(case_tac as)
    34 apply fastsimp
    35 apply fastsimp
    36 done
    37 
    38 lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
    39 by(induct as, auto)
    40 
    41 lemma Path_upd[simp]:
    42  "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
    43 by(induct as, simp, simp add:eq_sym_conv)
    44 
    45 
    46 subsection "Lists on the heap"
    47 
    48 constdefs
    49  List :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
    50 "List h x as == Path h x as 0"
    51 
    52 lemma [simp]: "List h x [] = (x = 0)"
    53 by(simp add:List_def)
    54 
    55 lemma [simp]:
    56  "List h x (a#as) = (x\<noteq>0 \<and> a=x \<and> (\<exists>y. h x = Some y \<and> List h y as))"
    57 by(simp add:List_def)
    58 
    59 lemma [simp]: "List h 0 as = (as = [])"
    60 by(case_tac as, simp_all)
    61 
    62 lemma List_non_null: "a\<noteq>0 \<Longrightarrow>
    63  List h a as = (\<exists>b bs. as = a#bs \<and> h a = Some b \<and> List h b bs)"
    64 by(case_tac as, simp_all)
    65 
    66 theorem notin_List_update[simp]:
    67  "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
    68 apply(induct as)
    69 apply simp
    70 apply(clarsimp simp add:fun_upd_apply)
    71 done
    72 
    73 lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
    74 by(induct as, auto simp add:List_non_null)
    75 
    76 lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
    77 by(blast intro:List_unique)
    78 
    79 lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
    80 by(induct as, auto)
    81 
    82 lemma List_hd_not_in_tl[simp]: "List h b as \<Longrightarrow> h a = Some b \<Longrightarrow> a \<notin> set as"
    83 apply (clarsimp simp add:in_set_conv_decomp)
    84 apply(frule List_app[THEN iffD1])
    85 apply(fastsimp dest: List_unique)
    86 done
    87 
    88 lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
    89 apply(induct as, simp)
    90 apply(fastsimp dest:List_hd_not_in_tl)
    91 done
    92 
    93 lemma list_in_heap: "\<And>p. List h p ps \<Longrightarrow> set ps \<subseteq> dom h"
    94 by(induct ps, auto)
    95 
    96 lemma list_ortho_sum1[simp]:
    97  "\<And>p. \<lbrakk> List h1 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
    98 by(induct ps, auto simp add:map_add_def split:option.split)
    99 
   100 lemma list_ortho_sum2[simp]:
   101  "\<And>p. \<lbrakk> List h2 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
   102 by(induct ps, auto simp add:map_add_def split:option.split)
   103 
   104 end