src/HOL/Hoare/Pointer_Examples.thy
 author wenzelm Wed Apr 10 21:46:28 2013 +0200 (2013-04-10) changeset 51693 1eb533ea1480 parent 44890 22f665a2e91c child 62042 6c6ccf573479 permissions -rw-r--r--
more antiquotations;
```     1 (*  Title:      HOL/Hoare/Pointer_Examples.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 fastforce
```
```    27  apply(fastforce 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(fastforce 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 fastforce
```
```    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 fastforce
```
```    56 apply fastforce
```
```    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 fastforce
```
```    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 fastforce
```
```    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 fastforce
```
```    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 fastforce
```
```    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 fastforce
```
```   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 fastforce
```
```   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 (fastforce 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"
```
```   220   where "cor P Q \<longleftrightarrow> (if P then True else Q)"
```
```   221
```
```   222 definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
```
```   223   where "cand P Q \<longleftrightarrow> (if P then Q else False)"
```
```   224
```
```   225 fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
```
```   226 where
```
```   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 (fastforce)
```
```   263
```
```   264 apply clarsimp
```
```   265 apply(rule conjI)
```
```   266 apply clarsimp
```
```   267 apply(rule conjI)
```
```   268 apply (fastforce 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 (fastforce 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 (fastforce)
```
```   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 axiomatization
```
```   341   ispath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" and
```
```   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 (fastforce)
```
```   397  apply (fastforce 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 (fastforce 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 definition new :: "'a set \<Rightarrow> 'a"
```
```   485   where "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 fastforce
```
```   510 done
```
```   511
```
```   512
```
```   513 end
```