src/HOL/Hoare/Pointer_Examples.thy
author nipkow
Mon Sep 12 07:55:43 2011 +0200 (2011-09-12)
changeset 44890 22f665a2e91c
parent 41959 b460124855b8
child 62042 6c6ccf573479
permissions -rw-r--r--
new fastforce replacing fastsimp - less confusing name
wenzelm@41959
     1
(*  Title:      HOL/Hoare/Pointer_Examples.thy
nipkow@13772
     2
    Author:     Tobias Nipkow
nipkow@13772
     3
    Copyright   2002 TUM
nipkow@13772
     4
wenzelm@41959
     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 \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
nipkow@13772
    20
  WHILE p \<noteq> Null
nipkow@13772
    21
  INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
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@44890
    26
  apply fastforce
nipkow@44890
    27
 apply(fastforce 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@44890
    33
 apply(fastforce 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@44890
    39
apply fastforce
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 \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and>
nipkow@14062
    47
   ps = Ps \<and> qs = Qs}
nipkow@14062
    48
  WHILE p \<noteq> Null
nipkow@14062
    49
  INV {List next p ps \<and> List next q qs \<and> set ps \<inter> set qs = {} \<and>
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@44890
    55
 apply fastforce
nipkow@44890
    56
apply fastforce
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 \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
nipkow@13772
    63
  WHILE p \<noteq> Null
nipkow@13772
    64
  INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
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 \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}"
nipkow@13772
    71
  thus "\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
nipkow@44890
    72
                rev ps @ qs = rev Ps @ Qs" by fastforce
nipkow@13772
    73
next
nipkow@13772
    74
  fix tl p q r
nipkow@13772
    75
  assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
nipkow@13772
    76
                   rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> Null"
nipkow@13772
    77
         (is "(\<exists>ps qs. ?I ps qs) \<and> _")
nipkow@13772
    78
  then obtain ps qs a where I: "?I ps qs \<and> p = Ref a"
nipkow@13772
    79
    by fast
nipkow@44890
    80
  then obtain ps' where "ps = a # ps'" by fastforce
nipkow@13772
    81
  hence "List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
nipkow@13772
    82
         List (tl(p \<rightarrow> q)) p       (a#qs) \<and>
nipkow@13772
    83
         set ps' \<inter> set (a#qs) = {} \<and>
nipkow@13772
    84
         rev ps' @ (a#qs) = rev Ps @ Qs"
nipkow@44890
    85
    using I by fastforce
nipkow@13772
    86
  thus "\<exists>ps' qs'. List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
nipkow@13772
    87
                  List (tl(p \<rightarrow> q)) p       qs' \<and>
nipkow@13772
    88
                  set ps' \<inter> set qs' = {} \<and>
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 "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
nipkow@13772
    93
                   rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null"
nipkow@44890
    94
  thus "List tl q (rev Ps @ Qs)" by fastforce
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 \<and> islist tl q \<and>
nipkow@13772
   102
   Ps = list tl p \<and> Qs = list tl q \<and> set Ps \<inter> set Qs = {}}
nipkow@13772
   103
  WHILE p \<noteq> Null
nipkow@13772
   104
  INV {islist tl p \<and> islist tl q \<and>
nipkow@13772
   105
       set(list tl p) \<inter> set(list tl q) = {} \<and>
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 \<and> 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 \<and> X \<in> set Ps}
nipkow@13772
   126
  WHILE p \<noteq> Null \<and> p \<noteq> Ref X
nipkow@13772
   127
  INV {\<exists>ps. List tl p ps \<and> X \<in> 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 \<noteq> Null \<and> p \<noteq> X
nipkow@13772
   142
  INV {\<exists>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@44890
   147
 apply fastforce
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) \<in> {(Ref x,tl x) |x. True}^*}
nipkow@13772
   157
  WHILE p \<noteq> Null \<and> p \<noteq> X
nipkow@13772
   158
  INV {(p,X) \<in> {(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 \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
nipkow@13772
   173
  WHILE p \<noteq> Null \<and> p \<noteq> Ref X
nipkow@13772
   174
  INV {p \<noteq> Null \<and> (addr p,X) \<in> {(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 \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and> size Qs \<le> size Ps}
nipkow@19397
   189
  pp := p;
nipkow@19397
   190
  WHILE q \<noteq> Null
nipkow@19397
   191
  INV {\<exists>as bs qs.
nipkow@19397
   192
    distinct as \<and> Path tl p as pp \<and> List tl pp bs \<and> List tl q qs \<and>
nipkow@19397
   193
    set bs \<inter> set qs = {} \<and> set as \<inter> (set bs \<union> set qs) = {} \<and>
nipkow@19397
   194
    size qs \<le> size bs \<and> 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@44890
   199
  apply fastforce
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@44890
   211
apply (fastforce 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 \<Rightarrow> bool \<Rightarrow> bool"
wenzelm@38353
   220
  where "cor P Q \<longleftrightarrow> (if P then True else Q)"
haftmann@35416
   221
wenzelm@38353
   222
definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
wenzelm@38353
   223
  where "cand P Q \<longleftrightarrow> (if P then Q else False)"
nipkow@13773
   224
wenzelm@38353
   225
fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> '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 \<inter> B) = (a \<notin> B & {} = A \<inter> B)"
nipkow@13772
   236
by blast
nipkow@13773
   237
lemma [simp]: "({} = A \<inter> insert b B) = (b \<notin> A & {} = A \<inter> B)"
nipkow@13773
   238
by blast
nipkow@13773
   239
lemma [simp]: "({} = A \<inter> (B \<union> C)) = ({} = A \<inter> B & {} = A \<inter> 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 \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and>
nipkow@13772
   244
  (p \<noteq> Null \<or> q \<noteq> Null)}
nipkow@13773
   245
 IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> 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 \<noteq> Null \<or> q \<noteq> Null
nipkow@13772
   249
 INV {EX rs ps qs a. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and>
nipkow@13772
   250
      distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
nipkow@13772
   251
      merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
nipkow@13772
   252
      rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
nipkow@13772
   253
      (tl a = p \<or> tl a = q)}
nipkow@13773
   254
 DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> 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,\<lambda>x y. hd x \<le> hd y))}"
nipkow@13772
   259
apply vcg_simp
nipkow@13773
   260
apply (simp_all add: cand_def cor_def)
nipkow@13772
   261
nipkow@44890
   262
apply (fastforce)
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@44890
   268
apply (fastforce 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@44890
   285
apply (fastforce 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 \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and>
nipkow@14074
   294
  (p \<noteq> Null \<or> q \<noteq> Null) \<and> ps = Ps \<and> qs = Qs}
nipkow@14074
   295
 IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> 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 \<noteq> Null \<or> q \<noteq> Null
nipkow@14074
   300
 INV {Path next r rs s \<and> List next p ps \<and> List next q qs \<and>
nipkow@14074
   301
      distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
nipkow@14074
   302
      merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y) =
nipkow@14074
   303
      rs @ a # merge(ps,qs,\<lambda>x y. elem x \<le> elem y) \<and>
nipkow@14074
   304
      (next a = p \<or> next a = q)}
nipkow@14074
   305
 DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> 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,\<lambda>x y. elem x \<le> elem y))}"
nipkow@14074
   311
apply vcg_simp
nipkow@14074
   312
apply (simp_all add: cand_def cor_def)
nipkow@14074
   313
nipkow@44890
   314
apply (fastforce)
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 \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" and
wenzelm@38353
   342
  path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> '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 \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow> ispath (f(a := r)) p q"
wenzelm@24499
   351
by (rule unproven)
nipkow@13773
   352
lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow>
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) \<Longrightarrow> ispath (f(a := q)) p q"
wenzelm@24499
   359
by (rule unproven)
nipkow@13773
   360
lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow>
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) \<Longrightarrow> f a = Ref b \<Longrightarrow>
nipkow@13773
   364
 b \<notin> set (path f p (Ref a))"
wenzelm@24499
   365
by (rule unproven)
nipkow@13773
   366
lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> islist f p"
wenzelm@24499
   367
by (rule unproven)
nipkow@13773
   368
lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> 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 \<Longrightarrow> 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 \<and> islist tl q & Qs = list tl q \<and>
nipkow@13773
   376
  set Ps \<inter> set Qs = {} \<and>
nipkow@13773
   377
  (p \<noteq> Null \<or> q \<noteq> Null)}
nipkow@13773
   378
 IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> 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 \<noteq> Null \<or> q \<noteq> Null
nipkow@13773
   382
 INV {EX rs ps qs a. ispath tl r s & rs = path tl r s \<and>
nipkow@13773
   383
      islist tl p & ps = list tl p \<and> islist tl q & qs = list tl q \<and>
nipkow@13773
   384
      distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
nipkow@13773
   385
      merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
nipkow@13773
   386
      rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
nipkow@13773
   387
      (tl a = p \<or> tl a = q)}
nipkow@13773
   388
 DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> 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,\<lambda>x y. hd x \<le> hd y))}"
nipkow@13773
   393
apply vcg_simp
nipkow@13773
   394
nipkow@13773
   395
apply (simp_all add: cand_def cor_def)
nipkow@44890
   396
  apply (fastforce)
nipkow@44890
   397
 apply (fastforce 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 \<and> distPath next root (r#Ps) root}
nipkow@19399
   413
  p := root; q := root^.next;
nipkow@19399
   414
  WHILE q \<noteq> root
nipkow@19399
   415
  INV {\<exists> ps qs. distPath next p ps root \<and> distPath next q qs root \<and> 
nipkow@19399
   416
             root = Ref r \<and> r \<notin> set Ps  \<and> set ps \<inter> set qs = {} \<and> 
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 \<and> 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 \<and> distPath next p (r#Ps) p}
nipkow@19399
   459
q:=Null;
nipkow@19399
   460
WHILE p \<noteq> Null
nipkow@19399
   461
INV
nipkow@19399
   462
{ ((q = Null) \<longrightarrow> (\<exists>ps. distPath next p (ps) (Ref r) \<and> ps = r#Ps)) \<and>
nipkow@19399
   463
  ((q \<noteq> Null) \<longrightarrow> (\<exists>ps qs. distPath next q (qs) (Ref r) \<and> List next p ps  \<and>
nipkow@19399
   464
                   set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps@[r])) \<and>
nipkow@19399
   465
  \<not> (p = Null \<and> q = Null) }
nipkow@19399
   466
DO tmp := p; p := p^.next; tmp^.next := q; q:=tmp OD
nipkow@19399
   467
{q = Ref r \<and> 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@44890
   473
  apply (fastforce 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 \<Rightarrow> 'a"
wenzelm@38353
   485
  where "new A = (SOME a. a \<notin> A)"
nipkow@13772
   486
nipkow@13772
   487
nipkow@13772
   488
lemma new_notin:
nipkow@13772
   489
 "\<lbrakk> ~finite(UNIV::'a set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow> new (A) \<notin> 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) \<Longrightarrow>
nipkow@13772
   498
  VARS xs elem next alloc p q
nipkow@13772
   499
  {Xs = xs \<and> p = (Null::'a ref)}
nipkow@13772
   500
  WHILE xs \<noteq> []
nipkow@13772
   501
  INV {islist next p \<and> set(list next p) \<subseteq> set alloc \<and>
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 \<and> 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@44890
   509
apply fastforce
nipkow@13772
   510
done
nipkow@13772
   511
nipkow@13772
   512
nipkow@13772
   513
end