moved Hoare_example to Examples; other minor improvements

--- a/src/HOL/IMP/Examples.ML	Tue Aug 08 13:23:45 2000 +0200
+++ b/src/HOL/IMP/Examples.ML	Tue Aug 08 14:15:24 2000 +0200
@@ -6,7 +6,30 @@
 
 Addsimps[update_def];
 
-section "Examples";
+section "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";
+by (etac 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";
+by (etac 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";
+
+
+section "Factorial";
 
 val step = resolve_tac evalc.intrs 1;
 val simp = Asm_simp_tac 1;
@@ -15,22 +38,26 @@
 by (ftac not_sym 1);
 by step;
 by  step;
+by simp;
 by step;
 by   simp;
 by  step;
 by   step;
+by  simp;
 by  step;
 by simp;
 by step;
 by   simp;
 by  step;
 by   step;
+by  simp;
 by  step;
 by simp;
 by step;
 by   simp;
 by  step;
 by   step;
+by  simp;
 by  step;
 by simp;
 by step;

--- a/src/HOL/IMP/Natural.ML	Tue Aug 08 13:23:45 2000 +0200
+++ b/src/HOL/IMP/Natural.ML	Tue Aug 08 14:15:24 2000 +0200
@@ -26,25 +26,3 @@
 (*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";
-by (etac 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";
-by (etac 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";

--- a/src/HOL/IMP/Transition.ML	Tue Aug 08 13:23:45 2000 +0200
+++ b/src/HOL/IMP/Transition.ML	Tue Aug 08 14:15:24 2000 +0200
@@ -24,13 +24,6 @@
 
 AddIs evalc1.intrs;
 
-Goal "(SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0";
-by (etac rel_pow_E2 1);
-by (Asm_full_simp_tac 1);
-by (Fast_tac 1);
-val hlemma = result();
-
-
 Goal "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
 \              (c;d, s) -*-> (SKIP, u)";
 by (induct_tac "n" 1);
@@ -38,7 +31,6 @@
 by (fast_tac  (claset() addIs [rtrancl_into_rtrancl2]addSDs [rel_pow_Suc_D2])1);
 qed_spec_mp "lemma1";
 
-
 Goal "<c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";
 by (etac evalc.induct 1);
 
@@ -63,6 +55,12 @@
 qed "evalc_impl_evalc1";
 
 
+Goal "(SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0";
+by (etac rel_pow_E2 1);
+by (Asm_full_simp_tac 1);
+by (Fast_tac 1);
+val hlemma = result();
+
 Goal "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
 \            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)";
 by (induct_tac "n" 1);
@@ -210,7 +208,7 @@
 Goal "!c1 s. (c1;c2,s) -n-> (SKIP,t) --> \
 \     (? i1 i2 u. (c1,s) -i1-> (SKIP,u) & (c2,u) -i2-> (SKIP,t) & i1<n & i2<n)";
 by (induct_tac "n" 1);
- by (fast_tac (claset() addSDs [hlemma]) 1);
+ by (Fast_tac 1);
 by (fast_tac (claset() addSIs [rel_pow_0_I,rel_pow_Suc_I2]
                       addSDs [rel_pow_Suc_D2] addss simpset()) 1);
 qed_spec_mp "comp_decomp_lemma";
@@ -221,7 +219,7 @@
 by (etac rel_pow_E2 1);
  by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1);
 by (case_tac "c" 1);
-    by (fast_tac (claset() addSDs [hlemma]) 1);
+    by (Fast_tac 1);
    by (Blast_tac 1);
   by (blast_tac (claset() addSDs [rel_pow_Suc_I2 RS comp_decomp_lemma]) 1);
  by (Blast_tac 1);