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