src/HOL/Hoare/Pointer_Examples.thy

--- a/src/HOL/Hoare/Pointer_Examples.thy	Fri Jun 20 18:13:16 2003 +0200
+++ b/src/HOL/Hoare/Pointer_Examples.thy	Sun Jun 22 01:06:46 2003 +0200
@@ -38,6 +38,22 @@
 apply fastsimp
 done
 
+text{* And now with ghost variables @{term ps} and @{term qs}. Even
+``more automatic''. *}
+
+lemma "VARS next p ps q qs r
+  {List next p Ps \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and>
+   ps = Ps \<and> qs = Qs}
+  WHILE p \<noteq> Null
+  INV {List next p ps \<and> List next q qs \<and> set ps \<inter> set qs = {} \<and>
+       rev ps @ qs = rev Ps @ Qs}
+  DO r := p; p := p^.next; r^.next := q; q := r;
+     qs := (hd ps) # qs; ps := tl ps OD
+  {List next q (rev Ps @ Qs)}"
+apply vcg_simp
+ apply fastsimp
+apply fastsimp
+done
 
 text "A longer readable version:"
 
@@ -316,6 +332,46 @@
 
 text"The proof is automatic, but requires a numbet of special lemmas."
 
+text{* And now with ghost variables: *}
+
+lemma "VARS elem next p q r s ps qs rs a
+ {List next p Ps \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and>
+  (p \<noteq> Null \<or> q \<noteq> Null) \<and> ps = Ps \<and> qs = Qs}
+ IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
+ THEN r := p; p := p^.next; ps := tl ps
+ ELSE r := q; q := q^.next; qs := tl qs FI;
+ s := r; rs := []; a := addr s;
+ WHILE p \<noteq> Null \<or> q \<noteq> Null
+ INV {Path next r rs s \<and> List next p ps \<and> List next q qs \<and>
+      distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
+      merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y) =
+      rs @ a # merge(ps,qs,\<lambda>x y. elem x \<le> elem y) \<and>
+      (next a = p \<or> next a = q)}
+ DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem))
+    THEN s^.next := p; p := p^.next; ps := tl ps
+    ELSE s^.next := q; q := q^.next; qs := tl qs FI;
+    rs := rs @ [a]; s := s^.next; a := addr s
+ OD
+ {List next r (merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y))}"
+apply vcg_simp
+apply (simp_all add: cand_def cor_def)
+
+apply (fastsimp)
+
+apply clarsimp
+apply(rule conjI)
+apply(clarsimp)
+apply(rule conjI)
+apply(clarsimp simp:eq_sym_conv)
+apply(clarsimp simp:eq_sym_conv)
+apply(clarsimp simp:eq_sym_conv)
+
+apply(clarsimp simp add:List_app)
+done
+
+text{* The proof is a LOT simpler because it does not need
+instantiations anymore, but it is still not quite automatic, probably
+because of this wrong orientation business. *}
 
 subsection "Storage allocation"