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
```