src/HOL/Hoare/SepLogHeap.thy
changeset 14074 93dfce3b6f86
child 16417 9bc16273c2d4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Hoare/SepLogHeap.thy	Thu Jun 26 18:14:04 2003 +0200
     1.3 @@ -0,0 +1,104 @@
     1.4 +(*  Title:      HOL/Hoare/Heap.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   2002 TUM
     1.8 +
     1.9 +Heap abstractions (at the moment only Path and List)
    1.10 +for Separation Logic.
    1.11 +*)
    1.12 +
    1.13 +theory SepLogHeap = Main:
    1.14 +
    1.15 +types heap = "(nat \<Rightarrow> nat option)"
    1.16 +
    1.17 +text{* Some means allocated, none means free. Address 0 serves as the
    1.18 +null reference. *}
    1.19 +
    1.20 +subsection "Paths in the heap"
    1.21 +
    1.22 +consts
    1.23 + Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
    1.24 +primrec
    1.25 +"Path h x [] y = (x = y)"
    1.26 +"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))"
    1.27 +
    1.28 +lemma [iff]: "Path h 0 xs y = (xs = [] \<and> y = 0)"
    1.29 +apply(case_tac xs)
    1.30 +apply fastsimp
    1.31 +apply fastsimp
    1.32 +done
    1.33 +
    1.34 +lemma [simp]: "x\<noteq>0 \<Longrightarrow> Path h x as z =
    1.35 + (as = [] \<and> z = x  \<or>  (\<exists>y bs. as = x#bs \<and> h x = Some y & Path h y bs z))"
    1.36 +apply(case_tac as)
    1.37 +apply fastsimp
    1.38 +apply fastsimp
    1.39 +done
    1.40 +
    1.41 +lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
    1.42 +by(induct as, auto)
    1.43 +
    1.44 +lemma Path_upd[simp]:
    1.45 + "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
    1.46 +by(induct as, simp, simp add:eq_sym_conv)
    1.47 +
    1.48 +
    1.49 +subsection "Lists on the heap"
    1.50 +
    1.51 +constdefs
    1.52 + List :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
    1.53 +"List h x as == Path h x as 0"
    1.54 +
    1.55 +lemma [simp]: "List h x [] = (x = 0)"
    1.56 +by(simp add:List_def)
    1.57 +
    1.58 +lemma [simp]:
    1.59 + "List h x (a#as) = (x\<noteq>0 \<and> a=x \<and> (\<exists>y. h x = Some y \<and> List h y as))"
    1.60 +by(simp add:List_def)
    1.61 +
    1.62 +lemma [simp]: "List h 0 as = (as = [])"
    1.63 +by(case_tac as, simp_all)
    1.64 +
    1.65 +lemma List_non_null: "a\<noteq>0 \<Longrightarrow>
    1.66 + List h a as = (\<exists>b bs. as = a#bs \<and> h a = Some b \<and> List h b bs)"
    1.67 +by(case_tac as, simp_all)
    1.68 +
    1.69 +theorem notin_List_update[simp]:
    1.70 + "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
    1.71 +apply(induct as)
    1.72 +apply simp
    1.73 +apply(clarsimp simp add:fun_upd_apply)
    1.74 +done
    1.75 +
    1.76 +lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
    1.77 +by(induct as, auto simp add:List_non_null)
    1.78 +
    1.79 +lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
    1.80 +by(blast intro:List_unique)
    1.81 +
    1.82 +lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
    1.83 +by(induct as, auto)
    1.84 +
    1.85 +lemma List_hd_not_in_tl[simp]: "List h b as \<Longrightarrow> h a = Some b \<Longrightarrow> a \<notin> set as"
    1.86 +apply (clarsimp simp add:in_set_conv_decomp)
    1.87 +apply(frule List_app[THEN iffD1])
    1.88 +apply(fastsimp dest: List_unique)
    1.89 +done
    1.90 +
    1.91 +lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
    1.92 +apply(induct as, simp)
    1.93 +apply(fastsimp dest:List_hd_not_in_tl)
    1.94 +done
    1.95 +
    1.96 +lemma list_in_heap: "\<And>p. List h p ps \<Longrightarrow> set ps \<subseteq> dom h"
    1.97 +by(induct ps, auto)
    1.98 +
    1.99 +lemma list_ortho_sum1[simp]:
   1.100 + "\<And>p. \<lbrakk> List h1 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
   1.101 +by(induct ps, auto simp add:map_add_def split:option.split)
   1.102 +
   1.103 +lemma list_ortho_sum2[simp]:
   1.104 + "\<And>p. \<lbrakk> List h2 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
   1.105 +by(induct ps, auto simp add:map_add_def split:option.split)
   1.106 +
   1.107 +end