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