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