src/HOL/Hoare/Pointer_Examples.thy
author haftmann
Tue Feb 23 10:11:15 2010 +0100 (2010-02-23)
changeset 35316 870dfea4f9c0
parent 24499 5a3ee202e0b0
child 35416 d8d7d1b785af
permissions -rw-r--r--
dropped axclass; dropped Id; session theory Hoare.thy
     1 (*  Title:      HOL/Hoare/Pointers.thy
     2     Author:     Tobias Nipkow
     3     Copyright   2002 TUM
     4 
     5 Examples of verifications of pointer programs
     6 *)
     7 
     8 theory Pointer_Examples imports HeapSyntax begin
     9 
    10 axiomatization where unproven: "PROP A"
    11 
    12 section "Verifications"
    13 
    14 subsection "List reversal"
    15 
    16 text "A short but unreadable proof:"
    17 
    18 lemma "VARS tl p q r
    19   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
    20   WHILE p \<noteq> Null
    21   INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    22                  rev ps @ qs = rev Ps @ Qs}
    23   DO r := p; p := p^.tl; r^.tl := q; q := r OD
    24   {List tl q (rev Ps @ Qs)}"
    25 apply vcg_simp
    26   apply fastsimp
    27  apply(fastsimp intro:notin_List_update[THEN iffD2])
    28 (* explicit:
    29  apply clarify
    30  apply(rename_tac ps b qs)
    31  apply clarsimp
    32  apply(rename_tac ps')
    33  apply(fastsimp intro:notin_List_update[THEN iffD2])
    34  apply(rule_tac x = ps' in exI)
    35  apply simp
    36  apply(rule_tac x = "b#qs" in exI)
    37  apply simp
    38 *)
    39 apply fastsimp
    40 done
    41 
    42 text{* And now with ghost variables @{term ps} and @{term qs}. Even
    43 ``more automatic''. *}
    44 
    45 lemma "VARS next p ps q qs r
    46   {List next p Ps \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and>
    47    ps = Ps \<and> qs = Qs}
    48   WHILE p \<noteq> Null
    49   INV {List next p ps \<and> List next q qs \<and> set ps \<inter> set qs = {} \<and>
    50        rev ps @ qs = rev Ps @ Qs}
    51   DO r := p; p := p^.next; r^.next := q; q := r;
    52      qs := (hd ps) # qs; ps := tl ps OD
    53   {List next q (rev Ps @ Qs)}"
    54 apply vcg_simp
    55  apply fastsimp
    56 apply fastsimp
    57 done
    58 
    59 text "A longer readable version:"
    60 
    61 lemma "VARS tl p q r
    62   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
    63   WHILE p \<noteq> Null
    64   INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    65                rev ps @ qs = rev Ps @ Qs}
    66   DO r := p; p := p^.tl; r^.tl := q; q := r OD
    67   {List tl q (rev Ps @ Qs)}"
    68 proof vcg
    69   fix tl p q r
    70   assume "List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}"
    71   thus "\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    72                 rev ps @ qs = rev Ps @ Qs" by fastsimp
    73 next
    74   fix tl p q r
    75   assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    76                    rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> Null"
    77          (is "(\<exists>ps qs. ?I ps qs) \<and> _")
    78   then obtain ps qs a where I: "?I ps qs \<and> p = Ref a"
    79     by fast
    80   then obtain ps' where "ps = a # ps'" by fastsimp
    81   hence "List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
    82          List (tl(p \<rightarrow> q)) p       (a#qs) \<and>
    83          set ps' \<inter> set (a#qs) = {} \<and>
    84          rev ps' @ (a#qs) = rev Ps @ Qs"
    85     using I by fastsimp
    86   thus "\<exists>ps' qs'. List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
    87                   List (tl(p \<rightarrow> q)) p       qs' \<and>
    88                   set ps' \<inter> set qs' = {} \<and>
    89                   rev ps' @ qs' = rev Ps @ Qs" by fast
    90 next
    91   fix tl p q r
    92   assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    93                    rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null"
    94   thus "List tl q (rev Ps @ Qs)" by fastsimp
    95 qed
    96 
    97 
    98 text{* Finaly, the functional version. A bit more verbose, but automatic! *}
    99 
   100 lemma "VARS tl p q r
   101   {islist tl p \<and> islist tl q \<and>
   102    Ps = list tl p \<and> Qs = list tl q \<and> set Ps \<inter> set Qs = {}}
   103   WHILE p \<noteq> Null
   104   INV {islist tl p \<and> islist tl q \<and>
   105        set(list tl p) \<inter> set(list tl q) = {} \<and>
   106        rev(list tl p) @ (list tl q) = rev Ps @ Qs}
   107   DO r := p; p := p^.tl; r^.tl := q; q := r OD
   108   {islist tl q \<and> list tl q = rev Ps @ Qs}"
   109 apply vcg_simp
   110   apply clarsimp
   111  apply clarsimp
   112 apply clarsimp
   113 done
   114 
   115 
   116 subsection "Searching in a list"
   117 
   118 text{*What follows is a sequence of successively more intelligent proofs that
   119 a simple loop finds an element in a linked list.
   120 
   121 We start with a proof based on the @{term List} predicate. This means it only
   122 works for acyclic lists. *}
   123 
   124 lemma "VARS tl p
   125   {List tl p Ps \<and> X \<in> set Ps}
   126   WHILE p \<noteq> Null \<and> p \<noteq> Ref X
   127   INV {\<exists>ps. List tl p ps \<and> X \<in> set ps}
   128   DO p := p^.tl OD
   129   {p = Ref X}"
   130 apply vcg_simp
   131   apply blast
   132  apply clarsimp
   133 apply clarsimp
   134 done
   135 
   136 text{*Using @{term Path} instead of @{term List} generalizes the correctness
   137 statement to cyclic lists as well: *}
   138 
   139 lemma "VARS tl p
   140   {Path tl p Ps X}
   141   WHILE p \<noteq> Null \<and> p \<noteq> X
   142   INV {\<exists>ps. Path tl p ps X}
   143   DO p := p^.tl OD
   144   {p = X}"
   145 apply vcg_simp
   146   apply blast
   147  apply fastsimp
   148 apply clarsimp
   149 done
   150 
   151 text{*Now it dawns on us that we do not need the list witness at all --- it
   152 suffices to talk about reachability, i.e.\ we can use relations directly. The
   153 first version uses a relation on @{typ"'a ref"}: *}
   154 
   155 lemma "VARS tl p
   156   {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
   157   WHILE p \<noteq> Null \<and> p \<noteq> X
   158   INV {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
   159   DO p := p^.tl OD
   160   {p = X}"
   161 apply vcg_simp
   162  apply clarsimp
   163  apply(erule converse_rtranclE)
   164   apply simp
   165  apply(clarsimp elim:converse_rtranclE)
   166 apply(fast elim:converse_rtranclE)
   167 done
   168 
   169 text{*Finally, a version based on a relation on type @{typ 'a}:*}
   170 
   171 lemma "VARS tl p
   172   {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
   173   WHILE p \<noteq> Null \<and> p \<noteq> Ref X
   174   INV {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
   175   DO p := p^.tl OD
   176   {p = Ref X}"
   177 apply vcg_simp
   178  apply clarsimp
   179  apply(erule converse_rtranclE)
   180   apply simp
   181  apply clarsimp
   182 apply clarsimp
   183 done
   184 
   185 subsection "Splicing two lists"
   186 
   187 lemma "VARS tl p q pp qq
   188   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and> size Qs \<le> size Ps}
   189   pp := p;
   190   WHILE q \<noteq> Null
   191   INV {\<exists>as bs qs.
   192     distinct as \<and> Path tl p as pp \<and> List tl pp bs \<and> List tl q qs \<and>
   193     set bs \<inter> set qs = {} \<and> set as \<inter> (set bs \<union> set qs) = {} \<and>
   194     size qs \<le> size bs \<and> splice Ps Qs = as @ splice bs qs}
   195   DO qq := q^.tl; q^.tl := pp^.tl; pp^.tl := q; pp := q^.tl; q := qq OD
   196   {List tl p (splice Ps Qs)}"
   197 apply vcg_simp
   198   apply(rule_tac x = "[]" in exI)
   199   apply fastsimp
   200  apply clarsimp
   201  apply(rename_tac y bs qqs)
   202  apply(case_tac bs) apply simp
   203  apply clarsimp
   204  apply(rename_tac x bbs)
   205  apply(rule_tac x = "as @ [x,y]" in exI)
   206  apply simp
   207  apply(rule_tac x = "bbs" in exI)
   208  apply simp
   209  apply(rule_tac x = "qqs" in exI)
   210  apply simp
   211 apply (fastsimp simp:List_app)
   212 done
   213 
   214 
   215 subsection "Merging two lists"
   216 
   217 text"This is still a bit rough, especially the proof."
   218 
   219 constdefs
   220  cor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
   221 "cor P Q == if P then True else Q"
   222  cand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
   223 "cand P Q == if P then Q else False"
   224 
   225 consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
   226 
   227 recdef merge "measure(%(xs,ys,f). size xs + size ys)"
   228 "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
   229                                 else y # merge(x#xs,ys,f))"
   230 "merge(x#xs,[],f) = x # merge(xs,[],f)"
   231 "merge([],y#ys,f) = y # merge([],ys,f)"
   232 "merge([],[],f) = []"
   233 
   234 text{* Simplifies the proof a little: *}
   235 
   236 lemma [simp]: "({} = insert a A \<inter> B) = (a \<notin> B & {} = A \<inter> B)"
   237 by blast
   238 lemma [simp]: "({} = A \<inter> insert b B) = (b \<notin> A & {} = A \<inter> B)"
   239 by blast
   240 lemma [simp]: "({} = A \<inter> (B \<union> C)) = ({} = A \<inter> B & {} = A \<inter> C)"
   241 by blast
   242 
   243 lemma "VARS hd tl p q r s
   244  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and>
   245   (p \<noteq> Null \<or> q \<noteq> Null)}
   246  IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
   247  THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
   248  s := r;
   249  WHILE p \<noteq> Null \<or> q \<noteq> Null
   250  INV {EX rs ps qs a. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and>
   251       distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
   252       merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
   253       rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
   254       (tl a = p \<or> tl a = q)}
   255  DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
   256     THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
   257     s := s^.tl
   258  OD
   259  {List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
   260 apply vcg_simp
   261 apply (simp_all add: cand_def cor_def)
   262 
   263 apply (fastsimp)
   264 
   265 apply clarsimp
   266 apply(rule conjI)
   267 apply clarsimp
   268 apply(rule conjI)
   269 apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   270 apply clarsimp
   271 apply(rule conjI)
   272 apply (clarsimp)
   273 apply(rule_tac x = "rs @ [a]" in exI)
   274 apply(clarsimp simp:eq_sym_conv)
   275 apply(rule_tac x = "bs" in exI)
   276 apply(clarsimp simp:eq_sym_conv)
   277 apply(rule_tac x = "ya#bsa" in exI)
   278 apply(simp)
   279 apply(clarsimp simp:eq_sym_conv)
   280 apply(rule_tac x = "rs @ [a]" in exI)
   281 apply(clarsimp simp:eq_sym_conv)
   282 apply(rule_tac x = "y#bs" in exI)
   283 apply(clarsimp simp:eq_sym_conv)
   284 apply(rule_tac x = "bsa" in exI)
   285 apply(simp)
   286 apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   287 
   288 apply(clarsimp simp add:List_app)
   289 done
   290 
   291 text{* And now with ghost variables: *}
   292 
   293 lemma "VARS elem next p q r s ps qs rs a
   294  {List next p Ps \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and>
   295   (p \<noteq> Null \<or> q \<noteq> Null) \<and> ps = Ps \<and> qs = Qs}
   296  IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
   297  THEN r := p; p := p^.next; ps := tl ps
   298  ELSE r := q; q := q^.next; qs := tl qs FI;
   299  s := r; rs := []; a := addr s;
   300  WHILE p \<noteq> Null \<or> q \<noteq> Null
   301  INV {Path next r rs s \<and> List next p ps \<and> List next q qs \<and>
   302       distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
   303       merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y) =
   304       rs @ a # merge(ps,qs,\<lambda>x y. elem x \<le> elem y) \<and>
   305       (next a = p \<or> next a = q)}
   306  DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
   307     THEN s^.next := p; p := p^.next; ps := tl ps
   308     ELSE s^.next := q; q := q^.next; qs := tl qs FI;
   309     rs := rs @ [a]; s := s^.next; a := addr s
   310  OD
   311  {List next r (merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y))}"
   312 apply vcg_simp
   313 apply (simp_all add: cand_def cor_def)
   314 
   315 apply (fastsimp)
   316 
   317 apply clarsimp
   318 apply(rule conjI)
   319 apply(clarsimp)
   320 apply(rule conjI)
   321 apply(clarsimp simp:neq_commute)
   322 apply(clarsimp simp:neq_commute)
   323 apply(clarsimp simp:neq_commute)
   324 
   325 apply(clarsimp simp add:List_app)
   326 done
   327 
   328 text{* The proof is a LOT simpler because it does not need
   329 instantiations anymore, but it is still not quite automatic, probably
   330 because of this wrong orientation business. *}
   331 
   332 text{* More of the previous proof without ghost variables can be
   333 automated, but the runtime goes up drastically. In general it is
   334 usually more efficient to give the witness directly than to have it
   335 found by proof.
   336 
   337 Now we try a functional version of the abstraction relation @{term
   338 Path}. Since the result is not that convincing, we do not prove any of
   339 the lemmas.*}
   340 
   341 consts ispath:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool"
   342        path:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
   343 
   344 text"First some basic lemmas:"
   345 
   346 lemma [simp]: "ispath f p p"
   347 by (rule unproven)
   348 lemma [simp]: "path f p p = []"
   349 by (rule unproven)
   350 lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow> ispath (f(a := r)) p q"
   351 by (rule unproven)
   352 lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow>
   353  path (f(a := r)) p q = path f p q"
   354 by (rule unproven)
   355 
   356 text"Some more specific lemmas needed by the example:"
   357 
   358 lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow> ispath (f(a := q)) p q"
   359 by (rule unproven)
   360 lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow>
   361  path (f(a := q)) p q = path (f(a := q)) p (Ref a) @ [a]"
   362 by (rule unproven)
   363 lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Ref b \<Longrightarrow>
   364  b \<notin> set (path f p (Ref a))"
   365 by (rule unproven)
   366 lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> islist f p"
   367 by (rule unproven)
   368 lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> list f p = path f p (Ref a) @ [a]"
   369 by (rule unproven)
   370 
   371 lemma [simp]: "islist f p \<Longrightarrow> distinct (list f p)"
   372 by (rule unproven)
   373 
   374 lemma "VARS hd tl p q r s
   375  {islist tl p & Ps = list tl p \<and> islist tl q & Qs = list tl q \<and>
   376   set Ps \<inter> set Qs = {} \<and>
   377   (p \<noteq> Null \<or> q \<noteq> Null)}
   378  IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
   379  THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
   380  s := r;
   381  WHILE p \<noteq> Null \<or> q \<noteq> Null
   382  INV {EX rs ps qs a. ispath tl r s & rs = path tl r s \<and>
   383       islist tl p & ps = list tl p \<and> islist tl q & qs = list tl q \<and>
   384       distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
   385       merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
   386       rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
   387       (tl a = p \<or> tl a = q)}
   388  DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
   389     THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
   390     s := s^.tl
   391  OD
   392  {islist tl r & list tl r = (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
   393 apply vcg_simp
   394 
   395 apply (simp_all add: cand_def cor_def)
   396   apply (fastsimp)
   397  apply (fastsimp simp: eq_sym_conv)
   398 apply(clarsimp)
   399 done
   400 
   401 text"The proof is automatic, but requires a numbet of special lemmas."
   402 
   403 
   404 subsection "Cyclic list reversal"
   405 
   406 
   407 text{* We consider two algorithms for the reversal of circular lists.
   408 *}
   409 
   410 lemma circular_list_rev_I:
   411   "VARS next root p q tmp
   412   {root = Ref r \<and> distPath next root (r#Ps) root}
   413   p := root; q := root^.next;
   414   WHILE q \<noteq> root
   415   INV {\<exists> ps qs. distPath next p ps root \<and> distPath next q qs root \<and> 
   416              root = Ref r \<and> r \<notin> set Ps  \<and> set ps \<inter> set qs = {} \<and> 
   417              Ps = (rev ps) @ qs  }
   418   DO tmp := q; q := q^.next; tmp^.next := p; p:=tmp OD;
   419   root^.next := p
   420   { root = Ref r \<and> distPath next root (r#rev Ps) root}"
   421 apply (simp only:distPath_def)
   422 apply vcg_simp
   423   apply (rule_tac x="[]" in exI)
   424   apply auto
   425  apply (drule (2) neq_dP)
   426  apply clarsimp
   427  apply(rule_tac x="a # ps" in exI)
   428 apply clarsimp
   429 done
   430 
   431 text{* In the beginning, we are able to assert @{term"distPath next
   432 root as root"}, with @{term"as"} set to @{term"[]"} or
   433 @{term"[r,a,b,c]"}. Note that @{term"Path next root as root"} would
   434 additionally give us an infinite number of lists with the recurring
   435 sequence @{term"[r,a,b,c]"}.
   436 
   437 The precondition states that there exists a non-empty non-repeating
   438 path \mbox{@{term "r # Ps"}} from pointer @{term root} to itself, given that
   439 @{term root} points to location @{term r}. Pointers @{term p} and
   440 @{term q} are then set to @{term root} and the successor of @{term
   441 root} respectively. If @{term "q = root"}, we have circled the loop,
   442 otherwise we set the @{term next} pointer field of @{term q} to point
   443 to @{term p}, and shift @{term p} and @{term q} one step forward. The
   444 invariant thus states that @{term p} and @{term q} point to two
   445 disjoint lists @{term ps} and @{term qs}, such that @{term"Ps = rev ps
   446 @ qs"}. After the loop terminates, one
   447 extra step is needed to close the loop. As expected, the postcondition
   448 states that the @{term distPath} from @{term root} to itself is now
   449 @{term "r # (rev Ps)"}.
   450 
   451 It may come as a surprise to the reader that the simple algorithm for
   452 acyclic list reversal, with modified annotations, works for cyclic
   453 lists as well: *}
   454 
   455 
   456 lemma circular_list_rev_II:
   457 "VARS next p q tmp
   458 {p = Ref r \<and> distPath next p (r#Ps) p}
   459 q:=Null;
   460 WHILE p \<noteq> Null
   461 INV
   462 { ((q = Null) \<longrightarrow> (\<exists>ps. distPath next p (ps) (Ref r) \<and> ps = r#Ps)) \<and>
   463   ((q \<noteq> Null) \<longrightarrow> (\<exists>ps qs. distPath next q (qs) (Ref r) \<and> List next p ps  \<and>
   464                    set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps@[r])) \<and>
   465   \<not> (p = Null \<and> q = Null) }
   466 DO tmp := p; p := p^.next; tmp^.next := q; q:=tmp OD
   467 {q = Ref r \<and> distPath next q (r # rev Ps) q}"
   468 apply (simp only:distPath_def)
   469 apply vcg_simp
   470   apply clarsimp
   471   apply clarsimp
   472  apply (case_tac "(q = Null)")
   473   apply (fastsimp intro: Path_is_List)
   474  apply clarsimp
   475  apply (rule_tac x= "bs" in exI)
   476  apply (rule_tac x= "y # qs" in exI)
   477  apply clarsimp
   478 apply (auto simp:fun_upd_apply)
   479 done
   480 
   481 
   482 subsection "Storage allocation"
   483 
   484 constdefs new :: "'a set \<Rightarrow> 'a"
   485 "new A == SOME a. a \<notin> A"
   486 
   487 
   488 lemma new_notin:
   489  "\<lbrakk> ~finite(UNIV::'a set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow> new (A) \<notin> B"
   490 apply(unfold new_def)
   491 apply(rule someI2_ex)
   492  apply (fast intro:ex_new_if_finite)
   493 apply (fast)
   494 done
   495 
   496 
   497 lemma "~finite(UNIV::'a set) \<Longrightarrow>
   498   VARS xs elem next alloc p q
   499   {Xs = xs \<and> p = (Null::'a ref)}
   500   WHILE xs \<noteq> []
   501   INV {islist next p \<and> set(list next p) \<subseteq> set alloc \<and>
   502        map elem (rev(list next p)) @ xs = Xs}
   503   DO q := Ref(new(set alloc)); alloc := (addr q)#alloc;
   504      q^.next := p; q^.elem := hd xs; xs := tl xs; p := q
   505   OD
   506   {islist next p \<and> map elem (rev(list next p)) = Xs}"
   507 apply vcg_simp
   508  apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
   509 apply fastsimp
   510 done
   511 
   512 
   513 end