src/HOL/Hoare/Pointer_Examples.thy
changeset 14074 93dfce3b6f86
parent 14062 7f0d5cc52615
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Hoare/Pointer_Examples.thy	Thu Jun 26 15:48:33 2003 +0200
     1.2 +++ b/src/HOL/Hoare/Pointer_Examples.thy	Thu Jun 26 18:14:04 2003 +0200
     1.3 @@ -258,10 +258,51 @@
     1.4  apply(clarsimp simp add:List_app)
     1.5  done
     1.6  
     1.7 +text{* And now with ghost variables: *}
     1.8  
     1.9 -text{* More of the proof can be automated, but the runtime goes up
    1.10 -drastically. In general it is usually more efficient to give the
    1.11 -witness directly than to have it found by proof.
    1.12 +lemma "VARS elem next p q r s ps qs rs a
    1.13 + {List next p Ps \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and>
    1.14 +  (p \<noteq> Null \<or> q \<noteq> Null) \<and> ps = Ps \<and> qs = Qs}
    1.15 + IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
    1.16 + THEN r := p; p := p^.next; ps := tl ps
    1.17 + ELSE r := q; q := q^.next; qs := tl qs FI;
    1.18 + s := r; rs := []; a := addr s;
    1.19 + WHILE p \<noteq> Null \<or> q \<noteq> Null
    1.20 + INV {Path next r rs s \<and> List next p ps \<and> List next q qs \<and>
    1.21 +      distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
    1.22 +      merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y) =
    1.23 +      rs @ a # merge(ps,qs,\<lambda>x y. elem x \<le> elem y) \<and>
    1.24 +      (next a = p \<or> next a = q)}
    1.25 + DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
    1.26 +    THEN s^.next := p; p := p^.next; ps := tl ps
    1.27 +    ELSE s^.next := q; q := q^.next; qs := tl qs FI;
    1.28 +    rs := rs @ [a]; s := s^.next; a := addr s
    1.29 + OD
    1.30 + {List next r (merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y))}"
    1.31 +apply vcg_simp
    1.32 +apply (simp_all add: cand_def cor_def)
    1.33 +
    1.34 +apply (fastsimp)
    1.35 +
    1.36 +apply clarsimp
    1.37 +apply(rule conjI)
    1.38 +apply(clarsimp)
    1.39 +apply(rule conjI)
    1.40 +apply(clarsimp simp:neq_commute)
    1.41 +apply(clarsimp simp:neq_commute)
    1.42 +apply(clarsimp simp:neq_commute)
    1.43 +
    1.44 +apply(clarsimp simp add:List_app)
    1.45 +done
    1.46 +
    1.47 +text{* The proof is a LOT simpler because it does not need
    1.48 +instantiations anymore, but it is still not quite automatic, probably
    1.49 +because of this wrong orientation business. *}
    1.50 +
    1.51 +text{* More of the previous proof without ghost variables can be
    1.52 +automated, but the runtime goes up drastically. In general it is
    1.53 +usually more efficient to give the witness directly than to have it
    1.54 +found by proof.
    1.55  
    1.56  Now we try a functional version of the abstraction relation @{term
    1.57  Path}. Since the result is not that convincing, we do not prove any of
    1.58 @@ -332,47 +373,6 @@
    1.59  
    1.60  text"The proof is automatic, but requires a numbet of special lemmas."
    1.61  
    1.62 -text{* And now with ghost variables: *}
    1.63 -
    1.64 -lemma "VARS elem next p q r s ps qs rs a
    1.65 - {List next p Ps \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and>
    1.66 -  (p \<noteq> Null \<or> q \<noteq> Null) \<and> ps = Ps \<and> qs = Qs}
    1.67 - IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
    1.68 - THEN r := p; p := p^.next; ps := tl ps
    1.69 - ELSE r := q; q := q^.next; qs := tl qs FI;
    1.70 - s := r; rs := []; a := addr s;
    1.71 - WHILE p \<noteq> Null \<or> q \<noteq> Null
    1.72 - INV {Path next r rs s \<and> List next p ps \<and> List next q qs \<and>
    1.73 -      distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
    1.74 -      merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y) =
    1.75 -      rs @ a # merge(ps,qs,\<lambda>x y. elem x \<le> elem y) \<and>
    1.76 -      (next a = p \<or> next a = q)}
    1.77 - DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
    1.78 -    THEN s^.next := p; p := p^.next; ps := tl ps
    1.79 -    ELSE s^.next := q; q := q^.next; qs := tl qs FI;
    1.80 -    rs := rs @ [a]; s := s^.next; a := addr s
    1.81 - OD
    1.82 - {List next r (merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y))}"
    1.83 -apply vcg_simp
    1.84 -apply (simp_all add: cand_def cor_def)
    1.85 -
    1.86 -apply (fastsimp)
    1.87 -
    1.88 -apply clarsimp
    1.89 -apply(rule conjI)
    1.90 -apply(clarsimp)
    1.91 -apply(rule conjI)
    1.92 -apply(clarsimp simp:eq_sym_conv)
    1.93 -apply(clarsimp simp:eq_sym_conv)
    1.94 -apply(clarsimp simp:eq_sym_conv)
    1.95 -
    1.96 -apply(clarsimp simp add:List_app)
    1.97 -done
    1.98 -
    1.99 -text{* The proof is a LOT simpler because it does not need
   1.100 -instantiations anymore, but it is still not quite automatic, probably
   1.101 -because of this wrong orientation business. *}
   1.102 -
   1.103  subsection "Storage allocation"
   1.104  
   1.105  constdefs new :: "'a set \<Rightarrow> 'a"