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