src/HOL/Hoare/Pointer_Examples.thy
author nipkow
Mon Jan 06 11:22:54 2003 +0100 (2003-01-06)
changeset 13772 73d041cc6a66
child 13773 58dc4ab362d0
permissions -rw-r--r--
Split Pointers.thy and automated one proof, which caused the runtime to explode
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@13772
     9
theory Pointer_Examples = Pointers:
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@13772
   173
consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
nipkow@13772
   174
nipkow@13772
   175
recdef merge "measure(%(xs,ys,f). size xs + size ys)"
nipkow@13772
   176
"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
nipkow@13772
   177
                                else y # merge(x#xs,ys,f))"
nipkow@13772
   178
"merge(x#xs,[],f) = x # merge(xs,[],f)"
nipkow@13772
   179
"merge([],y#ys,f) = y # merge([],ys,f)"
nipkow@13772
   180
"merge([],[],f) = []"
nipkow@13772
   181
nipkow@13772
   182
lemma imp_disjCL: "(P|Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (~P \<longrightarrow> Q \<longrightarrow> R))"
nipkow@13772
   183
by blast
nipkow@13772
   184
nipkow@13772
   185
declare imp_disjL[simp del] imp_disjCL[simp]
nipkow@13772
   186
nipkow@13772
   187
lemma "VARS hd tl p q r s
nipkow@13772
   188
 {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and>
nipkow@13772
   189
  (p \<noteq> Null \<or> q \<noteq> Null)}
nipkow@13772
   190
 IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd
nipkow@13772
   191
 THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
nipkow@13772
   192
 s := r;
nipkow@13772
   193
 WHILE p \<noteq> Null \<or> q \<noteq> Null
nipkow@13772
   194
 INV {EX rs ps qs a. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and>
nipkow@13772
   195
      distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
nipkow@13772
   196
      merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
nipkow@13772
   197
      rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
nipkow@13772
   198
      (tl a = p \<or> tl a = q)}
nipkow@13772
   199
 DO IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd
nipkow@13772
   200
    THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
nipkow@13772
   201
    s := s^.tl
nipkow@13772
   202
 OD
nipkow@13772
   203
 {List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
nipkow@13772
   204
apply vcg_simp
nipkow@13772
   205
nipkow@13772
   206
apply (fastsimp)
nipkow@13772
   207
nipkow@13772
   208
(* One big fastsimp does not seem to converge: *)
nipkow@13772
   209
apply clarsimp
nipkow@13772
   210
apply(rule conjI)
nipkow@13772
   211
apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
nipkow@13772
   212
apply clarsimp
nipkow@13772
   213
apply(rule conjI)
nipkow@13772
   214
apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
nipkow@13772
   215
apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
nipkow@13772
   216
nipkow@13772
   217
apply(clarsimp simp add:List_app)
nipkow@13772
   218
done
nipkow@13772
   219
nipkow@13772
   220
(* merging with islist/list instead of List? Unlikely to be simpler *)
nipkow@13772
   221
nipkow@13772
   222
subsection "Storage allocation"
nipkow@13772
   223
nipkow@13772
   224
constdefs new :: "'a set \<Rightarrow> 'a"
nipkow@13772
   225
"new A == SOME a. a \<notin> A"
nipkow@13772
   226
nipkow@13772
   227
nipkow@13772
   228
lemma new_notin:
nipkow@13772
   229
 "\<lbrakk> ~finite(UNIV::'a set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow> new (A) \<notin> B"
nipkow@13772
   230
apply(unfold new_def)
nipkow@13772
   231
apply(rule someI2_ex)
nipkow@13772
   232
 apply (fast intro:ex_new_if_finite)
nipkow@13772
   233
apply (fast)
nipkow@13772
   234
done
nipkow@13772
   235
nipkow@13772
   236
nipkow@13772
   237
lemma "~finite(UNIV::'a set) \<Longrightarrow>
nipkow@13772
   238
  VARS xs elem next alloc p q
nipkow@13772
   239
  {Xs = xs \<and> p = (Null::'a ref)}
nipkow@13772
   240
  WHILE xs \<noteq> []
nipkow@13772
   241
  INV {islist next p \<and> set(list next p) \<subseteq> set alloc \<and>
nipkow@13772
   242
       map elem (rev(list next p)) @ xs = Xs}
nipkow@13772
   243
  DO q := Ref(new(set alloc)); alloc := (addr q)#alloc;
nipkow@13772
   244
     q^.next := p; q^.elem := hd xs; xs := tl xs; p := q
nipkow@13772
   245
  OD
nipkow@13772
   246
  {islist next p \<and> map elem (rev(list next p)) = Xs}"
nipkow@13772
   247
apply vcg_simp
nipkow@13772
   248
 apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
nipkow@13772
   249
apply fastsimp
nipkow@13772
   250
done
nipkow@13772
   251
nipkow@13772
   252
nipkow@13772
   253
end