src/HOL/Hoare/Pointers0.thy
author nipkow
Sun Jan 05 21:03:14 2003 +0100 (2003-01-05)
changeset 13771 6cd59cc885a1
child 14746 9f7b31cf74d8
permissions -rw-r--r--
*** empty log message ***
nipkow@13771
     1
(*  Title:      HOL/Hoare/Pointers.thy
nipkow@13771
     2
    ID:         $Id$
nipkow@13771
     3
    Author:     Tobias Nipkow
nipkow@13771
     4
    Copyright   2002 TUM
nipkow@13771
     5
nipkow@13771
     6
This is like Pointers.thy, but instead of a type constructor 'a ref
nipkow@13771
     7
that adjoins Null to a type, Null is simply a distinguished element of
nipkow@13771
     8
the address type. This avoids the Ref constructor and thus simplifies
nipkow@13771
     9
specifications (a bit). However, the proofs don't seem to get simpler
nipkow@13771
    10
- in fact in some case they appear to get (a bit) more complicated.
nipkow@13771
    11
*)
nipkow@13771
    12
nipkow@13771
    13
theory Pointers0 = Hoare:
nipkow@13771
    14
nipkow@13771
    15
subsection "References"
nipkow@13771
    16
nipkow@13771
    17
axclass ref < type
nipkow@13771
    18
consts Null :: "'a::ref"
nipkow@13771
    19
nipkow@13771
    20
subsection "Field access and update"
nipkow@13771
    21
nipkow@13771
    22
syntax
nipkow@13771
    23
  "@fassign"  :: "'a::ref => id => 'v => 's com"
nipkow@13771
    24
   ("(2_^._ :=/ _)" [70,1000,65] 61)
nipkow@13771
    25
  "@faccess"  :: "'a::ref => ('a::ref \<Rightarrow> 'v) => 'v"
nipkow@13771
    26
   ("_^._" [65,1000] 65)
nipkow@13771
    27
translations
nipkow@13771
    28
  "p^.f := e"  =>  "f := fun_upd f p e"
nipkow@13771
    29
  "p^.f"       =>  "f p"
nipkow@13771
    30
nipkow@13771
    31
nipkow@13771
    32
text "An example due to Suzuki:"
nipkow@13771
    33
nipkow@13771
    34
lemma "VARS v n
nipkow@13771
    35
  {distinct[w,x,y,z]}
nipkow@13771
    36
  w^.v := (1::int); w^.n := x;
nipkow@13771
    37
  x^.v := 2; x^.n := y;
nipkow@13771
    38
  y^.v := 3; y^.n := z;
nipkow@13771
    39
  z^.v := 4; x^.n := z
nipkow@13771
    40
  {w^.n^.n^.v = 4}"
nipkow@13771
    41
by vcg_simp
nipkow@13771
    42
nipkow@13771
    43
nipkow@13771
    44
section "The heap"
nipkow@13771
    45
nipkow@13771
    46
subsection "Paths in the heap"
nipkow@13771
    47
nipkow@13771
    48
consts
nipkow@13771
    49
 Path :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
nipkow@13771
    50
primrec
nipkow@13771
    51
"Path h x [] y = (x = y)"
nipkow@13771
    52
"Path h x (a#as) y = (x \<noteq> Null \<and> x = a \<and> Path h (h a) as y)"
nipkow@13771
    53
nipkow@13771
    54
lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
nipkow@13771
    55
apply(case_tac xs)
nipkow@13771
    56
apply fastsimp
nipkow@13771
    57
apply fastsimp
nipkow@13771
    58
done
nipkow@13771
    59
nipkow@13771
    60
lemma [simp]: "a \<noteq> Null \<Longrightarrow> Path h a as z =
nipkow@13771
    61
 (as = [] \<and> z = a  \<or>  (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))"
nipkow@13771
    62
apply(case_tac as)
nipkow@13771
    63
apply fastsimp
nipkow@13771
    64
apply fastsimp
nipkow@13771
    65
done
nipkow@13771
    66
nipkow@13771
    67
lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
nipkow@13771
    68
by(induct as, simp+)
nipkow@13771
    69
nipkow@13771
    70
lemma [simp]: "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
nipkow@13771
    71
by(induct as, simp, simp add:eq_sym_conv)
nipkow@13771
    72
nipkow@13771
    73
subsection "Lists on the heap"
nipkow@13771
    74
nipkow@13771
    75
subsubsection "Relational abstraction"
nipkow@13771
    76
nipkow@13771
    77
constdefs
nipkow@13771
    78
 List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool"
nipkow@13771
    79
"List h x as == Path h x as Null"
nipkow@13771
    80
nipkow@13771
    81
lemma [simp]: "List h x [] = (x = Null)"
nipkow@13771
    82
by(simp add:List_def)
nipkow@13771
    83
nipkow@13771
    84
lemma [simp]: "List h x (a#as) = (x \<noteq> Null \<and> x = a \<and> List h (h a) as)"
nipkow@13771
    85
by(simp add:List_def)
nipkow@13771
    86
nipkow@13771
    87
lemma [simp]: "List h Null as = (as = [])"
nipkow@13771
    88
by(case_tac as, simp_all)
nipkow@13771
    89
nipkow@13771
    90
lemma List_Ref[simp]:
nipkow@13771
    91
 "a \<noteq> Null \<Longrightarrow> List h a as = (\<exists>bs. as = a#bs \<and> List h (h a) bs)"
nipkow@13771
    92
by(case_tac as, simp_all, fast)
nipkow@13771
    93
nipkow@13771
    94
theorem notin_List_update[simp]:
nipkow@13771
    95
 "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
nipkow@13771
    96
apply(induct as)
nipkow@13771
    97
apply simp
nipkow@13771
    98
apply(clarsimp simp add:fun_upd_apply)
nipkow@13771
    99
done
nipkow@13771
   100
nipkow@13771
   101
nipkow@13771
   102
declare fun_upd_apply[simp del]fun_upd_same[simp] fun_upd_other[simp]
nipkow@13771
   103
nipkow@13771
   104
lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
nipkow@13771
   105
by(induct as, simp, clarsimp)
nipkow@13771
   106
nipkow@13771
   107
lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
nipkow@13771
   108
by(blast intro:List_unique)
nipkow@13771
   109
nipkow@13771
   110
lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
nipkow@13771
   111
by(induct as, simp, clarsimp)
nipkow@13771
   112
nipkow@13771
   113
lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as"
nipkow@13771
   114
apply (clarsimp simp add:in_set_conv_decomp)
nipkow@13771
   115
apply(frule List_app[THEN iffD1])
nipkow@13771
   116
apply(fastsimp dest: List_unique)
nipkow@13771
   117
done
nipkow@13771
   118
nipkow@13771
   119
lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
nipkow@13771
   120
apply(induct as, simp)
nipkow@13771
   121
apply(fastsimp dest:List_hd_not_in_tl)
nipkow@13771
   122
done
nipkow@13771
   123
nipkow@13771
   124
subsection "Functional abstraction"
nipkow@13771
   125
nipkow@13771
   126
constdefs
nipkow@13771
   127
 islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool"
nipkow@13771
   128
"islist h p == \<exists>as. List h p as"
nipkow@13771
   129
 list :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list"
nipkow@13771
   130
"list h p == SOME as. List h p as"
nipkow@13771
   131
nipkow@13771
   132
lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
nipkow@13771
   133
apply(simp add:islist_def list_def)
nipkow@13771
   134
apply(rule iffI)
nipkow@13771
   135
apply(rule conjI)
nipkow@13771
   136
apply blast
nipkow@13771
   137
apply(subst some1_equality)
nipkow@13771
   138
  apply(erule List_unique1)
nipkow@13771
   139
 apply assumption
nipkow@13771
   140
apply(rule refl)
nipkow@13771
   141
apply simp
nipkow@13771
   142
apply(rule someI_ex)
nipkow@13771
   143
apply fast
nipkow@13771
   144
done
nipkow@13771
   145
nipkow@13771
   146
lemma [simp]: "islist h Null"
nipkow@13771
   147
by(simp add:islist_def)
nipkow@13771
   148
nipkow@13771
   149
lemma [simp]: "a \<noteq> Null \<Longrightarrow> islist h a = islist h (h a)"
nipkow@13771
   150
by(simp add:islist_def)
nipkow@13771
   151
nipkow@13771
   152
lemma [simp]: "list h Null = []"
nipkow@13771
   153
by(simp add:list_def)
nipkow@13771
   154
nipkow@13771
   155
lemma list_Ref_conv[simp]:
nipkow@13771
   156
 "\<lbrakk> a \<noteq> Null; islist h (h a) \<rbrakk> \<Longrightarrow> list h a = a # list h (h a)"
nipkow@13771
   157
apply(insert List_Ref[of _ h])
nipkow@13771
   158
apply(fastsimp simp:List_conv_islist_list)
nipkow@13771
   159
done
nipkow@13771
   160
nipkow@13771
   161
lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))"
nipkow@13771
   162
apply(insert List_hd_not_in_tl[of h])
nipkow@13771
   163
apply(simp add:List_conv_islist_list)
nipkow@13771
   164
done
nipkow@13771
   165
nipkow@13771
   166
lemma list_upd_conv[simp]:
nipkow@13771
   167
 "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> list (h(y := q)) p = list h p"
nipkow@13771
   168
apply(drule notin_List_update[of _ _ h q p])
nipkow@13771
   169
apply(simp add:List_conv_islist_list)
nipkow@13771
   170
done
nipkow@13771
   171
nipkow@13771
   172
lemma islist_upd[simp]:
nipkow@13771
   173
 "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> islist (h(y := q)) p"
nipkow@13771
   174
apply(frule notin_List_update[of _ _ h q p])
nipkow@13771
   175
apply(simp add:List_conv_islist_list)
nipkow@13771
   176
done
nipkow@13771
   177
nipkow@13771
   178
nipkow@13771
   179
section "Verifications"
nipkow@13771
   180
nipkow@13771
   181
subsection "List reversal"
nipkow@13771
   182
nipkow@13771
   183
text "A short but unreadable proof:"
nipkow@13771
   184
nipkow@13771
   185
lemma "VARS tl p q r
nipkow@13771
   186
  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
nipkow@13771
   187
  WHILE p \<noteq> Null
nipkow@13771
   188
  INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
nipkow@13771
   189
                 rev ps @ qs = rev Ps @ Qs}
nipkow@13771
   190
  DO r := p; p := p^.tl; r^.tl := q; q := r OD
nipkow@13771
   191
  {List tl q (rev Ps @ Qs)}"
nipkow@13771
   192
apply vcg_simp
nipkow@13771
   193
  apply fastsimp
nipkow@13771
   194
 apply(fastsimp intro:notin_List_update[THEN iffD2])
nipkow@13771
   195
(* explicily:
nipkow@13771
   196
 apply clarify
nipkow@13771
   197
 apply(rename_tac ps qs)
nipkow@13771
   198
 apply clarsimp
nipkow@13771
   199
 apply(rename_tac ps')
nipkow@13771
   200
 apply(rule_tac x = ps' in exI)
nipkow@13771
   201
 apply simp
nipkow@13771
   202
 apply(rule_tac x = "p#qs" in exI)
nipkow@13771
   203
 apply simp
nipkow@13771
   204
*)
nipkow@13771
   205
apply fastsimp
nipkow@13771
   206
done
nipkow@13771
   207
nipkow@13771
   208
nipkow@13771
   209
text "A longer readable version:"
nipkow@13771
   210
nipkow@13771
   211
lemma "VARS tl p q r
nipkow@13771
   212
  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
nipkow@13771
   213
  WHILE p \<noteq> Null
nipkow@13771
   214
  INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
nipkow@13771
   215
               rev ps @ qs = rev Ps @ Qs}
nipkow@13771
   216
  DO r := p; p := p^.tl; r^.tl := q; q := r OD
nipkow@13771
   217
  {List tl q (rev Ps @ Qs)}"
nipkow@13771
   218
proof vcg
nipkow@13771
   219
  fix tl p q r
nipkow@13771
   220
  assume "List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}"
nipkow@13771
   221
  thus "\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
nipkow@13771
   222
                rev ps @ qs = rev Ps @ Qs" by fastsimp
nipkow@13771
   223
next
nipkow@13771
   224
  fix tl p q r
nipkow@13771
   225
  assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
nipkow@13771
   226
                   rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> Null"
nipkow@13771
   227
         (is "(\<exists>ps qs. ?I ps qs) \<and> _")
nipkow@13771
   228
  then obtain ps qs where I: "?I ps qs \<and> p \<noteq> Null" by fast
nipkow@13771
   229
  then obtain ps' where "ps = p # ps'" by fastsimp
nipkow@13771
   230
  hence "List (tl(p := q)) (p^.tl) ps' \<and>
nipkow@13771
   231
         List (tl(p := q)) p       (p#qs) \<and>
nipkow@13771
   232
         set ps' \<inter> set (p#qs) = {} \<and>
nipkow@13771
   233
         rev ps' @ (p#qs) = rev Ps @ Qs"
nipkow@13771
   234
    using I by fastsimp
nipkow@13771
   235
  thus "\<exists>ps' qs'. List (tl(p := q)) (p^.tl) ps' \<and>
nipkow@13771
   236
                  List (tl(p := q)) p       qs' \<and>
nipkow@13771
   237
                  set ps' \<inter> set qs' = {} \<and>
nipkow@13771
   238
                  rev ps' @ qs' = rev Ps @ Qs" by fast
nipkow@13771
   239
next
nipkow@13771
   240
  fix tl p q r
nipkow@13771
   241
  assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
nipkow@13771
   242
                   rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null"
nipkow@13771
   243
  thus "List tl q (rev Ps @ Qs)" by fastsimp
nipkow@13771
   244
qed
nipkow@13771
   245
nipkow@13771
   246
nipkow@13771
   247
text{* Finaly, the functional version. A bit more verbose, but automatic! *}
nipkow@13771
   248
nipkow@13771
   249
lemma "VARS tl p q r
nipkow@13771
   250
  {islist tl p \<and> islist tl q \<and>
nipkow@13771
   251
   Ps = list tl p \<and> Qs = list tl q \<and> set Ps \<inter> set Qs = {}}
nipkow@13771
   252
  WHILE p \<noteq> Null
nipkow@13771
   253
  INV {islist tl p \<and> islist tl q \<and>
nipkow@13771
   254
       set(list tl p) \<inter> set(list tl q) = {} \<and>
nipkow@13771
   255
       rev(list tl p) @ (list tl q) = rev Ps @ Qs}
nipkow@13771
   256
  DO r := p; p := p^.tl; r^.tl := q; q := r OD
nipkow@13771
   257
  {islist tl q \<and> list tl q = rev Ps @ Qs}"
nipkow@13771
   258
apply vcg_simp
nipkow@13771
   259
  apply clarsimp
nipkow@13771
   260
 apply clarsimp
nipkow@13771
   261
apply clarsimp
nipkow@13771
   262
done
nipkow@13771
   263
nipkow@13771
   264
nipkow@13771
   265
subsection "Searching in a list"
nipkow@13771
   266
nipkow@13771
   267
text{*What follows is a sequence of successively more intelligent proofs that
nipkow@13771
   268
a simple loop finds an element in a linked list.
nipkow@13771
   269
nipkow@13771
   270
We start with a proof based on the @{term List} predicate. This means it only
nipkow@13771
   271
works for acyclic lists. *}
nipkow@13771
   272
nipkow@13771
   273
lemma "VARS tl p
nipkow@13771
   274
  {List tl p Ps \<and> X \<in> set Ps}
nipkow@13771
   275
  WHILE p \<noteq> Null \<and> p \<noteq> X
nipkow@13771
   276
  INV {p \<noteq> Null \<and> (\<exists>ps. List tl p ps \<and> X \<in> set ps)}
nipkow@13771
   277
  DO p := p^.tl OD
nipkow@13771
   278
  {p = X}"
nipkow@13771
   279
apply vcg_simp
nipkow@13771
   280
  apply(case_tac "p = Null")
nipkow@13771
   281
   apply clarsimp
nipkow@13771
   282
  apply fastsimp
nipkow@13771
   283
 apply clarsimp
nipkow@13771
   284
 apply fastsimp
nipkow@13771
   285
apply clarsimp
nipkow@13771
   286
done
nipkow@13771
   287
nipkow@13771
   288
text{*Using @{term Path} instead of @{term List} generalizes the correctness
nipkow@13771
   289
statement to cyclic lists as well: *}
nipkow@13771
   290
nipkow@13771
   291
lemma "VARS tl p
nipkow@13771
   292
  {Path tl p Ps X}
nipkow@13771
   293
  WHILE p \<noteq> Null \<and> p \<noteq> X
nipkow@13771
   294
  INV {\<exists>ps. Path tl p ps X}
nipkow@13771
   295
  DO p := p^.tl OD
nipkow@13771
   296
  {p = X}"
nipkow@13771
   297
apply vcg_simp
nipkow@13771
   298
  apply blast
nipkow@13771
   299
 apply clarsimp
nipkow@13771
   300
 apply(erule disjE)
nipkow@13771
   301
  apply clarsimp
nipkow@13771
   302
 apply fastsimp
nipkow@13771
   303
apply clarsimp
nipkow@13771
   304
done
nipkow@13771
   305
nipkow@13771
   306
text{*Now it dawns on us that we do not need the list witness at all --- it
nipkow@13771
   307
suffices to talk about reachability, i.e.\ we can use relations directly. *}
nipkow@13771
   308
nipkow@13771
   309
lemma "VARS tl p
nipkow@13771
   310
  {(p,X) \<in> {(x,y). y = tl x & x \<noteq> Null}^*}
nipkow@13771
   311
  WHILE p \<noteq> Null \<and> p \<noteq> X
nipkow@13771
   312
  INV {(p,X) \<in> {(x,y). y = tl x & x \<noteq> Null}^*}
nipkow@13771
   313
  DO p := p^.tl OD
nipkow@13771
   314
  {p = X}"
nipkow@13771
   315
apply vcg_simp
nipkow@13771
   316
 apply clarsimp
nipkow@13771
   317
 apply(erule converse_rtranclE)
nipkow@13771
   318
  apply simp
nipkow@13771
   319
 apply(simp)
nipkow@13771
   320
apply(fastsimp elim:converse_rtranclE)
nipkow@13771
   321
done
nipkow@13771
   322
nipkow@13771
   323
nipkow@13771
   324
subsection "Merging two lists"
nipkow@13771
   325
nipkow@13771
   326
text"This is still a bit rough, especially the proof."
nipkow@13771
   327
nipkow@13771
   328
consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
nipkow@13771
   329
nipkow@13771
   330
recdef merge "measure(%(xs,ys,f). size xs + size ys)"
nipkow@13771
   331
"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
nipkow@13771
   332
                                else y # merge(x#xs,ys,f))"
nipkow@13771
   333
"merge(x#xs,[],f) = x # merge(xs,[],f)"
nipkow@13771
   334
"merge([],y#ys,f) = y # merge([],ys,f)"
nipkow@13771
   335
"merge([],[],f) = []"
nipkow@13771
   336
nipkow@13771
   337
lemma imp_disjCL: "(P|Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (~P \<longrightarrow> Q \<longrightarrow> R))"
nipkow@13771
   338
by blast
nipkow@13771
   339
nipkow@13771
   340
declare disj_not1[simp del] imp_disjL[simp del] imp_disjCL[simp]
nipkow@13771
   341
nipkow@13771
   342
lemma "VARS hd tl p q r s
nipkow@13771
   343
 {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and>
nipkow@13771
   344
  (p \<noteq> Null \<or> q \<noteq> Null)}
nipkow@13771
   345
 IF if q = Null then True else p ~= Null & p^.hd \<le> q^.hd
nipkow@13771
   346
 THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
nipkow@13771
   347
 s := r;
nipkow@13771
   348
 WHILE p \<noteq> Null \<or> q \<noteq> Null
nipkow@13771
   349
 INV {EX rs ps qs. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and>
nipkow@13771
   350
      distinct(s # ps @ qs @ rs) \<and> s \<noteq> Null \<and>
nipkow@13771
   351
      merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
nipkow@13771
   352
      rs @ s # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
nipkow@13771
   353
      (tl s = p \<or> tl s = q)}
nipkow@13771
   354
 DO IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd
nipkow@13771
   355
    THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
nipkow@13771
   356
    s := s^.tl
nipkow@13771
   357
 OD
nipkow@13771
   358
 {List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
nipkow@13771
   359
apply vcg_simp
nipkow@13771
   360
nipkow@13771
   361
apply (fastsimp)
nipkow@13771
   362
nipkow@13771
   363
apply clarsimp
nipkow@13771
   364
apply(rule conjI)
nipkow@13771
   365
apply clarsimp
nipkow@13771
   366
apply(simp add:eq_sym_conv)
nipkow@13771
   367
apply(rule_tac x = "rs @ [s]" in exI)
nipkow@13771
   368
apply simp
nipkow@13771
   369
apply(rule_tac x = "bs" in exI)
nipkow@13771
   370
apply (fastsimp simp:eq_sym_conv)
nipkow@13771
   371
nipkow@13771
   372
apply clarsimp
nipkow@13771
   373
apply(rule conjI)
nipkow@13771
   374
apply clarsimp
nipkow@13771
   375
apply(rule_tac x = "rs @ [s]" in exI)
nipkow@13771
   376
apply simp
nipkow@13771
   377
apply(rule_tac x = "bsa" in exI)
nipkow@13771
   378
apply(rule conjI)
nipkow@13771
   379
apply (simp add:eq_sym_conv)
nipkow@13771
   380
apply(rule exI)
nipkow@13771
   381
apply(rule conjI)
nipkow@13771
   382
apply(rule_tac x = bs in exI)
nipkow@13771
   383
apply(rule conjI)
nipkow@13771
   384
apply(rule refl)
nipkow@13771
   385
apply (simp add:eq_sym_conv)
nipkow@13771
   386
apply (simp add:eq_sym_conv)
nipkow@13771
   387
apply (fast)
nipkow@13771
   388
nipkow@13771
   389
apply(rule conjI)
nipkow@13771
   390
apply clarsimp
nipkow@13771
   391
apply(rule_tac x = "rs @ [s]" in exI)
nipkow@13771
   392
apply simp
nipkow@13771
   393
apply(rule_tac x = bs in exI)
nipkow@13771
   394
apply (simp add:eq_sym_conv)
nipkow@13771
   395
apply clarsimp
nipkow@13771
   396
apply(rule_tac x = "rs @ [s]" in exI)
nipkow@13771
   397
apply (simp add:eq_sym_conv)
nipkow@13771
   398
apply(rule exI)
nipkow@13771
   399
apply(rule conjI)
nipkow@13771
   400
apply(rule_tac x = bsa in exI)
nipkow@13771
   401
apply(rule conjI)
nipkow@13771
   402
apply(rule refl)
nipkow@13771
   403
apply (simp add:eq_sym_conv)
nipkow@13771
   404
apply(rule_tac x = bs in exI)
nipkow@13771
   405
apply (simp add:eq_sym_conv)
nipkow@13771
   406
apply fast
nipkow@13771
   407
nipkow@13771
   408
apply(clarsimp simp add:List_app)
nipkow@13771
   409
done
nipkow@13771
   410
nipkow@13771
   411
(* TODO: merging with islist/list instead of List: an improvement?
nipkow@13771
   412
   needs (is)path, which is not so easy to prove either. *)
nipkow@13771
   413
nipkow@13771
   414
subsection "Storage allocation"
nipkow@13771
   415
nipkow@13771
   416
constdefs new :: "'a set \<Rightarrow> 'a::ref"
nipkow@13771
   417
"new A == SOME a. a \<notin> A & a \<noteq> Null"
nipkow@13771
   418
nipkow@13771
   419
nipkow@13771
   420
lemma new_notin:
nipkow@13771
   421
 "\<lbrakk> ~finite(UNIV::('a::ref)set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow>
nipkow@13771
   422
  new (A) \<notin> B & new A \<noteq> Null"
nipkow@13771
   423
apply(unfold new_def)
nipkow@13771
   424
apply(rule someI2_ex)
nipkow@13771
   425
 apply (fast dest:ex_new_if_finite[of "insert Null A"])
nipkow@13771
   426
apply (fast)
nipkow@13771
   427
done
nipkow@13771
   428
nipkow@13771
   429
lemma "~finite(UNIV::('a::ref)set) \<Longrightarrow>
nipkow@13771
   430
  VARS xs elem next alloc p q
nipkow@13771
   431
  {Xs = xs \<and> p = (Null::'a)}
nipkow@13771
   432
  WHILE xs \<noteq> []
nipkow@13771
   433
  INV {islist next p \<and> set(list next p) \<subseteq> set alloc \<and>
nipkow@13771
   434
       map elem (rev(list next p)) @ xs = Xs}
nipkow@13771
   435
  DO q := new(set alloc); alloc := q#alloc;
nipkow@13771
   436
     q^.next := p; q^.elem := hd xs; xs := tl xs; p := q
nipkow@13771
   437
  OD
nipkow@13771
   438
  {islist next p \<and> map elem (rev(list next p)) = Xs}"
nipkow@13771
   439
apply vcg_simp
nipkow@13771
   440
 apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
nipkow@13771
   441
apply fastsimp
nipkow@13771
   442
done
nipkow@13771
   443
nipkow@13771
   444
nipkow@13771
   445
end