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