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.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.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 -