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