src/HOL/Hoare/Pointer_Examples.thy
changeset 13772 73d041cc6a66
child 13773 58dc4ab362d0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Hoare/Pointer_Examples.thy	Mon Jan 06 11:22:54 2003 +0100
     1.3 @@ -0,0 +1,253 @@
     1.4 +(*  Title:      HOL/Hoare/Pointers.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   2002 TUM
     1.8 +
     1.9 +Examples of verifications of pointer programs
    1.10 +*)
    1.11 +
    1.12 +theory Pointer_Examples = Pointers:
    1.13 +
    1.14 +section "Verifications"
    1.15 +
    1.16 +subsection "List reversal"
    1.17 +
    1.18 +text "A short but unreadable proof:"
    1.19 +
    1.20 +lemma "VARS tl p q r
    1.21 +  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
    1.22 +  WHILE p \<noteq> Null
    1.23 +  INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    1.24 +                 rev ps @ qs = rev Ps @ Qs}
    1.25 +  DO r := p; p := p^.tl; r^.tl := q; q := r OD
    1.26 +  {List tl q (rev Ps @ Qs)}"
    1.27 +apply vcg_simp
    1.28 +  apply fastsimp
    1.29 + apply(fastsimp intro:notin_List_update[THEN iffD2])
    1.30 +(* explicit:
    1.31 + apply clarify
    1.32 + apply(rename_tac ps b qs)
    1.33 + apply clarsimp
    1.34 + apply(rename_tac ps')
    1.35 + apply(fastsimp intro:notin_List_update[THEN iffD2])
    1.36 + apply(rule_tac x = ps' in exI)
    1.37 + apply simp
    1.38 + apply(rule_tac x = "b#qs" in exI)
    1.39 + apply simp
    1.40 +*)
    1.41 +apply fastsimp
    1.42 +done
    1.43 +
    1.44 +
    1.45 +text "A longer readable version:"
    1.46 +
    1.47 +lemma "VARS tl p q r
    1.48 +  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
    1.49 +  WHILE p \<noteq> Null
    1.50 +  INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    1.51 +               rev ps @ qs = rev Ps @ Qs}
    1.52 +  DO r := p; p := p^.tl; r^.tl := q; q := r OD
    1.53 +  {List tl q (rev Ps @ Qs)}"
    1.54 +proof vcg
    1.55 +  fix tl p q r
    1.56 +  assume "List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}"
    1.57 +  thus "\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    1.58 +                rev ps @ qs = rev Ps @ Qs" by fastsimp
    1.59 +next
    1.60 +  fix tl p q r
    1.61 +  assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    1.62 +                   rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> Null"
    1.63 +         (is "(\<exists>ps qs. ?I ps qs) \<and> _")
    1.64 +  then obtain ps qs a where I: "?I ps qs \<and> p = Ref a"
    1.65 +    by fast
    1.66 +  then obtain ps' where "ps = a # ps'" by fastsimp
    1.67 +  hence "List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
    1.68 +         List (tl(p \<rightarrow> q)) p       (a#qs) \<and>
    1.69 +         set ps' \<inter> set (a#qs) = {} \<and>
    1.70 +         rev ps' @ (a#qs) = rev Ps @ Qs"
    1.71 +    using I by fastsimp
    1.72 +  thus "\<exists>ps' qs'. List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
    1.73 +                  List (tl(p \<rightarrow> q)) p       qs' \<and>
    1.74 +                  set ps' \<inter> set qs' = {} \<and>
    1.75 +                  rev ps' @ qs' = rev Ps @ Qs" by fast
    1.76 +next
    1.77 +  fix tl p q r
    1.78 +  assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    1.79 +                   rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null"
    1.80 +  thus "List tl q (rev Ps @ Qs)" by fastsimp
    1.81 +qed
    1.82 +
    1.83 +
    1.84 +text{* Finaly, the functional version. A bit more verbose, but automatic! *}
    1.85 +
    1.86 +lemma "VARS tl p q r
    1.87 +  {islist tl p \<and> islist tl q \<and>
    1.88 +   Ps = list tl p \<and> Qs = list tl q \<and> set Ps \<inter> set Qs = {}}
    1.89 +  WHILE p \<noteq> Null
    1.90 +  INV {islist tl p \<and> islist tl q \<and>
    1.91 +       set(list tl p) \<inter> set(list tl q) = {} \<and>
    1.92 +       rev(list tl p) @ (list tl q) = rev Ps @ Qs}
    1.93 +  DO r := p; p := p^.tl; r^.tl := q; q := r OD
    1.94 +  {islist tl q \<and> list tl q = rev Ps @ Qs}"
    1.95 +apply vcg_simp
    1.96 +  apply clarsimp
    1.97 + apply clarsimp
    1.98 +apply clarsimp
    1.99 +done
   1.100 +
   1.101 +
   1.102 +subsection "Searching in a list"
   1.103 +
   1.104 +text{*What follows is a sequence of successively more intelligent proofs that
   1.105 +a simple loop finds an element in a linked list.
   1.106 +
   1.107 +We start with a proof based on the @{term List} predicate. This means it only
   1.108 +works for acyclic lists. *}
   1.109 +
   1.110 +lemma "VARS tl p
   1.111 +  {List tl p Ps \<and> X \<in> set Ps}
   1.112 +  WHILE p \<noteq> Null \<and> p \<noteq> Ref X
   1.113 +  INV {\<exists>ps. List tl p ps \<and> X \<in> set ps}
   1.114 +  DO p := p^.tl OD
   1.115 +  {p = Ref X}"
   1.116 +apply vcg_simp
   1.117 +  apply blast
   1.118 + apply clarsimp
   1.119 +apply clarsimp
   1.120 +done
   1.121 +
   1.122 +text{*Using @{term Path} instead of @{term List} generalizes the correctness
   1.123 +statement to cyclic lists as well: *}
   1.124 +
   1.125 +lemma "VARS tl p
   1.126 +  {Path tl p Ps X}
   1.127 +  WHILE p \<noteq> Null \<and> p \<noteq> X
   1.128 +  INV {\<exists>ps. Path tl p ps X}
   1.129 +  DO p := p^.tl OD
   1.130 +  {p = X}"
   1.131 +apply vcg_simp
   1.132 +  apply blast
   1.133 + apply fastsimp
   1.134 +apply clarsimp
   1.135 +done
   1.136 +
   1.137 +text{*Now it dawns on us that we do not need the list witness at all --- it
   1.138 +suffices to talk about reachability, i.e.\ we can use relations directly. The
   1.139 +first version uses a relation on @{typ"'a ref"}: *}
   1.140 +
   1.141 +lemma "VARS tl p
   1.142 +  {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
   1.143 +  WHILE p \<noteq> Null \<and> p \<noteq> X
   1.144 +  INV {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
   1.145 +  DO p := p^.tl OD
   1.146 +  {p = X}"
   1.147 +apply vcg_simp
   1.148 + apply clarsimp
   1.149 + apply(erule converse_rtranclE)
   1.150 +  apply simp
   1.151 + apply(clarsimp elim:converse_rtranclE)
   1.152 +apply(fast elim:converse_rtranclE)
   1.153 +done
   1.154 +
   1.155 +text{*Finally, a version based on a relation on type @{typ 'a}:*}
   1.156 +
   1.157 +lemma "VARS tl p
   1.158 +  {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
   1.159 +  WHILE p \<noteq> Null \<and> p \<noteq> Ref X
   1.160 +  INV {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
   1.161 +  DO p := p^.tl OD
   1.162 +  {p = Ref X}"
   1.163 +apply vcg_simp
   1.164 + apply clarsimp
   1.165 + apply(erule converse_rtranclE)
   1.166 +  apply simp
   1.167 + apply clarsimp
   1.168 +apply clarsimp
   1.169 +done
   1.170 +
   1.171 +
   1.172 +subsection "Merging two lists"
   1.173 +
   1.174 +text"This is still a bit rough, especially the proof."
   1.175 +
   1.176 +consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
   1.177 +
   1.178 +recdef merge "measure(%(xs,ys,f). size xs + size ys)"
   1.179 +"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
   1.180 +                                else y # merge(x#xs,ys,f))"
   1.181 +"merge(x#xs,[],f) = x # merge(xs,[],f)"
   1.182 +"merge([],y#ys,f) = y # merge([],ys,f)"
   1.183 +"merge([],[],f) = []"
   1.184 +
   1.185 +lemma imp_disjCL: "(P|Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (~P \<longrightarrow> Q \<longrightarrow> R))"
   1.186 +by blast
   1.187 +
   1.188 +declare imp_disjL[simp del] imp_disjCL[simp]
   1.189 +
   1.190 +lemma "VARS hd tl p q r s
   1.191 + {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and>
   1.192 +  (p \<noteq> Null \<or> q \<noteq> Null)}
   1.193 + IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd
   1.194 + THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
   1.195 + s := r;
   1.196 + WHILE p \<noteq> Null \<or> q \<noteq> Null
   1.197 + INV {EX rs ps qs a. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and>
   1.198 +      distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
   1.199 +      merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
   1.200 +      rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
   1.201 +      (tl a = p \<or> tl a = q)}
   1.202 + DO IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd
   1.203 +    THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
   1.204 +    s := s^.tl
   1.205 + OD
   1.206 + {List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
   1.207 +apply vcg_simp
   1.208 +
   1.209 +apply (fastsimp)
   1.210 +
   1.211 +(* One big fastsimp does not seem to converge: *)
   1.212 +apply clarsimp
   1.213 +apply(rule conjI)
   1.214 +apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   1.215 +apply clarsimp
   1.216 +apply(rule conjI)
   1.217 +apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   1.218 +apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
   1.219 +
   1.220 +apply(clarsimp simp add:List_app)
   1.221 +done
   1.222 +
   1.223 +(* merging with islist/list instead of List? Unlikely to be simpler *)
   1.224 +
   1.225 +subsection "Storage allocation"
   1.226 +
   1.227 +constdefs new :: "'a set \<Rightarrow> 'a"
   1.228 +"new A == SOME a. a \<notin> A"
   1.229 +
   1.230 +
   1.231 +lemma new_notin:
   1.232 + "\<lbrakk> ~finite(UNIV::'a set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow> new (A) \<notin> B"
   1.233 +apply(unfold new_def)
   1.234 +apply(rule someI2_ex)
   1.235 + apply (fast intro:ex_new_if_finite)
   1.236 +apply (fast)
   1.237 +done
   1.238 +
   1.239 +
   1.240 +lemma "~finite(UNIV::'a set) \<Longrightarrow>
   1.241 +  VARS xs elem next alloc p q
   1.242 +  {Xs = xs \<and> p = (Null::'a ref)}
   1.243 +  WHILE xs \<noteq> []
   1.244 +  INV {islist next p \<and> set(list next p) \<subseteq> set alloc \<and>
   1.245 +       map elem (rev(list next p)) @ xs = Xs}
   1.246 +  DO q := Ref(new(set alloc)); alloc := (addr q)#alloc;
   1.247 +     q^.next := p; q^.elem := hd xs; xs := tl xs; p := q
   1.248 +  OD
   1.249 +  {islist next p \<and> map elem (rev(list next p)) = Xs}"
   1.250 +apply vcg_simp
   1.251 + apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
   1.252 +apply fastsimp
   1.253 +done
   1.254 +
   1.255 +
   1.256 +end