Included cyclic list examples
authornipkow
Mon Apr 10 11:33:22 2006 +0200 (2006-04-10)
changeset 19399fd2ba98056a2
parent 19398 8ad34412ea97
child 19400 17382f02079e
Included cyclic list examples
src/HOL/Hoare/Heap.thy
src/HOL/Hoare/Pointer_Examples.thy
     1.1 --- a/src/HOL/Hoare/Heap.thy	Mon Apr 10 08:30:26 2006 +0200
     1.2 +++ b/src/HOL/Hoare/Heap.thy	Mon Apr 10 11:33:22 2006 +0200
     1.3 @@ -58,6 +58,30 @@
     1.4  by simp
     1.5  
     1.6  
     1.7 +subsection "Non-repeating paths"
     1.8 +
     1.9 +constdefs
    1.10 +  distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
    1.11 +  "distPath h x as y   \<equiv>   Path h x as y  \<and>  distinct as"
    1.12 +
    1.13 +text{* The term @{term"distPath h x as y"} expresses the fact that a
    1.14 +non-repeating path @{term as} connects location @{term x} to location
    1.15 +@{term y} by means of the @{term h} field. In the case where @{text "x
    1.16 += y"}, and there is a cycle from @{term x} to itself, @{term as} can
    1.17 +be both @{term "[]"} and the non-repeating list of nodes in the
    1.18 +cycle. *}
    1.19 +
    1.20 +lemma neq_dP: "p \<noteq> q \<Longrightarrow> Path h p Ps q \<Longrightarrow> distinct Ps \<Longrightarrow>
    1.21 + EX a Qs. p = Ref a & Ps = a#Qs & a \<notin> set Qs"
    1.22 +by (case_tac Ps, auto)
    1.23 +
    1.24 +
    1.25 +lemma neq_dP_disp: "\<lbrakk> p \<noteq> q; distPath h p Ps q \<rbrakk> \<Longrightarrow>
    1.26 + EX a Qs. p = Ref a \<and> Ps = a#Qs \<and> a \<notin> set Qs"
    1.27 +apply (simp only:distPath_def)
    1.28 +by (case_tac Ps, auto)
    1.29 +
    1.30 +
    1.31  subsection "Lists on the heap"
    1.32  
    1.33  subsubsection "Relational abstraction"
    1.34 @@ -105,6 +129,13 @@
    1.35  apply(fastsimp dest:List_hd_not_in_tl)
    1.36  done
    1.37  
    1.38 +lemma Path_is_List:
    1.39 +  "\<lbrakk>Path h b Ps (Ref a); a \<notin> set Ps\<rbrakk> \<Longrightarrow> List (h(a := Null)) b (Ps @ [a])"
    1.40 +apply (induct Ps fixing: b)
    1.41 +apply (auto simp add:fun_upd_apply)
    1.42 +done
    1.43 +
    1.44 +
    1.45  subsection "Functional abstraction"
    1.46  
    1.47  constdefs
     2.1 --- a/src/HOL/Hoare/Pointer_Examples.thy	Mon Apr 10 08:30:26 2006 +0200
     2.2 +++ b/src/HOL/Hoare/Pointer_Examples.thy	Mon Apr 10 11:33:22 2006 +0200
     2.3 @@ -402,6 +402,85 @@
     2.4  
     2.5  text"The proof is automatic, but requires a numbet of special lemmas."
     2.6  
     2.7 +
     2.8 +subsection "Cyclic list reversal"
     2.9 +
    2.10 +
    2.11 +text{* We consider two algorithms for the reversal of circular lists.
    2.12 +*}
    2.13 +
    2.14 +lemma circular_list_rev_I:
    2.15 +  "VARS next root p q tmp
    2.16 +  {root = Ref r \<and> distPath next root (r#Ps) root}
    2.17 +  p := root; q := root^.next;
    2.18 +  WHILE q \<noteq> root
    2.19 +  INV {\<exists> ps qs. distPath next p ps root \<and> distPath next q qs root \<and> 
    2.20 +             root = Ref r \<and> r \<notin> set Ps  \<and> set ps \<inter> set qs = {} \<and> 
    2.21 +             Ps = (rev ps) @ qs  }
    2.22 +  DO tmp := q; q := q^.next; tmp^.next := p; p:=tmp OD;
    2.23 +  root^.next := p
    2.24 +  { root = Ref r \<and> distPath next root (r#rev Ps) root}"
    2.25 +apply (simp only:distPath_def)
    2.26 +apply vcg_simp
    2.27 +  apply (rule_tac x="[]" in exI)
    2.28 +  apply auto
    2.29 + apply (drule (2) neq_dP)
    2.30 + apply clarsimp
    2.31 + apply(rule_tac x="a # ps" in exI)
    2.32 +apply clarsimp
    2.33 +done
    2.34 +
    2.35 +text{* In the beginning, we are able to assert @{term"distPath next
    2.36 +root as root"}, with @{term"as"} set to @{term"[]"} or
    2.37 +@{term"[r,a,b,c]"}. Note that @{term"Path next root as root"} would
    2.38 +additionally give us an infinite number of lists with the recurring
    2.39 +sequence @{term"[r,a,b,c]"}.
    2.40 +
    2.41 +The precondition states that there exists a non-empty non-repeating
    2.42 +path \mbox{@{term "r # Ps"}} from pointer @{term root} to itself, given that
    2.43 +@{term root} points to location @{term r}. Pointers @{term p} and
    2.44 +@{term q} are then set to @{term root} and the successor of @{term
    2.45 +root} respectively. If @{term "q = root"}, we have circled the loop,
    2.46 +otherwise we set the @{term next} pointer field of @{term q} to point
    2.47 +to @{term p}, and shift @{term p} and @{term q} one step forward. The
    2.48 +invariant thus states that @{term p} and @{term q} point to two
    2.49 +disjoint lists @{term ps} and @{term qs}, such that @{term"Ps = rev ps
    2.50 +@ qs"}. After the loop terminates, one
    2.51 +extra step is needed to close the loop. As expected, the postcondition
    2.52 +states that the @{term distPath} from @{term root} to itself is now
    2.53 +@{term "r # (rev Ps)"}.
    2.54 +
    2.55 +It may come as a surprise to the reader that the simple algorithm for
    2.56 +acyclic list reversal, with modified annotations, works for cyclic
    2.57 +lists as well: *}
    2.58 +
    2.59 +
    2.60 +lemma circular_list_rev_II:
    2.61 +"VARS next p q tmp
    2.62 +{p = Ref r \<and> distPath next p (r#Ps) p}
    2.63 +q:=Null;
    2.64 +WHILE p \<noteq> Null
    2.65 +INV
    2.66 +{ ((q = Null) \<longrightarrow> (\<exists>ps. distPath next p (ps) (Ref r) \<and> ps = r#Ps)) \<and>
    2.67 +  ((q \<noteq> Null) \<longrightarrow> (\<exists>ps qs. distPath next q (qs) (Ref r) \<and> List next p ps  \<and>
    2.68 +                   set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps@[r])) \<and>
    2.69 +  \<not> (p = Null \<and> q = Null) }
    2.70 +DO tmp := p; p := p^.next; tmp^.next := q; q:=tmp OD
    2.71 +{q = Ref r \<and> distPath next q (r # rev Ps) q}"
    2.72 +apply (simp only:distPath_def)
    2.73 +apply vcg_simp
    2.74 +  apply clarsimp
    2.75 +  apply clarsimp
    2.76 + apply (case_tac "(q = Null)")
    2.77 +  apply (fastsimp intro: Path_is_List)
    2.78 + apply clarsimp
    2.79 + apply (rule_tac x= "bs" in exI)
    2.80 + apply (rule_tac x= "y # qs" in exI)
    2.81 + apply clarsimp
    2.82 +apply (auto simp:fun_upd_apply)
    2.83 +done
    2.84 +
    2.85 +
    2.86  subsection "Storage allocation"
    2.87  
    2.88  constdefs new :: "'a set \<Rightarrow> 'a"