1.1 --- a/src/HOL/IMP/Compiler.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/IMP/Compiler.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Tobias Nipkow, TUM
     1.7      Copyright   1996 TUM
     1.8  *)
     1.9 @@ -262,32 +261,32 @@
    1.10        assume H: "\<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
    1.11        show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
    1.12        proof cases
    1.13 -	assume b: "b s"
    1.14 -	then obtain m where m: "n = Suc m"
    1.15 +        assume b: "b s"
    1.16 +        then obtain m where m: "n = Suc m"
    1.17            and "\<langle>?C @ [?j2],[?j1],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
    1.18 -	  using H by fastsimp
    1.19 -	then obtain r n1 n2 where n1: "\<langle>?C,[],s\<rangle> -n1\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
    1.20 +          using H by fastsimp
    1.21 +        then obtain r n1 n2 where n1: "\<langle>?C,[],s\<rangle> -n1\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
    1.22            and n2: "\<langle>[?j2],rev ?C @ [?j1],r\<rangle> -n2\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
    1.23            and n12: "m = n1+n2"
    1.24 -	  using execn_decomp[of _ "[?j2]"]
    1.25 -	  by(simp del: execn_simp) fast
    1.26 -	have n2n: "n2 - 1 < n" using m n12 by arith
    1.27 -	note b
    1.28 -	moreover
    1.29 -	{ from n1 have "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
    1.30 -	    by (simp add:rtrancl_is_UN_rel_pow) fast
    1.31 -	  hence "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c r" by(rule IHc)
    1.32 -	}
    1.33 -	moreover
    1.34 -	{ have "n2 - 1 < n" using m n12 by arith
    1.35 -	  moreover from n2 have "\<langle>?W,[],r\<rangle> -n2- 1\<rightarrow> \<langle>[],rev ?W,t\<rangle>" by fastsimp
    1.36 -	  ultimately have "\<langle>?w,r\<rangle> \<longrightarrow>\<^sub>c t" by(rule IHm)
    1.37 -	}
    1.38 -	ultimately show ?thesis ..
    1.39 +          using execn_decomp[of _ "[?j2]"]
    1.40 +          by(simp del: execn_simp) fast
    1.41 +        have n2n: "n2 - 1 < n" using m n12 by arith
    1.42 +        note b
    1.43 +        moreover
    1.44 +        { from n1 have "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
    1.45 +            by (simp add:rtrancl_is_UN_rel_pow) fast
    1.46 +          hence "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c r" by(rule IHc)
    1.47 +        }
    1.48 +        moreover
    1.49 +        { have "n2 - 1 < n" using m n12 by arith
    1.50 +          moreover from n2 have "\<langle>?W,[],r\<rangle> -n2- 1\<rightarrow> \<langle>[],rev ?W,t\<rangle>" by fastsimp
    1.51 +          ultimately have "\<langle>?w,r\<rangle> \<longrightarrow>\<^sub>c t" by(rule IHm)
    1.52 +        }
    1.53 +        ultimately show ?thesis ..
    1.54        next
    1.55 -	assume b: "\<not> b s"
    1.56 -	hence "t = s" using H by simp
    1.57 -	with b show ?thesis by simp
    1.58 +        assume b: "\<not> b s"
    1.59 +        hence "t = s" using H by simp
    1.60 +        with b show ?thesis by simp
    1.61        qed
    1.62      qed
    1.63    }