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