1.1 --- a/src/HOL/IMP/Transition.ML	Fri Nov 12 10:57:28 1999 +0100
     1.2 +++ b/src/HOL/IMP/Transition.ML	Fri Nov 12 17:45:36 1999 +0100
     1.3 @@ -15,7 +15,8 @@
     1.4         ["(SKIP,s) -1-> t", 
     1.5  	"(x:=a,s) -1-> t",
     1.6  	"(c1;c2, s) -1-> t", 
     1.7 -	"(IF b THEN c1 ELSE c2, s) -1-> t"];
     1.8 +	"(IF b THEN c1 ELSE c2, s) -1-> t",
     1.9 +        "(WHILE b DO c, s) -1-> t"];
    1.10  
    1.11  val evalc1_E = evalc1.mk_cases "(WHILE b DO c,s) -1-> t";
    1.12  
    1.13 @@ -199,3 +200,30 @@
    1.14  Goal "(c,s) -*-> (SKIP,t) ==> <c,s> -c-> t";
    1.15  by (fast_tac (claset() addEs [FB_lemma2]) 1);
    1.16  qed "evalc1_impl_evalc";
    1.17 +
    1.18 +
    1.19 +section "The proof in Nielson and Nielson";
    1.20 +
    1.21 +(* The more precise n=i1+i2+1 is proved by the same script but complicates
    1.22 +   life further down, where i1,i2 < n is needed.
    1.23 +*)
    1.24 +Goal "!c1 s. (c1;c2,s) -n-> (SKIP,t) --> \
    1.25 +\     (? i1 i2 u. (c1,s) -i1-> (SKIP,u) & (c2,u) -i2-> (SKIP,t) & i1<n & i2<n)";
    1.26 +by(induct_tac "n" 1);
    1.27 + by (fast_tac (claset() addSDs [hlemma]) 1);
    1.28 +by(fast_tac (claset() addSIs [rel_pow_0_I,rel_pow_Suc_I2]
    1.29 +                      addSDs [rel_pow_Suc_D2] addss simpset()) 1);
    1.30 +qed_spec_mp "comp_decomp_lemma";
    1.31 +
    1.32 +Goal "!c s t. (c,s) -n-> (SKIP,t) --> <c,s> -c-> t";
    1.33 +by(res_inst_tac [("n","n")] less_induct 1);
    1.34 +by(Clarify_tac 1);
    1.35 +be rel_pow_E2 1;
    1.36 + by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1);
    1.37 +by(exhaust_tac "c" 1);
    1.38 +    by (fast_tac (claset() addSDs [hlemma]) 1);
    1.39 +   by(Blast_tac 1);
    1.40 +  by(blast_tac (claset() addSDs [rel_pow_Suc_I2 RS comp_decomp_lemma]) 1);
    1.41 + by(Blast_tac 1);
    1.42 +by(Blast_tac 1);
    1.43 +qed_spec_mp "evalc1_impl_evalc";