src/HOL/Hoare/Pointer_Examples.thy
changeset 14062 7f0d5cc52615
parent 13875 12997e3ddd8d
child 14074 93dfce3b6f86
     1.1 --- a/src/HOL/Hoare/Pointer_Examples.thy	Fri Jun 20 18:13:16 2003 +0200
     1.2 +++ b/src/HOL/Hoare/Pointer_Examples.thy	Sun Jun 22 01:06:46 2003 +0200
     1.3 @@ -38,6 +38,22 @@
     1.4  apply fastsimp
     1.5  done
     1.6  
     1.7 +text{* And now with ghost variables @{term ps} and @{term qs}. Even
     1.8 +``more automatic''. *}
     1.9 +
    1.10 +lemma "VARS next p ps q qs r
    1.11 +  {List next p Ps \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and>
    1.12 +   ps = Ps \<and> qs = Qs}
    1.13 +  WHILE p \<noteq> Null
    1.14 +  INV {List next p ps \<and> List next q qs \<and> set ps \<inter> set qs = {} \<and>
    1.15 +       rev ps @ qs = rev Ps @ Qs}
    1.16 +  DO r := p; p := p^.next; r^.next := q; q := r;
    1.17 +     qs := (hd ps) # qs; ps := tl ps OD
    1.18 +  {List next q (rev Ps @ Qs)}"
    1.19 +apply vcg_simp
    1.20 + apply fastsimp
    1.21 +apply fastsimp
    1.22 +done
    1.23  
    1.24  text "A longer readable version:"
    1.25  
    1.26 @@ -316,6 +332,46 @@
    1.27  
    1.28  text"The proof is automatic, but requires a numbet of special lemmas."
    1.29  
    1.30 +text{* And now with ghost variables: *}
    1.31 +
    1.32 +lemma "VARS elem next p q r s ps qs rs a
    1.33 + {List next p Ps \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and>
    1.34 +  (p \<noteq> Null \<or> q \<noteq> Null) \<and> ps = Ps \<and> qs = Qs}
    1.35 + IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
    1.36 + THEN r := p; p := p^.next; ps := tl ps
    1.37 + ELSE r := q; q := q^.next; qs := tl qs FI;
    1.38 + s := r; rs := []; a := addr s;
    1.39 + WHILE p \<noteq> Null \<or> q \<noteq> Null
    1.40 + INV {Path next r rs s \<and> List next p ps \<and> List next q qs \<and>
    1.41 +      distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
    1.42 +      merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y) =
    1.43 +      rs @ a # merge(ps,qs,\<lambda>x y. elem x \<le> elem y) \<and>
    1.44 +      (next a = p \<or> next a = q)}
    1.45 + DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
    1.46 +    THEN s^.next := p; p := p^.next; ps := tl ps
    1.47 +    ELSE s^.next := q; q := q^.next; qs := tl qs FI;
    1.48 +    rs := rs @ [a]; s := s^.next; a := addr s
    1.49 + OD
    1.50 + {List next r (merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y))}"
    1.51 +apply vcg_simp
    1.52 +apply (simp_all add: cand_def cor_def)
    1.53 +
    1.54 +apply (fastsimp)
    1.55 +
    1.56 +apply clarsimp
    1.57 +apply(rule conjI)
    1.58 +apply(clarsimp)
    1.59 +apply(rule conjI)
    1.60 +apply(clarsimp simp:eq_sym_conv)
    1.61 +apply(clarsimp simp:eq_sym_conv)
    1.62 +apply(clarsimp simp:eq_sym_conv)
    1.63 +
    1.64 +apply(clarsimp simp add:List_app)
    1.65 +done
    1.66 +
    1.67 +text{* The proof is a LOT simpler because it does not need
    1.68 +instantiations anymore, but it is still not quite automatic, probably
    1.69 +because of this wrong orientation business. *}
    1.70  
    1.71  subsection "Storage allocation"
    1.72