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