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
     1 (*  Title:      HOL/Hoare/Pointers.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   2002 TUM
     5 
     6 Examples of verifications of pointer programs
     7 *)
     8 
     9 theory Pointer_Examples = Pointers:
    10 
    11 section "Verifications"
    12 
    13 subsection "List reversal"
    14 
    15 text "A short but unreadable proof:"
    16 
    17 lemma "VARS tl p q r
    18   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
    19   WHILE p \<noteq> Null
    20   INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    21                  rev ps @ qs = rev Ps @ Qs}
    22   DO r := p; p := p^.tl; r^.tl := q; q := r OD
    23   {List tl q (rev Ps @ Qs)}"
    24 apply vcg_simp
    25   apply fastsimp
    26  apply(fastsimp intro:notin_List_update[THEN iffD2])
    27 (* explicit:
    28  apply clarify
    29  apply(rename_tac ps b qs)
    30  apply clarsimp
    31  apply(rename_tac ps')
    32  apply(fastsimp intro:notin_List_update[THEN iffD2])
    33  apply(rule_tac x = ps' in exI)
    34  apply simp
    35  apply(rule_tac x = "b#qs" in exI)
    36  apply simp
    37 *)
    38 apply fastsimp
    39 done
    40 
    41 
    42 text "A longer readable version:"
    43 
    44 lemma "VARS tl p q r
    45   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
    46   WHILE p \<noteq> Null
    47   INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    48                rev ps @ qs = rev Ps @ Qs}
    49   DO r := p; p := p^.tl; r^.tl := q; q := r OD
    50   {List tl q (rev Ps @ Qs)}"
    51 proof vcg
    52   fix tl p q r
    53   assume "List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}"
    54   thus "\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    55                 rev ps @ qs = rev Ps @ Qs" by fastsimp
    56 next
    57   fix tl p q r
    58   assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    59                    rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> Null"
    60          (is "(\<exists>ps qs. ?I ps qs) \<and> _")
    61   then obtain ps qs a where I: "?I ps qs \<and> p = Ref a"
    62     by fast
    63   then obtain ps' where "ps = a # ps'" by fastsimp
    64   hence "List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
    65          List (tl(p \<rightarrow> q)) p       (a#qs) \<and>
    66          set ps' \<inter> set (a#qs) = {} \<and>
    67          rev ps' @ (a#qs) = rev Ps @ Qs"
    68     using I by fastsimp
    69   thus "\<exists>ps' qs'. List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
    70                   List (tl(p \<rightarrow> q)) p       qs' \<and>
    71                   set ps' \<inter> set qs' = {} \<and>
    72                   rev ps' @ qs' = rev Ps @ Qs" by fast
    73 next
    74   fix tl p q r
    75   assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    76                    rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null"
    77   thus "List tl q (rev Ps @ Qs)" by fastsimp
    78 qed
    79 
    80 
    81 text{* Finaly, the functional version. A bit more verbose, but automatic! *}
    82 
    83 lemma "VARS tl p q r
    84   {islist tl p \<and> islist tl q \<and>
    85    Ps = list tl p \<and> Qs = list tl q \<and> set Ps \<inter> set Qs = {}}
    86   WHILE p \<noteq> Null
    87   INV {islist tl p \<and> islist tl q \<and>
    88        set(list tl p) \<inter> set(list tl q) = {} \<and>
    89        rev(list tl p) @ (list tl q) = rev Ps @ Qs}
    90   DO r := p; p := p^.tl; r^.tl := q; q := r OD
    91   {islist tl q \<and> list tl q = rev Ps @ Qs}"
    92 apply vcg_simp
    93   apply clarsimp
    94  apply clarsimp
    95 apply clarsimp
    96 done
    97 
    98 
    99 subsection "Searching in a list"
   100 
   101 text{*What follows is a sequence of successively more intelligent proofs that
   102 a simple loop finds an element in a linked list.
   103 
   104 We start with a proof based on the @{term List} predicate. This means it only
   105 works for acyclic lists. *}
   106 
   107 lemma "VARS tl p
   108   {List tl p Ps \<and> X \<in> set Ps}
   109   WHILE p \<noteq> Null \<and> p \<noteq> Ref X
   110   INV {\<exists>ps. List tl p ps \<and> X \<in> set ps}
   111   DO p := p^.tl OD
   112   {p = Ref X}"
   113 apply vcg_simp
   114   apply blast
   115  apply clarsimp
   116 apply clarsimp
   117 done
   118 
   119 text{*Using @{term Path} instead of @{term List} generalizes the correctness
   120 statement to cyclic lists as well: *}
   121 
   122 lemma "VARS tl p
   123   {Path tl p Ps X}
   124   WHILE p \<noteq> Null \<and> p \<noteq> X
   125   INV {\<exists>ps. Path tl p ps X}
   126   DO p := p^.tl OD
   127   {p = X}"
   128 apply vcg_simp
   129   apply blast
   130  apply fastsimp
   131 apply clarsimp
   132 done
   133 
   134 text{*Now it dawns on us that we do not need the list witness at all --- it
   135 suffices to talk about reachability, i.e.\ we can use relations directly. The
   136 first version uses a relation on @{typ"'a ref"}: *}
   137 
   138 lemma "VARS tl p
   139   {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
   140   WHILE p \<noteq> Null \<and> p \<noteq> X
   141   INV {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
   142   DO p := p^.tl OD
   143   {p = X}"
   144 apply vcg_simp
   145  apply clarsimp
   146  apply(erule converse_rtranclE)
   147   apply simp
   148  apply(clarsimp elim:converse_rtranclE)
   149 apply(fast elim:converse_rtranclE)
   150 done
   151 
   152 text{*Finally, a version based on a relation on type @{typ 'a}:*}
   153 
   154 lemma "VARS tl p
   155   {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
   156   WHILE p \<noteq> Null \<and> p \<noteq> Ref X
   157   INV {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
   158   DO p := p^.tl OD
   159   {p = Ref X}"
   160 apply vcg_simp
   161  apply clarsimp
   162  apply(erule converse_rtranclE)
   163   apply simp
   164  apply clarsimp
   165 apply clarsimp
   166 done
   167 
   168 
   169 subsection "Merging two lists"
   170 
   171 text"This is still a bit rough, especially the proof."
   172 
   173 consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
   174 
   175 recdef merge "measure(%(xs,ys,f). size xs + size ys)"
   176 "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
   177                                 else y # merge(x#xs,ys,f))"
   178 "merge(x#xs,[],f) = x # merge(xs,[],f)"
   179 "merge([],y#ys,f) = y # merge([],ys,f)"
   180 "merge([],[],f) = []"
   181 
   182 lemma imp_disjCL: "(P|Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (~P \<longrightarrow> Q \<longrightarrow> R))"
   183 by blast
   184 
   185 declare imp_disjL[simp del] imp_disjCL[simp]
   186 
   187 lemma "VARS hd tl p q r s
   188  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and>
   189   (p \<noteq> Null \<or> q \<noteq> Null)}
   190  IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd
   191  THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
   192  s := r;
   193  WHILE p \<noteq> Null \<or> q \<noteq> Null
   194  INV {EX rs ps qs a. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and>
   195       distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
   196       merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
   197       rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
   198       (tl a = p \<or> tl a = q)}
   199  DO IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd
   200     THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
   201     s := s^.tl
   202  OD
   203  {List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
   204 apply vcg_simp
   205 
   206 apply (fastsimp)
   207 
   208 (* One big fastsimp does not seem to converge: *)
   209 apply clarsimp
   210 apply(rule conjI)
   211 apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   212 apply clarsimp
   213 apply(rule conjI)
   214 apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   215 apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   216 
   217 apply(clarsimp simp add:List_app)
   218 done
   219 
   220 (* merging with islist/list instead of List? Unlikely to be simpler *)
   221 
   222 subsection "Storage allocation"
   223 
   224 constdefs new :: "'a set \<Rightarrow> 'a"
   225 "new A == SOME a. a \<notin> A"
   226 
   227 
   228 lemma new_notin:
   229  "\<lbrakk> ~finite(UNIV::'a set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow> new (A) \<notin> B"
   230 apply(unfold new_def)
   231 apply(rule someI2_ex)
   232  apply (fast intro:ex_new_if_finite)
   233 apply (fast)
   234 done
   235 
   236 
   237 lemma "~finite(UNIV::'a set) \<Longrightarrow>
   238   VARS xs elem next alloc p q
   239   {Xs = xs \<and> p = (Null::'a ref)}
   240   WHILE xs \<noteq> []
   241   INV {islist next p \<and> set(list next p) \<subseteq> set alloc \<and>
   242        map elem (rev(list next p)) @ xs = Xs}
   243   DO q := Ref(new(set alloc)); alloc := (addr q)#alloc;
   244      q^.next := p; q^.elem := hd xs; xs := tl xs; p := q
   245   OD
   246   {islist next p \<and> map elem (rev(list next p)) = Xs}"
   247 apply vcg_simp
   248  apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
   249 apply fastsimp
   250 done
   251 
   252 
   253 end