src/HOL/Hoare/Heap.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 44890 22f665a2e91c
child 58249 180f1b3508ed
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     1 (*  Title:      HOL/Hoare/Heap.thy
     2     Author:     Tobias Nipkow
     3     Copyright   2002 TUM
     4 
     5 Pointers, heaps and heap abstractions.
     6 See the paper by Mehta and Nipkow.
     7 *)
     8 
     9 theory Heap imports Main begin
    10 
    11 subsection "References"
    12 
    13 datatype 'a ref = Null | Ref 'a
    14 
    15 lemma not_Null_eq [iff]: "(x ~= Null) = (EX y. x = Ref y)"
    16   by (induct x) auto
    17 
    18 lemma not_Ref_eq [iff]: "(ALL y. x ~= Ref y) = (x = Null)"
    19   by (induct x) auto
    20 
    21 primrec addr :: "'a ref \<Rightarrow> 'a" where
    22   "addr (Ref a) = a"
    23 
    24 
    25 section "The heap"
    26 
    27 subsection "Paths in the heap"
    28 
    29 primrec Path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool" where
    30   "Path h x [] y \<longleftrightarrow> x = y"
    31 | "Path h x (a#as) y \<longleftrightarrow> x = Ref a \<and> Path h (h a) as y"
    32 
    33 lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
    34 apply(case_tac xs)
    35 apply fastforce
    36 apply fastforce
    37 done
    38 
    39 lemma [simp]: "Path h (Ref a) as z =
    40  (as = [] \<and> z = Ref a  \<or>  (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))"
    41 apply(case_tac as)
    42 apply fastforce
    43 apply fastforce
    44 done
    45 
    46 lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
    47 by(induct as, simp+)
    48 
    49 lemma Path_upd[simp]:
    50  "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
    51 by(induct as, simp, simp add:eq_sym_conv)
    52 
    53 lemma Path_snoc:
    54  "Path (f(a := q)) p as (Ref a) \<Longrightarrow> Path (f(a := q)) p (as @ [a]) q"
    55 by simp
    56 
    57 
    58 subsection "Non-repeating paths"
    59 
    60 definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
    61   where "distPath h x as y \<longleftrightarrow> Path h x as y \<and> distinct as"
    62 
    63 text{* The term @{term"distPath h x as y"} expresses the fact that a
    64 non-repeating path @{term as} connects location @{term x} to location
    65 @{term y} by means of the @{term h} field. In the case where @{text "x
    66 = y"}, and there is a cycle from @{term x} to itself, @{term as} can
    67 be both @{term "[]"} and the non-repeating list of nodes in the
    68 cycle. *}
    69 
    70 lemma neq_dP: "p \<noteq> q \<Longrightarrow> Path h p Ps q \<Longrightarrow> distinct Ps \<Longrightarrow>
    71  EX a Qs. p = Ref a & Ps = a#Qs & a \<notin> set Qs"
    72 by (case_tac Ps, auto)
    73 
    74 
    75 lemma neq_dP_disp: "\<lbrakk> p \<noteq> q; distPath h p Ps q \<rbrakk> \<Longrightarrow>
    76  EX a Qs. p = Ref a \<and> Ps = a#Qs \<and> a \<notin> set Qs"
    77 apply (simp only:distPath_def)
    78 by (case_tac Ps, auto)
    79 
    80 
    81 subsection "Lists on the heap"
    82 
    83 subsubsection "Relational abstraction"
    84 
    85 definition List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
    86   where "List h x as = Path h x as Null"
    87 
    88 lemma [simp]: "List h x [] = (x = Null)"
    89 by(simp add:List_def)
    90 
    91 lemma [simp]: "List h x (a#as) = (x = Ref a \<and> List h (h a) as)"
    92 by(simp add:List_def)
    93 
    94 lemma [simp]: "List h Null as = (as = [])"
    95 by(case_tac as, simp_all)
    96 
    97 lemma List_Ref[simp]: "List h (Ref a) as = (\<exists>bs. as = a#bs \<and> List h (h a) bs)"
    98 by(case_tac as, simp_all, fast)
    99 
   100 theorem notin_List_update[simp]:
   101  "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
   102 apply(induct as)
   103 apply simp
   104 apply(clarsimp simp add:fun_upd_apply)
   105 done
   106 
   107 lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
   108 by(induct as, simp, clarsimp)
   109 
   110 lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
   111 by(blast intro:List_unique)
   112 
   113 lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
   114 by(induct as, simp, clarsimp)
   115 
   116 lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as"
   117 apply (clarsimp simp add:in_set_conv_decomp)
   118 apply(frule List_app[THEN iffD1])
   119 apply(fastforce dest: List_unique)
   120 done
   121 
   122 lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
   123 apply(induct as, simp)
   124 apply(fastforce dest:List_hd_not_in_tl)
   125 done
   126 
   127 lemma Path_is_List:
   128   "\<lbrakk>Path h b Ps (Ref a); a \<notin> set Ps\<rbrakk> \<Longrightarrow> List (h(a := Null)) b (Ps @ [a])"
   129 apply (induct Ps arbitrary: b)
   130 apply (auto simp add:fun_upd_apply)
   131 done
   132 
   133 
   134 subsection "Functional abstraction"
   135 
   136 definition islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
   137   where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
   138 
   139 definition list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list"
   140   where "list h p = (SOME as. List h p as)"
   141 
   142 lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
   143 apply(simp add:islist_def list_def)
   144 apply(rule iffI)
   145 apply(rule conjI)
   146 apply blast
   147 apply(subst some1_equality)
   148   apply(erule List_unique1)
   149  apply assumption
   150 apply(rule refl)
   151 apply simp
   152 apply(rule someI_ex)
   153 apply fast
   154 done
   155 
   156 lemma [simp]: "islist h Null"
   157 by(simp add:islist_def)
   158 
   159 lemma [simp]: "islist h (Ref a) = islist h (h a)"
   160 by(simp add:islist_def)
   161 
   162 lemma [simp]: "list h Null = []"
   163 by(simp add:list_def)
   164 
   165 lemma list_Ref_conv[simp]:
   166  "islist h (h a) \<Longrightarrow> list h (Ref a) = a # list h (h a)"
   167 apply(insert List_Ref[of h])
   168 apply(fastforce simp:List_conv_islist_list)
   169 done
   170 
   171 lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))"
   172 apply(insert List_hd_not_in_tl[of h])
   173 apply(simp add:List_conv_islist_list)
   174 done
   175 
   176 lemma list_upd_conv[simp]:
   177  "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> list (h(y := q)) p = list h p"
   178 apply(drule notin_List_update[of _ _ h q p])
   179 apply(simp add:List_conv_islist_list)
   180 done
   181 
   182 lemma islist_upd[simp]:
   183  "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> islist (h(y := q)) p"
   184 apply(frule notin_List_update[of _ _ h q p])
   185 apply(simp add:List_conv_islist_list)
   186 done
   187 
   188 end