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