Included cyclic list examples

--- a/src/HOL/Hoare/Heap.thy	Mon Apr 10 08:30:26 2006 +0200
+++ b/src/HOL/Hoare/Heap.thy	Mon Apr 10 11:33:22 2006 +0200
@@ -58,6 +58,30 @@
 by simp
 
 
+subsection "Non-repeating paths"
+
+constdefs
+  distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
+  "distPath h x as y   \<equiv>   Path h x as y  \<and>  distinct as"
+
+text{* The term @{term"distPath h x as y"} expresses the fact that a
+non-repeating path @{term as} connects location @{term x} to location
+@{term y} by means of the @{term h} field. In the case where @{text "x
+= y"}, and there is a cycle from @{term x} to itself, @{term as} can
+be both @{term "[]"} and the non-repeating list of nodes in the
+cycle. *}
+
+lemma neq_dP: "p \<noteq> q \<Longrightarrow> Path h p Ps q \<Longrightarrow> distinct Ps \<Longrightarrow>
+ EX a Qs. p = Ref a & Ps = a#Qs & a \<notin> set Qs"
+by (case_tac Ps, auto)
+
+
+lemma neq_dP_disp: "\<lbrakk> p \<noteq> q; distPath h p Ps q \<rbrakk> \<Longrightarrow>
+ EX a Qs. p = Ref a \<and> Ps = a#Qs \<and> a \<notin> set Qs"
+apply (simp only:distPath_def)
+by (case_tac Ps, auto)
+
+
 subsection "Lists on the heap"
 
 subsubsection "Relational abstraction"
@@ -105,6 +129,13 @@
 apply(fastsimp dest:List_hd_not_in_tl)
 done
 
+lemma Path_is_List:
+  "\<lbrakk>Path h b Ps (Ref a); a \<notin> set Ps\<rbrakk> \<Longrightarrow> List (h(a := Null)) b (Ps @ [a])"
+apply (induct Ps fixing: b)
+apply (auto simp add:fun_upd_apply)
+done
+
+
 subsection "Functional abstraction"
 
 constdefs

--- a/src/HOL/Hoare/Pointer_Examples.thy	Mon Apr 10 08:30:26 2006 +0200
+++ b/src/HOL/Hoare/Pointer_Examples.thy	Mon Apr 10 11:33:22 2006 +0200
@@ -402,6 +402,85 @@
 
 text"The proof is automatic, but requires a numbet of special lemmas."
 
+
+subsection "Cyclic list reversal"
+
+
+text{* We consider two algorithms for the reversal of circular lists.
+*}
+
+lemma circular_list_rev_I:
+  "VARS next root p q tmp
+  {root = Ref r \<and> distPath next root (r#Ps) root}
+  p := root; q := root^.next;
+  WHILE q \<noteq> root
+  INV {\<exists> ps qs. distPath next p ps root \<and> distPath next q qs root \<and> 
+             root = Ref r \<and> r \<notin> set Ps  \<and> set ps \<inter> set qs = {} \<and> 
+             Ps = (rev ps) @ qs  }
+  DO tmp := q; q := q^.next; tmp^.next := p; p:=tmp OD;
+  root^.next := p
+  { root = Ref r \<and> distPath next root (r#rev Ps) root}"
+apply (simp only:distPath_def)
+apply vcg_simp
+  apply (rule_tac x="[]" in exI)
+  apply auto
+ apply (drule (2) neq_dP)
+ apply clarsimp
+ apply(rule_tac x="a # ps" in exI)
+apply clarsimp
+done
+
+text{* In the beginning, we are able to assert @{term"distPath next
+root as root"}, with @{term"as"} set to @{term"[]"} or
+@{term"[r,a,b,c]"}. Note that @{term"Path next root as root"} would
+additionally give us an infinite number of lists with the recurring
+sequence @{term"[r,a,b,c]"}.
+
+The precondition states that there exists a non-empty non-repeating
+path \mbox{@{term "r # Ps"}} from pointer @{term root} to itself, given that
+@{term root} points to location @{term r}. Pointers @{term p} and
+@{term q} are then set to @{term root} and the successor of @{term
+root} respectively. If @{term "q = root"}, we have circled the loop,
+otherwise we set the @{term next} pointer field of @{term q} to point
+to @{term p}, and shift @{term p} and @{term q} one step forward. The
+invariant thus states that @{term p} and @{term q} point to two
+disjoint lists @{term ps} and @{term qs}, such that @{term"Ps = rev ps
+@ qs"}. After the loop terminates, one
+extra step is needed to close the loop. As expected, the postcondition
+states that the @{term distPath} from @{term root} to itself is now
+@{term "r # (rev Ps)"}.
+
+It may come as a surprise to the reader that the simple algorithm for
+acyclic list reversal, with modified annotations, works for cyclic
+lists as well: *}
+
+
+lemma circular_list_rev_II:
+"VARS next p q tmp
+{p = Ref r \<and> distPath next p (r#Ps) p}
+q:=Null;
+WHILE p \<noteq> Null
+INV
+{ ((q = Null) \<longrightarrow> (\<exists>ps. distPath next p (ps) (Ref r) \<and> ps = r#Ps)) \<and>
+  ((q \<noteq> Null) \<longrightarrow> (\<exists>ps qs. distPath next q (qs) (Ref r) \<and> List next p ps  \<and>
+                   set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps@[r])) \<and>
+  \<not> (p = Null \<and> q = Null) }
+DO tmp := p; p := p^.next; tmp^.next := q; q:=tmp OD
+{q = Ref r \<and> distPath next q (r # rev Ps) q}"
+apply (simp only:distPath_def)
+apply vcg_simp
+  apply clarsimp
+  apply clarsimp
+ apply (case_tac "(q = Null)")
+  apply (fastsimp intro: Path_is_List)
+ apply clarsimp
+ apply (rule_tac x= "bs" in exI)
+ apply (rule_tac x= "y # qs" in exI)
+ apply clarsimp
+apply (auto simp:fun_upd_apply)
+done
+
+
 subsection "Storage allocation"
 
 constdefs new :: "'a set \<Rightarrow> 'a"