src/HOL/Hoare/Pointer_Examples.thy
author nipkow
Sun Mar 23 11:57:07 2003 +0100 (2003-03-23)
changeset 13875 12997e3ddd8d
parent 13773 58dc4ab362d0
child 14062 7f0d5cc52615
permissions -rw-r--r--
*** empty log message ***
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
nipkow@13875
     9
theory Pointer_Examples = HeapSyntax:
nipkow@13772
    10
nipkow@13772
    11
section "Verifications"
nipkow@13772
    12
nipkow@13772
    13
subsection "List reversal"
nipkow@13772
    14
nipkow@13772
    15
text "A short but unreadable proof:"
nipkow@13772
    16
nipkow@13772
    17
lemma "VARS tl p q r
nipkow@13772
    18
  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
nipkow@13772
    19
  WHILE p \<noteq> Null
nipkow@13772
    20
  INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
nipkow@13772
    21
                 rev ps @ qs = rev Ps @ Qs}
nipkow@13772
    22
  DO r := p; p := p^.tl; r^.tl := q; q := r OD
nipkow@13772
    23
  {List tl q (rev Ps @ Qs)}"
nipkow@13772
    24
apply vcg_simp
nipkow@13772
    25
  apply fastsimp
nipkow@13772
    26
 apply(fastsimp intro:notin_List_update[THEN iffD2])
nipkow@13772
    27
(* explicit:
nipkow@13772
    28
 apply clarify
nipkow@13772
    29
 apply(rename_tac ps b qs)
nipkow@13772
    30
 apply clarsimp
nipkow@13772
    31
 apply(rename_tac ps')
nipkow@13772
    32
 apply(fastsimp intro:notin_List_update[THEN iffD2])
nipkow@13772
    33
 apply(rule_tac x = ps' in exI)
nipkow@13772
    34
 apply simp
nipkow@13772
    35
 apply(rule_tac x = "b#qs" in exI)
nipkow@13772
    36
 apply simp
nipkow@13772
    37
*)
nipkow@13772
    38
apply fastsimp
nipkow@13772
    39
done
nipkow@13772
    40
nipkow@13772
    41
nipkow@13772
    42
text "A longer readable version:"
nipkow@13772
    43
nipkow@13772
    44
lemma "VARS tl p q r
nipkow@13772
    45
  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
nipkow@13772
    46
  WHILE p \<noteq> Null
nipkow@13772
    47
  INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
nipkow@13772
    48
               rev ps @ qs = rev Ps @ Qs}
nipkow@13772
    49
  DO r := p; p := p^.tl; r^.tl := q; q := r OD
nipkow@13772
    50
  {List tl q (rev Ps @ Qs)}"
nipkow@13772
    51
proof vcg
nipkow@13772
    52
  fix tl p q r
nipkow@13772
    53
  assume "List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}"
nipkow@13772
    54
  thus "\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
nipkow@13772
    55
                rev ps @ qs = rev Ps @ Qs" by fastsimp
nipkow@13772
    56
next
nipkow@13772
    57
  fix tl p q r
nipkow@13772
    58
  assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
nipkow@13772
    59
                   rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> Null"
nipkow@13772
    60
         (is "(\<exists>ps qs. ?I ps qs) \<and> _")
nipkow@13772
    61
  then obtain ps qs a where I: "?I ps qs \<and> p = Ref a"
nipkow@13772
    62
    by fast
nipkow@13772
    63
  then obtain ps' where "ps = a # ps'" by fastsimp
nipkow@13772
    64
  hence "List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
nipkow@13772
    65
         List (tl(p \<rightarrow> q)) p       (a#qs) \<and>
nipkow@13772
    66
         set ps' \<inter> set (a#qs) = {} \<and>
nipkow@13772
    67
         rev ps' @ (a#qs) = rev Ps @ Qs"
nipkow@13772
    68
    using I by fastsimp
nipkow@13772
    69
  thus "\<exists>ps' qs'. List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
nipkow@13772
    70
                  List (tl(p \<rightarrow> q)) p       qs' \<and>
nipkow@13772
    71
                  set ps' \<inter> set qs' = {} \<and>
nipkow@13772
    72
                  rev ps' @ qs' = rev Ps @ Qs" by fast
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> \<not> p \<noteq> Null"
nipkow@13772
    77
  thus "List tl q (rev Ps @ Qs)" by fastsimp
nipkow@13772
    78
qed
nipkow@13772
    79
nipkow@13772
    80
nipkow@13772
    81
text{* Finaly, the functional version. A bit more verbose, but automatic! *}
nipkow@13772
    82
nipkow@13772
    83
lemma "VARS tl p q r
nipkow@13772
    84
  {islist tl p \<and> islist tl q \<and>
nipkow@13772
    85
   Ps = list tl p \<and> Qs = list tl q \<and> set Ps \<inter> set Qs = {}}
nipkow@13772
    86
  WHILE p \<noteq> Null
nipkow@13772
    87
  INV {islist tl p \<and> islist tl q \<and>
nipkow@13772
    88
       set(list tl p) \<inter> set(list tl q) = {} \<and>
nipkow@13772
    89
       rev(list tl p) @ (list tl q) = rev Ps @ Qs}
nipkow@13772
    90
  DO r := p; p := p^.tl; r^.tl := q; q := r OD
nipkow@13772
    91
  {islist tl q \<and> list tl q = rev Ps @ Qs}"
nipkow@13772
    92
apply vcg_simp
nipkow@13772
    93
  apply clarsimp
nipkow@13772
    94
 apply clarsimp
nipkow@13772
    95
apply clarsimp
nipkow@13772
    96
done
nipkow@13772
    97
nipkow@13772
    98
nipkow@13772
    99
subsection "Searching in a list"
nipkow@13772
   100
nipkow@13772
   101
text{*What follows is a sequence of successively more intelligent proofs that
nipkow@13772
   102
a simple loop finds an element in a linked list.
nipkow@13772
   103
nipkow@13772
   104
We start with a proof based on the @{term List} predicate. This means it only
nipkow@13772
   105
works for acyclic lists. *}
nipkow@13772
   106
nipkow@13772
   107
lemma "VARS tl p
nipkow@13772
   108
  {List tl p Ps \<and> X \<in> set Ps}
nipkow@13772
   109
  WHILE p \<noteq> Null \<and> p \<noteq> Ref X
nipkow@13772
   110
  INV {\<exists>ps. List tl p ps \<and> X \<in> set ps}
nipkow@13772
   111
  DO p := p^.tl OD
nipkow@13772
   112
  {p = Ref X}"
nipkow@13772
   113
apply vcg_simp
nipkow@13772
   114
  apply blast
nipkow@13772
   115
 apply clarsimp
nipkow@13772
   116
apply clarsimp
nipkow@13772
   117
done
nipkow@13772
   118
nipkow@13772
   119
text{*Using @{term Path} instead of @{term List} generalizes the correctness
nipkow@13772
   120
statement to cyclic lists as well: *}
nipkow@13772
   121
nipkow@13772
   122
lemma "VARS tl p
nipkow@13772
   123
  {Path tl p Ps X}
nipkow@13772
   124
  WHILE p \<noteq> Null \<and> p \<noteq> X
nipkow@13772
   125
  INV {\<exists>ps. Path tl p ps X}
nipkow@13772
   126
  DO p := p^.tl OD
nipkow@13772
   127
  {p = X}"
nipkow@13772
   128
apply vcg_simp
nipkow@13772
   129
  apply blast
nipkow@13772
   130
 apply fastsimp
nipkow@13772
   131
apply clarsimp
nipkow@13772
   132
done
nipkow@13772
   133
nipkow@13772
   134
text{*Now it dawns on us that we do not need the list witness at all --- it
nipkow@13772
   135
suffices to talk about reachability, i.e.\ we can use relations directly. The
nipkow@13772
   136
first version uses a relation on @{typ"'a ref"}: *}
nipkow@13772
   137
nipkow@13772
   138
lemma "VARS tl p
nipkow@13772
   139
  {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
nipkow@13772
   140
  WHILE p \<noteq> Null \<and> p \<noteq> X
nipkow@13772
   141
  INV {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
nipkow@13772
   142
  DO p := p^.tl OD
nipkow@13772
   143
  {p = X}"
nipkow@13772
   144
apply vcg_simp
nipkow@13772
   145
 apply clarsimp
nipkow@13772
   146
 apply(erule converse_rtranclE)
nipkow@13772
   147
  apply simp
nipkow@13772
   148
 apply(clarsimp elim:converse_rtranclE)
nipkow@13772
   149
apply(fast elim:converse_rtranclE)
nipkow@13772
   150
done
nipkow@13772
   151
nipkow@13772
   152
text{*Finally, a version based on a relation on type @{typ 'a}:*}
nipkow@13772
   153
nipkow@13772
   154
lemma "VARS tl p
nipkow@13772
   155
  {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
nipkow@13772
   156
  WHILE p \<noteq> Null \<and> p \<noteq> Ref X
nipkow@13772
   157
  INV {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
nipkow@13772
   158
  DO p := p^.tl OD
nipkow@13772
   159
  {p = Ref X}"
nipkow@13772
   160
apply vcg_simp
nipkow@13772
   161
 apply clarsimp
nipkow@13772
   162
 apply(erule converse_rtranclE)
nipkow@13772
   163
  apply simp
nipkow@13772
   164
 apply clarsimp
nipkow@13772
   165
apply clarsimp
nipkow@13772
   166
done
nipkow@13772
   167
nipkow@13772
   168
nipkow@13772
   169
subsection "Merging two lists"
nipkow@13772
   170
nipkow@13772
   171
text"This is still a bit rough, especially the proof."
nipkow@13772
   172
nipkow@13773
   173
constdefs
nipkow@13773
   174
 cor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
nipkow@13773
   175
"cor P Q == if P then True else Q"
nipkow@13773
   176
 cand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
nipkow@13773
   177
"cand P Q == if P then Q else False"
nipkow@13773
   178
nipkow@13772
   179
consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
nipkow@13772
   180
nipkow@13772
   181
recdef merge "measure(%(xs,ys,f). size xs + size ys)"
nipkow@13772
   182
"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
nipkow@13772
   183
                                else y # merge(x#xs,ys,f))"
nipkow@13772
   184
"merge(x#xs,[],f) = x # merge(xs,[],f)"
nipkow@13772
   185
"merge([],y#ys,f) = y # merge([],ys,f)"
nipkow@13772
   186
"merge([],[],f) = []"
nipkow@13772
   187
nipkow@13773
   188
text{* Simplifies the proof a little: *}
nipkow@13773
   189
nipkow@13773
   190
lemma [simp]: "({} = insert a A \<inter> B) = (a \<notin> B & {} = A \<inter> B)"
nipkow@13772
   191
by blast
nipkow@13773
   192
lemma [simp]: "({} = A \<inter> insert b B) = (b \<notin> A & {} = A \<inter> B)"
nipkow@13773
   193
by blast
nipkow@13773
   194
lemma [simp]: "({} = A \<inter> (B \<union> C)) = ({} = A \<inter> B & {} = A \<inter> C)"
nipkow@13773
   195
by blast
nipkow@13772
   196
nipkow@13772
   197
lemma "VARS hd tl p q r s
nipkow@13772
   198
 {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and>
nipkow@13772
   199
  (p \<noteq> Null \<or> q \<noteq> Null)}
nipkow@13773
   200
 IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
nipkow@13772
   201
 THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
nipkow@13772
   202
 s := r;
nipkow@13772
   203
 WHILE p \<noteq> Null \<or> q \<noteq> Null
nipkow@13772
   204
 INV {EX rs ps qs a. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and>
nipkow@13772
   205
      distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
nipkow@13772
   206
      merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
nipkow@13772
   207
      rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
nipkow@13772
   208
      (tl a = p \<or> tl a = q)}
nipkow@13773
   209
 DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
nipkow@13772
   210
    THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
nipkow@13772
   211
    s := s^.tl
nipkow@13772
   212
 OD
nipkow@13772
   213
 {List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
nipkow@13772
   214
apply vcg_simp
nipkow@13773
   215
apply (simp_all add: cand_def cor_def)
nipkow@13772
   216
nipkow@13772
   217
apply (fastsimp)
nipkow@13772
   218
nipkow@13773
   219
apply clarsimp
nipkow@13773
   220
apply(rule conjI)
nipkow@13772
   221
apply clarsimp
nipkow@13772
   222
apply(rule conjI)
nipkow@13772
   223
apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
nipkow@13772
   224
apply clarsimp
nipkow@13772
   225
apply(rule conjI)
nipkow@13773
   226
apply (clarsimp)
nipkow@13773
   227
apply(rule_tac x = "rs @ [a]" in exI)
nipkow@13773
   228
apply(clarsimp simp:eq_sym_conv)
nipkow@13773
   229
apply(rule_tac x = "bs" in exI)
nipkow@13773
   230
apply(clarsimp simp:eq_sym_conv)
nipkow@13773
   231
apply(rule_tac x = "ya#bsa" in exI)
nipkow@13773
   232
apply(simp)
nipkow@13773
   233
apply(clarsimp simp:eq_sym_conv)
nipkow@13773
   234
apply(rule_tac x = "rs @ [a]" in exI)
nipkow@13773
   235
apply(clarsimp simp:eq_sym_conv)
nipkow@13773
   236
apply(rule_tac x = "y#bs" in exI)
nipkow@13773
   237
apply(clarsimp simp:eq_sym_conv)
nipkow@13773
   238
apply(rule_tac x = "bsa" in exI)
nipkow@13773
   239
apply(simp)
nipkow@13772
   240
apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
nipkow@13772
   241
nipkow@13772
   242
apply(clarsimp simp add:List_app)
nipkow@13772
   243
done
nipkow@13772
   244
nipkow@13773
   245
nipkow@13773
   246
text{* More of the proof can be automated, but the runtime goes up
nipkow@13773
   247
drastically. In general it is usually more efficient to give the
nipkow@13773
   248
witness directly than to have it found by proof.
nipkow@13773
   249
nipkow@13773
   250
Now we try a functional version of the abstraction relation @{term
nipkow@13773
   251
Path}. Since the result is not that convincing, we do not prove any of
nipkow@13773
   252
the lemmas.*}
nipkow@13773
   253
nipkow@13773
   254
consts ispath:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool"
nipkow@13773
   255
       path:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
nipkow@13773
   256
nipkow@13773
   257
ML"set quick_and_dirty"
nipkow@13773
   258
nipkow@13773
   259
text"First some basic lemmas:"
nipkow@13773
   260
nipkow@13773
   261
lemma [simp]: "ispath f p p"
nipkow@13773
   262
sorry
nipkow@13773
   263
lemma [simp]: "path f p p = []"
nipkow@13773
   264
sorry
nipkow@13773
   265
lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow> ispath (f(a := r)) p q"
nipkow@13773
   266
sorry
nipkow@13773
   267
lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow>
nipkow@13773
   268
 path (f(a := r)) p q = path f p q"
nipkow@13773
   269
sorry
nipkow@13773
   270
nipkow@13773
   271
text"Some more specific lemmas needed by the example:"
nipkow@13773
   272
nipkow@13773
   273
lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow> ispath (f(a := q)) p q"
nipkow@13773
   274
sorry
nipkow@13773
   275
lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow>
nipkow@13773
   276
 path (f(a := q)) p q = path (f(a := q)) p (Ref a) @ [a]"
nipkow@13773
   277
sorry
nipkow@13773
   278
lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Ref b \<Longrightarrow>
nipkow@13773
   279
 b \<notin> set (path f p (Ref a))"
nipkow@13773
   280
sorry
nipkow@13773
   281
lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> islist f p"
nipkow@13773
   282
sorry
nipkow@13773
   283
lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> list f p = path f p (Ref a) @ [a]"
nipkow@13773
   284
sorry
nipkow@13773
   285
nipkow@13773
   286
lemma [simp]: "islist f p \<Longrightarrow> distinct (list f p)"
nipkow@13773
   287
sorry
nipkow@13773
   288
ML"reset quick_and_dirty"
nipkow@13773
   289
nipkow@13773
   290
lemma "VARS hd tl p q r s
nipkow@13773
   291
 {islist tl p & Ps = list tl p \<and> islist tl q & Qs = list tl q \<and>
nipkow@13773
   292
  set Ps \<inter> set Qs = {} \<and>
nipkow@13773
   293
  (p \<noteq> Null \<or> q \<noteq> Null)}
nipkow@13773
   294
 IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
nipkow@13773
   295
 THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
nipkow@13773
   296
 s := r;
nipkow@13773
   297
 WHILE p \<noteq> Null \<or> q \<noteq> Null
nipkow@13773
   298
 INV {EX rs ps qs a. ispath tl r s & rs = path tl r s \<and>
nipkow@13773
   299
      islist tl p & ps = list tl p \<and> islist tl q & qs = list tl q \<and>
nipkow@13773
   300
      distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
nipkow@13773
   301
      merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
nipkow@13773
   302
      rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
nipkow@13773
   303
      (tl a = p \<or> tl a = q)}
nipkow@13773
   304
 DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
nipkow@13773
   305
    THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
nipkow@13773
   306
    s := s^.tl
nipkow@13773
   307
 OD
nipkow@13773
   308
 {islist tl r & list tl r = (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
nipkow@13773
   309
apply vcg_simp
nipkow@13773
   310
nipkow@13773
   311
apply (simp_all add: cand_def cor_def)
nipkow@13773
   312
  apply (fastsimp)
nipkow@13773
   313
 apply (fastsimp simp: eq_sym_conv)
nipkow@13773
   314
apply(clarsimp)
nipkow@13773
   315
done
nipkow@13773
   316
nipkow@13773
   317
text"The proof is automatic, but requires a numbet of special lemmas."
nipkow@13773
   318
nipkow@13772
   319
nipkow@13772
   320
subsection "Storage allocation"
nipkow@13772
   321
nipkow@13772
   322
constdefs new :: "'a set \<Rightarrow> 'a"
nipkow@13772
   323
"new A == SOME a. a \<notin> A"
nipkow@13772
   324
nipkow@13772
   325
nipkow@13772
   326
lemma new_notin:
nipkow@13772
   327
 "\<lbrakk> ~finite(UNIV::'a set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow> new (A) \<notin> B"
nipkow@13772
   328
apply(unfold new_def)
nipkow@13772
   329
apply(rule someI2_ex)
nipkow@13772
   330
 apply (fast intro:ex_new_if_finite)
nipkow@13772
   331
apply (fast)
nipkow@13772
   332
done
nipkow@13772
   333
nipkow@13772
   334
nipkow@13772
   335
lemma "~finite(UNIV::'a set) \<Longrightarrow>
nipkow@13772
   336
  VARS xs elem next alloc p q
nipkow@13772
   337
  {Xs = xs \<and> p = (Null::'a ref)}
nipkow@13772
   338
  WHILE xs \<noteq> []
nipkow@13772
   339
  INV {islist next p \<and> set(list next p) \<subseteq> set alloc \<and>
nipkow@13772
   340
       map elem (rev(list next p)) @ xs = Xs}
nipkow@13772
   341
  DO q := Ref(new(set alloc)); alloc := (addr q)#alloc;
nipkow@13772
   342
     q^.next := p; q^.elem := hd xs; xs := tl xs; p := q
nipkow@13772
   343
  OD
nipkow@13772
   344
  {islist next p \<and> map elem (rev(list next p)) = Xs}"
nipkow@13772
   345
apply vcg_simp
nipkow@13772
   346
 apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
nipkow@13772
   347
apply fastsimp
nipkow@13772
   348
done
nipkow@13772
   349
nipkow@13772
   350
nipkow@13772
   351
end