diff --git a/src/HOL/Hoare/Arith2.thy b/src/HOL/Hoare/Arith2.thy
--- a/src/HOL/Hoare/Arith2.thy
+++ b/src/HOL/Hoare/Arith2.thy
@@ -1,89 +1,89 @@
 (*  Title:      HOL/Hoare/Arith2.thy
     Author:     Norbert Galm
     Copyright   1995 TUM
-
-More arithmetic.  Much of this duplicates ex/Primes.
 *)
 
+section \<open>More arithmetic\<close>
+
 theory Arith2
-imports Main
+  imports Main
 begin
 
 definition cd :: "[nat, nat, nat] \<Rightarrow> bool"
   where "cd x m n \<longleftrightarrow> x dvd m \<and> x dvd n"
 
 definition gcd :: "[nat, nat] \<Rightarrow> nat"
   where "gcd m n = (SOME x. cd x m n & (\<forall>y.(cd y m n) \<longrightarrow> y\<le>x))"
 
 primrec fac :: "nat \<Rightarrow> nat"
 where
   "fac 0 = Suc 0"
 | "fac (Suc n) = Suc n * fac n"
 
 
-subsubsection \<open>cd\<close>
+subsection \<open>cd\<close>
 
 lemma cd_nnn: "0<n \<Longrightarrow> cd n n n"
   apply (simp add: cd_def)
   done
 
 lemma cd_le: "[| cd x m n; 0<m; 0<n |] ==> x<=m & x<=n"
   apply (unfold cd_def)
   apply (blast intro: dvd_imp_le)
   done
 
 lemma cd_swap: "cd x m n = cd x n m"
   apply (unfold cd_def)
   apply blast
   done
 
 lemma cd_diff_l: "n\<le>m \<Longrightarrow> cd x m n = cd x (m-n) n"
   apply (unfold cd_def)
   apply (fastforce dest: dvd_diffD)
   done
 
 lemma cd_diff_r: "m\<le>n \<Longrightarrow> cd x m n = cd x m (n-m)"
   apply (unfold cd_def)
   apply (fastforce dest: dvd_diffD)
   done
 
 
-subsubsection \<open>gcd\<close>
+subsection \<open>gcd\<close>
 
 lemma gcd_nnn: "0<n \<Longrightarrow> n = gcd n n"
   apply (unfold gcd_def)
   apply (frule cd_nnn)
   apply (rule some_equality [symmetric])
   apply (blast dest: cd_le)
   apply (blast intro: le_antisym dest: cd_le)
   done
 
 lemma gcd_swap: "gcd m n = gcd n m"
   apply (simp add: gcd_def cd_swap)
   done
 
 lemma gcd_diff_l: "n\<le>m \<Longrightarrow> gcd m n = gcd (m-n) n"
   apply (unfold gcd_def)
   apply (subgoal_tac "n\<le>m \<Longrightarrow> \<forall>x. cd x m n = cd x (m-n) n")
   apply simp
   apply (rule allI)
   apply (erule cd_diff_l)
   done
 
 lemma gcd_diff_r: "m\<le>n \<Longrightarrow> gcd m n = gcd m (n-m)"
   apply (unfold gcd_def)
   apply (subgoal_tac "m\<le>n \<Longrightarrow> \<forall>x. cd x m n = cd x m (n-m) ")
   apply simp
   apply (rule allI)
   apply (erule cd_diff_r)
   done
 
 
-subsubsection \<open>pow\<close>
+subsection \<open>pow\<close>
 
 lemma sq_pow_div2 [simp]:
     "m mod 2 = 0 \<Longrightarrow> ((n::nat)*n)^(m div 2) = n^m"
   apply (simp add: power2_eq_square [symmetric] power_mult [symmetric] minus_mod_eq_mult_div [symmetric])
   done
 
 end
diff --git a/src/HOL/Hoare/Examples.thy b/src/HOL/Hoare/Examples.thy
--- a/src/HOL/Hoare/Examples.thy
+++ b/src/HOL/Hoare/Examples.thy
@@ -1,347 +1,349 @@
 (*  Title:      HOL/Hoare/Examples.thy
     Author:     Norbert Galm
     Copyright   1998 TUM
 *)
 
-chapter \<open>Various examples\<close>
+section \<open>Various examples\<close>
 
-theory Examples imports Hoare_Logic Arith2 begin
+theory Examples
+  imports Hoare_Logic Arith2
+begin
 
-section \<open>ARITHMETIC\<close>
+subsection \<open>Arithmetic\<close>
 
-subsection \<open>multiplication by successive addition\<close>
+subsubsection \<open>Multiplication by successive addition\<close>
 
 lemma multiply_by_add: "VARS m s a b
   {a=A \<and> b=B}
   m := 0; s := 0;
   WHILE m\<noteq>a
   INV {s=m*b \<and> a=A \<and> b=B}
   DO s := s+b; m := m+(1::nat) OD
   {s = A*B}"
 by vcg_simp
 
 lemma multiply_by_add_time: "VARS m s a b t
   {a=A \<and> b=B \<and> t=0}
   m := 0; t := t+1; s := 0; t := t+1;
   WHILE m\<noteq>a
   INV {s=m*b \<and> a=A \<and> b=B \<and> t = 2*m + 2}
   DO s := s+b; t := t+1; m := m+(1::nat); t := t+1 OD
   {s = A*B \<and> t = 2*A + 2}"
 by vcg_simp
 
 lemma multiply_by_add2: "VARS M N P :: int
  {m=M \<and> n=N}
  IF M < 0 THEN M := -M; N := -N ELSE SKIP FI;
  P := 0;
  WHILE 0 < M
  INV {0 \<le> M \<and> (\<exists>p. p = (if m<0 then -m else m) & p*N = m*n & P = (p-M)*N)}
  DO P := P+N; M := M - 1 OD
  {P = m*n}"
 apply vcg_simp
  apply (auto simp add:int_distrib)
 done
 
 lemma multiply_by_add2_time: "VARS M N P t :: int
  {m=M \<and> n=N \<and> t=0}
  IF M < 0 THEN M := -M; t := t+1; N := -N; t := t+1 ELSE SKIP FI;
  P := 0; t := t+1;
  WHILE 0 < M
  INV {0 \<le> M & (\<exists>p. p = (if m<0 then -m else m) & p*N = m*n & P = (p-M)*N & t \<ge> 0 & t \<le> 2*(p-M)+3)}
  DO P := P+N; t := t+1; M := M - 1; t := t+1 OD
  {P = m*n & t \<le> 2*abs m + 3}"
 apply vcg_simp
  apply (auto simp add:int_distrib)
 done
 
 
-subsection \<open>Euclid's algorithm for GCD\<close>
+subsubsection \<open>Euclid's algorithm for GCD\<close>
 
 lemma Euclid_GCD: "VARS a b
  {0<A & 0<B}
  a := A; b := B;
  WHILE  a \<noteq> b
  INV {0<a & 0<b & gcd A B = gcd a b}
  DO IF a<b THEN b := b-a ELSE a := a-b FI OD
  {a = gcd A B}"
 apply vcg
   \<comment> \<open>Now prove the verification conditions\<close>
   apply auto
   apply(simp add: gcd_diff_r less_imp_le)
  apply(simp add: linorder_not_less gcd_diff_l)
 apply(erule gcd_nnn)
 done
 
 lemma Euclid_GCD_time: "VARS a b t
  {0<A & 0<B & t=0}
  a := A; t := t+1; b := B; t := t+1; 
  WHILE  a \<noteq> b
  INV {0<a & 0<b & gcd A B = gcd a b & a\<le>A & b\<le>B & t \<le> max A B - max a b + 2}
  DO IF a<b THEN b := b-a; t := t+1 ELSE a := a-b; t := t+1 FI OD
  {a = gcd A B & t \<le> max A B + 2}"
 apply vcg
   \<comment> \<open>Now prove the verification conditions\<close>
   apply auto
   apply(simp add: gcd_diff_r less_imp_le)
  apply(simp add: linorder_not_less gcd_diff_l)
 apply(erule gcd_nnn)
 done
 
 
-subsection \<open>Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM\<close>
+subsubsection \<open>Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM\<close>
 
 text \<open>
   From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
   where it is given without the invariant. Instead of defining \<open>scm\<close>
   explicitly we have used the theorem \<open>scm x y = x * y / gcd x y\<close> and avoided
   division by mupltiplying with \<open>gcd x y\<close>.
 \<close>
 
 lemmas distribs =
   diff_mult_distrib diff_mult_distrib2 add_mult_distrib add_mult_distrib2
 
 lemma gcd_scm: "VARS a b x y
  {0<A & 0<B & a=A & b=B & x=B & y=A}
  WHILE  a ~= b
  INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y}
  DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD
  {a = gcd A B & 2*A*B = a*(x+y)}"
 apply vcg
   apply simp
  apply(simp add: distribs gcd_diff_r linorder_not_less gcd_diff_l)
 apply(simp add: distribs gcd_nnn)
 done
 
 
-subsection \<open>Power by iterated squaring and multiplication\<close>
+subsubsection \<open>Power by iterated squaring and multiplication\<close>
 
 lemma power_by_mult: "VARS a b c
  {a=A & b=B}
  c := (1::nat);
  WHILE b ~= 0
  INV {A^B = c * a^b}
  DO  WHILE b mod 2 = 0
      INV {A^B = c * a^b}
      DO  a := a*a; b := b div 2 OD;
      c := c*a; b := b - 1
  OD
  {c = A^B}"
 apply vcg_simp
 apply(case_tac "b")
  apply simp
 apply simp
 done
 
 
-subsection \<open>Factorial\<close>
+subsubsection \<open>Factorial\<close>
 
 lemma factorial: "VARS a b
  {a=A}
  b := 1;
  WHILE a > 0
  INV {fac A = b * fac a}
  DO b := b*a; a := a - 1 OD
  {b = fac A}"
 apply vcg_simp
 apply(clarsimp split: nat_diff_split)
 done
 
 lemma factorial_time: "VARS a b t
  {a=A & t=0}
  b := 1; t := t+1;
  WHILE a > 0
  INV {fac A = b * fac a & a \<le> A & t = 2*(A-a)+1}
  DO b := b*a; t := t+1; a := a - 1; t := t+1 OD
  {b = fac A & t = 2*A + 1}"
 apply vcg_simp
 apply(clarsimp split: nat_diff_split)
 done
 
 lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
 by(induct i, simp_all)
 
 lemma factorial2: "VARS i f
  {True}
  i := (1::nat); f := 1;
  WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
  DO f := f*i; i := i+1 OD
  {f = fac n}"
 apply vcg_simp
 apply(subgoal_tac "i = Suc n")
 apply simp
 apply arith
 done
 
 lemma factorial2_time: "VARS i f t
  {t=0}
  i := (1::nat); t := t+1; f := 1; t := t+1;
  WHILE i \<le> n INV {f = fac(i - 1) & 1 \<le> i & i \<le> n+1 & t = 2*(i-1)+2}
  DO f := f*i; t := t+1; i := i+1; t := t+1 OD
  {f = fac n & t = 2*n+2}"
 apply vcg_simp
  apply auto
 apply(subgoal_tac "i = Suc n")
  apply simp
 apply arith
 done
 
 
-subsection \<open>Square root\<close>
+subsubsection \<open>Square root\<close>
 
 \<comment> \<open>the easy way:\<close>
 
 lemma sqrt: "VARS r x
  {True}
  r := (0::nat);
  WHILE (r+1)*(r+1) <= X
  INV {r*r \<le> X}
  DO r := r+1 OD
  {r*r <= X & X < (r+1)*(r+1)}"
 apply vcg_simp
 done
 
 lemma sqrt_time: "VARS r t
  {t=0}
  r := (0::nat); t := t+1;
  WHILE (r+1)*(r+1) <= X
  INV {r*r \<le> X & t = r+1}
  DO r := r+1; t := t+1 OD
  {r*r <= X & X < (r+1)*(r+1) & (t-1)*(t-1) \<le> X}"
 apply vcg_simp
 done
 
 \<comment> \<open>without multiplication\<close>
 lemma sqrt_without_multiplication: "VARS u w r
  {x=X}
  u := 1; w := 1; r := (0::nat);
  WHILE w <= X
  INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= X}
  DO r := r + 1; w := w + u + 2; u := u + 2 OD
  {r*r <= X & X < (r+1)*(r+1)}"
 apply vcg_simp
 done
 
 
-section \<open>LISTS\<close>
+subsection \<open>Lists\<close>
 
 lemma imperative_reverse: "VARS y x
  {x=X}
  y:=[];
  WHILE x ~= []
  INV {rev(x)@y = rev(X)}
  DO y := (hd x # y); x := tl x OD
  {y=rev(X)}"
 apply vcg_simp
  apply(simp add: neq_Nil_conv)
  apply auto
 done
 
 lemma imperative_reverse_time: "VARS y x t
  {x=X & t=0}
  y:=[]; t := t+1;
  WHILE x ~= []
  INV {rev(x)@y = rev(X) & t = 2*(length y) + 1}
  DO y := (hd x # y); t := t+1; x := tl x; t := t+1 OD
  {y=rev(X) & t = 2*length X + 1}"
 apply vcg_simp
  apply(simp add: neq_Nil_conv)
  apply auto
 done
 
 lemma imperative_append: "VARS x y
  {x=X & y=Y}
  x := rev(x);
  WHILE x~=[]
  INV {rev(x)@y = X@Y}
  DO y := (hd x # y);
     x := tl x
  OD
  {y = X@Y}"
 apply vcg_simp
 apply(simp add: neq_Nil_conv)
 apply auto
 done
 
 lemma imperative_append_time_no_rev: "VARS x y t
  {x=X & y=Y}
  x := rev(x); t := 0;
  WHILE x~=[]
  INV {rev(x)@y = X@Y & length x \<le> length X & t = 2 * (length X - length x)}
  DO y := (hd x # y); t := t+1;
     x := tl x; t := t+1
  OD
  {y = X@Y & t = 2 * length X}"
 apply vcg_simp
 apply(simp add: neq_Nil_conv)
 apply auto
 done
 
 
-section \<open>ARRAYS\<close>
+subsection \<open>Arrays\<close>
 
-subsection \<open>Search for a key\<close>
+subsubsection \<open>Search for a key\<close>
 
 lemma zero_search: "VARS A i
  {True}
  i := 0;
  WHILE i < length A & A!i \<noteq> key
  INV {\<forall>j. j<i --> A!j \<noteq> key}
  DO i := i+1 OD
  {(i < length A --> A!i = key) &
   (i = length A --> (\<forall>j. j < length A \<longrightarrow> A!j \<noteq> key))}"
 apply vcg_simp
 apply(blast elim!: less_SucE)
 done
 
 lemma zero_search_time: "VARS A i t
  {t=0}
  i := 0; t := t+1;
  WHILE i < length A \<and> A!i \<noteq> key
  INV {(\<forall>j. j<i \<longrightarrow> A!j \<noteq> key) \<and> i \<le> length A \<and> t = i+1}
  DO i := i+1; t := t+1 OD
  {(i < length A \<longrightarrow> A!i = key) \<and>
   (i = length A \<longrightarrow> (\<forall>j. j < length A --> A!j \<noteq> key)) \<and> t \<le> length A + 1}"
 apply vcg_simp
 apply(blast elim!: less_SucE)
 done
 
 text \<open>
   The \<open>partition\<close> procedure for quicksort.
     \<^item> \<open>A\<close> is the array to be sorted (modelled as a list).
     \<^item> Elements of \<open>A\<close> must be of class order to infer at the end
       that the elements between u and l are equal to pivot.
 
   Ambiguity warnings of parser are due to \<open>:=\<close> being used
   both for assignment and list update.
 \<close>
 lemma lem: "m - Suc 0 < n ==> m < Suc n"
 by arith
 
 
 lemma Partition:
 "[| leq == \<lambda>A i. \<forall>k. k<i \<longrightarrow> A!k \<le> pivot;
     geq == \<lambda>A i. \<forall>k. i<k \<and> k<length A \<longrightarrow> pivot \<le> A!k |] ==>
  VARS A u l
  {0 < length(A::('a::order)list)}
  l := 0; u := length A - Suc 0;
  WHILE l \<le> u
   INV {leq A l \<and> geq A u \<and> u<length A \<and> l\<le>length A}
   DO WHILE l < length A \<and> A!l \<le> pivot
      INV {leq A l & geq A u \<and> u<length A \<and> l\<le>length A}
      DO l := l+1 OD;
      WHILE 0 < u & pivot \<le> A!u
      INV {leq A l & geq A u  \<and> u<length A \<and> l\<le>length A}
      DO u := u - 1 OD;
      IF l \<le> u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI
   OD
  {leq A u & (\<forall>k. u<k \<and> k<l --> A!k = pivot) \<and> geq A l}"
 \<comment> \<open>expand and delete abbreviations first\<close>
 apply (simp)
 apply (erule thin_rl)+
 apply vcg_simp
    apply (force simp: neq_Nil_conv)
   apply (blast elim!: less_SucE intro: Suc_leI)
  apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
 apply (force simp: nth_list_update)
 done
 
 end
diff --git a/src/HOL/Hoare/ExamplesAbort.thy b/src/HOL/Hoare/ExamplesAbort.thy
--- a/src/HOL/Hoare/ExamplesAbort.thy
+++ b/src/HOL/Hoare/ExamplesAbort.thy
@@ -1,28 +1,30 @@
 (*  Title:      HOL/Hoare/ExamplesAbort.thy
     Author:     Tobias Nipkow
     Copyright   1998 TUM
-
-Some small examples for programs that may abort.
 *)
 
-theory ExamplesAbort imports Hoare_Logic_Abort begin
+section \<open>Some small examples for programs that may abort\<close>
+
+theory ExamplesAbort
+  imports Hoare_Logic_Abort
+begin
 
 lemma "VARS x y z::nat
  {y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}"
 by vcg_simp
 
 lemma
  "VARS a i j
  {k <= length a & i < k & j < k} j < length a \<rightarrow> a[i] := a!j {True}"
 by vcg_simp
 
 lemma "VARS (a::int list) i
  {True}
  i := 0;
  WHILE i < length a
  INV {i <= length a}
  DO a[i] := 7; i := i+1 OD
  {True}"
 by vcg_simp
 
 end
diff --git a/src/HOL/Hoare/ExamplesTC.thy b/src/HOL/Hoare/ExamplesTC.thy
--- a/src/HOL/Hoare/ExamplesTC.thy
+++ b/src/HOL/Hoare/ExamplesTC.thy
@@ -1,118 +1,116 @@
 (* Title:      Examples using Hoare Logic for Total Correctness
    Author:     Walter Guttmann
 *)
 
 section \<open>Examples using Hoare Logic for Total Correctness\<close>
 
 theory ExamplesTC
-
-imports Hoare_Logic
-
+  imports Hoare_Logic
 begin
 
 text \<open>
 This theory demonstrates a few simple partial- and total-correctness proofs.
 The first example is taken from HOL/Hoare/Examples.thy written by N. Galm.
 We have added the invariant \<open>m \<le> a\<close>.
 \<close>
 
 lemma multiply_by_add: "VARS m s a b
   {a=A \<and> b=B}
   m := 0; s := 0;
   WHILE m\<noteq>a
   INV {s=m*b \<and> a=A \<and> b=B \<and> m\<le>a}
   DO s := s+b; m := m+(1::nat) OD
   {s = A*B}"
   by vcg_simp
 
 text \<open>
 Here is the total-correctness proof for the same program.
 It needs the additional invariant \<open>m \<le> a\<close>.
 \<close>
 
 lemma multiply_by_add_tc: "VARS m s a b
   [a=A \<and> b=B]
   m := 0; s := 0;
   WHILE m\<noteq>a
   INV {s=m*b \<and> a=A \<and> b=B \<and> m\<le>a}
   VAR {a-m}
   DO s := s+b; m := m+(1::nat) OD
   [s = A*B]"
   apply vcg_tc_simp
   by auto
 
 text \<open>
 Next, we prove partial correctness of a program that computes powers.
 \<close>
 
 lemma power: "VARS (p::int) i
   { True }
   p := 1;
   i := 0;
   WHILE i < n
     INV { p = x^i \<and> i \<le> n }
      DO p := p * x;
         i := i + 1
      OD
   { p = x^n }"
   apply vcg_simp
   by auto
 
 text \<open>
 Here is its total-correctness proof.
 \<close>
 
 lemma power_tc: "VARS (p::int) i
   [ True ]
   p := 1;
   i := 0;
   WHILE i < n
     INV { p = x^i \<and> i \<le> n }
     VAR { n - i }
      DO p := p * x;
         i := i + 1
      OD
   [ p = x^n ]"
   apply vcg_tc
   by auto
 
 text \<open>
 The last example is again taken from HOL/Hoare/Examples.thy.
 We have modified it to integers so it requires precondition \<open>0 \<le> x\<close>.
 \<close>
 
 lemma sqrt_tc: "VARS r
   [0 \<le> (x::int)]
   r := 0;
   WHILE (r+1)*(r+1) <= x
   INV {r*r \<le> x}
   VAR {nat (x-r)}
   DO r := r+1 OD
   [r*r \<le> x \<and> x < (r+1)*(r+1)]"
   apply vcg_tc_simp
   by (smt (verit) div_pos_pos_trivial mult_less_0_iff nonzero_mult_div_cancel_left)
 
 text \<open>
 A total-correctness proof allows us to extract a function for further use.
 For every input satisfying the precondition the function returns an output satisfying the postcondition.
 \<close>
 
 lemma sqrt_exists:
   "0 \<le> (x::int) \<Longrightarrow> \<exists>r' . r'*r' \<le> x \<and> x < (r'+1)*(r'+1)"
   using tc_extract_function sqrt_tc by blast
 
 definition "sqrt (x::int) \<equiv> (SOME r' . r'*r' \<le> x \<and> x < (r'+1)*(r'+1))"
 
 lemma sqrt_function:
   assumes "0 \<le> (x::int)"
     and "r' = sqrt x"
   shows "r'*r' \<le> x \<and> x < (r'+1)*(r'+1)"
 proof -
   let ?P = "\<lambda>r' . r'*r' \<le> x \<and> x < (r'+1)*(r'+1)"
   have "?P (SOME z . ?P z)"
     by (metis (mono_tags, lifting) assms(1) sqrt_exists some_eq_imp)
   thus ?thesis
     using assms(2) sqrt_def by auto
 qed
 
 end
diff --git a/src/HOL/Hoare/Heap.thy b/src/HOL/Hoare/Heap.thy
--- a/src/HOL/Hoare/Heap.thy
+++ b/src/HOL/Hoare/Heap.thy
@@ -1,188 +1,191 @@
 (*  Title:      HOL/Hoare/Heap.thy
     Author:     Tobias Nipkow
     Copyright   2002 TUM
-
-Pointers, heaps and heap abstractions.
-See the paper by Mehta and Nipkow.
 *)
 
-theory Heap imports Main begin
+section \<open>Pointers, heaps and heap abstractions\<close>
+
+text \<open>See the paper by Mehta and Nipkow.\<close>
+
+theory Heap
+  imports Main
+begin
 
 subsection "References"
 
 datatype 'a ref = Null | Ref 'a
 
 lemma not_Null_eq [iff]: "(x \<noteq> Null) = (\<exists>y. x = Ref y)"
   by (induct x) auto
 
 lemma not_Ref_eq [iff]: "(\<forall>y. x \<noteq> Ref y) = (x = Null)"
   by (induct x) auto
 
 primrec addr :: "'a ref \<Rightarrow> 'a" where
   "addr (Ref a) = a"
 
 
-section "The heap"
+subsection "The heap"
 
-subsection "Paths in the heap"
+subsubsection "Paths in the heap"
 
 primrec Path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool" where
   "Path h x [] y \<longleftrightarrow> x = y"
 | "Path h x (a#as) y \<longleftrightarrow> x = Ref a \<and> Path h (h a) as y"
 
 lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
 apply(case_tac xs)
 apply fastforce
 apply fastforce
 done
 
 lemma [simp]: "Path h (Ref a) as z =
  (as = [] \<and> z = Ref a  \<or>  (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))"
 apply(case_tac as)
 apply fastforce
 apply fastforce
 done
 
 lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
 by(induct as, simp+)
 
 lemma Path_upd[simp]:
  "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
 by(induct as, simp, simp add:eq_sym_conv)
 
 lemma Path_snoc:
  "Path (f(a := q)) p as (Ref a) \<Longrightarrow> Path (f(a := q)) p (as @ [a]) q"
 by simp
 
 
-subsection "Non-repeating paths"
+subsubsection "Non-repeating paths"
 
 definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
   where "distPath h x as y \<longleftrightarrow> Path h x as y \<and> distinct as"
 
 text\<open>The term \<^term>\<open>distPath h x as y\<close> expresses the fact that a
 non-repeating path \<^term>\<open>as\<close> connects location \<^term>\<open>x\<close> to location
 \<^term>\<open>y\<close> by means of the \<^term>\<open>h\<close> field. In the case where \<open>x
 = y\<close>, and there is a cycle from \<^term>\<open>x\<close> to itself, \<^term>\<open>as\<close> can
 be both \<^term>\<open>[]\<close> and the non-repeating list of nodes in the
 cycle.\<close>
 
 lemma neq_dP: "p \<noteq> q \<Longrightarrow> Path h p Ps q \<Longrightarrow> distinct Ps \<Longrightarrow>
  \<exists>a Qs. p = Ref a \<and> Ps = a#Qs \<and> a \<notin> set Qs"
 by (case_tac Ps, auto)
 
 
 lemma neq_dP_disp: "\<lbrakk> p \<noteq> q; distPath h p Ps q \<rbrakk> \<Longrightarrow>
  \<exists>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 "Lists on the heap"
 
-subsubsection "Relational abstraction"
+paragraph "Relational abstraction"
 
 definition List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
   where "List h x as = Path h x as Null"
 
 lemma [simp]: "List h x [] = (x = Null)"
 by(simp add:List_def)
 
 lemma [simp]: "List h x (a#as) = (x = Ref a \<and> List h (h a) as)"
 by(simp add:List_def)
 
 lemma [simp]: "List h Null as = (as = [])"
 by(case_tac as, simp_all)
 
 lemma List_Ref[simp]: "List h (Ref a) as = (\<exists>bs. as = a#bs \<and> List h (h a) bs)"
 by(case_tac as, simp_all, fast)
 
 theorem notin_List_update[simp]:
  "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
 apply(induct as)
 apply simp
 apply(clarsimp simp add:fun_upd_apply)
 done
 
 lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
 by(induct as, simp, clarsimp)
 
 lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
 by(blast intro:List_unique)
 
 lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
 by(induct as, simp, clarsimp)
 
 lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as"
 apply (clarsimp simp add:in_set_conv_decomp)
 apply(frule List_app[THEN iffD1])
 apply(fastforce dest: List_unique)
 done
 
 lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
 apply(induct as, simp)
 apply(fastforce 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 arbitrary: b)
 apply (auto simp add:fun_upd_apply)
 done
 
 
-subsection "Functional abstraction"
+subsubsection "Functional abstraction"
 
 definition islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
   where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
 
 definition list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list"
   where "list h p = (SOME as. List h p as)"
 
 lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
 apply(simp add:islist_def list_def)
 apply(rule iffI)
 apply(rule conjI)
 apply blast
 apply(subst some1_equality)
   apply(erule List_unique1)
  apply assumption
 apply(rule refl)
 apply simp
 apply(rule someI_ex)
 apply fast
 done
 
 lemma [simp]: "islist h Null"
 by(simp add:islist_def)
 
 lemma [simp]: "islist h (Ref a) = islist h (h a)"
 by(simp add:islist_def)
 
 lemma [simp]: "list h Null = []"
 by(simp add:list_def)
 
 lemma list_Ref_conv[simp]:
  "islist h (h a) \<Longrightarrow> list h (Ref a) = a # list h (h a)"
 apply(insert List_Ref[of h])
 apply(fastforce simp:List_conv_islist_list)
 done
 
 lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))"
 apply(insert List_hd_not_in_tl[of h])
 apply(simp add:List_conv_islist_list)
 done
 
 lemma list_upd_conv[simp]:
  "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> list (h(y := q)) p = list h p"
 apply(drule notin_List_update[of _ _ h q p])
 apply(simp add:List_conv_islist_list)
 done
 
 lemma islist_upd[simp]:
  "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> islist (h(y := q)) p"
 apply(frule notin_List_update[of _ _ h q p])
 apply(simp add:List_conv_islist_list)
 done
 
 end
diff --git a/src/HOL/Hoare/HeapSyntax.thy b/src/HOL/Hoare/HeapSyntax.thy
--- a/src/HOL/Hoare/HeapSyntax.thy
+++ b/src/HOL/Hoare/HeapSyntax.thy
@@ -1,38 +1,42 @@
 (*  Title:      HOL/Hoare/HeapSyntax.thy
     Author:     Tobias Nipkow
     Copyright   2002 TUM
 *)
 
-theory HeapSyntax imports Hoare_Logic Heap begin
+section \<open>Heap syntax\<close>
+
+theory HeapSyntax
+  imports Hoare_Logic Heap
+begin
 
 subsection "Field access and update"
 
 syntax
   "_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
    ("_/'((_ \<rightarrow> _)')" [1000,0] 900)
   "_fassign"  :: "'a ref => id => 'v => 's com"
    ("(2_^._ :=/ _)" [70,1000,65] 61)
   "_faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    ("_^._" [65,1000] 65)
 translations
   "f(r \<rightarrow> v)" == "f(CONST addr r := v)"
   "p^.f := e" => "f := f(p \<rightarrow> e)"
   "p^.f" => "f(CONST addr p)"
 
 
 declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
 
 
 text "An example due to Suzuki:"
 
 lemma "VARS v n
   {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
    distinct[w0,x0,y0,z0]}
   w^.v := (1::int); w^.n := x;
   x^.v := 2; x^.n := y;
   y^.v := 3; y^.n := z;
   z^.v := 4; x^.n := z
   {w^.n^.n^.v = 4}"
 by vcg_simp
 
 end
diff --git a/src/HOL/Hoare/HeapSyntaxAbort.thy b/src/HOL/Hoare/HeapSyntaxAbort.thy
--- a/src/HOL/Hoare/HeapSyntaxAbort.thy
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy
@@ -1,46 +1,50 @@
 (*  Title:      HOL/Hoare/HeapSyntaxAbort.thy
     Author:     Tobias Nipkow
     Copyright   2002 TUM
 *)
 
-theory HeapSyntaxAbort imports Hoare_Logic_Abort Heap begin
+section \<open>Heap syntax (abort)\<close>
+
+theory HeapSyntaxAbort
+  imports Hoare_Logic_Abort Heap
+begin
 
 subsection "Field access and update"
 
 text\<open>Heap update \<open>p^.h := e\<close> is now guarded against \<^term>\<open>p\<close>
 being Null. However, \<^term>\<open>p\<close> may still be illegal,
 e.g. uninitialized or dangling. To guard against that, one needs a
 more detailed model of the heap where allocated and free addresses are
 distinguished, e.g. by making the heap a map, or by carrying the set
 of free addresses around. This is needed anyway as soon as we want to
 reason about storage allocation/deallocation.\<close>
 
 syntax
   "_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
    ("_/'((_ \<rightarrow> _)')" [1000,0] 900)
   "_fassign"  :: "'a ref => id => 'v => 's com"
    ("(2_^._ :=/ _)" [70,1000,65] 61)
   "_faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    ("_^._" [65,1000] 65)
 translations
   "_refupdate f r v" == "f(CONST addr r := v)"
   "p^.f := e" => "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)"
   "p^.f" => "f(CONST addr p)"
 
 
 declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
 
 
 text "An example due to Suzuki:"
 
 lemma "VARS v n
   {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
    distinct[w0,x0,y0,z0]}
   w^.v := (1::int); w^.n := x;
   x^.v := 2; x^.n := y;
   y^.v := 3; y^.n := z;
   z^.v := 4; x^.n := z
   {w^.n^.n^.v = 4}"
 by vcg_simp
 
 end
diff --git a/src/HOL/Hoare/Hoare_Logic.thy b/src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy
+++ b/src/HOL/Hoare/Hoare_Logic.thy
@@ -1,216 +1,218 @@
 (*  Title:      HOL/Hoare/Hoare_Logic.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Copyright   1998 TUM
     Author:     Walter Guttmann (extension to total-correctness proofs)
 *)
 
-section \<open>Sugared semantic embedding of Hoare logic\<close>
+section \<open>Hoare logic\<close>
+
+theory Hoare_Logic
+  imports Hoare_Syntax Hoare_Tac
+begin
+
+subsection \<open>Sugared semantic embedding of Hoare logic\<close>
 
 text \<open>
   Strictly speaking a shallow embedding (as implemented by Norbert Galm
   following Mike Gordon) would suffice. Maybe the datatype com comes in useful
   later.
 \<close>
 
-theory Hoare_Logic
-imports Hoare_Syntax Hoare_Tac
-begin
-
 type_synonym 'a bexp = "'a set"
 type_synonym 'a assn = "'a set"
 type_synonym 'a var = "'a \<Rightarrow> nat"
 
 datatype 'a com =
   Basic "'a \<Rightarrow> 'a"
 | Seq "'a com" "'a com"
 | Cond "'a bexp" "'a com" "'a com"
 | While "'a bexp" "'a assn" "'a var" "'a com"
 
 abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
 type_synonym 'a sem = "'a => 'a => bool"
 
 inductive Sem :: "'a com \<Rightarrow> 'a sem"
 where
   "Sem (Basic f) s (f s)"
 | "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (Seq c1 c2) s s'"
 | "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (Cond b c1 c2) s s'"
 | "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (Cond b c1 c2) s s'"
 | "s \<notin> b \<Longrightarrow> Sem (While b x y c) s s"
 | "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b x y c) s'' s' \<Longrightarrow>
    Sem (While b x y c) s s'"
 
 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
   where "Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> p \<longrightarrow> s' \<in> q"
 
 definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
   where "ValidTC p c q \<equiv> \<forall>s. s \<in> p \<longrightarrow> (\<exists>t. Sem c s t \<and> t \<in> q)"
 
 inductive_cases [elim!]:
   "Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'"
   "Sem (Cond b c1 c2) s s'"
 
 lemma Sem_deterministic:
   assumes "Sem c s s1"
       and "Sem c s s2"
     shows "s1 = s2"
 proof -
   have "Sem c s s1 \<Longrightarrow> (\<forall>s2. Sem c s s2 \<longrightarrow> s1 = s2)"
     by (induct rule: Sem.induct) (subst Sem.simps, blast)+
   thus ?thesis
     using assms by simp
 qed
 
 lemma tc_implies_pc:
   "ValidTC p c q \<Longrightarrow> Valid p c q"
   by (metis Sem_deterministic Valid_def ValidTC_def)
 
 lemma tc_extract_function:
   "ValidTC p c q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
   by (metis ValidTC_def)
 
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
 by (auto simp:Valid_def)
 
 lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
 by (auto simp:Valid_def)
 
 lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (Seq c1 c2) R"
 by (auto simp:Valid_def)
 
 lemma CondRule:
  "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
   \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
 by (auto simp:Valid_def)
 
 lemma While_aux:
   assumes "Sem (While b i v c) s s'"
   shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
     s \<in> I \<Longrightarrow> s' \<in> I \<and> s' \<notin> b"
   using assms
   by (induct "While b i v c" s s') auto
 
 lemma WhileRule:
  "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i v c) q"
 apply (clarsimp simp:Valid_def)
 apply(drule While_aux)
   apply assumption
  apply blast
 apply blast
 done
 
 lemma SkipRuleTC:
   assumes "p \<subseteq> q"
     shows "ValidTC p (Basic id) q"
   by (metis assms Sem.intros(1) ValidTC_def id_apply subsetD)
 
 lemma BasicRuleTC:
   assumes "p \<subseteq> {s. f s \<in> q}"
     shows "ValidTC p (Basic f) q"
   by (metis assms Ball_Collect Sem.intros(1) ValidTC_def)
 
 lemma SeqRuleTC:
   assumes "ValidTC p c1 q"
       and "ValidTC q c2 r"
     shows "ValidTC p (Seq c1 c2) r"
   by (meson assms Sem.intros(2) ValidTC_def)
 
 lemma CondRuleTC:
  assumes "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}"
      and "ValidTC w c1 q"
      and "ValidTC w' c2 q"
    shows "ValidTC p (Cond b c1 c2) q"
 proof (unfold ValidTC_def, rule allI)
   fix s
   show "s \<in> p \<longrightarrow> (\<exists>t . Sem (Cond b c1 c2) s t \<and> t \<in> q)"
     apply (cases "s \<in> b")
     apply (metis (mono_tags, lifting) assms(1,2) Ball_Collect Sem.intros(3) ValidTC_def)
     by (metis (mono_tags, lifting) assms(1,3) Ball_Collect Sem.intros(4) ValidTC_def)
 qed
 
 lemma WhileRuleTC:
   assumes "p \<subseteq> i"
       and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (i \<inter> {s . v s < n})"
       and "i \<inter> uminus b \<subseteq> q"
     shows "ValidTC p (While b i v c) q"
 proof -
   {
     fix s n
     have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) s t \<and> t \<in> q)"
     proof (induction "n" arbitrary: s rule: less_induct)
       fix n :: nat
       fix s :: 'a
       assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b i v c) s t \<and> t \<in> q)"
       show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) s t \<and> t \<in> q)"
       proof (rule impI, cases "s \<in> b")
         assume 2: "s \<in> b" and "s \<in> i \<and> v s = n"
         hence "s \<in> i \<inter> b \<inter> {s . v s = n}"
           using assms(1) by auto
         hence "\<exists>t . Sem c s t \<and> t \<in> i \<inter> {s . v s < n}"
           by (metis assms(2) ValidTC_def)
         from this obtain t where 3: "Sem c s t \<and> t \<in> i \<inter> {s . v s < n}"
           by auto
         hence "\<exists>u . Sem (While b i v c) t u \<and> u \<in> q"
           using 1 by auto
         thus "\<exists>t . Sem (While b i v c) s t \<and> t \<in> q"
           using 2 3 Sem.intros(6) by force
       next
         assume "s \<notin> b" and "s \<in> i \<and> v s = n"
         thus "\<exists>t . Sem (While b i v c) s t \<and> t \<in> q"
           using Sem.intros(5) assms(3) by fastforce
       qed
     qed
   }
   thus ?thesis
     using assms(1) ValidTC_def by force
 qed
 
 
-subsection \<open>Concrete syntax\<close>
+subsubsection \<open>Concrete syntax\<close>
 
 setup \<open>
   Hoare_Syntax.setup
    {Basic = \<^const_syntax>\<open>Basic\<close>,
     Skip = \<^const_syntax>\<open>annskip\<close>,
     Seq = \<^const_syntax>\<open>Seq\<close>,
     Cond = \<^const_syntax>\<open>Cond\<close>,
     While = \<^const_syntax>\<open>While\<close>,
     Valid = \<^const_syntax>\<open>Valid\<close>,
     ValidTC = \<^const_syntax>\<open>ValidTC\<close>}
 \<close>
 
 
-subsection \<open>Proof methods: VCG\<close>
+subsubsection \<open>Proof methods: VCG\<close>
 
 declare BasicRule [Hoare_Tac.BasicRule]
   and SkipRule [Hoare_Tac.SkipRule]
   and SeqRule [Hoare_Tac.SeqRule]
   and CondRule [Hoare_Tac.CondRule]
   and WhileRule [Hoare_Tac.WhileRule]
 
 declare BasicRuleTC [Hoare_Tac.BasicRuleTC]
   and SkipRuleTC [Hoare_Tac.SkipRuleTC]
   and SeqRuleTC [Hoare_Tac.SeqRuleTC]
   and CondRuleTC [Hoare_Tac.CondRuleTC]
   and WhileRuleTC [Hoare_Tac.WhileRuleTC]
 
 method_setup vcg = \<open>
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\<close>
   "verification condition generator"
 
 method_setup vcg_simp = \<open>
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
   "verification condition generator plus simplification"
 
 method_setup vcg_tc = \<open>
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\<close>
   "verification condition generator"
 
 method_setup vcg_tc_simp = \<open>
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
   "verification condition generator plus simplification"
 
 end
diff --git a/src/HOL/Hoare/Hoare_Logic_Abort.thy b/src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy
@@ -1,236 +1,236 @@
 (*  Title:      HOL/Hoare/Hoare_Logic_Abort.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Copyright   2003 TUM
     Author:     Walter Guttmann (extension to total-correctness proofs)
 *)
 
 section \<open>Hoare Logic with an Abort statement for modelling run time errors\<close>
 
 theory Hoare_Logic_Abort
-imports Hoare_Syntax Hoare_Tac
+  imports Hoare_Syntax Hoare_Tac
 begin
 
 type_synonym 'a bexp = "'a set"
 type_synonym 'a assn = "'a set"
 type_synonym 'a var = "'a \<Rightarrow> nat"
 
 datatype 'a com =
   Basic "'a \<Rightarrow> 'a"
 | Abort
 | Seq "'a com" "'a com"
 | Cond "'a bexp" "'a com" "'a com"
 | While "'a bexp" "'a assn" "'a var" "'a com"
 
 abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
 type_synonym 'a sem = "'a option => 'a option => bool"
 
 inductive Sem :: "'a com \<Rightarrow> 'a sem"
 where
   "Sem (Basic f) None None"
 | "Sem (Basic f) (Some s) (Some (f s))"
 | "Sem Abort s None"
 | "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (Seq c1 c2) s s'"
 | "Sem (Cond b c1 c2) None None"
 | "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (Cond b c1 c2) (Some s) s'"
 | "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (Cond b c1 c2) (Some s) s'"
 | "Sem (While b x y c) None None"
 | "s \<notin> b \<Longrightarrow> Sem (While b x y c) (Some s) (Some s)"
 | "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b x y c) s'' s' \<Longrightarrow>
    Sem (While b x y c) (Some s) s'"
 
 inductive_cases [elim!]:
   "Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'"
   "Sem (Cond b c1 c2) s s'"
 
 lemma Sem_deterministic:
   assumes "Sem c s s1"
       and "Sem c s s2"
     shows "s1 = s2"
 proof -
   have "Sem c s s1 \<Longrightarrow> (\<forall>s2. Sem c s s2 \<longrightarrow> s1 = s2)"
     by (induct rule: Sem.induct) (subst Sem.simps, blast)+
   thus ?thesis
     using assms by simp
 qed
 
 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
   where "Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` p \<longrightarrow> s' \<in> Some ` q"
 
 definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
   where "ValidTC p c q \<equiv> \<forall>s . s \<in> p \<longrightarrow> (\<exists>t . Sem c (Some s) (Some t) \<and> t \<in> q)"
 
 lemma tc_implies_pc:
   "ValidTC p c q \<Longrightarrow> Valid p c q"
   by (smt Sem_deterministic ValidTC_def Valid_def image_iff)
 
 lemma tc_extract_function:
   "ValidTC p c q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
   by (meson ValidTC_def)
 
 text \<open>The proof rules for partial correctness\<close>
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
 by (auto simp:Valid_def)
 
 lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
 by (auto simp:Valid_def)
 
 lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (Seq c1 c2) R"
 by (auto simp:Valid_def)
 
 lemma CondRule:
  "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
   \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
 by (fastforce simp:Valid_def image_def)
 
 lemma While_aux:
   assumes "Sem (While b i v c) s s'"
   shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
     s \<in> Some ` I \<Longrightarrow> s' \<in> Some ` (I \<inter> -b)"
   using assms
   by (induct "While b i v c" s s') auto
 
 lemma WhileRule:
  "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i v c) q"
 apply (clarsimp simp:Valid_def)
 apply(drule While_aux)
   apply assumption
  apply blast
 apply blast
 done
 
 lemma AbortRule: "p \<subseteq> {s. False} \<Longrightarrow> Valid p Abort q"
 by(auto simp:Valid_def)
 
 text \<open>The proof rules for total correctness\<close>
 
 lemma SkipRuleTC:
   assumes "p \<subseteq> q"
     shows "ValidTC p (Basic id) q"
   by (metis Sem.intros(2) ValidTC_def assms id_def subsetD)
 
 lemma BasicRuleTC:
   assumes "p \<subseteq> {s. f s \<in> q}"
     shows "ValidTC p (Basic f) q"
   by (metis Ball_Collect Sem.intros(2) ValidTC_def assms)
 
 lemma SeqRuleTC:
   assumes "ValidTC p c1 q"
       and "ValidTC q c2 r"
     shows "ValidTC p (Seq c1 c2) r"
   by (meson assms Sem.intros(4) ValidTC_def)
 
 lemma CondRuleTC:
  assumes "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}"
      and "ValidTC w c1 q"
      and "ValidTC w' c2 q"
    shows "ValidTC p (Cond b c1 c2) q"
 proof (unfold ValidTC_def, rule allI)
   fix s
   show "s \<in> p \<longrightarrow> (\<exists>t . Sem (Cond b c1 c2) (Some s) (Some t) \<and> t \<in> q)"
     apply (cases "s \<in> b")
     apply (metis (mono_tags, lifting) Ball_Collect Sem.intros(6) ValidTC_def assms(1,2))
     by (metis (mono_tags, lifting) Ball_Collect Sem.intros(7) ValidTC_def assms(1,3))
 qed
 
 lemma WhileRuleTC:
   assumes "p \<subseteq> i"
       and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (i \<inter> {s . v s < n})"
       and "i \<inter> uminus b \<subseteq> q"
     shows "ValidTC p (While b i v c) q"
 proof -
   {
     fix s n
     have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q)"
     proof (induction "n" arbitrary: s rule: less_induct)
       fix n :: nat
       fix s :: 'a
       assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q)"
       show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q)"
       proof (rule impI, cases "s \<in> b")
         assume 2: "s \<in> b" and "s \<in> i \<and> v s = n"
         hence "s \<in> i \<inter> b \<inter> {s . v s = n}"
           using assms(1) by auto
         hence "\<exists>t . Sem c (Some s) (Some t) \<and> t \<in> i \<inter> {s . v s < n}"
           by (metis assms(2) ValidTC_def)
         from this obtain t where 3: "Sem c (Some s) (Some t) \<and> t \<in> i \<inter> {s . v s < n}"
           by auto
         hence "\<exists>u . Sem (While b i v c) (Some t) (Some u) \<and> u \<in> q"
           using 1 by auto
         thus "\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q"
           using 2 3 Sem.intros(10) by force
       next
         assume "s \<notin> b" and "s \<in> i \<and> v s = n"
         thus "\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q"
           using Sem.intros(9) assms(3) by fastforce
       qed
     qed
   }
   thus ?thesis
     using assms(1) ValidTC_def by force
 qed
 
 
 subsection \<open>Concrete syntax\<close>
 
 setup \<open>
   Hoare_Syntax.setup
    {Basic = \<^const_syntax>\<open>Basic\<close>,
     Skip = \<^const_syntax>\<open>annskip\<close>,
     Seq = \<^const_syntax>\<open>Seq\<close>,
     Cond = \<^const_syntax>\<open>Cond\<close>,
     While = \<^const_syntax>\<open>While\<close>,
     Valid = \<^const_syntax>\<open>Valid\<close>,
     ValidTC = \<^const_syntax>\<open>ValidTC\<close>}
 \<close>
 
 \<comment> \<open>Special syntax for guarded statements and guarded array updates:\<close>
 syntax
   "_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
   "_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70, 65] 61)
 translations
   "P \<rightarrow> c" \<rightleftharpoons> "IF P THEN c ELSE CONST Abort FI"
   "a[i] := v" \<rightharpoonup> "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
   \<comment> \<open>reverse translation not possible because of duplicate \<open>a\<close>\<close>
 
 text \<open>
   Note: there is no special syntax for guarded array access. Thus
   you must write \<open>j < length a \<rightarrow> a[i] := a!j\<close>.
 \<close>
 
 
 subsection \<open>Proof methods: VCG\<close>
 
 declare BasicRule [Hoare_Tac.BasicRule]
   and SkipRule [Hoare_Tac.SkipRule]
   and AbortRule [Hoare_Tac.AbortRule]
   and SeqRule [Hoare_Tac.SeqRule]
   and CondRule [Hoare_Tac.CondRule]
   and WhileRule [Hoare_Tac.WhileRule]
 
 declare BasicRuleTC [Hoare_Tac.BasicRuleTC]
   and SkipRuleTC [Hoare_Tac.SkipRuleTC]
   and SeqRuleTC [Hoare_Tac.SeqRuleTC]
   and CondRuleTC [Hoare_Tac.CondRuleTC]
   and WhileRuleTC [Hoare_Tac.WhileRuleTC]
 
 method_setup vcg = \<open>
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\<close>
   "verification condition generator"
 
 method_setup vcg_simp = \<open>
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
   "verification condition generator plus simplification"
 
 method_setup vcg_tc = \<open>
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\<close>
   "verification condition generator"
 
 method_setup vcg_tc_simp = \<open>
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
   "verification condition generator plus simplification"
 
 end
diff --git a/src/HOL/Hoare/Hoare_Syntax.thy b/src/HOL/Hoare/Hoare_Syntax.thy
--- a/src/HOL/Hoare/Hoare_Syntax.thy
+++ b/src/HOL/Hoare/Hoare_Syntax.thy
@@ -1,32 +1,32 @@
 (*  Title:      HOL/Hoare/Hoare_Syntax.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Author:     Walter Guttmann (extension to total-correctness proofs)
+*)
 
-Concrete syntax for Hoare logic, with translations for variables.
-*)
+section \<open>Concrete syntax for Hoare logic, with translations for variables\<close>
 
 theory Hoare_Syntax
   imports Main
 begin
 
 syntax
   "_assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'com"  ("(2_ :=/ _)" [70, 65] 61)
   "_Seq" :: "'com \<Rightarrow> 'com \<Rightarrow> 'com"  ("(_;/ _)" [61,60] 60)
   "_Cond" :: "'bexp \<Rightarrow> 'com \<Rightarrow> 'com \<Rightarrow> 'com"  ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
   "_While" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'var \<Rightarrow> 'com \<Rightarrow> 'com"  ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61)
 
 syntax
   "_While0" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'com \<Rightarrow> 'com"  ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
 translations
   "WHILE b INV {x} DO c OD" \<rightharpoonup> "WHILE b INV {x} VAR {0} DO c OD"
 
 syntax
  "_hoare_vars" :: "[idts, 'assn,'com, 'assn] \<Rightarrow> bool"  ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
  "_hoare_vars_tc" :: "[idts, 'assn, 'com, 'assn] \<Rightarrow> bool"  ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
 syntax (output)
  "_hoare" :: "['assn, 'com, 'assn] \<Rightarrow> bool"  ("{_} // _ // {_}" [0,55,0] 50)
  "_hoare_tc" :: "['assn, 'com, 'assn] \<Rightarrow> bool"  ("[_] // _ // [_]" [0,55,0] 50)
 
 ML_file \<open>hoare_syntax.ML\<close>
 
 end
diff --git a/src/HOL/Hoare/Hoare_Tac.thy b/src/HOL/Hoare/Hoare_Tac.thy
--- a/src/HOL/Hoare/Hoare_Tac.thy
+++ b/src/HOL/Hoare/Hoare_Tac.thy
@@ -1,35 +1,35 @@
 (*  Title:      HOL/Hoare/Hoare_Tac.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Author:     Walter Guttmann (extension to total-correctness proofs)
+*)
 
-Derivation of the proof rules and, most importantly, the VCG tactic.
-*)
+section \<open>Hoare logic VCG tactic\<close>
 
 theory Hoare_Tac
   imports Main
 begin
 
 context
 begin
 
 qualified named_theorems BasicRule
 qualified named_theorems SkipRule
 qualified named_theorems AbortRule
 qualified named_theorems SeqRule
 qualified named_theorems CondRule
 qualified named_theorems WhileRule
 
 qualified named_theorems BasicRuleTC
 qualified named_theorems SkipRuleTC
 qualified named_theorems SeqRuleTC
 qualified named_theorems CondRuleTC
 qualified named_theorems WhileRuleTC
 
 lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
   by blast
 
 ML_file \<open>hoare_tac.ML\<close>
 
 end
 
 end
diff --git a/src/HOL/Hoare/Pointer_Examples.thy b/src/HOL/Hoare/Pointer_Examples.thy
--- a/src/HOL/Hoare/Pointer_Examples.thy
+++ b/src/HOL/Hoare/Pointer_Examples.thy
@@ -1,501 +1,505 @@
 (*  Title:      HOL/Hoare/Pointer_Examples.thy
     Author:     Tobias Nipkow
     Copyright   2002 TUM
-
-Examples of verifications of pointer programs.
 *)
 
-theory Pointer_Examples imports HeapSyntax begin
+section \<open>Examples of verifications of pointer programs\<close>
+
+theory Pointer_Examples
+  imports HeapSyntax
+begin
 
 axiomatization where unproven: "PROP A"
 
-section "Verifications"
 
-subsection "List reversal"
+subsection "Verifications"
+
+subsubsection "List reversal"
 
 text "A short but unreadable proof:"
 
 lemma "VARS tl p q r
   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
   WHILE p \<noteq> Null
   INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
                  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 fastforce
   apply(fastforce intro:notin_List_update[THEN iffD2])
   \<comment> \<open>explicit:\<close>
   \<^cancel>\<open>apply clarify\<close>
   \<^cancel>\<open>apply(rename_tac ps b qs)\<close>
   \<^cancel>\<open>apply clarsimp\<close>
   \<^cancel>\<open>apply(rename_tac ps')\<close>
   \<^cancel>\<open>apply(fastforce intro:notin_List_update[THEN iffD2])\<close>
   done
 
 text\<open>And now with ghost variables \<^term>\<open>ps\<close> and \<^term>\<open>qs\<close>. Even
 ``more automatic''.\<close>
 
 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 fastforce
 done
 
 text "A longer readable version:"
 
 lemma "VARS tl p q r
   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
   WHILE p \<noteq> Null
   INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
                rev ps @ qs = rev Ps @ Qs}
   DO r := p; p := p^.tl; r^.tl := q; q := r OD
   {List tl q (rev Ps @ Qs)}"
 proof vcg
   fix tl p q r
   assume "List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}"
   thus "\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
                 rev ps @ qs = rev Ps @ Qs" by fastforce
 next
   fix tl p q r
   assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
                    rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> Null"
          (is "(\<exists>ps qs. ?I ps qs) \<and> _")
   then obtain ps qs a where I: "?I ps qs \<and> p = Ref a"
     by fast
   then obtain ps' where "ps = a # ps'" by fastforce
   hence "List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
          List (tl(p \<rightarrow> q)) p       (a#qs) \<and>
          set ps' \<inter> set (a#qs) = {} \<and>
          rev ps' @ (a#qs) = rev Ps @ Qs"
     using I by fastforce
   thus "\<exists>ps' qs'. List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
                   List (tl(p \<rightarrow> q)) p       qs' \<and>
                   set ps' \<inter> set qs' = {} \<and>
                   rev ps' @ qs' = rev Ps @ Qs" by fast
 next
   fix tl p q r
   assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
                    rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null"
   thus "List tl q (rev Ps @ Qs)" by fastforce
 qed
 
 
 text\<open>Finaly, the functional version. A bit more verbose, but automatic!\<close>
 
 lemma "VARS tl p q r
   {islist tl p \<and> islist tl q \<and>
    Ps = list tl p \<and> Qs = list tl q \<and> set Ps \<inter> set Qs = {}}
   WHILE p \<noteq> Null
   INV {islist tl p \<and> islist tl q \<and>
        set(list tl p) \<inter> set(list tl q) = {} \<and>
        rev(list tl p) @ (list tl q) = rev Ps @ Qs}
   DO r := p; p := p^.tl; r^.tl := q; q := r OD
   {islist tl q \<and> list tl q = rev Ps @ Qs}"
 apply vcg_simp
   apply clarsimp
  apply clarsimp
 done
 
 
-subsection "Searching in a list"
+subsubsection "Searching in a list"
 
 text\<open>What follows is a sequence of successively more intelligent proofs that
 a simple loop finds an element in a linked list.
 
 We start with a proof based on the \<^term>\<open>List\<close> predicate. This means it only
 works for acyclic lists.\<close>
 
 lemma "VARS tl p
   {List tl p Ps \<and> X \<in> set Ps}
   WHILE p \<noteq> Null \<and> p \<noteq> Ref X
   INV {\<exists>ps. List tl p ps \<and> X \<in> set ps}
   DO p := p^.tl OD
   {p = Ref X}"
 apply vcg_simp
   apply blast
  apply clarsimp
 apply clarsimp
 done
 
 text\<open>Using \<^term>\<open>Path\<close> instead of \<^term>\<open>List\<close> generalizes the correctness
 statement to cyclic lists as well:\<close>
 
 lemma "VARS tl p
   {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 = X}"
 apply vcg_simp
   apply blast
  apply fastforce
 apply clarsimp
 done
 
 text\<open>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>\<open>'a ref\<close>:\<close>
 
 lemma "VARS tl p
   {(p,X) \<in> {(Ref x,tl x) |x. True}\<^sup>*}
   WHILE p \<noteq> Null \<and> p \<noteq> X
   INV {(p,X) \<in> {(Ref x,tl x) |x. True}\<^sup>*}
   DO p := p^.tl OD
   {p = X}"
 apply vcg_simp
  apply clarsimp
  apply(erule converse_rtranclE)
   apply simp
  apply(clarsimp elim:converse_rtranclE)
 apply(fast elim:converse_rtranclE)
 done
 
 text\<open>Finally, a version based on a relation on type \<^typ>\<open>'a\<close>:\<close>
 
 lemma "VARS tl p
   {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}\<^sup>*}
   WHILE p \<noteq> Null \<and> p \<noteq> Ref X
   INV {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}\<^sup>*}
   DO p := p^.tl OD
   {p = Ref X}"
 apply vcg_simp
  apply clarsimp
  apply(erule converse_rtranclE)
   apply simp
  apply clarsimp
 apply clarsimp
 done
 
-subsection "Splicing two lists"
+
+subsubsection "Splicing two lists"
 
 lemma "VARS tl p q pp qq
   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and> size Qs \<le> size Ps}
   pp := p;
   WHILE q \<noteq> Null
   INV {\<exists>as bs qs.
     distinct as \<and> Path tl p as pp \<and> List tl pp bs \<and> List tl q qs \<and>
     set bs \<inter> set qs = {} \<and> set as \<inter> (set bs \<union> set qs) = {} \<and>
     size qs \<le> size bs \<and> splice Ps Qs = as @ splice bs qs}
   DO qq := q^.tl; q^.tl := pp^.tl; pp^.tl := q; pp := q^.tl; q := qq OD
   {List tl p (splice Ps Qs)}"
 apply vcg_simp
   apply(rule_tac x = "[]" in exI)
   apply fastforce
  apply clarsimp
  apply(rename_tac y bs qqs)
  apply(case_tac bs) apply simp
  apply clarsimp
  apply(rename_tac x bbs)
  apply(rule_tac x = "as @ [x,y]" in exI)
  apply simp
  apply(rule_tac x = "bbs" in exI)
  apply simp
  apply(rule_tac x = "qqs" in exI)
  apply simp
 apply (fastforce simp:List_app)
 done
 
 
-subsection "Merging two lists"
+subsubsection "Merging two lists"
 
 text"This is still a bit rough, especially the proof."
 
 definition cor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
   where "cor P Q \<longleftrightarrow> (if P then True else Q)"
 
 definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
   where "cand P Q \<longleftrightarrow> (if P then Q else False)"
 
 fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
 where
   "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
                                   else y # merge(x#xs,ys,f))"
 | "merge(x#xs,[],f) = x # merge(xs,[],f)"
 | "merge([],y#ys,f) = y # merge([],ys,f)"
 | "merge([],[],f) = []"
 
 text\<open>Simplifies the proof a little:\<close>
 
 lemma [simp]: "({} = insert a A \<inter> B) = (a \<notin> B & {} = A \<inter> B)"
 by blast
 lemma [simp]: "({} = A \<inter> insert b B) = (b \<notin> A & {} = A \<inter> B)"
 by blast
 lemma [simp]: "({} = A \<inter> (B \<union> C)) = ({} = A \<inter> B & {} = A \<inter> C)"
 by blast
 
 lemma "VARS hd tl p q r s
  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and>
   (p \<noteq> Null \<or> q \<noteq> Null)}
  IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
  THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
  s := r;
  WHILE p \<noteq> Null \<or> q \<noteq> Null
  INV {\<exists>rs ps qs a. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and>
       distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
       merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
       rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
       (tl a = p \<or> tl a = q)}
  DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
     THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
     s := s^.tl
  OD
  {List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
 apply vcg_simp
 apply (simp_all add: cand_def cor_def)
 
 apply (fastforce)
 
 apply clarsimp
 apply(rule conjI)
 apply clarsimp
 apply(rule conjI)
 apply (fastforce intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
 apply clarsimp
 apply(rule conjI)
 apply (clarsimp)
 apply(rule_tac x = "rs @ [a]" in exI)
 apply(clarsimp simp:eq_sym_conv)
 apply(rule_tac x = "bs" in exI)
 apply(clarsimp simp:eq_sym_conv)
 apply(rule_tac x = "ya#bsa" in exI)
 apply(simp)
 apply(clarsimp simp:eq_sym_conv)
 apply(rule_tac x = "rs @ [a]" in exI)
 apply(clarsimp simp:eq_sym_conv)
 apply(rule_tac x = "y#bs" in exI)
 apply(clarsimp simp:eq_sym_conv)
 apply(rule_tac x = "bsa" in exI)
 apply(simp)
 apply (fastforce intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
 
 apply(clarsimp simp add:List_app)
 done
 
 text\<open>And now with ghost variables:\<close>
 
 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 (fastforce)
 
 apply clarsimp
 apply(rule conjI)
 apply(clarsimp)
 apply(rule conjI)
 apply(clarsimp simp:neq_commute)
 apply(clarsimp simp:neq_commute)
 apply(clarsimp simp:neq_commute)
 
 apply(clarsimp simp add:List_app)
 done
 
 text\<open>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.\<close>
 
 text\<open>More of the previous proof without ghost variables can be
 automated, but the runtime goes up drastically. In general it is
 usually more efficient to give the witness directly than to have it
 found by proof.
 
 Now we try a functional version of the abstraction relation \<^term>\<open>Path\<close>. Since the result is not that convincing, we do not prove any of
 the lemmas.\<close>
 
 axiomatization
   ispath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" and
   path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
 
 text"First some basic lemmas:"
 
 lemma [simp]: "ispath f p p"
 by (rule unproven)
 lemma [simp]: "path f p p = []"
 by (rule unproven)
 lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow> ispath (f(a := r)) p q"
 by (rule unproven)
 lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow>
  path (f(a := r)) p q = path f p q"
 by (rule unproven)
 
 text"Some more specific lemmas needed by the example:"
 
 lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow> ispath (f(a := q)) p q"
 by (rule unproven)
 lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow>
  path (f(a := q)) p q = path (f(a := q)) p (Ref a) @ [a]"
 by (rule unproven)
 lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Ref b \<Longrightarrow>
  b \<notin> set (path f p (Ref a))"
 by (rule unproven)
 lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> islist f p"
 by (rule unproven)
 lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> list f p = path f p (Ref a) @ [a]"
 by (rule unproven)
 
 lemma [simp]: "islist f p \<Longrightarrow> distinct (list f p)"
 by (rule unproven)
 
 lemma "VARS hd tl p q r s
  {islist tl p \<and> Ps = list tl p \<and> islist tl q \<and> Qs = list tl q \<and>
   set Ps \<inter> set Qs = {} \<and>
   (p \<noteq> Null \<or> q \<noteq> Null)}
  IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
  THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
  s := r;
  WHILE p \<noteq> Null \<or> q \<noteq> Null
  INV {\<exists>rs ps qs a. ispath tl r s \<and> rs = path tl r s \<and>
       islist tl p \<and> ps = list tl p \<and> islist tl q \<and> qs = list tl q \<and>
       distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
       merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
       rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
       (tl a = p \<or> tl a = q)}
  DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
     THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
     s := s^.tl
  OD
  {islist tl r & list tl r = (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
 apply vcg_simp
 
 apply (simp_all add: cand_def cor_def)
   apply (fastforce)
  apply (fastforce simp: eq_sym_conv)
 apply(clarsimp)
 done
 
 text"The proof is automatic, but requires a numbet of special lemmas."
 
 
-subsection "Cyclic list reversal"
+subsubsection "Cyclic list reversal"
 
 
 text\<open>We consider two algorithms for the reversal of circular lists.
 \<close>
 
 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\<open>In the beginning, we are able to assert \<^term>\<open>distPath next
 root as root\<close>, with \<^term>\<open>as\<close> set to \<^term>\<open>[]\<close> or
 \<^term>\<open>[r,a,b,c]\<close>. Note that \<^term>\<open>Path next root as root\<close> would
 additionally give us an infinite number of lists with the recurring
 sequence \<^term>\<open>[r,a,b,c]\<close>.
 
 The precondition states that there exists a non-empty non-repeating
 path \mbox{\<^term>\<open>r # Ps\<close>} from pointer \<^term>\<open>root\<close> to itself, given that
 \<^term>\<open>root\<close> points to location \<^term>\<open>r\<close>. Pointers \<^term>\<open>p\<close> and
 \<^term>\<open>q\<close> are then set to \<^term>\<open>root\<close> and the successor of \<^term>\<open>root\<close> respectively. If \<^term>\<open>q = root\<close>, we have circled the loop,
 otherwise we set the \<^term>\<open>next\<close> pointer field of \<^term>\<open>q\<close> to point
 to \<^term>\<open>p\<close>, and shift \<^term>\<open>p\<close> and \<^term>\<open>q\<close> one step forward. The
 invariant thus states that \<^term>\<open>p\<close> and \<^term>\<open>q\<close> point to two
 disjoint lists \<^term>\<open>ps\<close> and \<^term>\<open>qs\<close>, such that \<^term>\<open>Ps = rev ps
 @ qs\<close>. After the loop terminates, one
 extra step is needed to close the loop. As expected, the postcondition
 states that the \<^term>\<open>distPath\<close> from \<^term>\<open>root\<close> to itself is now
 \<^term>\<open>r # (rev Ps)\<close>.
 
 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:\<close>
 
 
 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 (case_tac "(q = Null)")
   apply (fastforce 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"
+subsubsection "Storage allocation"
 
 definition new :: "'a set \<Rightarrow> 'a"
   where "new A = (SOME a. a \<notin> A)"
 
 
 lemma new_notin:
  "\<lbrakk> ~finite(UNIV::'a set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow> new (A) \<notin> B"
 apply(unfold new_def)
 apply(rule someI2_ex)
  apply (fast intro:ex_new_if_finite)
 apply (fast)
 done
 
 
 lemma "~finite(UNIV::'a set) \<Longrightarrow>
   VARS xs elem next alloc p q
   {Xs = xs \<and> p = (Null::'a ref)}
   WHILE xs \<noteq> []
   INV {islist next p \<and> set(list next p) \<subseteq> set alloc \<and>
        map elem (rev(list next p)) @ xs = Xs}
   DO q := Ref(new(set alloc)); alloc := (addr q)#alloc;
      q^.next := p; q^.elem := hd xs; xs := tl xs; p := q
   OD
   {islist next p \<and> map elem (rev(list next p)) = Xs}"
 apply vcg_simp
  apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
 done
 
 
 end
diff --git a/src/HOL/Hoare/Pointer_ExamplesAbort.thy b/src/HOL/Hoare/Pointer_ExamplesAbort.thy
--- a/src/HOL/Hoare/Pointer_ExamplesAbort.thy
+++ b/src/HOL/Hoare/Pointer_ExamplesAbort.thy
@@ -1,28 +1,30 @@
 (*  Title:      HOL/Hoare/Pointer_ExamplesAbort.thy
     Author:     Tobias Nipkow
     Copyright   2002 TUM
-
-Examples of verifications of pointer programs
 *)
 
-theory Pointer_ExamplesAbort imports HeapSyntaxAbort begin
+section \<open>Examples of verifications of pointer programs\<close>
 
-section "Verifications"
+theory Pointer_ExamplesAbort
+  imports HeapSyntaxAbort
+begin
 
-subsection "List reversal"
+subsection "Verifications"
+
+subsubsection "List reversal"
 
 text "Interestingly, this proof is the same as for the unguarded program:"
 
 lemma "VARS tl p q r
   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
   WHILE p \<noteq> Null
   INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
                  rev ps @ qs = rev Ps @ Qs}
   DO r := p; (p \<noteq> Null \<rightarrow> p := p^.tl); r^.tl := q; q := r OD
   {List tl q (rev Ps @ Qs)}"
 apply vcg_simp
   apply fastforce
  apply(fastforce intro:notin_List_update[THEN iffD2])
 done
 
 end
diff --git a/src/HOL/Hoare/Pointers0.thy b/src/HOL/Hoare/Pointers0.thy
--- a/src/HOL/Hoare/Pointers0.thy
+++ b/src/HOL/Hoare/Pointers0.thy
@@ -1,431 +1,434 @@
 (*  Title:      HOL/Hoare/Pointers0.thy
     Author:     Tobias Nipkow
     Copyright   2002 TUM
 
 This is like Pointers.thy, but instead of a type constructor 'a ref
 that adjoins Null to a type, Null is simply a distinguished element of
 the address type. This avoids the Ref constructor and thus simplifies
 specifications (a bit). However, the proofs don't seem to get simpler
 - in fact in some case they appear to get (a bit) more complicated.
 *)
 
-theory Pointers0 imports Hoare_Logic begin
+section \<open>Alternative pointers\<close>
+
+theory Pointers0
+  imports Hoare_Logic
+begin
 
 subsection "References"
 
 class ref =
   fixes Null :: 'a
 
 subsection "Field access and update"
 
 syntax
   "_fassign"  :: "'a::ref => id => 'v => 's com"
    ("(2_^._ :=/ _)" [70,1000,65] 61)
   "_faccess"  :: "'a::ref => ('a::ref \<Rightarrow> 'v) => 'v"
    ("_^._" [65,1000] 65)
 translations
   "p^.f := e"  =>  "f := CONST fun_upd f p e"
   "p^.f"       =>  "f p"
 
 
 text "An example due to Suzuki:"
 
 lemma "VARS v n
   {distinct[w,x,y,z]}
   w^.v := (1::int); w^.n := x;
   x^.v := 2; x^.n := y;
   y^.v := 3; y^.n := z;
   z^.v := 4; x^.n := z
   {w^.n^.n^.v = 4}"
 by vcg_simp
 
 
-section "The heap"
+subsection "The heap"
 
-subsection "Paths in the heap"
+subsubsection "Paths in the heap"
 
 primrec Path :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
 where
   "Path h x [] y = (x = y)"
 | "Path h x (a#as) y = (x \<noteq> Null \<and> x = a \<and> Path h (h a) as y)"
 
 lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
 apply(case_tac xs)
 apply fastforce
 apply fastforce
 done
 
 lemma [simp]: "a \<noteq> Null \<Longrightarrow> Path h a as z =
  (as = [] \<and> z = a  \<or>  (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))"
 apply(case_tac as)
 apply fastforce
 apply fastforce
 done
 
 lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
 by(induct as, simp+)
 
 lemma [simp]: "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
 by(induct as, simp, simp add:eq_sym_conv)
 
-subsection "Lists on the heap"
+subsubsection "Lists on the heap"
 
-subsubsection "Relational abstraction"
+paragraph "Relational abstraction"
 
 definition List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool"
   where "List h x as = Path h x as Null"
 
 lemma [simp]: "List h x [] = (x = Null)"
 by(simp add:List_def)
 
 lemma [simp]: "List h x (a#as) = (x \<noteq> Null \<and> x = a \<and> List h (h a) as)"
 by(simp add:List_def)
 
 lemma [simp]: "List h Null as = (as = [])"
 by(case_tac as, simp_all)
 
 lemma List_Ref[simp]:
  "a \<noteq> Null \<Longrightarrow> List h a as = (\<exists>bs. as = a#bs \<and> List h (h a) bs)"
 by(case_tac as, simp_all, fast)
 
 theorem notin_List_update[simp]:
  "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
 apply(induct as)
 apply simp
 apply(clarsimp simp add:fun_upd_apply)
 done
 
 
 declare fun_upd_apply[simp del]fun_upd_same[simp] fun_upd_other[simp]
 
 lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
 by(induct as, simp, clarsimp)
 
 lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
 by(blast intro:List_unique)
 
 lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
 by(induct as, simp, clarsimp)
 
 lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as"
 apply (clarsimp simp add:in_set_conv_decomp)
 apply(frule List_app[THEN iffD1])
 apply(fastforce dest: List_unique)
 done
 
 lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
 apply(induct as, simp)
 apply(fastforce dest:List_hd_not_in_tl)
 done
 
-subsection "Functional abstraction"
+subsubsection "Functional abstraction"
 
 definition islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool"
   where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
 
 definition list :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list"
   where "list h p = (SOME as. List h p as)"
 
 lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
 apply(simp add:islist_def list_def)
 apply(rule iffI)
 apply(rule conjI)
 apply blast
 apply(subst some1_equality)
   apply(erule List_unique1)
  apply assumption
 apply(rule refl)
 apply simp
 apply(rule someI_ex)
 apply fast
 done
 
 lemma [simp]: "islist h Null"
 by(simp add:islist_def)
 
 lemma [simp]: "a \<noteq> Null \<Longrightarrow> islist h a = islist h (h a)"
 by(simp add:islist_def)
 
 lemma [simp]: "list h Null = []"
 by(simp add:list_def)
 
 lemma list_Ref_conv[simp]:
  "\<lbrakk> a \<noteq> Null; islist h (h a) \<rbrakk> \<Longrightarrow> list h a = a # list h (h a)"
 apply(insert List_Ref[of _ h])
 apply(fastforce simp:List_conv_islist_list)
 done
 
 lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))"
 apply(insert List_hd_not_in_tl[of h])
 apply(simp add:List_conv_islist_list)
 done
 
 lemma list_upd_conv[simp]:
  "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> list (h(y := q)) p = list h p"
 apply(drule notin_List_update[of _ _ h q p])
 apply(simp add:List_conv_islist_list)
 done
 
 lemma islist_upd[simp]:
  "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> islist (h(y := q)) p"
 apply(frule notin_List_update[of _ _ h q p])
 apply(simp add:List_conv_islist_list)
 done
 
 
-section "Verifications"
+subsection "Verifications"
 
-subsection "List reversal"
+subsubsection "List reversal"
 
 text "A short but unreadable proof:"
 
 lemma "VARS tl p q r
   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
   WHILE p \<noteq> Null
   INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
                  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 fastforce
   apply(fastforce intro:notin_List_update[THEN iffD2])
   \<comment> \<open>explicit:\<close>
   \<^cancel>\<open>apply clarify\<close>
   \<^cancel>\<open>apply(rename_tac ps qs)\<close>
   \<^cancel>\<open>apply clarsimp\<close>
   \<^cancel>\<open>apply(rename_tac ps')\<close>
   \<^cancel>\<open>apply(rule_tac x = ps' in exI)\<close>
   \<^cancel>\<open>apply simp\<close>
   \<^cancel>\<open>apply(rule_tac x = "p#qs" in exI)\<close>
   \<^cancel>\<open>apply simp\<close>
   done
 
 
 text "A longer readable version:"
 
 lemma "VARS tl p q r
   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
   WHILE p \<noteq> Null
   INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
                rev ps @ qs = rev Ps @ Qs}
   DO r := p; p := p^.tl; r^.tl := q; q := r OD
   {List tl q (rev Ps @ Qs)}"
 proof vcg
   fix tl p q r
   assume "List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}"
   thus "\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
                 rev ps @ qs = rev Ps @ Qs" by fastforce
 next
   fix tl p q r
   assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
                    rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> Null"
          (is "(\<exists>ps qs. ?I ps qs) \<and> _")
   then obtain ps qs where I: "?I ps qs \<and> p \<noteq> Null" by fast
   then obtain ps' where "ps = p # ps'" by fastforce
   hence "List (tl(p := q)) (p^.tl) ps' \<and>
          List (tl(p := q)) p       (p#qs) \<and>
          set ps' \<inter> set (p#qs) = {} \<and>
          rev ps' @ (p#qs) = rev Ps @ Qs"
     using I by fastforce
   thus "\<exists>ps' qs'. List (tl(p := q)) (p^.tl) ps' \<and>
                   List (tl(p := q)) p       qs' \<and>
                   set ps' \<inter> set qs' = {} \<and>
                   rev ps' @ qs' = rev Ps @ Qs" by fast
 next
   fix tl p q r
   assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
                    rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null"
   thus "List tl q (rev Ps @ Qs)" by fastforce
 qed
 
 
 text\<open>Finaly, the functional version. A bit more verbose, but automatic!\<close>
 
 lemma "VARS tl p q r
   {islist tl p \<and> islist tl q \<and>
    Ps = list tl p \<and> Qs = list tl q \<and> set Ps \<inter> set Qs = {}}
   WHILE p \<noteq> Null
   INV {islist tl p \<and> islist tl q \<and>
        set(list tl p) \<inter> set(list tl q) = {} \<and>
        rev(list tl p) @ (list tl q) = rev Ps @ Qs}
   DO r := p; p := p^.tl; r^.tl := q; q := r OD
   {islist tl q \<and> list tl q = rev Ps @ Qs}"
 apply vcg_simp
   apply clarsimp
  apply clarsimp
 done
 
 
-subsection "Searching in a list"
+subsubsection "Searching in a list"
 
 text\<open>What follows is a sequence of successively more intelligent proofs that
 a simple loop finds an element in a linked list.
 
 We start with a proof based on the \<^term>\<open>List\<close> predicate. This means it only
 works for acyclic lists.\<close>
 
 lemma "VARS tl p
   {List tl p Ps \<and> X \<in> set Ps}
   WHILE p \<noteq> Null \<and> p \<noteq> X
   INV {p \<noteq> Null \<and> (\<exists>ps. List tl p ps \<and> X \<in> set ps)}
   DO p := p^.tl OD
   {p = X}"
 apply vcg_simp
   apply(case_tac "p = Null")
    apply clarsimp
   apply fastforce
  apply clarsimp
  apply fastforce
 apply clarsimp
 done
 
 text\<open>Using \<^term>\<open>Path\<close> instead of \<^term>\<open>List\<close> generalizes the correctness
 statement to cyclic lists as well:\<close>
 
 lemma "VARS tl p
   {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 = X}"
 apply vcg_simp
   apply blast
  apply fastforce
 apply clarsimp
 done
 
 text\<open>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.\<close>
 
 lemma "VARS tl p
   {(p,X) \<in> {(x,y). y = tl x & x \<noteq> Null}\<^sup>*}
   WHILE p \<noteq> Null \<and> p \<noteq> X
   INV {(p,X) \<in> {(x,y). y = tl x & x \<noteq> Null}\<^sup>*}
   DO p := p^.tl OD
   {p = X}"
 apply vcg_simp
  apply clarsimp
  apply(erule converse_rtranclE)
   apply simp
  apply(simp)
 apply(fastforce elim:converse_rtranclE)
 done
 
 
-subsection "Merging two lists"
+subsubsection "Merging two lists"
 
 text"This is still a bit rough, especially the proof."
 
 fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" where
 "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
                                 else y # merge(x#xs,ys,f))" |
 "merge(x#xs,[],f) = x # merge(xs,[],f)" |
 "merge([],y#ys,f) = y # merge([],ys,f)" |
 "merge([],[],f) = []"
 
 lemma imp_disjCL: "(P|Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (~P \<longrightarrow> Q \<longrightarrow> R))"
 by blast
 
 declare disj_not1[simp del] imp_disjL[simp del] imp_disjCL[simp]
 
 lemma "VARS hd tl p q r s
  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and>
   (p \<noteq> Null \<or> q \<noteq> Null)}
  IF if q = Null then True else p ~= Null & p^.hd \<le> q^.hd
  THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
  s := r;
  WHILE p \<noteq> Null \<or> q \<noteq> Null
  INV {\<exists>rs ps qs. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and>
       distinct(s # ps @ qs @ rs) \<and> s \<noteq> Null \<and>
       merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
       rs @ s # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
       (tl s = p \<or> tl s = q)}
  DO IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd
     THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
     s := s^.tl
  OD
  {List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
 apply vcg_simp
 
 apply (fastforce)
 
 apply clarsimp
 apply(rule conjI)
 apply clarsimp
 apply(simp add:eq_sym_conv)
 apply(rule_tac x = "rs @ [s]" in exI)
 apply simp
 apply(rule_tac x = "bs" in exI)
 apply (fastforce simp:eq_sym_conv)
 
 apply clarsimp
 apply(rule conjI)
 apply clarsimp
 apply(rule_tac x = "rs @ [s]" in exI)
 apply simp
 apply(rule_tac x = "bsa" in exI)
 apply(rule conjI)
 apply (simp add:eq_sym_conv)
 apply(rule exI)
 apply(rule conjI)
 apply(rule_tac x = bs in exI)
 apply(rule conjI)
 apply(rule refl)
 apply (simp add:eq_sym_conv)
 apply (simp add:eq_sym_conv)
 
 apply(rule conjI)
 apply clarsimp
 apply(rule_tac x = "rs @ [s]" in exI)
 apply simp
 apply(rule_tac x = bs in exI)
 apply (simp add:eq_sym_conv)
 apply clarsimp
 apply(rule_tac x = "rs @ [s]" in exI)
 apply (simp add:eq_sym_conv)
 apply(rule exI)
 apply(rule conjI)
 apply(rule_tac x = bsa in exI)
 apply(rule conjI)
 apply(rule refl)
 apply (simp add:eq_sym_conv)
 apply(rule_tac x = bs in exI)
 apply (simp add:eq_sym_conv)
 
 apply(clarsimp simp add:List_app)
 done
 
 (* TODO: merging with islist/list instead of List: an improvement?
    needs (is)path, which is not so easy to prove either. *)
 
-subsection "Storage allocation"
+subsubsection "Storage allocation"
 
 definition new :: "'a set \<Rightarrow> 'a::ref"
   where "new A = (SOME a. a \<notin> A & a \<noteq> Null)"
 
 
 lemma new_notin:
  "\<lbrakk> ~finite(UNIV::('a::ref)set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow>
   new (A) \<notin> B & new A \<noteq> Null"
 apply(unfold new_def)
 apply(rule someI2_ex)
  apply (fast dest:ex_new_if_finite[of "insert Null A"])
 apply (fast)
 done
 
 lemma "~finite(UNIV::('a::ref)set) \<Longrightarrow>
   VARS xs elem next alloc p q
   {Xs = xs \<and> p = (Null::'a)}
   WHILE xs \<noteq> []
   INV {islist next p \<and> set(list next p) \<subseteq> set alloc \<and>
        map elem (rev(list next p)) @ xs = Xs}
   DO q := new(set alloc); alloc := q#alloc;
      q^.next := p; q^.elem := hd xs; xs := tl xs; p := q
   OD
   {islist next p \<and> map elem (rev(list next p)) = Xs}"
 apply vcg_simp
  apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
 done
 
-
 end
diff --git a/src/HOL/Hoare/SchorrWaite.thy b/src/HOL/Hoare/SchorrWaite.thy
--- a/src/HOL/Hoare/SchorrWaite.thy
+++ b/src/HOL/Hoare/SchorrWaite.thy
@@ -1,576 +1,575 @@
 (*  Title:      HOL/Hoare/SchorrWaite.thy
     Author:     Farhad Mehta
     Copyright   2003 TUM
-
-Proof of the Schorr-Waite graph marking algorithm.
 *)
 
+section \<open>Proof of the Schorr-Waite graph marking algorithm\<close>
 
-theory SchorrWaite imports HeapSyntax begin
+theory SchorrWaite
+  imports HeapSyntax
+begin
 
-section \<open>Machinery for the Schorr-Waite proof\<close>
+subsection \<open>Machinery for the Schorr-Waite proof\<close>
 
 definition
   \<comment> \<open>Relations induced by a mapping\<close>
   rel :: "('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<times> 'a) set"
   where "rel m = {(x,y). m x = Ref y}"
 
 definition
   relS :: "('a \<Rightarrow> 'a ref) set \<Rightarrow> ('a \<times> 'a) set"
   where "relS M = (\<Union>m \<in> M. rel m)"
 
 definition
   addrs :: "'a ref set \<Rightarrow> 'a set"
   where "addrs P = {a. Ref a \<in> P}"
 
 definition
   reachable :: "('a \<times> 'a) set \<Rightarrow> 'a ref set \<Rightarrow> 'a set"
   where "reachable r P = (r\<^sup>* `` addrs P)"
 
 lemmas rel_defs = relS_def rel_def
 
 text \<open>Rewrite rules for relations induced by a mapping\<close>
 
 lemma self_reachable: "b \<in> B \<Longrightarrow> b \<in> R\<^sup>* `` B"
 apply blast
 done
 
 lemma oneStep_reachable: "b \<in> R``B \<Longrightarrow> b \<in> R\<^sup>* `` B"
 apply blast
 done
 
 lemma still_reachable: "\<lbrakk>B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Rb\<^sup>* `` B \<subseteq> Ra\<^sup>* `` A "
 apply (clarsimp simp only:Image_iff)
 apply (erule rtrancl_induct)
  apply blast
 apply (subgoal_tac "(y, z) \<in> Ra\<union>(Rb-Ra)")
  apply (erule UnE)
  apply (auto intro:rtrancl_into_rtrancl)
 apply blast
 done
 
 lemma still_reachable_eq: "\<lbrakk> A\<subseteq>Rb\<^sup>*``B; B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Ra-Rb. y \<in>(Rb\<^sup>*``B); \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Ra\<^sup>*``A =  Rb\<^sup>*``B "
 apply (rule equalityI)
  apply (erule still_reachable ,assumption)+
 done
 
 lemma reachable_null: "reachable mS {Null} = {}"
 apply (simp add: reachable_def addrs_def)
 done
 
 lemma reachable_empty: "reachable mS {} = {}"
 apply (simp add: reachable_def addrs_def)
 done
 
 lemma reachable_union: "(reachable mS aS \<union> reachable mS bS) = reachable mS (aS \<union> bS)"
 apply (simp add: reachable_def rel_defs addrs_def)
 apply blast
 done
 
 lemma reachable_union_sym: "reachable r (insert a aS) = (r\<^sup>* `` addrs {a}) \<union> reachable r aS"
 apply (simp add: reachable_def rel_defs addrs_def)
 apply blast
 done
 
 lemma rel_upd1: "(a,b) \<notin> rel (r(q:=t)) \<Longrightarrow> (a,b) \<in> rel r \<Longrightarrow> a=q"
 apply (rule classical)
 apply (simp add:rel_defs fun_upd_apply)
 done
 
 lemma rel_upd2: "(a,b)  \<notin> rel r \<Longrightarrow> (a,b) \<in> rel (r(q:=t)) \<Longrightarrow> a=q"
 apply (rule classical)
 apply (simp add:rel_defs fun_upd_apply)
 done
 
 definition
   \<comment> \<open>Restriction of a relation\<close>
   restr ::"('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set"       ("(_/ | _)" [50, 51] 50)
   where "restr r m = {(x,y). (x,y) \<in> r \<and> \<not> m x}"
 
 text \<open>Rewrite rules for the restriction of a relation\<close>
 
 lemma restr_identity[simp]:
  " (\<forall>x. \<not> m x) \<Longrightarrow> (R |m) = R"
 by (auto simp add:restr_def)
 
 lemma restr_rtrancl[simp]: " \<lbrakk>m l\<rbrakk> \<Longrightarrow> (R | m)\<^sup>* `` {l} = {l}"
 by (auto simp add:restr_def elim:converse_rtranclE)
 
 lemma [simp]: " \<lbrakk>m l\<rbrakk> \<Longrightarrow> (l,x) \<in> (R | m)\<^sup>* = (l=x)"
 by (auto simp add:restr_def elim:converse_rtranclE)
 
 lemma restr_upd: "((rel (r (q := t)))|(m(q := True))) = ((rel (r))|(m(q := True))) "
 apply (auto simp:restr_def rel_def fun_upd_apply)
 apply (rename_tac a b)
 apply (case_tac "a=q")
  apply auto
 done
 
 lemma restr_un: "((r \<union> s)|m) = (r|m) \<union> (s|m)"
   by (auto simp add:restr_def)
 
 lemma rel_upd3: "(a, b) \<notin> (r|(m(q := t))) \<Longrightarrow> (a,b) \<in> (r|m) \<Longrightarrow> a = q "
 apply (rule classical)
 apply (simp add:restr_def fun_upd_apply)
 done
 
 definition
   \<comment> \<open>A short form for the stack mapping function for List\<close>
   S :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref)"
   where "S c l r = (\<lambda>x. if c x then r x else l x)"
 
 text \<open>Rewrite rules for Lists using S as their mapping\<close>
 
 lemma [rule_format,simp]:
  "\<forall>p. a \<notin> set stack \<longrightarrow> List (S c l r) p stack = List (S (c(a:=x)) (l(a:=y)) (r(a:=z))) p stack"
 apply(induct_tac stack)
  apply(simp add:fun_upd_apply S_def)+
 done
 
 lemma [rule_format,simp]:
  "\<forall>p. a \<notin> set stack \<longrightarrow> List (S c l (r(a:=z))) p stack = List (S c l r) p stack"
 apply(induct_tac stack)
  apply(simp add:fun_upd_apply S_def)+
 done
 
 lemma [rule_format,simp]:
  "\<forall>p. a \<notin> set stack \<longrightarrow> List (S c (l(a:=z)) r) p stack = List (S c l r) p stack"
 apply(induct_tac stack)
  apply(simp add:fun_upd_apply S_def)+
 done
 
 lemma [rule_format,simp]:
  "\<forall>p. a \<notin> set stack \<longrightarrow> List (S (c(a:=z)) l r) p stack = List (S c l r) p stack"
 apply(induct_tac stack)
  apply(simp add:fun_upd_apply S_def)+
 done
 
 primrec
   \<comment> \<open>Recursive definition of what is means for a the graph/stack structure to be reconstructible\<close>
   stkOk :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow>'a list \<Rightarrow>  bool"
 where
   stkOk_nil:  "stkOk c l r iL iR t [] = True"
 | stkOk_cons:
     "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and> 
       iL p = (if c p then l p else t) \<and>
       iR p = (if c p then t else r p))"
 
 text \<open>Rewrite rules for stkOk\<close>
 
 lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
   stkOk (c(x := f)) l r iL iR t xs = stkOk c l r iL iR t xs"
 apply (induct xs)
  apply (auto simp:eq_sym_conv)
 done
 
 lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
  stkOk c (l(x := g)) r iL iR t xs = stkOk c l r iL iR t xs"
 apply (induct xs)
  apply (auto simp:eq_sym_conv)
 done
 
 lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
  stkOk c l (r(x := g)) iL iR t xs = stkOk c l r iL iR t xs"
 apply (induct xs)
  apply (auto simp:eq_sym_conv)
 done
 
 lemma stkOk_r_rewrite [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
   stkOk c l (r(x := g)) iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
 apply (induct xs)
  apply (auto simp:eq_sym_conv)
 done
 
 lemma [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
  stkOk c (l(x := g)) r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
 apply (induct xs)
  apply (auto simp:eq_sym_conv)
 done
 
 lemma [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
  stkOk (c(x := g)) l r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
 apply (induct xs)
  apply (auto simp:eq_sym_conv)
 done
 
 
-section\<open>The Schorr-Waite algorithm\<close>
-
+subsection \<open>The Schorr-Waite algorithm\<close>
 
 theorem SchorrWaiteAlgorithm: 
 "VARS c m l r t p q root
  {R = reachable (relS {l, r}) {root} \<and> (\<forall>x. \<not> m x) \<and> iR = r \<and> iL = l} 
  t := root; p := Null;
  WHILE p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m
  INV {\<exists>stack.
           List (S c l r) p stack \<and>                                      \<comment> \<open>\<open>i1\<close>\<close>
           (\<forall>x \<in> set stack. m x) \<and>                                       \<comment> \<open>\<open>i2\<close>\<close>
           R = reachable (relS{l, r}) {t,p} \<and>                            \<comment> \<open>\<open>i3\<close>\<close>
           (\<forall>x. x \<in> R \<and> \<not>m x \<longrightarrow>                                         \<comment> \<open>\<open>i4\<close>\<close>
                  x \<in> reachable (relS{l,r}|m) ({t}\<union>set(map r stack))) \<and>
           (\<forall>x. m x \<longrightarrow> x \<in> R) \<and>                                         \<comment> \<open>\<open>i5\<close>\<close>
           (\<forall>x. x \<notin> set stack \<longrightarrow> r x = iR x \<and> l x = iL x) \<and>             \<comment> \<open>\<open>i6\<close>\<close>
           (stkOk c l r iL iR t stack)                                   \<comment> \<open>\<open>i7\<close>\<close>}
  DO IF t = Null \<or> t^.m
       THEN IF p^.c
                THEN q := t; t := p; p := p^.r; t^.r := q                \<comment> \<open>\<open>pop\<close>\<close>
                ELSE q := t; t := p^.r; p^.r := p^.l;                    \<comment> \<open>\<open>swing\<close>\<close>
                         p^.l := q; p^.c := True          FI    
       ELSE q := p; p := t; t := t^.l; p^.l := q;                        \<comment> \<open>\<open>push\<close>\<close>
                p^.m := True; p^.c := False            FI       OD
  {(\<forall>x. (x \<in> R) = m x) \<and> (r = iR \<and> l = iL) }"
   (is "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}")
 proof (vcg)
   let "While {(c, m, l, r, t, p, q, root). ?whileB m t p}
     {(c, m, l, r, t, p, q, root). ?inv c m l r t p} _ ?body" = ?c3
   {
 
     fix c m l r t p q root
     assume "?Pre c m l r root"
     thus "?inv c m l r root Null"  by (auto simp add: reachable_def addrs_def)
   next
 
     fix c m l r t p q
     let "\<exists>stack. ?Inv stack"  =  "?inv c m l r t p"
     assume a: "?inv c m l r t p \<and> \<not>(p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m)"  
     then obtain stack where inv: "?Inv stack" by blast
     from a have pNull: "p = Null" and tDisj: "t=Null \<or> (t\<noteq>Null \<and> t^.m )" by auto
     let "?I1 \<and> _ \<and> _ \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> _"  =  "?Inv stack"
     from inv have i1: "?I1" and i4: "?I4" and i5: "?I5" and i6: "?I6" by simp+
     from pNull i1 have stackEmpty: "stack = []" by simp
     from tDisj i4 have RisMarked[rule_format]: "\<forall>x.  x \<in> R \<longrightarrow> m x"  by(auto simp: reachable_def addrs_def stackEmpty)
     from i5 i6 show "(\<forall>x.(x \<in> R) = m x) \<and> r = iR \<and> l = iL"  by(auto simp: stackEmpty fun_eq_iff intro:RisMarked)
 
   next   
       fix c m l r t p q root
       let "\<exists>stack. ?Inv stack"  =  "?inv c m l r t p"
       let "\<exists>stack. ?popInv stack"  =  "?inv c m l (r(p \<rightarrow> t)) p (p^.r)"
       let "\<exists>stack. ?swInv stack"  =
         "?inv (c(p \<rightarrow> True)) m (l(p \<rightarrow> t)) (r(p \<rightarrow> p^.l)) (p^.r) p"
       let "\<exists>stack. ?puInv stack"  =
         "?inv (c(t \<rightarrow> False)) (m(t \<rightarrow> True)) (l(t \<rightarrow> p)) r (t^.l) t"
       let "?ifB1"  =  "(t = Null \<or> t^.m)"
       let "?ifB2"  =  "p^.c" 
 
       assume "(\<exists>stack.?Inv stack) \<and> (p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m)" (is "_ \<and> ?whileB")
       then obtain stack where inv: "?Inv stack" and whileB: "?whileB" by blast
       let "?I1 \<and> ?I2 \<and> ?I3 \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> ?I7" = "?Inv stack"
       from inv have i1: "?I1" and i2: "?I2" and i3: "?I3" and i4: "?I4"
                   and i5: "?I5" and i6: "?I6" and i7: "?I7" by simp+        
       have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
 
       show "(?ifB1 \<longrightarrow> (?ifB2 \<longrightarrow> (\<exists>stack.?popInv stack)) \<and> 
                             (\<not>?ifB2 \<longrightarrow> (\<exists>stack.?swInv stack)) ) \<and>
               (\<not>?ifB1 \<longrightarrow> (\<exists>stack.?puInv stack))"
       proof - 
         {
           assume ifB1: "t = Null \<or> t^.m" and ifB2: "p^.c"
           from ifB1 whileB have pNotNull: "p \<noteq> Null" by auto
           then obtain addr_p where addr_p_eq: "p = Ref addr_p" by auto
           with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl"
             by auto
           with i2 have m_addr_p: "p^.m" by auto
           have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
           from stack_eq stackDist have p_notin_stack_tl: "addr p \<notin> set stack_tl" by simp
           let "?poI1\<and> ?poI2\<and> ?poI3\<and> ?poI4\<and> ?poI5\<and> ?poI6\<and> ?poI7" = "?popInv stack_tl"
           have "?popInv stack_tl"
           proof -
 
             \<comment> \<open>List property is maintained:\<close>
             from i1 p_notin_stack_tl ifB2
             have poI1: "List (S c l (r(p \<rightarrow> t))) (p^.r) stack_tl" 
               by(simp add: addr_p_eq stack_eq, simp add: S_def)
 
             moreover
             \<comment> \<open>Everything on the stack is marked:\<close>
             from i2 have poI2: "\<forall> x \<in> set stack_tl. m x" by (simp add:stack_eq)
             moreover
 
             \<comment> \<open>Everything is still reachable:\<close>
             let "(R = reachable ?Ra ?A)" = "?I3"
             let "?Rb" = "(relS {l, r(p \<rightarrow> t)})"
             let "?B" = "{p, p^.r}"
             \<comment> \<open>Our goal is \<open>R = reachable ?Rb ?B\<close>.\<close>
             have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" (is "?L = ?R")
             proof
               show "?L \<subseteq> ?R"
               proof (rule still_reachable)
                 show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" by(fastforce simp:addrs_def relS_def rel_def addr_p_eq 
                      intro:oneStep_reachable Image_iff[THEN iffD2])
                 show "\<forall>(x,y) \<in> ?Ra-?Rb. y \<in> (?Rb\<^sup>* `` addrs ?B)" by (clarsimp simp:relS_def) 
                      (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
               qed
               show "?R \<subseteq> ?L"
               proof (rule still_reachable)
                 show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
                   by(fastforce simp:addrs_def rel_defs addr_p_eq 
                       intro:oneStep_reachable Image_iff[THEN iffD2])
               next
                 show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
                   by (clarsimp simp:relS_def) 
                      (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd2)
               qed
             qed
             with i3 have poI3: "R = reachable ?Rb ?B"  by (simp add:reachable_def) 
             moreover
 
             \<comment> \<open>If it is reachable and not marked, it is still reachable using...\<close>
             let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A"  =  ?I4        
             let "?Rb" = "relS {l, r(p \<rightarrow> t)} | m"
             let "?B" = "{p} \<union> set (map (r(p \<rightarrow> t)) stack_tl)"
             \<comment> \<open>Our goal is \<open>\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B\<close>.\<close>
             let ?T = "{t, p^.r}"
 
             have "?Ra\<^sup>* `` addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
             proof (rule still_reachable)
               have rewrite: "\<forall>s\<in>set stack_tl. (r(p \<rightarrow> t)) s = r s"
                 by (auto simp add:p_notin_stack_tl intro:fun_upd_other) 
               show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
                 by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
               show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
                 by (clarsimp simp:restr_def relS_def) 
                   (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
             qed
             \<comment> \<open>We now bring a term from the right to the left of the subset relation.\<close>
             hence subset: "?Ra\<^sup>* `` addrs ?A - ?Rb\<^sup>* `` addrs ?T \<subseteq> ?Rb\<^sup>* `` addrs ?B"
               by blast
             have poI4: "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B"
             proof (rule allI, rule impI)
               fix x
               assume a: "x \<in> R \<and> \<not> m x"
               \<comment> \<open>First, a disjunction on \<^term>\<open>p^.r\<close> used later in the proof\<close>
               have pDisj:"p^.r = Null \<or> (p^.r \<noteq> Null \<and> p^.r^.m)" using poI1 poI2 
                 by auto
               \<comment> \<open>\<^term>\<open>x\<close> belongs to the left hand side of @{thm[source] subset}:\<close>
               have incl: "x \<in> ?Ra\<^sup>*``addrs ?A" using  a i4 by (simp only:reachable_def, clarsimp)
               have excl: "x \<notin> ?Rb\<^sup>*`` addrs ?T" using pDisj ifB1 a by (auto simp add:addrs_def)
               \<comment> \<open>And therefore also belongs to the right hand side of @{thm[source]subset},\<close>
               \<comment> \<open>which corresponds to our goal.\<close>
               from incl excl subset  show "x \<in> reachable ?Rb ?B" by (auto simp add:reachable_def)
             qed
             moreover
 
             \<comment> \<open>If it is marked, then it is reachable\<close>
             from i5 have poI5: "\<forall>x. m x \<longrightarrow> x \<in> R" .
             moreover
 
             \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close>
             from i7 i6 ifB2 
             have poI6: "\<forall>x. x \<notin> set stack_tl \<longrightarrow> (r(p \<rightarrow> t)) x = iR x \<and> l x = iL x" 
               by(auto simp: addr_p_eq stack_eq fun_upd_apply)
 
             moreover
 
             \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close>
             from p_notin_stack_tl i7 have poI7: "stkOk c l (r(p \<rightarrow> t)) iL iR p stack_tl"
               by (clarsimp simp:stack_eq addr_p_eq)
 
             ultimately show "?popInv stack_tl" by simp
           qed
           hence "\<exists>stack. ?popInv stack" ..
         }
         moreover
 
         \<comment> \<open>Proofs of the Swing and Push arm follow.\<close>
         \<comment> \<open>Since they are in principle simmilar to the Pop arm proof,\<close>
         \<comment> \<open>we show fewer comments and use frequent pattern matching.\<close>
         {
           \<comment> \<open>Swing arm\<close>
           assume ifB1: "?ifB1" and nifB2: "\<not>?ifB2"
           from ifB1 whileB have pNotNull: "p \<noteq> Null" by clarsimp
           then obtain addr_p where addr_p_eq: "p = Ref addr_p" by clarsimp
           with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl" by clarsimp
           with i2 have m_addr_p: "p^.m" by clarsimp
           from stack_eq stackDist have p_notin_stack_tl: "(addr p) \<notin> set stack_tl"
             by simp
           let "?swI1\<and>?swI2\<and>?swI3\<and>?swI4\<and>?swI5\<and>?swI6\<and>?swI7" = "?swInv stack"
           have "?swInv stack"
           proof -
             
             \<comment> \<open>List property is maintained:\<close>
             from i1 p_notin_stack_tl nifB2
             have swI1: "?swI1"
               by (simp add:addr_p_eq stack_eq, simp add:S_def)
             moreover
             
             \<comment> \<open>Everything on the stack is marked:\<close>
             from i2
             have swI2: "?swI2" .
             moreover
             
             \<comment> \<open>Everything is still reachable:\<close>
             let "R = reachable ?Ra ?A" = "?I3"
             let "R = reachable ?Rb ?B" = "?swI3"
             have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
             proof (rule still_reachable_eq)
               show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
                 by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
             next
               show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
                 by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
             next
               show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
                 by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
             next
               show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
                 by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
             qed
             with i3
             have swI3: "?swI3" by (simp add:reachable_def) 
             moreover
 
             \<comment> \<open>If it is reachable and not marked, it is still reachable using...\<close>
             let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
             let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?swI4
             let ?T = "{t}"
             have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
             proof (rule still_reachable)
               have rewrite: "(\<forall>s\<in>set stack_tl. (r(addr p := l(addr p))) s = r s)"
                 by (auto simp add:p_notin_stack_tl intro:fun_upd_other)
               show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
                 by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
             next
               show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
                 by (clarsimp simp:relS_def restr_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
             qed
             then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
               by blast
             have ?swI4
             proof (rule allI, rule impI)
               fix x
               assume a: "x \<in> R \<and>\<not> m x"
               with i4 addr_p_eq stack_eq  have inc: "x \<in> ?Ra\<^sup>*``addrs ?A" 
                 by (simp only:reachable_def, clarsimp)
               with ifB1 a 
               have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T" 
                 by (auto simp add:addrs_def)
               from inc exc subset  show "x \<in> reachable ?Rb ?B" 
                 by (auto simp add:reachable_def)
             qed
             moreover
             
             \<comment> \<open>If it is marked, then it is reachable\<close>
             from i5
             have "?swI5" .
             moreover
 
             \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close>
             from i6 stack_eq
             have "?swI6"
               by clarsimp           
             moreover
 
             \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close>
             from stackDist i7 nifB2 
             have "?swI7"
               by (clarsimp simp:addr_p_eq stack_eq)
 
             ultimately show ?thesis by auto
           qed
           then have "\<exists>stack. ?swInv stack" by blast
         }
         moreover
 
         {
           \<comment> \<open>Push arm\<close>
           assume nifB1: "\<not>?ifB1"
           from nifB1 whileB have tNotNull: "t \<noteq> Null" by clarsimp
           then obtain addr_t where addr_t_eq: "t = Ref addr_t" by clarsimp
           with i1 obtain new_stack where new_stack_eq: "new_stack = (addr t) # stack" by clarsimp
           from tNotNull nifB1 have n_m_addr_t: "\<not> (t^.m)" by clarsimp
           with i2 have t_notin_stack: "(addr t) \<notin> set stack" by blast
           let "?puI1\<and>?puI2\<and>?puI3\<and>?puI4\<and>?puI5\<and>?puI6\<and>?puI7" = "?puInv new_stack"
           have "?puInv new_stack"
           proof -
             
             \<comment> \<open>List property is maintained:\<close>
             from i1 t_notin_stack
             have puI1: "?puI1"
               by (simp add:addr_t_eq new_stack_eq, simp add:S_def)
             moreover
             
             \<comment> \<open>Everything on the stack is marked:\<close>
             from i2
             have puI2: "?puI2" 
               by (simp add:new_stack_eq fun_upd_apply)
             moreover
             
             \<comment> \<open>Everything is still reachable:\<close>
             let "R = reachable ?Ra ?A" = "?I3"
             let "R = reachable ?Rb ?B" = "?puI3"
             have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
             proof (rule still_reachable_eq)
               show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
                 by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
             next
               show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
                 by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
             next
               show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
                 by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
             next
               show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
                 by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
             qed
             with i3
             have puI3: "?puI3" by (simp add:reachable_def) 
             moreover
             
             \<comment> \<open>If it is reachable and not marked, it is still reachable using...\<close>
             let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
             let "\<forall>x. x \<in> R \<and> \<not> ?new_m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?puI4
             let ?T = "{t}"
             have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
             proof (rule still_reachable)
               show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
                 by (fastforce simp:new_stack_eq addrs_def intro:self_reachable)
             next
               show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
                 by (clarsimp simp:relS_def new_stack_eq restr_un restr_upd) 
                    (fastforce simp add:rel_def Image_iff restr_def addrs_def fun_upd_apply addr_t_eq dest:rel_upd3)
             qed
             then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
               by blast
             have ?puI4
             proof (rule allI, rule impI)
               fix x
               assume a: "x \<in> R \<and> \<not> ?new_m x"
               have xDisj: "x=(addr t) \<or> x\<noteq>(addr t)" by simp
               with i4 a have inc: "x \<in> ?Ra\<^sup>*``addrs ?A"
                 by (fastforce simp:addr_t_eq addrs_def reachable_def intro:self_reachable)
               have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T"
                 using xDisj a n_m_addr_t
                 by (clarsimp simp add:addrs_def addr_t_eq) 
               from inc exc subset  show "x \<in> reachable ?Rb ?B" 
                 by (auto simp add:reachable_def)
             qed  
             moreover
             
             \<comment> \<open>If it is marked, then it is reachable\<close>
             from i5
             have "?puI5"
               by (auto simp:addrs_def i3 reachable_def addr_t_eq fun_upd_apply intro:self_reachable)
             moreover
             
             \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close>
             from i6 
             have "?puI6"
               by (simp add:new_stack_eq)
             moreover
 
             \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close>
             from stackDist i6 t_notin_stack i7
             have "?puI7" by (clarsimp simp:addr_t_eq new_stack_eq)
 
             ultimately show ?thesis by auto
           qed
           then have "\<exists>stack. ?puInv stack" by blast
 
         }
         ultimately show ?thesis by blast
       qed
     }
   qed
 
 end
-
diff --git a/src/HOL/Hoare/SepLogHeap.thy b/src/HOL/Hoare/SepLogHeap.thy
--- a/src/HOL/Hoare/SepLogHeap.thy
+++ b/src/HOL/Hoare/SepLogHeap.thy
@@ -1,93 +1,95 @@
 (*  Title:      HOL/Hoare/SepLogHeap.thy
     Author:     Tobias Nipkow
     Copyright   2002 TUM
-
-Heap abstractions (at the moment only Path and List)
-for Separation Logic.
 *)
 
+section \<open>Heap abstractions for Separation Logic\<close>
+
+text \<open>(at the moment only Path and List)\<close>
+
 theory SepLogHeap
-imports Main
+  imports Main
 begin
 
 type_synonym heap = "(nat \<Rightarrow> nat option)"
 
 text\<open>\<open>Some\<close> means allocated, \<open>None\<close> means
 free. Address \<open>0\<close> serves as the null reference.\<close>
 
+
 subsection "Paths in the heap"
 
 primrec Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
 where
   "Path h x [] y = (x = y)"
 | "Path h x (a#as) y = (x\<noteq>0 \<and> a=x \<and> (\<exists>b. h x = Some b \<and> Path h b as y))"
 
 lemma [iff]: "Path h 0 xs y = (xs = [] \<and> y = 0)"
 by (cases xs) simp_all
 
 lemma [simp]: "x\<noteq>0 \<Longrightarrow> Path h x as z =
  (as = [] \<and> z = x  \<or>  (\<exists>y bs. as = x#bs \<and> h x = Some y & Path h y bs z))"
 by (cases as) auto
 
 lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
 by (induct as) auto
 
 lemma Path_upd[simp]:
  "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
 by (induct as) simp_all
 
 
 subsection "Lists on the heap"
 
 definition List :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
   where "List h x as = Path h x as 0"
 
 lemma [simp]: "List h x [] = (x = 0)"
 by (simp add: List_def)
 
 lemma [simp]:
  "List h x (a#as) = (x\<noteq>0 \<and> a=x \<and> (\<exists>y. h x = Some y \<and> List h y as))"
 by (simp add: List_def)
 
 lemma [simp]: "List h 0 as = (as = [])"
 by (cases as) simp_all
 
 lemma List_non_null: "a\<noteq>0 \<Longrightarrow>
  List h a as = (\<exists>b bs. as = a#bs \<and> h a = Some b \<and> List h b bs)"
 by (cases as) simp_all
 
 theorem notin_List_update[simp]:
  "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
 by (induct as) simp_all
 
 lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
 by (induct as) (auto simp add:List_non_null)
 
 lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
 by (blast intro: List_unique)
 
 lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
 by (induct as) auto
 
 lemma List_hd_not_in_tl[simp]: "List h b as \<Longrightarrow> h a = Some b \<Longrightarrow> a \<notin> set as"
 apply (clarsimp simp add:in_set_conv_decomp)
 apply(frule List_app[THEN iffD1])
 apply(fastforce dest: List_unique)
 done
 
 lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
 by (induct as) (auto dest:List_hd_not_in_tl)
 
 lemma list_in_heap: "\<And>p. List h p ps \<Longrightarrow> set ps \<subseteq> dom h"
 by (induct ps) auto
 
 lemma list_ortho_sum1[simp]:
  "\<And>p. \<lbrakk> List h1 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
 by (induct ps) (auto simp add:map_add_def split:option.split)
 
 
 lemma list_ortho_sum2[simp]:
  "\<And>p. \<lbrakk> List h2 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
 by (induct ps) (auto simp add:map_add_def split:option.split)
 
 end
diff --git a/src/HOL/Hoare/Separation.thy b/src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy
+++ b/src/HOL/Hoare/Separation.thy
@@ -1,216 +1,219 @@
 (*  Title:      HOL/Hoare/Separation.thy
     Author:     Tobias Nipkow
     Copyright   2003 TUM
 
 A first attempt at a nice syntactic embedding of separation logic.
 Already builds on the theory for list abstractions.
 
 If we suppress the H parameter for "List", we have to hardwired this
 into parser and pretty printer, which is not very modular.
 Alternative: some syntax like <P> which stands for P H. No more
 compact, but avoids the funny H.
-
 *)
 
-theory Separation imports Hoare_Logic_Abort SepLogHeap begin
+section \<open>Separation logic\<close>
+
+theory Separation
+  imports Hoare_Logic_Abort SepLogHeap
+begin
 
 text\<open>The semantic definition of a few connectives:\<close>
 
 definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55)
   where "h1 \<bottom> h2 \<longleftrightarrow> dom h1 \<inter> dom h2 = {}"
 
 definition is_empty :: "heap \<Rightarrow> bool"
   where "is_empty h \<longleftrightarrow> h = Map.empty"
 
 definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
   where "singl h x y \<longleftrightarrow> dom h = {x} & h x = Some y"
 
 definition star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
   where "star P Q = (\<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2)"
 
 definition wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
   where "wand P Q = (\<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h'))"
 
 text\<open>This is what assertions look like without any syntactic sugar:\<close>
 
 lemma "VARS x y z w h
  {star (%h. singl h x y) (%h. singl h z w) h}
  SKIP
  {x \<noteq> z}"
 apply vcg
 apply(auto simp:star_def ortho_def singl_def)
 done
 
 text\<open>Now we add nice input syntax.  To suppress the heap parameter
 of the connectives, we assume it is always called H and add/remove it
 upon parsing/printing. Thus every pointer program needs to have a
 program variable H, and assertions should not contain any locally
 bound Hs - otherwise they may bind the implicit H.\<close>
 
 syntax
  "_emp" :: "bool" ("emp")
  "_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]")
  "_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
  "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60)
 
 (* FIXME does not handle "_idtdummy" *)
 ML \<open>
 \<comment> \<open>\<open>free_tr\<close> takes care of free vars in the scope of separation logic connectives:
     they are implicitly applied to the heap\<close>
 fun free_tr(t as Free _) = t $ Syntax.free "H"
 \<^cancel>\<open>| free_tr((list as Free("List",_))$ p $ ps) = list $ Syntax.free "H" $ p $ ps\<close>
   | free_tr t = t
 
 fun emp_tr [] = Syntax.const \<^const_syntax>\<open>is_empty\<close> $ Syntax.free "H"
   | emp_tr ts = raise TERM ("emp_tr", ts);
 fun singl_tr [p, q] = Syntax.const \<^const_syntax>\<open>singl\<close> $ Syntax.free "H" $ p $ q
   | singl_tr ts = raise TERM ("singl_tr", ts);
 fun star_tr [P,Q] = Syntax.const \<^const_syntax>\<open>star\<close> $
       absfree ("H", dummyT) (free_tr P) $ absfree ("H", dummyT) (free_tr Q) $
       Syntax.free "H"
   | star_tr ts = raise TERM ("star_tr", ts);
 fun wand_tr [P, Q] = Syntax.const \<^const_syntax>\<open>wand\<close> $
       absfree ("H", dummyT) P $ absfree ("H", dummyT) Q $ Syntax.free "H"
   | wand_tr ts = raise TERM ("wand_tr", ts);
 \<close>
 
 parse_translation \<open>
  [(\<^syntax_const>\<open>_emp\<close>, K emp_tr),
   (\<^syntax_const>\<open>_singl\<close>, K singl_tr),
   (\<^syntax_const>\<open>_star\<close>, K star_tr),
   (\<^syntax_const>\<open>_wand\<close>, K wand_tr)]
 \<close>
 
 text\<open>Now it looks much better:\<close>
 
 lemma "VARS H x y z w
  {[x\<mapsto>y] ** [z\<mapsto>w]}
  SKIP
  {x \<noteq> z}"
 apply vcg
 apply(auto simp:star_def ortho_def singl_def)
 done
 
 lemma "VARS H x y z w
  {emp ** emp}
  SKIP
  {emp}"
 apply vcg
 apply(auto simp:star_def ortho_def is_empty_def)
 done
 
 text\<open>But the output is still unreadable. Thus we also strip the heap
 parameters upon output:\<close>
 
 ML \<open>
 local
 
 fun strip (Abs(_,_,(t as Const("_free",_) $ Free _) $ Bound 0)) = t
   | strip (Abs(_,_,(t as Free _) $ Bound 0)) = t
 \<^cancel>\<open>| strip (Abs(_,_,((list as Const("List",_))$ Bound 0 $ p $ ps))) = list$p$ps\<close>
   | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t
   | strip (Abs(_,_,P)) = P
   | strip (Const(\<^const_syntax>\<open>is_empty\<close>,_)) = Syntax.const \<^syntax_const>\<open>_emp\<close>
   | strip t = t;
 
 in
 
 fun is_empty_tr' [_] = Syntax.const \<^syntax_const>\<open>_emp\<close>
 fun singl_tr' [_,p,q] = Syntax.const \<^syntax_const>\<open>_singl\<close> $ p $ q
 fun star_tr' [P,Q,_] = Syntax.const \<^syntax_const>\<open>_star\<close> $ strip P $ strip Q
 fun wand_tr' [P,Q,_] = Syntax.const \<^syntax_const>\<open>_wand\<close> $ strip P $ strip Q
 
 end
 \<close>
 
 print_translation \<open>
  [(\<^const_syntax>\<open>is_empty\<close>, K is_empty_tr'),
   (\<^const_syntax>\<open>singl\<close>, K singl_tr'),
   (\<^const_syntax>\<open>star\<close>, K star_tr'),
   (\<^const_syntax>\<open>wand\<close>, K wand_tr')]
 \<close>
 
 text\<open>Now the intermediate proof states are also readable:\<close>
 
 lemma "VARS H x y z w
  {[x\<mapsto>y] ** [z\<mapsto>w]}
  y := w
  {x \<noteq> z}"
 apply vcg
 apply(auto simp:star_def ortho_def singl_def)
 done
 
 lemma "VARS H x y z w
  {emp ** emp}
  SKIP
  {emp}"
 apply vcg
 apply(auto simp:star_def ortho_def is_empty_def)
 done
 
 text\<open>So far we have unfolded the separation logic connectives in
 proofs. Here comes a simple example of a program proof that uses a law
 of separation logic instead.\<close>
 
 \<comment> \<open>a law of separation logic\<close>
 lemma star_comm: "P ** Q = Q ** P"
   by(auto simp add:star_def ortho_def dest: map_add_comm)
 
 lemma "VARS H x y z w
  {P ** Q}
  SKIP
  {Q ** P}"
 apply vcg
 apply(simp add: star_comm)
 done
 
 
 lemma "VARS H
  {p\<noteq>0 \<and> [p \<mapsto> x] ** List H q qs}
  H := H(p \<mapsto> q)
  {List H p (p#qs)}"
 apply vcg
 apply(simp add: star_def ortho_def singl_def)
 apply clarify
 apply(subgoal_tac "p \<notin> set qs")
  prefer 2
  apply(blast dest:list_in_heap)
 apply simp
 done
 
 lemma "VARS H p q r
   {List H p Ps ** List H q Qs}
   WHILE p \<noteq> 0
   INV {\<exists>ps qs. (List H p ps ** List H q qs) \<and> rev ps @ qs = rev Ps @ Qs}
   DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD
   {List H q (rev Ps @ Qs)}"
 apply vcg
 apply(simp_all add: star_def ortho_def singl_def)
 
 apply fastforce
 
 apply (clarsimp simp add:List_non_null)
 apply(rename_tac ps')
 apply(rule_tac x = ps' in exI)
 apply(rule_tac x = "p#qs" in exI)
 apply simp
 apply(rule_tac x = "h1(p:=None)" in exI)
 apply(rule_tac x = "h2(p\<mapsto>q)" in exI)
 apply simp
 apply(rule conjI)
  apply(rule ext)
  apply(simp add:map_add_def split:option.split)
 apply(rule conjI)
  apply blast
 apply(simp add:map_add_def split:option.split)
 apply(rule conjI)
 apply(subgoal_tac "p \<notin> set qs")
  prefer 2
  apply(blast dest:list_in_heap)
 apply(simp)
 apply fast
 
 apply(fastforce)
 done
 
 end
diff --git a/src/HOL/Hoare/document/root.tex b/src/HOL/Hoare/document/root.tex
--- a/src/HOL/Hoare/document/root.tex
+++ b/src/HOL/Hoare/document/root.tex
@@ -1,37 +1,46 @@
-\documentclass[11pt,a4paper]{report}
+\documentclass[11pt,a4paper]{article}
 \usepackage{graphicx}
 \usepackage[english]{babel}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}
 \isabellestyle{it}
 
 \begin{document}
 
 \title{Hoare Logic}
-\author{Various}
+\author{
+  Norbert Galm \\
+  Walter Guttmann \\
+  Farhad Mehta \\
+  Tobias Nipkow \\
+  Leonor Prensa Nieto}
 \maketitle
 
 \begin{abstract}
 These theories contain a Hoare logic for a simple imperative
 programming language with while-loops, including a verification
 condition generator.
 
 Special infrastructure for modelling and reasoning about pointer
 programs is provided, together with many examples, including Schorr-Waite.
 See \cite{MehtaN-CADE03,MehtaN-IC05} for an excellent exposition.
 \end{abstract}
 
 \pagestyle{plain}
 \thispagestyle{empty}
 \tableofcontents
 
-\newpage
+\begin{center}
+  \includegraphics[scale=0.5]{session_graph}
+\end{center}
+
+\clearpage
 
 \input{session}
 
 \bibliographystyle{plain}
 \bibliography{root}
 
 \end{document}