# HG changeset patch
# User nipkow
# Date 910026173 -3600
# Node ID 7d4ac02677a6546fa1e61c3f980a15f6c417a626
# Parent  e3a98a7c0634dcd838bc3dd56f99abc08f819182
New example

diff -r e3a98a7c0634 -r 7d4ac02677a6 src/HOL/IMP/Natural.ML
--- a/src/HOL/IMP/Natural.ML	Mon Nov 02 15:31:29 1998 +0100
+++ b/src/HOL/IMP/Natural.ML	Mon Nov 02 18:02:53 1998 +0100
@@ -23,3 +23,25 @@
 (*blast_tac needs Unify.search_bound, trace_bound := 40*)
 by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case])));
 qed_spec_mp "com_det";
+
+(** An example due to Tony Hoare **)
+
+Goal "[| !x. P x --> Q x; <w,s> -c-> t |] ==> \
+\ !c. w = While P c --> <While Q c,t> -c-> u --> <While Q c,s> -c-> u";
+be evalc.induct 1;
+by(Auto_tac);
+val lemma1 = result() RS spec RS mp RS mp;
+
+Goal "[| !x. P x --> Q x; <w,s> -c-> u |] ==> \
+\ !c. w = While Q c --> <While P c; While Q c,s> -c-> u";
+be evalc.induct 1;
+by(ALLGOALS Asm_simp_tac);
+by(Blast_tac 1);
+by(case_tac "P s" 1);
+by(Auto_tac);
+val lemma2 = result() RS spec RS mp;
+
+Goal "!x. P x --> Q x ==> \
+\ (<While P c; While Q c, s> -c-> t) = (<While Q c, s> -c-> t)";
+by(blast_tac (claset() addIs [lemma1,lemma2]) 1);
+qed "Hoare_example";