src/HOL/Hoare/Pointer_Examples.thy
author krauss
Mon Mar 01 17:05:57 2010 +0100 (2010-03-01)
changeset 35419 d78659d1723e
parent 35416 d8d7d1b785af
child 38353 d98baa2cf589
permissions -rw-r--r--
more recdef (and old primrec) hunting
     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 definition cor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
   220 "cor P Q == if P then True else Q"
   221 
   222 definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
   223 "cand P Q == if P then Q else False"
   224 
   225 fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" where
   226 "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
   227                                 else y # merge(x#xs,ys,f))" |
   228 "merge(x#xs,[],f) = x # merge(xs,[],f)" |
   229 "merge([],y#ys,f) = y # merge([],ys,f)" |
   230 "merge([],[],f) = []"
   231 
   232 text{* Simplifies the proof a little: *}
   233 
   234 lemma [simp]: "({} = insert a A \<inter> B) = (a \<notin> B & {} = A \<inter> B)"
   235 by blast
   236 lemma [simp]: "({} = A \<inter> insert b B) = (b \<notin> A & {} = A \<inter> B)"
   237 by blast
   238 lemma [simp]: "({} = A \<inter> (B \<union> C)) = ({} = A \<inter> B & {} = A \<inter> C)"
   239 by blast
   240 
   241 lemma "VARS hd tl p q r s
   242  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and>
   243   (p \<noteq> Null \<or> q \<noteq> Null)}
   244  IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
   245  THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
   246  s := r;
   247  WHILE p \<noteq> Null \<or> q \<noteq> Null
   248  INV {EX rs ps qs a. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and>
   249       distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
   250       merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
   251       rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
   252       (tl a = p \<or> tl a = q)}
   253  DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
   254     THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
   255     s := s^.tl
   256  OD
   257  {List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
   258 apply vcg_simp
   259 apply (simp_all add: cand_def cor_def)
   260 
   261 apply (fastsimp)
   262 
   263 apply clarsimp
   264 apply(rule conjI)
   265 apply clarsimp
   266 apply(rule conjI)
   267 apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   268 apply clarsimp
   269 apply(rule conjI)
   270 apply (clarsimp)
   271 apply(rule_tac x = "rs @ [a]" in exI)
   272 apply(clarsimp simp:eq_sym_conv)
   273 apply(rule_tac x = "bs" in exI)
   274 apply(clarsimp simp:eq_sym_conv)
   275 apply(rule_tac x = "ya#bsa" in exI)
   276 apply(simp)
   277 apply(clarsimp simp:eq_sym_conv)
   278 apply(rule_tac x = "rs @ [a]" in exI)
   279 apply(clarsimp simp:eq_sym_conv)
   280 apply(rule_tac x = "y#bs" in exI)
   281 apply(clarsimp simp:eq_sym_conv)
   282 apply(rule_tac x = "bsa" in exI)
   283 apply(simp)
   284 apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   285 
   286 apply(clarsimp simp add:List_app)
   287 done
   288 
   289 text{* And now with ghost variables: *}
   290 
   291 lemma "VARS elem next p q r s ps qs rs a
   292  {List next p Ps \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and>
   293   (p \<noteq> Null \<or> q \<noteq> Null) \<and> ps = Ps \<and> qs = Qs}
   294  IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
   295  THEN r := p; p := p^.next; ps := tl ps
   296  ELSE r := q; q := q^.next; qs := tl qs FI;
   297  s := r; rs := []; a := addr s;
   298  WHILE p \<noteq> Null \<or> q \<noteq> Null
   299  INV {Path next r rs s \<and> List next p ps \<and> List next q qs \<and>
   300       distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
   301       merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y) =
   302       rs @ a # merge(ps,qs,\<lambda>x y. elem x \<le> elem y) \<and>
   303       (next a = p \<or> next a = q)}
   304  DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
   305     THEN s^.next := p; p := p^.next; ps := tl ps
   306     ELSE s^.next := q; q := q^.next; qs := tl qs FI;
   307     rs := rs @ [a]; s := s^.next; a := addr s
   308  OD
   309  {List next r (merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y))}"
   310 apply vcg_simp
   311 apply (simp_all add: cand_def cor_def)
   312 
   313 apply (fastsimp)
   314 
   315 apply clarsimp
   316 apply(rule conjI)
   317 apply(clarsimp)
   318 apply(rule conjI)
   319 apply(clarsimp simp:neq_commute)
   320 apply(clarsimp simp:neq_commute)
   321 apply(clarsimp simp:neq_commute)
   322 
   323 apply(clarsimp simp add:List_app)
   324 done
   325 
   326 text{* The proof is a LOT simpler because it does not need
   327 instantiations anymore, but it is still not quite automatic, probably
   328 because of this wrong orientation business. *}
   329 
   330 text{* More of the previous proof without ghost variables can be
   331 automated, but the runtime goes up drastically. In general it is
   332 usually more efficient to give the witness directly than to have it
   333 found by proof.
   334 
   335 Now we try a functional version of the abstraction relation @{term
   336 Path}. Since the result is not that convincing, we do not prove any of
   337 the lemmas.*}
   338 
   339 consts ispath:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool"
   340        path:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
   341 
   342 text"First some basic lemmas:"
   343 
   344 lemma [simp]: "ispath f p p"
   345 by (rule unproven)
   346 lemma [simp]: "path f p p = []"
   347 by (rule unproven)
   348 lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow> ispath (f(a := r)) p q"
   349 by (rule unproven)
   350 lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow>
   351  path (f(a := r)) p q = path f p q"
   352 by (rule unproven)
   353 
   354 text"Some more specific lemmas needed by the example:"
   355 
   356 lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow> ispath (f(a := q)) p q"
   357 by (rule unproven)
   358 lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow>
   359  path (f(a := q)) p q = path (f(a := q)) p (Ref a) @ [a]"
   360 by (rule unproven)
   361 lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Ref b \<Longrightarrow>
   362  b \<notin> set (path f p (Ref a))"
   363 by (rule unproven)
   364 lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> islist f p"
   365 by (rule unproven)
   366 lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> list f p = path f p (Ref a) @ [a]"
   367 by (rule unproven)
   368 
   369 lemma [simp]: "islist f p \<Longrightarrow> distinct (list f p)"
   370 by (rule unproven)
   371 
   372 lemma "VARS hd tl p q r s
   373  {islist tl p & Ps = list tl p \<and> islist tl q & Qs = list tl q \<and>
   374   set Ps \<inter> set Qs = {} \<and>
   375   (p \<noteq> Null \<or> q \<noteq> Null)}
   376  IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
   377  THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
   378  s := r;
   379  WHILE p \<noteq> Null \<or> q \<noteq> Null
   380  INV {EX rs ps qs a. ispath tl r s & rs = path tl r s \<and>
   381       islist tl p & ps = list tl p \<and> islist tl q & qs = list tl q \<and>
   382       distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
   383       merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
   384       rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
   385       (tl a = p \<or> tl a = q)}
   386  DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
   387     THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
   388     s := s^.tl
   389  OD
   390  {islist tl r & list tl r = (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
   391 apply vcg_simp
   392 
   393 apply (simp_all add: cand_def cor_def)
   394   apply (fastsimp)
   395  apply (fastsimp simp: eq_sym_conv)
   396 apply(clarsimp)
   397 done
   398 
   399 text"The proof is automatic, but requires a numbet of special lemmas."
   400 
   401 
   402 subsection "Cyclic list reversal"
   403 
   404 
   405 text{* We consider two algorithms for the reversal of circular lists.
   406 *}
   407 
   408 lemma circular_list_rev_I:
   409   "VARS next root p q tmp
   410   {root = Ref r \<and> distPath next root (r#Ps) root}
   411   p := root; q := root^.next;
   412   WHILE q \<noteq> root
   413   INV {\<exists> ps qs. distPath next p ps root \<and> distPath next q qs root \<and> 
   414              root = Ref r \<and> r \<notin> set Ps  \<and> set ps \<inter> set qs = {} \<and> 
   415              Ps = (rev ps) @ qs  }
   416   DO tmp := q; q := q^.next; tmp^.next := p; p:=tmp OD;
   417   root^.next := p
   418   { root = Ref r \<and> distPath next root (r#rev Ps) root}"
   419 apply (simp only:distPath_def)
   420 apply vcg_simp
   421   apply (rule_tac x="[]" in exI)
   422   apply auto
   423  apply (drule (2) neq_dP)
   424  apply clarsimp
   425  apply(rule_tac x="a # ps" in exI)
   426 apply clarsimp
   427 done
   428 
   429 text{* In the beginning, we are able to assert @{term"distPath next
   430 root as root"}, with @{term"as"} set to @{term"[]"} or
   431 @{term"[r,a,b,c]"}. Note that @{term"Path next root as root"} would
   432 additionally give us an infinite number of lists with the recurring
   433 sequence @{term"[r,a,b,c]"}.
   434 
   435 The precondition states that there exists a non-empty non-repeating
   436 path \mbox{@{term "r # Ps"}} from pointer @{term root} to itself, given that
   437 @{term root} points to location @{term r}. Pointers @{term p} and
   438 @{term q} are then set to @{term root} and the successor of @{term
   439 root} respectively. If @{term "q = root"}, we have circled the loop,
   440 otherwise we set the @{term next} pointer field of @{term q} to point
   441 to @{term p}, and shift @{term p} and @{term q} one step forward. The
   442 invariant thus states that @{term p} and @{term q} point to two
   443 disjoint lists @{term ps} and @{term qs}, such that @{term"Ps = rev ps
   444 @ qs"}. After the loop terminates, one
   445 extra step is needed to close the loop. As expected, the postcondition
   446 states that the @{term distPath} from @{term root} to itself is now
   447 @{term "r # (rev Ps)"}.
   448 
   449 It may come as a surprise to the reader that the simple algorithm for
   450 acyclic list reversal, with modified annotations, works for cyclic
   451 lists as well: *}
   452 
   453 
   454 lemma circular_list_rev_II:
   455 "VARS next p q tmp
   456 {p = Ref r \<and> distPath next p (r#Ps) p}
   457 q:=Null;
   458 WHILE p \<noteq> Null
   459 INV
   460 { ((q = Null) \<longrightarrow> (\<exists>ps. distPath next p (ps) (Ref r) \<and> ps = r#Ps)) \<and>
   461   ((q \<noteq> Null) \<longrightarrow> (\<exists>ps qs. distPath next q (qs) (Ref r) \<and> List next p ps  \<and>
   462                    set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps@[r])) \<and>
   463   \<not> (p = Null \<and> q = Null) }
   464 DO tmp := p; p := p^.next; tmp^.next := q; q:=tmp OD
   465 {q = Ref r \<and> distPath next q (r # rev Ps) q}"
   466 apply (simp only:distPath_def)
   467 apply vcg_simp
   468   apply clarsimp
   469   apply clarsimp
   470  apply (case_tac "(q = Null)")
   471   apply (fastsimp intro: Path_is_List)
   472  apply clarsimp
   473  apply (rule_tac x= "bs" in exI)
   474  apply (rule_tac x= "y # qs" in exI)
   475  apply clarsimp
   476 apply (auto simp:fun_upd_apply)
   477 done
   478 
   479 
   480 subsection "Storage allocation"
   481 
   482 definition new :: "'a set \<Rightarrow> 'a" where
   483 "new A == SOME a. a \<notin> A"
   484 
   485 
   486 lemma new_notin:
   487  "\<lbrakk> ~finite(UNIV::'a set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow> new (A) \<notin> B"
   488 apply(unfold new_def)
   489 apply(rule someI2_ex)
   490  apply (fast intro:ex_new_if_finite)
   491 apply (fast)
   492 done
   493 
   494 
   495 lemma "~finite(UNIV::'a set) \<Longrightarrow>
   496   VARS xs elem next alloc p q
   497   {Xs = xs \<and> p = (Null::'a ref)}
   498   WHILE xs \<noteq> []
   499   INV {islist next p \<and> set(list next p) \<subseteq> set alloc \<and>
   500        map elem (rev(list next p)) @ xs = Xs}
   501   DO q := Ref(new(set alloc)); alloc := (addr q)#alloc;
   502      q^.next := p; q^.elem := hd xs; xs := tl xs; p := q
   503   OD
   504   {islist next p \<and> map elem (rev(list next p)) = Xs}"
   505 apply vcg_simp
   506  apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
   507 apply fastsimp
   508 done
   509 
   510 
   511 end