# HG changeset patch
# User nipkow
# Date 1036657604 -3600
# Node ID d041e5ce52d76872d8597a0f433944c00812c604
# Parent  d7ef5a3b359159e9b01228da8250734fdfa5c792
small improvements

diff -r d7ef5a3b3591 -r d041e5ce52d7 src/HOL/Hoare/Pointers.thy
--- a/src/HOL/Hoare/Pointers.thy	Thu Nov 07 09:08:25 2002 +0100
+++ b/src/HOL/Hoare/Pointers.thy	Thu Nov 07 09:26:44 2002 +0100
@@ -126,9 +126,11 @@
 
 subsection"List reversal"
 
-lemma "|- VARS tl p q r. 
+text{* A tactic script: *}
+
+lemma "|- VARS tl p q r.
   {list tl p As \<and> list tl q Bs \<and> set As \<inter> set Bs = {}}
-  WHILE p ~= None
+  WHILE p \<noteq> None
   INV {\<exists>As' Bs'. list tl p As' \<and> list tl q Bs' \<and> set As' \<inter> set Bs' = {} \<and>
                  rev As' @ Bs' = rev As @ Bs}
   DO r := p; p := p^:tl; r^.tl := q; q := r OD
@@ -138,9 +140,6 @@
 apply(rule_tac x = As in exI)
 apply simp
 
-prefer 2
-apply clarsimp
-
 apply clarify
 apply(rename_tac As' b Bs')
 apply clarsimp
@@ -149,8 +148,41 @@
 apply simp
 apply(rule_tac x = "b#Bs'" in exI)
 apply simp
+
+apply clarsimp
 done
 
+text{*A readable(?) proof: *}
+
+lemma "|- VARS tl p q r.
+  {list tl p As \<and> list tl q Bs \<and> set As \<inter> set Bs = {}}
+  WHILE p \<noteq> None
+  INV {\<exists>As' Bs'. list tl p As' \<and> list tl q Bs' \<and> set As' \<inter> set Bs' = {} \<and>
+                 rev As' @ Bs' = rev As @ Bs}
+  DO r := p; p := p^:tl; r^.tl := q; q := r OD
+  {list tl q (rev As @ Bs)}"
+ (is "Valid {(tl,p,q,r).?P tl p q r}
+            (While _ {(tl,p,q,r). \<exists>As' Bs'. ?I tl p q r As' Bs'} _)
+            {(tl,p,q,r).?Q tl p q r}")
+proof vcg
+  fix tl p q r
+  assume "?P tl p q r"
+  hence "?I tl p q r As Bs" by simp
+  thus "\<exists>As' Bs'. ?I tl p q r As' Bs'" by rules
+next
+  fix tl p q r
+  assume "(\<exists>As' Bs'. ?I tl p q r As' Bs') \<and> p \<noteq> None"
+  then obtain As' Bs' a where I: "?I tl p q r As' Bs'" "p = Some a" by fast
+  then obtain As'' where "As' = a # As''" by fastsimp
+  hence "?I (tl(the p := q)) (p^:tl) p p As'' (a#Bs')" using I by fastsimp
+  thus "\<exists>As' Bs'. ?I (tl(the p := q)) (p^:tl) p p As' Bs'" by rules
+next
+  fix tl p q r
+  assume "(\<exists>As' Bs'. ?I tl p q r As' Bs') \<and> \<not> p \<noteq> None"
+  thus "?Q tl p q r" by clarsimp
+qed
+
+
 subsection{*Searching in a list*}
 
 text{*What follows is a sequence of successively more intelligent proofs that
@@ -262,7 +294,7 @@
 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> None \<or> q \<noteq> None)}
- IF q = None \<or> p \<noteq> None \<and> p^:hd \<le> q^:hd
+ IF if q = None then True else p \<noteq> None \<and> p^:hd \<le> q^:hd
  THEN r := p; p := p^:tl ELSE r := q; q := q^:tl FI;
  s := r;
  WHILE p \<noteq> None \<or> q \<noteq> None
@@ -271,60 +303,49 @@
       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 q = None \<or> p \<noteq> None \<and> p^:hd \<le> q^:hd
+ DO IF if q = None then True else p \<noteq> None \<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 (fastsimp)
+
 apply clarsimp
 apply(rule conjI)
 apply clarsimp
-apply(rule exI, rule conjI, rule disjI1, rule refl)
-apply (fastsimp)
-apply(rule conjI)
-apply clarsimp
-apply(rule exI, rule conjI, rule disjI1, rule refl)
-apply clarsimp
-apply(rule exI)
-apply(rule conjI)
-apply assumption
-apply(rule exI)
-apply(rule conjI)
-apply(rule exI)
-apply(rule conjI)
-apply(rule refl)
-apply assumption
-apply (fastsimp)
-apply(case_tac p)
-apply clarsimp
-apply(rule exI, rule conjI, rule disjI1, rule refl)
-apply (fastsimp)
-apply clarsimp
-apply(rule exI, rule conjI, rule disjI1, rule refl)
-apply(rule exI)
-apply(rule conjI)
-apply(rule exI)
-apply(rule conjI)
-apply(rule refl)
-apply assumption
-apply (fastsimp)
+apply(simp add:eq_sym_conv)
+apply(rule_tac x = "rs @ [a]" in exI)
+apply simp
+apply(rule_tac x = "bs" in exI)
+apply (fastsimp simp:eq_sym_conv)
 
 apply clarsimp
 apply(rule conjI)
 apply clarsimp
 apply(rule_tac x = "rs @ [a]" in exI)
 apply simp
-apply(rule_tac x = "bs" in exI)
-apply (fastsimp simp:eq_sym_conv)
+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 (fast)
 
 apply(rule conjI)
 apply clarsimp
 apply(rule_tac x = "rs @ [a]" in exI)
 apply simp
-apply(rule_tac x = "bs" in exI)
-apply(rule conjI)
+apply(rule_tac x = bs in exI)
+apply (simp add:eq_sym_conv)
+apply clarsimp
+apply(rule_tac x = "rs @ [a]" in exI)
 apply (simp add:eq_sym_conv)
 apply(rule exI)
 apply(rule conjI)
@@ -332,25 +353,9 @@
 apply(rule conjI)
 apply(rule refl)
 apply (simp add:eq_sym_conv)
-apply (fastsimp simp:eq_sym_conv)
-apply(case_tac p)
-apply clarsimp
-apply(rule_tac x = "rs @ [a]" in exI)
-apply simp
-apply(rule_tac x = "bs" in exI)
-apply (fastsimp simp:eq_sym_conv)
-
-apply clarsimp
-apply(rule_tac x = "rs @ [a]" in exI)
-apply simp
-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(rule_tac x = bsa in exI)
-apply (fastsimp simp:eq_sym_conv)
+apply fast
 
 apply(clarsimp simp add:list_app)
 done