src/HOL/Hoare/Pointers.thy

                  rev ps @ qs = rev Ps @ Qs}
   DO r := p; p := p^.tl; r^.tl := q; q := r OD
   {List tl q (rev Ps @ Qs)}"
 apply vcg_simp
   apply fastsimp
+ apply(fastsimp intro:notin_List_update[THEN iffD2])
+(* explicit:
  apply clarify
  apply(rename_tac ps b qs)
  apply clarsimp
  apply(rename_tac ps')
+ apply(fastsimp intro:notin_List_update[THEN iffD2])
  apply(rule_tac x = ps' in exI)
  apply simp
  apply(rule_tac x = "b#qs" in exI)
  apply simp
+*)
 apply fastsimp
 done
 
 
 text "A longer readable version:"

 works for acyclic lists. *}
 
 lemma "VARS tl p
   {List tl p Ps \<and> X \<in> set Ps}
   WHILE p \<noteq> Null \<and> p \<noteq> Ref X
-  INV {p \<noteq> Null \<and> (\<exists>ps. List tl p ps \<and> X \<in> set ps)}
+  INV {\<exists>ps. List tl p ps \<and> X \<in> set ps}
   DO p := p^.tl OD
   {p = Ref X}"
 apply vcg_simp
-  apply(case_tac p)
-   apply clarsimp
-  apply fastsimp
- apply clarsimp
- apply fastsimp
+  apply blast
+ apply clarsimp
 apply clarsimp
 done
 
 text{*Using @{term Path} instead of @{term List} generalizes the correctness
 statement to cyclic lists as well: *}
 
 lemma "VARS tl p
-  {Path tl p Ps (Ref X)}
-  WHILE p \<noteq> Null \<and> p \<noteq> Ref X
-  INV {p \<noteq> Null \<and> (\<exists>ps. Path tl p ps (Ref X))}
+  {Path tl p Ps X}
+  WHILE p \<noteq> Null \<and> p \<noteq> X
+  INV {\<exists>ps. Path tl p ps X}
   DO p := p^.tl OD
-  {p = Ref X}"
-apply vcg_simp
-  apply(case_tac p)
-   apply clarsimp
-  apply(rule conjI)
-   apply simp
+  {p = X}"
+apply vcg_simp
   apply blast
- apply clarsimp
- apply(erule disjE)
-  apply clarsimp
- apply(erule disjE)
-  apply clarsimp
- apply clarsimp
+ apply fastsimp
 apply clarsimp
 done
 
 text{*Now it dawns on us that we do not need the list witness at all --- it
 suffices to talk about reachability, i.e.\ we can use relations directly. The
-first version uses a relation on @{typ"'a option"} and needs a lemma: *}
-
-lemma lem1: "(\<forall>(x,y) \<in>r. a \<noteq> x) \<Longrightarrow> ((a,b) \<in> r^* = (a=b))"
-apply(rule iffI)
- apply(erule converse_rtranclE)
-  apply assumption
- apply blast
-apply simp
-done
+first version uses a relation on @{typ"'a ref"}: *}
 
 lemma "VARS tl p
-  {Ref X \<in> ({(Ref x,tl x) |x. True}^* `` {p})}
-  WHILE p \<noteq> Null \<and> p \<noteq> Ref X
-  INV {p \<noteq> Null \<and> Ref X \<in> ({(Ref x,tl x) |x. True}^* `` {p})}
+  {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
+  WHILE p \<noteq> Null \<and> p \<noteq> X
+  INV {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
   DO p := p^.tl OD
-  {p = Ref X}"
-apply vcg_simp
-  apply(case_tac p)
-   apply(simp add:lem1 eq_sym_conv)
-  apply simp
+  {p = X}"
+apply vcg_simp
  apply clarsimp
  apply(erule converse_rtranclE)
   apply simp
- apply(clarsimp simp add:lem1 eq_sym_conv)
-apply clarsimp
-done
-
-text{*Finally, the simplest version, based on a relation on type @{typ 'a}:*}
+ apply(clarsimp elim:converse_rtranclE)
+apply(fast elim:converse_rtranclE)
+done
+
+text{*Finally, a version based on a relation on type @{typ 'a}:*}
 
 lemma "VARS tl p
-  {p \<noteq> Null \<and> X \<in> ({(x,y). tl x = Ref y}^* `` {addr p})}
+  {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
   WHILE p \<noteq> Null \<and> p \<noteq> Ref X
-  INV {p \<noteq> Null \<and> X \<in> ({(x,y). tl x = Ref y}^* `` {addr p})}
+  INV {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
   DO p := p^.tl OD
   {p = Ref X}"
 apply vcg_simp
  apply clarsimp
  apply(erule converse_rtranclE)