# HG changeset patch
# User wenzelm
# Date 1134069350 -3600
# Node ID 2bffdf62fe7fc67f2c1a946bc62706bb0814c69b
# Parent  d93fdf00f8a6fc028fbeb2eb1c440442e3316fd3
tuned proofs;

diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/IMP/Compiler0.thy
--- a/src/HOL/IMP/Compiler0.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Compiler0.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -47,7 +47,7 @@
   "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
                ("_ |-/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
 
-translations  
+translations
   "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P"
   "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)"
   "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^i)"
@@ -80,69 +80,64 @@
 
 subsection "Context lifting lemmas"
 
-text {* 
+text {*
   Some lemmas for lifting an execution into a prefix and suffix
   of instructions; only needed for the first proof.
 *}
 lemma app_right_1:
-  assumes A: "is1 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
+  assumes "is1 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
   shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
-proof -
- from A show ?thesis
- by induct force+
-qed
+  using prems
+  by induct auto
 
 lemma app_left_1:
-  assumes A: "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
+  assumes "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
   shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -1\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
-proof -
- from A show ?thesis
- by induct force+
-qed
+  using prems
+  by induct auto
 
 declare rtrancl_induct2 [induct set: rtrancl]
 
 lemma app_right:
-assumes A: "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
-shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
-proof -
- from A show ?thesis
- proof induct
-   show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp
- next
-   fix s1' i1' s2 i2
-   assume "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1',i1'\<rangle>"
-          "is1 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
-   thus "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
-     by(blast intro:app_right_1 rtrancl_trans)
- qed
+  assumes "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
+  shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
+  using prems
+proof induct
+  show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp
+next
+  fix s1' i1' s2 i2
+  assume "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1',i1'\<rangle>"
+    and "is1 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
+  thus "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
+    by (blast intro: app_right_1 rtrancl_trans)
 qed
 
 lemma app_left:
-assumes A: "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
-shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
-proof -
-  from A show ?thesis
-  proof induct
-    show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp
-  next
-    fix s1' i1' s2 i2
-    assume "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1',length is1 + i1'\<rangle>"
-           "is2 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
-    thus "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s2,length is1 + i2\<rangle>"
-      by(blast intro:app_left_1 rtrancl_trans)
- qed
+  assumes "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
+  shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
+using prems
+proof induct
+  show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp
+next
+  fix s1' i1' s2 i2
+  assume "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1',length is1 + i1'\<rangle>"
+    and "is2 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
+  thus "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s2,length is1 + i2\<rangle>"
+    by (blast intro: app_left_1 rtrancl_trans)
 qed
 
 lemma app_left2:
   "\<lbrakk> is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
-   is1 @ is2 \<turnstile> \<langle>s1,j1\<rangle> -*\<rightarrow> \<langle>s2,j2\<rangle>"
-  by (simp add:app_left)
+    is1 @ is2 \<turnstile> \<langle>s1,j1\<rangle> -*\<rightarrow> \<langle>s2,j2\<rangle>"
+  by (simp add: app_left)
 
 lemma app1_left:
-  "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
-   instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>"
-  by(erule app_left[of _ _ _ _ _ "[instr]",simplified])
+  assumes "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
+  shows "instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>"
+proof -
+  from app_left [OF prems, of "[instr]"]
+  show ?thesis by simp
+qed
 
 subsection "Compiler correctness"
 
@@ -154,69 +149,68 @@
   The first proof; The statement is very intuitive,
   but application of induction hypothesis requires the above lifting lemmas
 *}
-theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-shows "compile c \<turnstile> \<langle>s,0\<rangle> -*\<rightarrow> \<langle>t,length(compile c)\<rangle>" (is "?P c s t")
-proof -
-  from A show ?thesis
-  proof induct
-    show "\<And>s. ?P \<SKIP> s s" by simp
-  next
-    show "\<And>a s x. ?P (x :== a) s (s[x\<mapsto> a s])" by force
-  next
-    fix c0 c1 s0 s1 s2
-    assume "?P c0 s0 s1"
-    hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>"
-      by(rule app_right)
-    moreover assume "?P c1 s1 s2"
-    hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow>
-           \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
-    proof -
-      show "\<And>is1 is2 s1 s2 i2.
-	      is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
-	      is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
-	using app_left[of _ 0] by simp
-    qed
-    ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow>
-                       \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
-      by (rule rtrancl_trans)
-    thus "?P (c0; c1) s0 s2" by simp
-  next
-    fix b c0 c1 s0 s1
-    let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
-    assume "b s0" and IH: "?P c0 s0 s1"
-    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
-    also from IH
-    have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)+1\<rangle>"
-      by(auto intro:app1_left app_right)
-    also have "?comp \<turnstile> \<langle>s1,length(compile c0)+1\<rangle> -1\<rightarrow> \<langle>s1,length ?comp\<rangle>"
-      by(auto)
-    finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
-  next
-    fix b c0 c1 s0 s1
-    let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
-    assume "\<not>b s0" and IH: "?P c1 s0 s1"
-    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto
-    also from IH
-    have "?comp \<turnstile> \<langle>s0,length(compile c0)+2\<rangle> -*\<rightarrow> \<langle>s1,length ?comp\<rangle>"
-      by(force intro!:app_left2 app1_left)
-    finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
-  next
-    fix b c and s::state
-    assume "\<not>b s"
-    thus "?P (\<WHILE> b \<DO> c) s s" by force
-  next
-    fix b c and s0::state and s1 s2
-    let ?comp = "compile(\<WHILE> b \<DO> c)"
-    assume "b s0" and
-      IHc: "?P c s0 s1" and IHw: "?P (\<WHILE> b \<DO> c) s1 s2"
-    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
-    also from IHc
-    have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c)+1\<rangle>"
-      by(auto intro:app1_left app_right)
-    also have "?comp \<turnstile> \<langle>s1,length(compile c)+1\<rangle> -1\<rightarrow> \<langle>s1,0\<rangle>" by simp
-    also note IHw
-    finally show "?P (\<WHILE> b \<DO> c) s0 s2".
+theorem
+  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+  shows "compile c \<turnstile> \<langle>s,0\<rangle> -*\<rightarrow> \<langle>t,length(compile c)\<rangle>" (is "?P c s t")
+  using prems
+proof induct
+  show "\<And>s. ?P \<SKIP> s s" by simp
+next
+  show "\<And>a s x. ?P (x :== a) s (s[x\<mapsto> a s])" by force
+next
+  fix c0 c1 s0 s1 s2
+  assume "?P c0 s0 s1"
+  hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>"
+    by (rule app_right)
+  moreover assume "?P c1 s1 s2"
+  hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow>
+    \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
+  proof -
+    show "\<And>is1 is2 s1 s2 i2.
+      is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
+      is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
+      using app_left[of _ 0] by simp
   qed
+  ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow>
+      \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
+    by (rule rtrancl_trans)
+  thus "?P (c0; c1) s0 s2" by simp
+next
+  fix b c0 c1 s0 s1
+  let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
+  assume "b s0" and IH: "?P c0 s0 s1"
+  hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
+  also from IH
+  have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)+1\<rangle>"
+    by(auto intro:app1_left app_right)
+  also have "?comp \<turnstile> \<langle>s1,length(compile c0)+1\<rangle> -1\<rightarrow> \<langle>s1,length ?comp\<rangle>"
+    by(auto)
+  finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
+next
+  fix b c0 c1 s0 s1
+  let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
+  assume "\<not>b s0" and IH: "?P c1 s0 s1"
+  hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto
+  also from IH
+  have "?comp \<turnstile> \<langle>s0,length(compile c0)+2\<rangle> -*\<rightarrow> \<langle>s1,length ?comp\<rangle>"
+    by (force intro!: app_left2 app1_left)
+  finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
+next
+  fix b c and s::state
+  assume "\<not>b s"
+  thus "?P (\<WHILE> b \<DO> c) s s" by force
+next
+  fix b c and s0::state and s1 s2
+  let ?comp = "compile(\<WHILE> b \<DO> c)"
+  assume "b s0" and
+    IHc: "?P c s0 s1" and IHw: "?P (\<WHILE> b \<DO> c) s1 s2"
+  hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
+  also from IHc
+  have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c)+1\<rangle>"
+    by (auto intro: app1_left app_right)
+  also have "?comp \<turnstile> \<langle>s1,length(compile c)+1\<rangle> -1\<rightarrow> \<langle>s1,0\<rangle>" by simp
+  also note IHw
+  finally show "?P (\<WHILE> b \<DO> c) s0 s2".
 qed
 
 text {*
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Denotation.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -12,9 +12,9 @@
 
 constdefs
   Gamma :: "[bexp,com_den] => (com_den => com_den)"
-  "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union> 
+  "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
                        {(s,t). s=t \<and> \<not>b s})"
-    
+
 consts
   C :: "com => com_den"
 
@@ -33,7 +33,7 @@
   by (unfold Gamma_def mono_def) fast
 
 lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
-apply (simp (no_asm)) 
+apply simp
 apply (subst lfp_unfold [OF Gamma_mono])  --{*lhs only*}
 apply (simp add: Gamma_def)
 done
@@ -42,7 +42,7 @@
 
 lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)"
 (* start with rule induction *)
-apply (erule evalc.induct)
+apply (induct set: evalc)
 apply auto
 (* while *)
 apply (unfold Gamma_def)
@@ -54,15 +54,14 @@
 
 (* Denotational Semantics implies Operational Semantics *)
 
-lemma com2 [rule_format]: "\<forall>s t. (s,t)\<in>C(c) \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-apply (induct_tac "c")
+lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+apply (induct c fixing: s t)
 
-apply (simp_all (no_asm_use))
+apply simp_all
 apply fast
 apply fast
 
 (* while *)
-apply (intro strip)
 apply (erule lfp_induct [OF _ Gamma_mono])
 apply (unfold Gamma_def)
 apply fast
@@ -72,7 +71,6 @@
 (**** Proof of Equivalence ****)
 
 lemma denotational_is_natural: "(s,t) \<in> C(c)  =  (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
-apply (fast elim: com2 dest: com1)
-done
+  by (fast elim: com2 dest: com1)
 
 end
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/IMP/Examples.thy
--- a/src/HOL/IMP/Examples.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Examples.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -8,7 +8,7 @@
 
 theory Examples imports Natural begin
 
-constdefs  
+constdefs
   factorial :: "loc => loc => com"
   "factorial a b == b :== (%s. 1);
                     \<WHILE> (%s. s a ~= 0) \<DO>
@@ -18,16 +18,16 @@
 
 subsection "An example due to Tony Hoare"
 
-lemma lemma1 [rule_format (no_asm)]: 
-  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t |] ==>
-  !c. w = While P c \<longrightarrow> \<langle>While Q c,t\<rangle> \<longrightarrow>\<^sub>c u \<longrightarrow> \<langle>While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
-apply (erule evalc.induct)
-apply auto
-done
+lemma lemma1:
+  assumes 1: "!x. P x \<longrightarrow> Q x"
+    and 2: "\<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t"
+  shows "w = While P c \<Longrightarrow> \<langle>While Q c,t\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> \<langle>While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
+  using 2 apply induct
+  using 1 apply auto
+  done
 
-
-lemma lemma2 [rule_format (no_asm)]: 
-  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c u |] ==>  
+lemma lemma2 [rule_format (no_asm)]:
+  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c u |] ==>
   !c. w = While Q c \<longrightarrow> \<langle>While P c; While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
 apply (erule evalc.induct)
 apply (simp_all (no_asm_simp))
@@ -36,19 +36,16 @@
 apply auto
 done
 
-
-lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>  
+lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>
   (\<langle>While P c; While Q c, s\<rangle> \<longrightarrow>\<^sub>c t) = (\<langle>While Q c, s\<rangle> \<longrightarrow>\<^sub>c t)"
   by (blast intro: lemma1 lemma2 dest: semi [THEN iffD1])
 
 
 subsection "Factorial"
 
-lemma factorial_3: "a~=b ==>  
-  \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
-apply (unfold factorial_def)
-apply simp
-done
+lemma factorial_3: "a~=b ==>
+    \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
+  by (simp add: factorial_def)
 
 text {* the same in single step mode: *}
 lemmas [simp del] = evalc_cases
@@ -82,5 +79,5 @@
 apply (rule evalc.intros)
 apply simp
 done
-  
+
 end
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/IMP/Expr.thy
--- a/src/HOL/IMP/Expr.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Expr.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -134,12 +134,11 @@
   by (rule,cases set: evalb) auto
 
 
-lemma aexp_iff:
-  "!!n. ((a,s) -a-> n) = (A a s = n)"
-  by (induct a) auto
+lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"
+  by (induct a fixing: n) auto
 
 lemma bexp_iff:
-  "!!w. ((b,s) -b-> w) = (B b s = w)"
-  by (induct b) (auto simp add: aexp_iff)
+  "((b,s) -b-> w) = (B b s = w)"
+  by (induct b fixing: w) (auto simp add: aexp_iff)
 
 end
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Hoare.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -32,7 +32,7 @@
 constdefs wp :: "com => assn => assn"
           "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
 
-(*  
+(*
 Soundness (and part of) relative completeness of Hoare rules
 wrt denotational semantics
 *)
@@ -52,7 +52,7 @@
 
 lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
 apply (unfold hoare_valid_def)
-apply (erule hoare.induct)
+apply (induct set: hoare)
      apply (simp_all (no_asm_simp))
   apply fast
  apply fast
@@ -80,7 +80,7 @@
 apply fast
 done
 
-lemma wp_If: 
+lemma wp_If:
  "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
 apply (unfold wp_def)
 apply (simp (no_asm))
@@ -88,7 +88,7 @@
 apply fast
 done
 
-lemma wp_While_True: 
+lemma wp_While_True:
   "b s ==> wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
 apply (unfold wp_def)
 apply (subst C_While_If)
@@ -104,12 +104,11 @@
 lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
 
 (*Not suitable for rewriting: LOOPS!*)
-lemma wp_While_if: 
+lemma wp_While_if:
   "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
-apply (simp (no_asm))
-done
+  by simp
 
-lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =  
+lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
    (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
 apply (simp (no_asm))
 apply (rule iffI)
@@ -131,18 +130,17 @@
 
 declare C_while [simp del]
 
-lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If 
+lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
 
-lemma wp_is_pre [rule_format (no_asm)]: "!Q. |- {wp c Q} c {Q}"
-apply (induct_tac "c")
+lemma wp_is_pre: "|- {wp c Q} c {Q}"
+apply (induct c fixing: Q)
     apply (simp_all (no_asm))
     apply fast+
  apply (blast intro: hoare_conseq1)
-apply safe
 apply (rule hoare_conseq2)
  apply (rule hoare.While)
  apply (rule hoare_conseq1)
-  prefer 2 apply (fast)
+  prefer 2 apply fast
   apply safe
  apply simp
 apply simp
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/IMP/Machines.thy
--- a/src/HOL/IMP/Machines.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Machines.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -1,28 +1,31 @@
+
+(* $Id$ *)
+
 theory Machines imports Natural begin
 
 lemma rtrancl_eq: "R^* = Id \<union> (R O R^*)"
-by(fast intro:rtrancl.intros elim:rtranclE)
+  by (fast intro: rtrancl.intros elim: rtranclE)
 
 lemma converse_rtrancl_eq: "R^* = Id \<union> (R^* O R)"
-by(subst r_comp_rtrancl_eq[symmetric], rule rtrancl_eq)
+  by (subst r_comp_rtrancl_eq[symmetric], rule rtrancl_eq)
 
 lemmas converse_rel_powE = rel_pow_E2
 
 lemma R_O_Rn_commute: "R O R^n = R^n O R"
-by(induct_tac n, simp, simp add: O_assoc[symmetric])
+  by (induct n) (simp, simp add: O_assoc [symmetric])
 
 lemma converse_in_rel_pow_eq:
-"((x,z) \<in> R^n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R^m))"
+  "((x,z) \<in> R^n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R^m))"
 apply(rule iffI)
  apply(blast elim:converse_rel_powE)
 apply (fastsimp simp add:gr0_conv_Suc R_O_Rn_commute)
 done
 
 lemma rel_pow_plus: "R^(m+n) = R^n O R^m"
-by(induct n, simp, simp add:O_assoc)
+  by (induct n) (simp, simp add: O_assoc)
 
 lemma rel_pow_plusI: "\<lbrakk> (x,y) \<in> R^m; (y,z) \<in> R^n \<rbrakk> \<Longrightarrow> (x,z) \<in> R^(m+n)"
-by(simp add:rel_pow_plus rel_compI)
+  by (simp add: rel_pow_plus rel_compI)
 
 subsection "Instructions"
 
@@ -33,7 +36,7 @@
 
 subsection "M0 with PC"
 
-consts  exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set" 
+consts  exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set"
 syntax
   "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
                ("(_/ |- (1<_,/_>)/ -1-> (1<_,/_>))" [50,0,0,0,0] 50)
@@ -58,7 +61,7 @@
   "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
                ("(_/ |- (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
 
-translations  
+translations
   "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)"
   "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^*"
   "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^n"
@@ -97,7 +100,7 @@
   "_stepan" :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool"
                ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
 
-translations  
+translations
   "\<langle>p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : stepa1"
   "\<langle>p,q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^*)"
   "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^i)"
@@ -156,7 +159,7 @@
 lemma direction1:
  "\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle> \<Longrightarrow>
   rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>"
-apply(erule stepa1.induct)
+apply(induct set: stepa1)
    apply(simp add:exec01.SET)
   apply(fastsimp intro:exec01.JMPFT)
  apply simp
@@ -187,9 +190,9 @@
 *)
 lemma direction2:
  "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
- \<forall>p q p' q'. rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
+  rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
           rev p' @ q' = rev p @ q \<longrightarrow> \<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>"
-apply(erule exec01.induct)
+apply(induct fixing: p q p' q' set: exec01)
    apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
    apply(drule sym)
    apply simp
@@ -216,6 +219,6 @@
 theorem M_eqiv:
 "(\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>) =
  (rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>)"
-by(fast dest:direction1 direction2)
+  by (blast dest: direction1 direction2)
 
 end
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/IMP/Natural.thy
--- a/src/HOL/IMP/Natural.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Natural.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -11,7 +11,7 @@
 
 subsection "Execution of commands"
 
-consts  evalc   :: "(com \<times> state \<times> state) set" 
+consts  evalc   :: "(com \<times> state \<times> state) set"
 syntax "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("<_,_>/ -c-> _" [0,0,60] 60)
 
 syntax (xsymbols)
@@ -21,7 +21,7 @@
   "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
 
 text {*
-  We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started 
+  We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started
   in state @{text s}, terminates in state @{text s'}}. Formally,
   @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} is just another form of saying \emph{the tuple
   @{text "(c,s,s')"} is part of the relation @{text evalc}}:
@@ -39,7 +39,7 @@
   The big-step execution relation @{text evalc} is defined inductively:
 *}
 inductive evalc
-  intros 
+  intros
   Skip:    "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s"
   Assign:  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s[x\<mapsto>a s]"
 
@@ -49,7 +49,7 @@
   IfFalse: "\<not>b s \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
 
   WhileFalse: "\<not>b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s"
-  WhileTrue:  "b s \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s'  
+  WhileTrue:  "b s \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s'
                \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s'"
 
 lemmas evalc.intros [intro] -- "use those rules in automatic proofs"
@@ -60,7 +60,7 @@
 @{thm [display] evalc.induct [no_vars]}
 
 
-(@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's 
+(@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's
   meta symbols for @{text "\<forall>"} and @{text "\<longrightarrow>"})
 *}
 
@@ -70,35 +70,35 @@
   syntactic category there is always only one rule applicable. That
   means we can use the rules in both directions. The proofs for this
   are all the same: one direction is trivial, the other one is shown
-  by using the @{text evalc} rules backwards: 
+  by using the @{text evalc} rules backwards:
 *}
-lemma skip: 
+lemma skip:
   "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
   by (rule, erule evalc.elims) auto
 
-lemma assign: 
-  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s[x\<mapsto>a s])" 
+lemma assign:
+  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s[x\<mapsto>a s])"
   by (rule, erule evalc.elims) auto
 
-lemma semi: 
+lemma semi:
   "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s' = (\<exists>s''. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>c s')"
   by (rule, erule evalc.elims) auto
 
-lemma ifTrue: 
-  "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" 
+lemma ifTrue:
+  "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'"
   by (rule, erule evalc.elims) auto
 
-lemma ifFalse: 
+lemma ifFalse:
   "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'"
   by (rule, erule evalc.elims) auto
 
-lemma whileFalse: 
+lemma whileFalse:
   "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
-  by (rule, erule evalc.elims) auto  
+  by (rule, erule evalc.elims) auto
 
-lemma whileTrue: 
-  "b s \<Longrightarrow> 
-  \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' = 
+lemma whileTrue:
+  "b s \<Longrightarrow>
+  \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' =
   (\<exists>s''. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s')"
   by (rule, erule evalc.elims) auto
 
@@ -112,7 +112,7 @@
   big-step semantics when \emph{@{text c} started in @{text s} terminates
   in @{text s'} iff @{text c'} started in the same @{text s} also terminates
   in the same @{text s'}}. Formally:
-*} 
+*}
 constdefs
   equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _")
   "c \<sim> c' \<equiv> \<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
@@ -120,7 +120,7 @@
 text {*
   Proof rules telling Isabelle to unfold the definition
   if there is something to be proved about equivalent
-  statements: *} 
+  statements: *}
 lemma equivI [intro!]:
   "(\<And>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s') \<Longrightarrow> c \<sim> c'"
   by (unfold equiv_c_def) blast
@@ -141,7 +141,7 @@
   "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)" (is "?w \<sim> ?if")
 proof -
   -- "to show the equivalence, we look at the derivation tree for"
-  -- "each side and from that construct a derivation tree for the other side"  
+  -- "each side and from that construct a derivation tree for the other side"
   { fix s s' assume w: "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"
     -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
     -- "then both statements do nothing:"
@@ -159,8 +159,8 @@
       -- "then the whole @{text \<IF>}"
       with b have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule IfTrue)
     }
-    ultimately 
-    -- "both cases together give us what we want:"      
+    ultimately
+    -- "both cases together give us what we want:"
     have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   }
   moreover
@@ -180,9 +180,9 @@
         "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
       -- "with this information, we can build a derivation tree for the @{text \<WHILE>}"
       with b
-      have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule WhileTrue) 
+      have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule WhileTrue)
     }
-    ultimately 
+    ultimately
     -- "both cases together again give us what we want:"
     have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   }
@@ -196,91 +196,89 @@
 text {*
 The following proof presents all the details:
 *}
-theorem com_det: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<and> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<longrightarrow> u=t"
-proof clarify -- "transform the goal into canonical form"
-  assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-  thus "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u=t" 
-  proof (induct set: evalc)
-    fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
-    thus "u = s" by simp
-  next
-    fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
-    thus "u = s[x \<mapsto> a s]" by simp      
-  next
-    fix c0 c1 s s1 s2 u
-    assume IH0: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
-    assume IH1: "\<And>u. \<langle>c1,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
+theorem com_det:
+  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
+  shows "u = t"
+  using prems
+proof (induct fixing: u set: evalc)
+  fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
+  thus "u = s" by simp
+next
+  fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
+  thus "u = s[x \<mapsto> a s]" by simp
+next
+  fix c0 c1 s s1 s2 u
+  assume IH0: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
+  assume IH1: "\<And>u. \<langle>c1,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
 
-    assume "\<langle>c0;c1, s\<rangle> \<longrightarrow>\<^sub>c u"
-    then obtain s' where
+  assume "\<langle>c0;c1, s\<rangle> \<longrightarrow>\<^sub>c u"
+  then obtain s' where
       c0: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" and
-      c1: "\<langle>c1,s'\<rangle> \<longrightarrow>\<^sub>c u" 
-      by auto
+      c1: "\<langle>c1,s'\<rangle> \<longrightarrow>\<^sub>c u"
+    by auto
 
-    from c0 IH0 have "s'=s2" by blast
-    with c1 IH1 show "u=s1" by blast
-  next
-    fix b c0 c1 s s1 u
-    assume IH: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1" 
+  from c0 IH0 have "s'=s2" by blast
+  with c1 IH1 show "u=s1" by blast
+next
+  fix b c0 c1 s s1 u
+  assume IH: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
 
-    assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
-    hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
-    with IH show "u = s1" by blast
-  next
-    fix b c0 c1 s s1 u
-    assume IH: "\<And>u. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1" 
+  assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
+  hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
+  with IH show "u = s1" by blast
+next
+  fix b c0 c1 s s1 u
+  assume IH: "\<And>u. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
 
-    assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
-    hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
-    with IH show "u = s1" by blast
-  next
-    fix b c s u
-    assume "\<not>b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
-    thus "u = s" by simp
-  next
-    fix b c s s1 s2 u
-    assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
-    assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
-    
-    assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
-    then obtain s' where
+  assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
+  hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
+  with IH show "u = s1" by blast
+next
+  fix b c s u
+  assume "\<not>b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
+  thus "u = s" by simp
+next
+  fix b c s s1 s2 u
+  assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
+  assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
+
+  assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
+  then obtain s' where
       c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
-      w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u" 
-      by auto
-    
-    from c "IH\<^sub>c" have "s' = s2" by blast
-    with w "IH\<^sub>w" show "u = s1" by blast
-  qed
+      w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
+    by auto
+
+  from c "IH\<^sub>c" have "s' = s2" by blast
+  with w "IH\<^sub>w" show "u = s1" by blast
 qed
 
 
 text {*
   This is the proof as you might present it in a lecture. The remaining
-  cases are simple enough to be proved automatically: 
-*} 
-theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<and> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<longrightarrow> u=t" 
-proof clarify
-  assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-  thus "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u=t" 
-  proof (induct set: evalc)
-    -- "the simple @{text \<SKIP>} case for demonstration:"
-    fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
-    thus "u = s" by simp
-  next
-    -- "and the only really interesting case, @{text \<WHILE>}:"
-    fix b c s s1 s2 u
-    assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
-    assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
-    
-    assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
-    then obtain s' where
+  cases are simple enough to be proved automatically:
+*}
+theorem
+  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
+  shows "u = t"
+  using prems
+proof (induct fixing: u)
+  -- "the simple @{text \<SKIP>} case for demonstration:"
+  fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
+  thus "u = s" by simp
+next
+  -- "and the only really interesting case, @{text \<WHILE>}:"
+  fix b c s s1 s2 u
+  assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
+  assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
+
+  assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
+  then obtain s' where
       c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
       w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
-      by auto
-    
-    from c "IH\<^sub>c" have "s' = s2" by blast
-    with w "IH\<^sub>w" show "u = s1" by blast
-  qed (best dest: evalc_cases [THEN iffD1])+ -- "prove the rest automatically"
-qed
+    by auto
+
+  from c "IH\<^sub>c" have "s' = s2" by blast
+  with w "IH\<^sub>w" show "u = s1" by blast
+qed (best dest: evalc_cases [THEN iffD1])+ -- "prove the rest automatically"
 
 end
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Transition.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -15,16 +15,16 @@
   We formalize the transition semantics as in \cite{Nielson}. This
   makes some of the rules a bit more intuitive, but also requires
   some more (internal) formal overhead.
-  
-  Since configurations that have terminated are written without 
-  a statement, the transition relation is not 
+
+  Since configurations that have terminated are written without
+  a statement, the transition relation is not
   @{typ "((com \<times> state) \<times> (com \<times> state)) set"}
   but instead:
 *}
 consts evalc1 :: "((com option \<times> state) \<times> (com option \<times> state)) set"
 
 text {*
-  Some syntactic sugar that we will use to hide the 
+  Some syntactic sugar that we will use to hide the
   @{text option} part in configurations:
 *}
 syntax
@@ -65,21 +65,21 @@
 
 translations
   "cs \<longrightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1"
-  "cs -n\<rightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1^n" 
-  "cs \<longrightarrow>\<^sub>1\<^sup>* cs'" == "(cs,cs') \<in> evalc1^*" 
+  "cs -n\<rightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1^n"
+  "cs \<longrightarrow>\<^sub>1\<^sup>* cs'" == "(cs,cs') \<in> evalc1^*"
 
-  -- {* Isabelle converts @{text "(cs0,(c1,s1))"} to @{term "(cs0,c1,s1)"}, 
+  -- {* Isabelle/HOL converts @{text "(cs0,(c1,s1))"} to @{term "(cs0,c1,s1)"},
         so we also include: *}
-  "cs0 \<longrightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1"   
+  "cs0 \<longrightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1"
   "cs0 -n\<rightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^n"
-  "cs0 \<longrightarrow>\<^sub>1\<^sup>* (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^*" 
+  "cs0 \<longrightarrow>\<^sub>1\<^sup>* (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^*"
 
 text {*
   Now, finally, we are set to write down the rules for our small step semantics:
 *}
 inductive evalc1
   intros
-  Skip:    "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>"  
+  Skip:    "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>"
   Assign:  "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> a s]\<rangle>"
 
   Semi1:   "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0;c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s'\<rangle>"
@@ -96,42 +96,40 @@
 (* fixme: move to Relation_Power.thy *)
 lemma rel_pow_Suc_E2 [elim!]:
   "[| (x, z) \<in> R ^ Suc n; !!y. [| (x, y) \<in> R; (y, z) \<in> R ^ n |] ==> P |] ==> P"
-  by (drule rel_pow_Suc_D2) blast
+  by (blast dest: rel_pow_Suc_D2)
 
 lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
-proof -
-  assume "p \<in> R\<^sup>*"
-  moreover obtain x y where p: "p = (x,y)" by (cases p)
-  ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
-  hence "\<exists>n. (x,y) \<in> R^n"
+proof (induct p)
+  fix x y
+  assume "(x, y) \<in> R\<^sup>*"
+  thus "\<exists>n. (x, y) \<in> R^n"
   proof induct
-    fix a have "(a,a) \<in> R^0" by simp
-    thus "\<exists>n. (a,a) \<in> R ^ n" ..
+    fix a have "(a, a) \<in> R^0" by simp
+    thus "\<exists>n. (a, a) \<in> R ^ n" ..
   next
-    fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
-    then obtain n where "(a,b) \<in> R^n" ..
-    moreover assume "(b,c) \<in> R"
-    ultimately have "(a,c) \<in> R^(Suc n)" by auto
-    thus "\<exists>n. (a,c) \<in> R^n" ..
+    fix a b c assume "\<exists>n. (a, b) \<in> R ^ n"
+    then obtain n where "(a, b) \<in> R^n" ..
+    moreover assume "(b, c) \<in> R"
+    ultimately have "(a, c) \<in> R^(Suc n)" by auto
+    thus "\<exists>n. (a, c) \<in> R^n" ..
   qed
-  with p show ?thesis by hypsubst
-qed  
-(*>*)    
+qed
+(*>*)
 text {*
-  As for the big step semantics you can read these rules in a 
+  As for the big step semantics you can read these rules in a
   syntax directed way:
 *}
-lemma SKIP_1: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s\<rangle>)" 
-  by (rule, cases set: evalc1, auto)      
+lemma SKIP_1: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s\<rangle>)"
+  by (rule, cases set: evalc1, auto)
 
 lemma Assign_1: "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s[x \<mapsto> a s]\<rangle>)"
   by (rule, cases set: evalc1, auto)
 
-lemma Cond_1: 
+lemma Cond_1:
   "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 y = ((b s \<longrightarrow> y = \<langle>c1, s\<rangle>) \<and> (\<not>b s \<longrightarrow> y = \<langle>c2, s\<rangle>))"
   by (rule, cases set: evalc1, auto)
 
-lemma While_1: 
+lemma While_1:
   "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>, s\<rangle>)"
   by (rule, cases set: evalc1, auto)
 
@@ -140,7 +138,7 @@
 
 subsection "Examples"
 
-lemma 
+lemma
   "s x = 0 \<Longrightarrow> \<langle>\<WHILE> \<lambda>s. s x \<noteq> 1 \<DO> (x:== \<lambda>s. s x+1), s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x \<mapsto> 1]\<rangle>"
   (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* _")
 proof -
@@ -148,45 +146,45 @@
   let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
   assume [simp]: "s x = 0"
   have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1  \<langle>?if, s\<rangle>" ..
-  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp 
-  also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1, simp)
+  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp
+  also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1) simp
   also have "\<langle>?w, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 1]\<rangle>" ..
   also have "\<langle>?if, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle>" by (simp add: update_def)
   also have "\<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> 1]\<rangle>" ..
   finally show ?thesis ..
 qed
 
-lemma 
+lemma
   "s x = 2 \<Longrightarrow> \<langle>\<WHILE> \<lambda>s. s x \<noteq> 1 \<DO> (x:== \<lambda>s. s x+1), s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'"
   (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'")
 proof -
   let ?c = "x:== \<lambda>s. s x+1"
-  let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"  
+  let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
   assume [simp]: "s x = 2"
   note update_def [simp]
   have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1  \<langle>?if, s\<rangle>" ..
   also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp
-  also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 3]\<rangle>" by (rule Semi1, simp)
+  also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 3]\<rangle>" by (rule Semi1) simp
   also have "\<langle>?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 3]\<rangle>" ..
   also have "\<langle>?if, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1  \<langle>?c; ?w, s[x \<mapsto> 3]\<rangle>" by simp
-  also have "\<langle>?c; ?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 4]\<rangle>" by (rule Semi1, simp)
+  also have "\<langle>?c; ?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 4]\<rangle>" by (rule Semi1) simp
   also have "\<langle>?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 4]\<rangle>" ..
   also have "\<langle>?if, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1  \<langle>?c; ?w, s[x \<mapsto> 4]\<rangle>" by simp
-  also have "\<langle>?c; ?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 5]\<rangle>" by (rule Semi1, simp) 
+  also have "\<langle>?c; ?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 5]\<rangle>" by (rule Semi1) simp
   oops
 
 subsection "Basic properties"
 
-text {* 
+text {*
   There are no \emph{stuck} programs:
 *}
 lemma no_stuck: "\<exists>y. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 y"
 proof (induct c)
   -- "case Semi:"
-  fix c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" 
+  fix c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y"
   then obtain y where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" ..
   then obtain c1' s' where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<or> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1',s'\<rangle>"
-    by (cases y, cases "fst y", auto)
+    by (cases y, cases "fst y") auto
   thus "\<exists>s'. \<langle>c1;c2,s\<rangle> \<longrightarrow>\<^sub>1 s'" by auto
 next
   -- "case If:"
@@ -198,22 +196,22 @@
   If a configuration does not contain a statement, the program
   has terminated and there is no next configuration:
 *}
-lemma stuck [elim!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1 y \<Longrightarrow> P" 
+lemma stuck [elim!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1 y \<Longrightarrow> P"
   by (auto elim: evalc1.elims)
 
-lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>" 
-  by (erule rtrancl_induct) auto 
+lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>"
+  by (induct set: rtrancl) auto
 
 (*<*)
-(* fixme: relpow.simps don't work *)
+(* FIXME: relpow.simps don't work *)
 lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by simp
-lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp 
+lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp
 lemmas [simp del] = relpow.simps
 (*>*)
 lemma evalc1_None_0 [simp, dest!]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
   by (cases n) auto
 
-lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1" 
+lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1"
   by (cases n) auto
 
 subsection "Equivalence to natural semantics (after Nielson and Nielson)"
@@ -223,72 +221,70 @@
   decomposition and composition.
 *}
 lemma semiD:
-  "\<And>c1 c2 s s''. \<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> 
+  "\<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow>
   \<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> n = i+j"
-  (is "PROP ?P n")
-proof (induct n)
-  show "PROP ?P 0" by simp
+proof (induct n fixing: c1 c2 s s'')
+  case 0
+  then show ?case by simp
 next
-  fix n assume IH: "PROP ?P n"
-  show "PROP ?P (Suc n)"
-  proof -
-    fix c1 c2 s s''
-    assume "\<langle>c1; c2, s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
-    then obtain y where
+  case (Suc n)
+
+  from `\<langle>c1; c2, s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
+  obtain y where
       1: "\<langle>c1; c2, s\<rangle> \<longrightarrow>\<^sub>1 y" and
       n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
-      by blast
+    by blast
 
-    from 1
-    show "\<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> Suc n = i+j"
-      (is "\<exists>i j s'. ?Q i j s'")
-    proof (cases set: evalc1)
-      case Semi1
-      then obtain s' where
+  from 1
+  show "\<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> Suc n = i+j"
+    (is "\<exists>i j s'. ?Q i j s'")
+  proof (cases set: evalc1)
+    case Semi1
+    then obtain s' where
         "y = \<langle>c2, s'\<rangle>" and "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
-        by auto
-      with 1 n have "?Q 1 n s'" by simp
-      thus ?thesis by blast
-    next
-      case Semi2
-      then obtain c1' s' where
+      by auto
+    with 1 n have "?Q 1 n s'" by simp
+    thus ?thesis by blast
+  next
+    case Semi2
+    then obtain c1' s' where
         y:  "y = \<langle>c1'; c2, s'\<rangle>" and
         c1: "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'\<rangle>"
-        by auto
-      with n have "\<langle>c1'; c2, s'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp 
-      with IH obtain i j s0 where 
+      by auto
+    with n have "\<langle>c1'; c2, s'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp
+    with Suc.hyps obtain i j s0 where
         c1': "\<langle>c1',s'\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
         c2:  "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
         i:   "n = i+j"
-        by fast
-          
-      from c1 c1'
-      have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto intro: rel_pow_Suc_I2)
-      with c2 i
-      have "?Q (i+1) j s0" by simp
-      thus ?thesis by blast
-    qed auto -- "the remaining cases cannot occur"
-  qed
+      by fast
+
+    from c1 c1'
+    have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto intro: rel_pow_Suc_I2)
+    with c2 i
+    have "?Q (i+1) j s0" by simp
+    thus ?thesis by blast
+  qed auto -- "the remaining cases cannot occur"
 qed
 
 
-lemma semiI: 
-  "\<And>c0 s s''. \<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-proof (induct n)
-  fix c0 s s'' assume "\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
-  hence False by simp
-  thus "?thesis c0 s s''" ..
+lemma semiI:
+  "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+proof (induct n fixing: c0 s s'')
+  case 0
+  from `\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
+  have False by simp
+  thus ?case ..
 next
-  fix c0 s s'' n 
-  assume c0: "\<langle>c0,s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
-  assume c1: "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-  assume IH: "\<And>c0 s s''.
-    \<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-  from c0 obtain y where 
+  case (Suc n)
+  note c0 = `\<langle>c0,s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
+  note c1 = `\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>`
+  note IH = `\<And>c0 s s''.
+    \<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>`
+  from c0 obtain y where
     1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 y" and n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
   from 1 obtain c0' s0' where
-    "y = \<langle>s0'\<rangle> \<or> y = \<langle>c0', s0'\<rangle>" 
-    by (cases y, cases "fst y", auto)
+      "y = \<langle>s0'\<rangle> \<or> y = \<langle>c0', s0'\<rangle>"
+    by (cases y, cases "fst y") auto
   moreover
   { assume y: "y = \<langle>s0'\<rangle>"
     with n have "s'' = s0'" by simp
@@ -312,57 +308,55 @@
 text {*
   The easy direction of the equivalence proof:
 *}
-lemma evalc_imp_evalc1: 
-  "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-proof -
-  assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
-  thus "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-  proof induct
-    fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto
-  next
-    fix x a s show "\<langle>x :== a ,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x\<mapsto>a s]\<rangle>" by auto
-  next
-    fix c0 c1 s s'' s'
-    assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
-    then obtain n where "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
-    moreover
-    assume "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-    ultimately
-    show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule semiI)
-  next
-    fix s::state and b c0 c1 s'
-    assume "b s"
-    hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0,s\<rangle>" by simp
-    also assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" 
-    finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
-  next
-    fix s::state and b c0 c1 s'
-    assume "\<not>b s"
-    hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>" by simp
-    also assume "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-    finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
-  next
-    fix b c and s::state
-    assume b: "\<not>b s"
-    let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>"
-    have "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
-    also have "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" by (simp add: b)
-    also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" by blast
-    finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
-  next
-    fix b c s s'' s'
-    let ?w  = "\<WHILE> b \<DO> c"
-    let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>"
-    assume w: "\<langle>?w,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-    assume c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
-    assume b: "b s"
-    have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
-    also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c; ?w, s\<rangle>" by (simp add: b)
-    also 
-    from c obtain n where "\<langle>c,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
-    with w have "\<langle>c; ?w,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by - (rule semiI)
-    finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" ..
-  qed
+lemma evalc_imp_evalc1:
+  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
+  shows "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+  using prems
+proof induct
+  fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto
+next
+  fix x a s show "\<langle>x :== a ,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x\<mapsto>a s]\<rangle>" by auto
+next
+  fix c0 c1 s s'' s'
+  assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
+  then obtain n where "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
+  moreover
+  assume "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+  ultimately
+  show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule semiI)
+next
+  fix s::state and b c0 c1 s'
+  assume "b s"
+  hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0,s\<rangle>" by simp
+  also assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+  finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
+next
+  fix s::state and b c0 c1 s'
+  assume "\<not>b s"
+  hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>" by simp
+  also assume "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+  finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
+next
+  fix b c and s::state
+  assume b: "\<not>b s"
+  let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>"
+  have "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
+  also have "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" by (simp add: b)
+  also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" by blast
+  finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
+next
+  fix b c s s'' s'
+  let ?w  = "\<WHILE> b \<DO> c"
+  let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>"
+  assume w: "\<langle>?w,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+  assume c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
+  assume b: "b s"
+  have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
+  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c; ?w, s\<rangle>" by (simp add: b)
+  also
+  from c obtain n where "\<langle>c,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
+  with w have "\<langle>c; ?w,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by - (rule semiI)
+  finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" ..
 qed
 
 text {*
@@ -373,42 +367,42 @@
 proof
   assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
   show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
-next  
+next
   assume "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
   moreover
-  have "\<And>c s s'. \<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" 
-  proof (induct rule: nat_less_induct)
+  have "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
+  proof (induct fixing: c s s' rule: less_induct)
     fix n
-    assume IH: "\<forall>m. m < n \<longrightarrow> (\<forall>c s s'. \<langle>c, s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s')"
+    assume IH: "\<And>m c s s'. m < n \<Longrightarrow> \<langle>c,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
     fix c s s'
     assume c:  "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
     then obtain m where n: "n = Suc m" by (cases n) auto
-    with c obtain y where 
+    with c obtain y where
       c': "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1 y" and m: "y -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by blast
-    show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" 
+    show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
     proof (cases c)
       case SKIP
       with c n show ?thesis by auto
-    next 
+    next
       case Assign
       with c n show ?thesis by auto
     next
       fix c1 c2 assume semi: "c = (c1; c2)"
       with c obtain i j s'' where
-        c1: "\<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
-        c2: "\<langle>c2, s''\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" and
-        ij: "n = i+j"
+          c1: "\<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
+          c2: "\<langle>c2, s''\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" and
+          ij: "n = i+j"
         by (blast dest: semiD)
-      from c1 c2 obtain 
+      from c1 c2 obtain
         "0 < i" and "0 < j" by (cases i, auto, cases j, auto)
       with ij obtain
         i: "i < n" and j: "j < n" by simp
-      from c1 i IH
-      have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" by blast
+      from IH i c1
+      have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" .
       moreover
-      from c2 j IH
-      have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" by blast
+      from IH j c2
+      have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" .
       moreover
       note semi
       ultimately
@@ -417,33 +411,33 @@
       fix b c1 c2 assume If: "c = \<IF> b \<THEN> c1 \<ELSE> c2"
       { assume True: "b s = True"
         with If c n
-        have "\<langle>c1,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto      
+        have "\<langle>c1,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto
         with n IH
         have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
         with If True
-        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp        
+        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
       }
       moreover
       { assume False: "b s = False"
         with If c n
-        have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto      
+        have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto
         with n IH
         have "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
         with If False
-        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp        
+        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
       }
       ultimately
       show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases "b s") auto
     next
       fix b c' assume w: "c = \<WHILE> b \<DO> c'"
-      with c n 
+      with c n
       have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
         (is "\<langle>?if,_\<rangle> -m\<rightarrow>\<^sub>1 _") by auto
       with n IH
       have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
       moreover note unfold_while [of b c']
       -- {* @{thm unfold_while [of b c']} *}
-      ultimately      
+      ultimately
       have "\<langle>\<WHILE> b \<DO> c',s\<rangle> \<longrightarrow>\<^sub>c s'" by (blast dest: equivD2)
       with w show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
     qed
@@ -458,11 +452,11 @@
 declare rel_pow_0_E [elim!]
 
 text {*
-  Winskel's small step rules are a bit different \cite{Winskel}; 
+  Winskel's small step rules are a bit different \cite{Winskel};
   we introduce their equivalents as derived rules:
 *}
 lemma whileFalse1 [intro]:
-  "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>")  
+  "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>")
 proof -
   assume "\<not>b s"
   have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
@@ -472,7 +466,7 @@
 qed
 
 lemma whileTrue1 [intro]:
-  "b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;\<WHILE> b \<DO> c, s\<rangle>" 
+  "b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;\<WHILE> b \<DO> c, s\<rangle>"
   (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>")
 proof -
   assume "b s"
@@ -481,8 +475,8 @@
   finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" ..
 qed
 
-inductive_cases evalc1_SEs: 
-  "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1 t" 
+inductive_cases evalc1_SEs:
+  "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1 t"
   "\<langle>x:==a,s\<rangle> \<longrightarrow>\<^sub>1 t"
   "\<langle>c1;c2, s\<rangle> \<longrightarrow>\<^sub>1 t"
   "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 t"
@@ -493,53 +487,53 @@
 declare evalc1_SEs [elim!]
 
 lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
-apply (erule evalc.induct)
+apply (induct set: evalc)
 
--- SKIP 
+-- SKIP
 apply blast
 
--- ASSIGN 
+-- ASSIGN
 apply fast
 
--- SEMI 
+-- SEMI
 apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI)
 
--- IF 
+-- IF
 apply (fast intro: converse_rtrancl_into_rtrancl)
 apply (fast intro: converse_rtrancl_into_rtrancl)
 
--- WHILE 
+-- WHILE
 apply fast
 apply (fast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI)
 
 done
 
 
-lemma lemma2 [rule_format (no_asm)]: 
-  "\<forall>c d s u. \<langle>c;d,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<longrightarrow> (\<exists>t m. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<and> \<langle>d,t\<rangle> -m\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<and> m \<le> n)"
-apply (induct_tac "n")
+lemma lemma2:
+  "\<langle>c;d,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<Longrightarrow> \<exists>t m. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<and> \<langle>d,t\<rangle> -m\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<and> m \<le> n"
+apply (induct n fixing: c d s u)
  -- "case n = 0"
  apply fastsimp
 -- "induction step"
-apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2 
+apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2
             elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl)
 done
 
-lemma evalc1_impl_evalc [rule_format (no_asm)]: 
-  "\<forall>s t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-apply (induct_tac "c")
+lemma evalc1_impl_evalc:
+  "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+apply (induct c fixing: s t)
 apply (safe dest!: rtrancl_imp_UN_rel_pow)
 
 -- SKIP
 apply (simp add: SKIP_n)
 
--- ASSIGN 
+-- ASSIGN
 apply (fastsimp elim: rel_pow_E2)
 
 -- SEMI
 apply (fast dest!: rel_pow_imp_rtrancl lemma2)
 
--- IF 
+-- IF
 apply (erule rel_pow_E2)
 apply simp
 apply (fast dest!: rel_pow_imp_rtrancl)
@@ -548,7 +542,7 @@
 apply (rename_tac b c s t n)
 apply (erule_tac P = "?X -n\<rightarrow>\<^sub>1 ?Y" in rev_mp)
 apply (rule_tac x = "s" in spec)
-apply (induct_tac "n" rule: nat_less_induct)
+apply (induct_tac n rule: nat_less_induct)
 apply (intro strip)
 apply (erule rel_pow_E2)
  apply simp
@@ -560,10 +554,11 @@
  apply (erule rel_pow_E2)
   apply simp
  apply (clarify dest!: lemma2)
+ apply atomize
  apply (erule allE, erule allE, erule impE, assumption)
  apply (erule_tac x=mb in allE, erule impE, fastsimp)
  apply blast
--- WhileFalse 
+-- WhileFalse
 apply (erule rel_pow_E2)
  apply simp
 apply (simp add: SKIP_n)
@@ -572,8 +567,7 @@
 
 text {* proof of the equivalence of evalc and evalc1 *}
 lemma evalc1_eq_evalc: "(\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle>) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
-apply (fast elim!: evalc1_impl_evalc evalc_impl_evalc1)
-done
+  by (fast elim!: evalc1_impl_evalc evalc_impl_evalc1)
 
 
 subsection "A proof without n"
@@ -582,49 +576,50 @@
   The inductions are a bit awkward to write in this section,
   because @{text None} as result statement in the small step
   semantics doesn't have a direct counterpart in the big step
-  semantics. 
+  semantics.
 
   Winskel's small step rule set (using the @{text "\<SKIP>"} statement
   to indicate termination) is better suited for this proof.
 *}
 
-lemma my_lemma1 [rule_format (no_asm)]: 
-  "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle> \<Longrightarrow> \<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3 \<Longrightarrow> \<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
+lemma my_lemma1:
+  assumes "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>"
+    and "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
+  shows "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
 proof -
   -- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *}
-  have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle> \<Longrightarrow> \<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3 \<longrightarrow> 
-       \<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
-    apply (erule converse_rtrancl_induct2)
+  from prems
+  have "\<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
+    apply (induct rule: converse_rtrancl_induct2)
      apply simp
     apply (rename_tac c s')
     apply simp
     apply (rule conjI)
-     apply fast 
+     apply fast
     apply clarify
     apply (case_tac c)
     apply (auto intro: converse_rtrancl_into_rtrancl)
     done
-  moreover assume "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>" "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
-  ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" by simp
+  then show ?thesis by simp
 qed
 
 lemma evalc_impl_evalc1': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
-apply (erule evalc.induct)
+apply (induct set: evalc)
 
--- SKIP 
+-- SKIP
 apply fast
 
 -- ASSIGN
 apply fast
 
--- SEMI 
+-- SEMI
 apply (fast intro: my_lemma1)
 
 -- IF
 apply (fast intro: converse_rtrancl_into_rtrancl)
-apply (fast intro: converse_rtrancl_into_rtrancl) 
+apply (fast intro: converse_rtrancl_into_rtrancl)
 
--- WHILE 
+-- WHILE
 apply fast
 apply (fast intro: converse_rtrancl_into_rtrancl my_lemma1)
 
@@ -645,18 +640,18 @@
 
 Lemma 2
 ((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t
-  => 
+  =>
 <c,s> -c-> t
 
 This is proved by rule induction on the  -*-> relation
-and the induction step makes use of a third lemma: 
+and the induction step makes use of a third lemma:
 
 Lemma 3
 ((c,s) --> (c',s')) /\ <c',s'> -c'-> t
-  => 
+  =>
 <c,s> -c-> t
 
-This captures the essence of the proof, as it shows that <c',s'> 
+This captures the essence of the proof, as it shows that <c',s'>
 behaves as the continuation of <c,s> with respect to the natural
 semantics.
 The proof of Lemma 3 goes by rule induction on the --> relation,
@@ -668,24 +663,22 @@
 
 inductive_cases evalc1_term_cases: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
 
-lemma FB_lemma3 [rule_format]:
-  "(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<longrightarrow>
-  (\<forall>t. \<langle>if c'=None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t)"
-  apply (erule evalc1.induct)
-  apply (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
-  done
+lemma FB_lemma3:
+  "(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
+  \<langle>if c'=None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t"
+  by (induct fixing: t set: evalc1)
+    (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
 
-lemma FB_lemma2 [rule_format]:
-  "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<longrightarrow> 
-   \<langle>if c' = None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t" 
-  apply (erule converse_rtrancl_induct2)
+lemma FB_lemma2:
+  "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
+   \<langle>if c' = None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t"
+  apply (induct rule: converse_rtrancl_induct2)
    apply simp
   apply clarsimp
   apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
   done
 
 lemma evalc1_impl_evalc': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-  apply (fastsimp dest: FB_lemma2)
-  done
+  by (fastsimp dest: FB_lemma2)
 
 end
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/VC.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -28,14 +28,14 @@
   "awp Askip Q = Q"
   "awp (Aass x a) Q = (\<lambda>s. Q(s[x\<mapsto>a s]))"
   "awp (Asemi c d) Q = awp c (awp d Q)"
-  "awp (Aif b c d) Q = (\<lambda>s. (b s-->awp c Q s) & (~b s-->awp d Q s))" 
+  "awp (Aif b c d) Q = (\<lambda>s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
   "awp (Awhile b I c) Q = I"
 
 primrec
   "vc Askip Q = (\<lambda>s. True)"
   "vc (Aass x a) Q = (\<lambda>s. True)"
   "vc (Asemi c d) Q = (\<lambda>s. vc c (awp d Q) s & vc d Q s)"
-  "vc (Aif b c d) Q = (\<lambda>s. vc c Q s & vc d Q s)" 
+  "vc (Aif b c d) Q = (\<lambda>s. vc c Q s & vc d Q s)"
   "vc (Awhile b I c) Q = (\<lambda>s. (I s & ~b s --> Q s) &
                               (I s & b s --> awp c I s) & vc c I s)"
 
@@ -69,49 +69,50 @@
 
 lemma l: "!s. P s --> P s" by fast
 
-lemma vc_sound: "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}"
-apply (induct_tac "c")
+lemma vc_sound: "(!s. vc c Q s) --> |- {awp c Q} astrip c {Q}"
+apply (induct c fixing: Q)
     apply (simp_all (no_asm))
     apply fast
    apply fast
   apply fast
  (* if *)
+ apply atomize
  apply (tactic "Deepen_tac 4 1")
 (* while *)
-apply (intro allI impI) 
+apply atomize
+apply (intro allI impI)
 apply (rule conseq)
   apply (rule l)
  apply (rule While)
  defer
  apply fast
-apply (rule_tac P="awp acom fun2" in conseq)
+apply (rule_tac P="awp c fun2" in conseq)
   apply fast
  apply fast
 apply fast
 done
 
-lemma awp_mono [rule_format (no_asm)]: 
+lemma awp_mono [rule_format (no_asm)]:
   "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
-apply (induct_tac "c")
+apply (induct c)
     apply (simp_all (no_asm_simp))
 apply (rule allI, rule allI, rule impI)
 apply (erule allE, erule allE, erule mp)
 apply (erule allE, erule allE, erule mp, assumption)
 done
 
-
-lemma vc_mono [rule_format (no_asm)]: 
+lemma vc_mono [rule_format (no_asm)]:
   "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
-apply (induct_tac "c")
+apply (induct c)
     apply (simp_all (no_asm_simp))
 apply safe
-apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp) 
+apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp)
 prefer 2 apply assumption
 apply (fast elim: awp_mono)
 done
 
 lemma vc_complete: assumes der: "|- {P}c{Q}"
-  shows "(? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))"
+  shows "(\<exists>ac. astrip ac = c & (\<forall>s. vc ac Q s) & (\<forall>s. P s --> awp ac Q s))"
   (is "? ac. ?Eq P c Q ac")
 using der
 proof induct
@@ -149,9 +150,7 @@
   case conseq thus ?case by(fast elim!: awp_mono vc_mono)
 qed
 
-lemma vcawp_vc_awp: "!Q. vcawp c Q = (vc c Q, awp c Q)"
-apply (induct_tac "c")
-apply (simp_all (no_asm_simp) add: Let_def)
-done
+lemma vcawp_vc_awp: "vcawp c Q = (vc c Q, awp c Q)"
+  by (induct c fixing: Q) (simp_all add: Let_def)
 
 end
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/Library/Quotient.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -163,15 +163,13 @@
 *}
 
 theorem quot_cond_function:
-  "(!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)) ==>
-    (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
-      ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
-    P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
-  (is "PROP ?eq ==> PROP ?cong ==> _ ==> _")
+  assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)"
+    and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
+      ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
+    and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
+  shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
 proof -
-  assume cong: "PROP ?cong"
-  assume "PROP ?eq" and "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
-  hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
+  from eq and P have "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
   also have "... = g a b"
   proof (rule cong)
     show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
@@ -185,18 +183,16 @@
 qed
 
 theorem quot_function:
-  "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
-    (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
-    f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
-proof -
-  case rule_context from this TrueI
-  show ?thesis by (rule quot_cond_function)
-qed
+  assumes "!!X Y. f X Y == g (pick X) (pick Y)"
+    and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
+  shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
+  using prems and TrueI
+  by (rule quot_cond_function)
 
 theorem quot_function':
   "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
     (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
     f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
-  by  (rule quot_function) (simp only: quot_equality)+
+  by (rule quot_function) (simp_all only: quot_equality)
 
 end
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -67,8 +67,9 @@
 
 hide const while_aux
 
-lemma def_while_unfold: assumes fdef: "f == while test do"
-      shows "f x = (if test x then f(do x) else x)"
+lemma def_while_unfold:
+  assumes fdef: "f == while test do"
+  shows "f x = (if test x then f(do x) else x)"
 proof -
   have "f x = while test do x" using fdef by simp
   also have "\<dots> = (if test x then while test do (do x) else x)"
@@ -82,22 +83,16 @@
  The proof rule for @{term while}, where @{term P} is the invariant.
 *}
 
-theorem while_rule_lemma[rule_format]:
-  "[| !!s. P s ==> b s ==> P (c s);
-      !!s. P s ==> \<not> b s ==> Q s;
-      wf {(t, s). P s \<and> b s \<and> t = c s} |] ==>
-    P s --> Q (while b c s)"
-proof -
-  case rule_context
-  assume wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
-  show ?thesis
-    apply (induct s rule: wf [THEN wf_induct])
-    apply simp
-    apply clarify
-    apply (subst while_unfold)
-    apply (simp add: rule_context)
-    done
-qed
+theorem while_rule_lemma:
+  assumes invariant: "!!s. P s ==> b s ==> P (c s)"
+    and terminate: "!!s. P s ==> \<not> b s ==> Q s"
+    and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
+  shows "P s \<Longrightarrow> Q (while b c s)"
+  apply (induct s rule: wf [THEN wf_induct])
+  apply simp
+  apply (subst while_unfold)
+  apply (simp add: invariant terminate)
+  done
 
 theorem while_rule:
   "[| P s;
@@ -148,7 +143,7 @@
 back into equality. *}
 
 lemma seteq: "(A = B) = ((!a : A. a:B) & (!b:B. b:A))"
-by blast
+  by blast
 
 theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
   P {0, 4, 2}"
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/MicroJava/BV/Err.thy
--- a/src/HOL/MicroJava/BV/Err.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -257,15 +257,14 @@
 done
 
 lemma OK_plus_OK_eq_Err_conv [simp]:
-  "\<lbrakk> x:A; y:A; semilat(err A, le r, fe) \<rbrakk> \<Longrightarrow> 
-  ((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))"
+  assumes "x:A" and "y:A" and "semilat(err A, le r, fe)"
+  shows "((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))"
 proof -
   have plus_le_conv3: "\<And>A x y z f r. 
     \<lbrakk> semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \<rbrakk> 
     \<Longrightarrow> x <=_r z \<and> y <=_r z"
     by (rule semilat.plus_le_conv [THEN iffD1])
-  case rule_context
-  thus ?thesis
+  from prems show ?thesis
   apply (rule_tac iffI)
    apply clarify
    apply (drule OK_le_err_OK [THEN iffD2])
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -159,9 +159,9 @@
   done
 
 lemma (in semilat) merges_pres_le_ub:
-shows "\<lbrakk> set ts <= A; set ss <= A;
-         \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts; ss <=[r] ts \<rbrakk>
-  \<Longrightarrow> merges f ps ss <=[r] ts"
+  assumes "set ts <= A" and "set ss <= A"
+    and "\<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts" and "ss <=[r] ts"
+  shows "merges f ps ss <=[r] ts"
 proof -
   { fix t ts ps
     have
@@ -182,8 +182,7 @@
     done 
   } note this [dest]
   
-  case rule_context
-  thus ?thesis by blast
+  from prems show ?thesis by blast
 qed
 
 
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/MicroJava/BV/Product.thy
--- a/src/HOL/MicroJava/BV/Product.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/MicroJava/BV/Product.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -72,15 +72,15 @@
 
 
 lemma plus_eq_Err_conv [simp]:
-  "\<lbrakk> x:A; y:A; semilat(err A, Err.le r, lift2 f) \<rbrakk> 
-  \<Longrightarrow> (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
+  assumes "x:A" and "y:A"
+    and "semilat(err A, Err.le r, lift2 f)"
+  shows "(x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
 proof -
   have plus_le_conv2:
     "\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
                  OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z"
     by (rule semilat.plus_le_conv [THEN iffD1])
-  case rule_context
-  thus ?thesis
+  from prems show ?thesis
   apply (rule_tac iffI)
    apply clarify
    apply (drule OK_le_err_OK [THEN iffD2])
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/Product_Type.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -223,14 +223,13 @@
   done
 
 lemma Pair_inject:
-  "(a, b) = (a', b') ==> (a = a' ==> b = b' ==> R) ==> R"
-proof -
-  case rule_context [unfolded Pair_def]
-  show ?thesis
-    apply (rule inj_on_Abs_Prod [THEN inj_onD, THEN Pair_Rep_inject, THEN conjE])
-    apply (rule rule_context ProdI)+
-    .
-qed
+  assumes "(a, b) = (a', b')"
+    and "a = a' ==> b = b' ==> R"
+  shows R
+  apply (insert prems [unfolded Pair_def])
+  apply (rule inj_on_Abs_Prod [THEN inj_onD, THEN Pair_Rep_inject, THEN conjE])
+  apply (assumption | rule ProdI)+
+  done
 
 lemma Pair_eq [iff]: "((a, b) = (a', b')) = (a = a' & b = b')"
   by (blast elim!: Pair_inject)
@@ -507,11 +506,11 @@
 lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: split c p"
 by (simp only: split_tupled_all, simp)
 
-lemma mem_splitE: "[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q"
-proof -
-  case rule_context [unfolded split_def]
-  show ?thesis by (rule rule_context surjective_pairing)+
-qed
+lemma mem_splitE:
+  assumes major: "z: split c p"
+    and cases: "!!x y. [| p = (x,y); z: c x y |] ==> Q"
+  shows Q
+  by (rule major [unfolded split_def] cases surjective_pairing)+
 
 declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
 declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
@@ -533,15 +532,14 @@
 *}
 
 lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
-by (rule ext, fast)
+  by (rule ext) fast
 
 lemma split_eta_SetCompr2 [simp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
-by (rule ext, fast)
+  by (rule ext) fast
 
 lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
   -- {* Allows simplifications of nested splits in case of independent predicates. *}
-  apply (rule ext, blast)
-  done
+  by (rule ext) blast
 
 (* Do NOT make this a simp rule as it
    a) only helps in special situations
@@ -549,7 +547,7 @@
 *)
 lemma split_comp_eq: 
 "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
-by (rule ext, auto)
+  by (rule ext) auto
 
 lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)"
   by blast
@@ -595,20 +593,15 @@
   done
 
 lemma prod_fun_imageE [elim!]:
-  "[| c: (prod_fun f g)`r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P
-    |] ==> P"
-proof -
-  case rule_context
-  assume major: "c: (prod_fun f g)`r"
-  show ?thesis
-    apply (rule major [THEN imageE])
-    apply (rule_tac p = x in PairE)
-    apply (rule rule_context)
-     prefer 2
-     apply blast
-    apply (blast intro: prod_fun)
-    done
-qed
+  assumes major: "c: (prod_fun f g)`r"
+    and cases: "!!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P"
+  shows P
+  apply (rule major [THEN imageE])
+  apply (rule_tac p = x in PairE)
+  apply (rule cases)
+   apply (blast intro: prod_fun)
+  apply blast
+  done
 
 
 constdefs
@@ -619,10 +612,10 @@
  "upd_snd f == prod_fun id f"
 
 lemma upd_fst_conv [simp]: "upd_fst f (x,y) = (f x,y)" 
-by (simp add: upd_fst_def)
+  by (simp add: upd_fst_def)
 
 lemma upd_snd_conv [simp]: "upd_snd f (x,y) = (x,f y)" 
-by (simp add: upd_snd_def)
+  by (simp add: upd_snd_def)
 
 text {*
   \bigskip Disjoint union of a family of sets -- Sigma.
@@ -644,10 +637,10 @@
 *}
 
 lemma SigmaD1: "(a, b) : Sigma A B ==> a : A"
-by blast
+  by blast
 
 lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a"
-by blast
+  by blast
 
 lemma SigmaE2:
     "[| (a, b) : Sigma A B;
@@ -658,7 +651,7 @@
 lemma Sigma_cong:
      "\<lbrakk>A = B; !!x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk>
       \<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
-by auto
+  by auto
 
 lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
   by blast
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/Real/Rational.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -332,16 +332,13 @@
 qed
 
 theorem rat_function:
-  "(!!q r. f q r == g (fraction_of q) (fraction_of r)) ==>
-    (!!a b a' b' c d c' d'.
+  assumes "!!q r. f q r == g (fraction_of q) (fraction_of r)"
+    and "!!a b a' b' c d c' d'.
       \<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor> ==> \<lfloor>fract c d\<rfloor> = \<lfloor>fract c' d'\<rfloor> ==>
       b \<noteq> 0 ==> b' \<noteq> 0 ==> d \<noteq> 0 ==> d' \<noteq> 0 ==>
-      g (fract a b) (fract c d) = g (fract a' b') (fract c' d')) ==>
-    f (Fract a b) (Fract c d) = g (fract a b) (fract c d)"
-proof -
-  case rule_context from this TrueI
-  show ?thesis by (rule rat_cond_function)
-qed
+      g (fract a b) (fract c d) = g (fract a' b') (fract c' d')"
+  shows "f (Fract a b) (Fract c d) = g (fract a b) (fract c d)"
+  using prems and TrueI by (rule rat_cond_function)
 
 
 subsubsection {* Standard operations on rational numbers *}
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/Transitive_Closure.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -81,7 +81,7 @@
 lemmas rtrancl_induct2 =
   rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
                  consumes 1, case_names refl step]
- 
+
 lemma trans_rtrancl: "trans(r^*)"
   -- {* transitivity of transitive closure!! -- by induction *}
 proof (rule transI)
@@ -94,21 +94,17 @@
 lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
 
 lemma rtranclE:
-  "[| (a::'a,b) : r^*;  (a = b) ==> P;
-      !!y.[| (a,y) : r^*; (y,b) : r |] ==> P
-   |] ==> P"
+  assumes major: "(a::'a,b) : r^*"
+    and cases: "(a = b) ==> P"
+      "!!y. [| (a,y) : r^*; (y,b) : r |] ==> P"
+  shows P
   -- {* elimination of @{text rtrancl} -- by induction on a special formula *}
-proof -
-  assume major: "(a::'a,b) : r^*"
-  case rule_context
-  show ?thesis
-    apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")
-     apply (rule_tac [2] major [THEN rtrancl_induct])
-      prefer 2 apply (blast!)
-      prefer 2 apply (blast!)
-    apply (erule asm_rl exE disjE conjE prems)+
-    done
-qed
+  apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")
+   apply (rule_tac [2] major [THEN rtrancl_induct])
+    prefer 2 apply blast
+   prefer 2 apply blast
+  apply (erule asm_rl exE disjE conjE cases)+
+  done
 
 lemma converse_rtrancl_into_rtrancl:
   "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*"
@@ -187,21 +183,16 @@
                  consumes 1, case_names refl step]
 
 lemma converse_rtranclE:
-  "[| (x,z):r^*;
-      x=z ==> P;
-      !!y. [| (x,y):r; (y,z):r^* |] ==> P
-   |] ==> P"
-proof -
-  assume major: "(x,z):r^*"
-  case rule_context
-  show ?thesis
-    apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
-     apply (rule_tac [2] major [THEN converse_rtrancl_induct])
-      prefer 2 apply iprover
-     prefer 2 apply iprover
-    apply (erule asm_rl exE disjE conjE prems)+
-    done
-qed
+  assumes major: "(x,z):r^*"
+    and cases: "x=z ==> P"
+      "!!y. [| (x,y):r; (y,z):r^* |] ==> P"
+  shows P
+  apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
+   apply (rule_tac [2] major [THEN converse_rtrancl_induct])
+    prefer 2 apply iprover
+   prefer 2 apply iprover
+  apply (erule asm_rl exE disjE conjE cases)+
+  done
 
 ML_setup {*
   bind_thm ("converse_rtranclE2", split_rule
@@ -258,17 +249,12 @@
 qed
 
 lemma trancl_trans_induct:
-  "[| (x,y) : r^+;
-      !!x y. (x,y) : r ==> P x y;
-      !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z
-   |] ==> P x y"
+  assumes major: "(x,y) : r^+"
+    and cases: "!!x y. (x,y) : r ==> P x y"
+      "!!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z"
+  shows "P x y"
   -- {* Another induction rule for trancl, incorporating transitivity *}
-proof -
-  assume major: "(x,y) : r^+"
-  case rule_context
-  show ?thesis
-    by (iprover intro: r_into_trancl major [THEN trancl_induct] prems)
-qed
+  by (iprover intro: r_into_trancl major [THEN trancl_induct] cases)
 
 inductive_cases tranclE: "(a, b) : r^+"
 
@@ -279,9 +265,9 @@
   -- {* Transitivity of @{term "r^+"} *}
 proof (rule transI)
   fix x y z
-  assume "(x, y) \<in> r^+"
+  assume xy: "(x, y) \<in> r^+"
   assume "(y, z) \<in> r^+"
-  thus "(x, z) \<in> r^+" by induct (iprover!)+
+  thus "(x, z) \<in> r^+" by induct (insert xy, iprover)+
 qed
 
 lemmas trancl_trans = trans_trancl [THEN transD, standard]
@@ -323,19 +309,15 @@
     intro!: trancl_converseI trancl_converseD)
 
 lemma converse_trancl_induct:
-  "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y);
-      !!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y) |]
-    ==> P(a)"
-proof -
-  assume major: "(a,b) : r^+"
-  case rule_context
-  show ?thesis
-    apply (rule major [THEN converseI, THEN trancl_converseI [THEN trancl_induct]])
-     apply (rule prems)
-     apply (erule converseD)
-    apply (blast intro: prems dest!: trancl_converseD)
-    done
-qed
+  assumes major: "(a,b) : r^+"
+    and cases: "!!y. (y,b) : r ==> P(y)"
+      "!!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y)"
+  shows "P a"
+  apply (rule major [THEN converseI, THEN trancl_converseI [THEN trancl_induct]])
+   apply (rule cases)
+   apply (erule converseD)
+  apply (blast intro: prems dest!: trancl_converseD)
+  done
 
 lemma tranclD: "(x, y) \<in> R^+ ==> EX z. (x, z) \<in> R \<and> (z, y) \<in> R^*"
   apply (erule converse_trancl_induct, auto)
@@ -343,15 +325,14 @@
   done
 
 lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"
-by(blast elim: tranclE dest: trancl_into_rtrancl)
+  by (blast elim: tranclE dest: trancl_into_rtrancl)
 
 lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y"
   by (blast dest: r_into_trancl)
 
 lemma trancl_subset_Sigma_aux:
     "(a, b) \<in> r^* ==> r \<subseteq> A \<times> A ==> a = b \<or> a \<in> A"
-  apply (erule rtrancl_induct, auto)
-  done
+  by (induct rule: rtrancl_induct) auto
 
 lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A"
   apply (rule subsetI)
@@ -477,16 +458,16 @@
     val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl";
     val rtrancl_trans = thm "rtrancl_trans";
 
-  fun decomp (Trueprop $ t) = 
-    let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) = 
-	let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
-	      | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
-	      | decr r = (r,"r");
-	    val (rel,r) = decr rel;
-	in SOME (a,b,rel,r) end
-      | dec _ =  NONE 
+  fun decomp (Trueprop $ t) =
+    let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
+        let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
+              | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
+              | decr r = (r,"r");
+            val (rel,r) = decr rel;
+        in SOME (a,b,rel,r) end
+      | dec _ =  NONE
     in dec t end;
-  
+
   end); (* struct *)
 
 change_simpset (fn ss => ss
@@ -499,7 +480,7 @@
 
 method_setup trancl =
   {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trancl_tac)) *}
-  {* simple transitivity reasoner *}	    
+  {* simple transitivity reasoner *}
 method_setup rtrancl =
   {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (rtrancl_tac)) *}
   {* simple transitivity reasoner *}
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/Unix/Unix.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -255,16 +255,16 @@
     lookup root path = Some file"
   by (simp add: access_def split: option.splits if_splits)
 
-lemma access_update_other: "path' \<parallel> path \<Longrightarrow>
-  access (update path' opt root) path uid perms = access root path uid perms"
+lemma access_update_other:
+  assumes parallel: "path' \<parallel> path"
+  shows "access (update path' opt root) path uid perms = access root path uid perms"
 proof -
-  assume "path' \<parallel> path"
-  then obtain y z xs ys zs where
+  from parallel obtain y z xs ys zs where
       "y \<noteq> z" and "path' = xs @ y # ys" and "path = xs @ z # zs"
     by (blast dest: parallel_decomp)
-  hence "lookup (update path' opt root) path = lookup root path"
+  then have "lookup (update path' opt root) path = lookup root path"
     by (blast intro: lookup_update_other)
-  thus ?thesis by (simp only: access_def)
+  then show ?thesis by (simp only: access_def)
 qed
 
 
@@ -437,36 +437,35 @@
   relation.
 *}
 
-theorem transition_uniq: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root \<midarrow>x\<rightarrow> root'' \<Longrightarrow> root' = root''"
-proof -
-  assume root: "root \<midarrow>x\<rightarrow> root'"
-  assume "root \<midarrow>x\<rightarrow> root''"
-  thus "root' = root''"
-  proof cases
-    case read
-    with root show ?thesis by cases auto
-  next
-    case write
-    with root show ?thesis by cases auto
-  next
-    case chmod
-    with root show ?thesis by cases auto
-  next
-    case creat
-    with root show ?thesis by cases auto
-  next
-    case unlink
-    with root show ?thesis by cases auto
-  next
-    case mkdir
-    with root show ?thesis by cases auto
-  next
-    case rmdir
-    with root show ?thesis by cases auto
-  next
-    case readdir
-    with root show ?thesis by cases fastsimp+
-  qed
+theorem transition_uniq:
+  assumes root': "root \<midarrow>x\<rightarrow> root'"
+    and root'': "root \<midarrow>x\<rightarrow> root''"
+  shows "root' = root''"
+  using root''
+proof cases
+  case read
+  with root' show ?thesis by cases auto
+next
+  case write
+  with root' show ?thesis by cases auto
+next
+  case chmod
+  with root' show ?thesis by cases auto
+next
+  case creat
+  with root' show ?thesis by cases auto
+next
+  case unlink
+  with root' show ?thesis by cases auto
+next
+  case mkdir
+  with root' show ?thesis by cases auto
+next
+  case rmdir
+  with root' show ?thesis by cases auto
+next
+  case readdir
+  with root' show ?thesis by cases fastsimp+
 qed
 
 text {*
@@ -476,24 +475,20 @@
 *}
 
 theorem transition_type_safe:
-  "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> \<exists>att dir. root = Env att dir
-    \<Longrightarrow> \<exists>att dir. root' = Env att dir"
-proof -
-  assume tr: "root \<midarrow>x\<rightarrow> root'"
-  assume inv: "\<exists>att dir. root = Env att dir"
-  show ?thesis
-  proof (cases "path_of x")
-    case Nil
-    with tr inv show ?thesis
-      by cases (auto simp add: access_def split: if_splits)
-  next
-    case Cons
-    from tr obtain opt where
-        "root' = root \<or> root' = update (path_of x) opt root"
-      by cases auto
-    with inv Cons show ?thesis
-      by (auto simp add: update_eq split: list.splits)
-  qed
+  assumes tr: "root \<midarrow>x\<rightarrow> root'"
+    and inv: "\<exists>att dir. root = Env att dir"
+  shows "\<exists>att dir. root' = Env att dir"
+proof (cases "path_of x")
+  case Nil
+  with tr inv show ?thesis
+    by cases (auto simp add: access_def split: if_splits)
+next
+  case Cons
+  from tr obtain opt where
+      "root' = root \<or> root' = update (path_of x) opt root"
+    by cases auto
+  with inv Cons show ?thesis
+    by (auto simp add: update_eq split: list.splits)
 qed
 
 text {*
@@ -539,21 +534,21 @@
 lemma transitions_nil_eq: "root =[]\<Rightarrow> root' = (root = root')"
 proof
   assume "root =[]\<Rightarrow> root'"
-  thus "root = root'" by cases simp_all
+  then show "root = root'" by cases simp_all
 next
   assume "root = root'"
-  thus "root =[]\<Rightarrow> root'" by (simp only: transitions.nil)
+  then show "root =[]\<Rightarrow> root'" by (simp only: transitions.nil)
 qed
 
 lemma transitions_cons_eq:
   "root =(x # xs)\<Rightarrow> root'' = (\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root'')"
 proof
   assume "root =(x # xs)\<Rightarrow> root''"
-  thus "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''"
+  then show "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''"
     by cases auto
 next
   assume "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''"
-  thus "root =(x # xs)\<Rightarrow> root''"
+  then show "root =(x # xs)\<Rightarrow> root''"
     by (blast intro: transitions.cons)
 qed
 
@@ -568,13 +563,13 @@
   by (simp add: transitions_nil_eq)
 
 lemma transitions_consD:
-  "root =(x # xs)\<Rightarrow> root'' \<Longrightarrow> root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root''"
+  assumes list: "root =(x # xs)\<Rightarrow> root''"
+    and hd: "root \<midarrow>x\<rightarrow> root'"
+  shows "root' =xs\<Rightarrow> root''"
 proof -
-  assume "root =(x # xs)\<Rightarrow> root''"
-  then obtain r' where r': "root \<midarrow>x\<rightarrow> r'" and root'': "r' =xs\<Rightarrow> root''"
+  from list obtain r' where r': "root \<midarrow>x\<rightarrow> r'" and root'': "r' =xs\<Rightarrow> root''"
     by cases simp_all
-  assume "root \<midarrow>x\<rightarrow> root'"
-  with r' have "r' = root'" by (rule transition_uniq)
+  from r' hd have "r' = root'" by (rule transition_uniq)
   with root'' show "root' =xs\<Rightarrow> root''" by simp
 qed
 
@@ -586,26 +581,20 @@
 *}
 
 lemma transitions_invariant:
-  "(\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow>  P x \<Longrightarrow> Q r') \<Longrightarrow>
-    root =xs\<Rightarrow> root' \<Longrightarrow> Q root \<Longrightarrow> \<forall>x \<in> set xs. P x \<Longrightarrow> Q root'"
-proof -
-  assume r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow>  P x \<Longrightarrow> Q r'"
-  assume "root =xs\<Rightarrow> root'"
-  thus "Q root \<Longrightarrow> (\<forall>x \<in> set xs. P x) \<Longrightarrow> Q root'" (is "PROP ?P root xs root'")
-  proof (induct root xs root')
-    fix root assume "Q root"
-    thus "Q root" .
-  next
-    fix root root' root'' and x xs
-    assume root': "root \<midarrow>x\<rightarrow> root'"
-    assume hyp: "PROP ?P root' xs root''"
-    assume Q: "Q root"
-    assume P: "\<forall>x \<in> set (x # xs). P x"
-    hence "P x" by simp
-    with root' Q have Q': "Q root'" by (rule r)
-    from P have "\<forall>x \<in> set xs. P x" by simp
-    with Q' show "Q root''" by (rule hyp)
-  qed
+  assumes r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow>  P x \<Longrightarrow> Q r'"
+    and trans: "root =xs\<Rightarrow> root'"
+  shows "Q root \<Longrightarrow> \<forall>x \<in> set xs. P x \<Longrightarrow> Q root'"
+  using trans
+proof induct
+  case nil
+  show ?case by assumption
+next
+  case (cons root root' root'' x xs)
+  note P = `\<forall>x \<in> set (x # xs). P x`
+  then have "P x" by simp
+  with `root \<midarrow>x\<rightarrow> root'` and `Q root` have Q': "Q root'" by (rule r)
+  from P have "\<forall>x \<in> set xs. P x" by simp
+  with Q' show "Q root''" by (rule cons.hyps)
 qed
 
 text {*
@@ -675,31 +664,23 @@
   executed we may destruct it backwardly into individual transitions.
 *}
 
-lemma can_exec_snocD: "\<And>root. can_exec root (xs @ [y])
+lemma can_exec_snocD: "can_exec root (xs @ [y])
     \<Longrightarrow> \<exists>root' root''. root =xs\<Rightarrow> root' \<and> root' \<midarrow>y\<rightarrow> root''"
-  (is "PROP ?P xs" is "\<And>root. ?A root xs \<Longrightarrow> ?C root xs")
-proof (induct xs)
-  fix root
-  {
-    assume "?A root []"
-    thus "?C root []"
-      by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
-  next
-    fix x xs
-    assume hyp: "PROP ?P xs"
-    assume asm: "?A root (x # xs)"
-    show "?C root (x # xs)"
-    proof -
-      from asm obtain r root'' where x: "root \<midarrow>x\<rightarrow> r" and
-          xs_y: "r =(xs @ [y])\<Rightarrow> root''"
-        by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
-      from xs_y hyp obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'"
-        by (unfold can_exec_def) blast
-      from x xs have "root =(x # xs)\<Rightarrow> root'"
-        by (rule transitions.cons)
-      with y show ?thesis by blast
-    qed
-  }
+proof (induct xs fixing: root)
+  case Nil
+  then show ?case
+    by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
+next
+  case (Cons x xs)
+  from `can_exec root ((x # xs) @ [y])` obtain r root'' where
+      x: "root \<midarrow>x\<rightarrow> r" and
+      xs_y: "r =(xs @ [y])\<Rightarrow> root''"
+    by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
+  from xs_y Cons.hyps obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'"
+    by (unfold can_exec_def) blast
+  from x xs have "root =(x # xs)\<Rightarrow> root'"
+    by (rule transitions.cons)
+  with y show ?case by blast
 qed
 
 
@@ -803,16 +784,12 @@
 *}
 
 theorem general_procedure:
-  "(\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False) \<Longrightarrow>
-    (\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root) \<Longrightarrow>
-    (\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow>  P x \<Longrightarrow> Q r') \<Longrightarrow>
-    init users =bs\<Rightarrow> root \<Longrightarrow>
-      \<not> (\<exists>xs. (\<forall>x \<in> set xs. P x) \<and> can_exec root (xs @ [y]))"
+  assumes cannot_y: "\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False"
+    and init_inv: "\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root"
+    and preserve_inv: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'"
+    and init_result: "init users =bs\<Rightarrow> root"
+  shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. P x) \<and> can_exec root (xs @ [y]))"
 proof -
-  assume cannot_y: "\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False"
-  assume init_inv: "\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root"
-  assume preserve_inv: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'"
-  assume init_result: "init users =bs\<Rightarrow> root"
   {
     fix xs
     assume Ps: "\<forall>x \<in> set xs. P x"
@@ -825,7 +802,7 @@
       by (rule transitions_invariant)
     from this y have False by (rule cannot_y)
   }
-  thus ?thesis by blast
+  then show ?thesis by blast
 qed
 
 text {*
@@ -930,38 +907,36 @@
   we just have to inspect rather special cases.
 *}
 
-lemma (in invariant)
-  cannot_rmdir: "invariant root bogus_path \<Longrightarrow>
-    root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root' \<Longrightarrow> False"
+lemma (in invariant) cannot_rmdir:
+  assumes inv: "invariant root bogus_path"
+    and rmdir: "root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root'"
+  shows False
 proof -
-  assume "invariant root bogus_path"
-  then obtain "file" where "access root bogus_path user\<^isub>1 {} = Some file"
+  from inv obtain "file" where "access root bogus_path user\<^isub>1 {} = Some file"
     by (unfold invariant_def) blast
   moreover
-  assume "root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root'"
-  then obtain att where
+  from rmdir obtain att where
       "access root [user\<^isub>1, name\<^isub>1] user\<^isub>1 {} = Some (Env att empty)"
     by cases auto
-  hence "access root ([user\<^isub>1, name\<^isub>1] @ [name\<^isub>2]) user\<^isub>1 {} = empty name\<^isub>2"
+  then have "access root ([user\<^isub>1, name\<^isub>1] @ [name\<^isub>2]) user\<^isub>1 {} = empty name\<^isub>2"
     by (simp only: access_empty_lookup lookup_append_some) simp
   ultimately show False by (simp add: bogus_path_def)
 qed
 
 lemma (in invariant)
-  init_invariant: "init users =bogus\<Rightarrow> root \<Longrightarrow> invariant root bogus_path"
-proof -
-  note eval = facts access_def init_def
-  case rule_context thus ?thesis
-    apply (unfold bogus_def bogus_path_def)
-    apply (drule transitions_consD, rule transition.intros,
+  assumes init: "init users =bogus\<Rightarrow> root"
+  notes eval = facts access_def init_def
+  shows init_invariant: "invariant root bogus_path"
+  using init
+  apply (unfold bogus_def bogus_path_def)
+  apply (drule transitions_consD, rule transition.intros,
       (force simp add: eval)+, (simp add: eval)?)+
-      -- "evaluate all operations"
-    apply (drule transitions_nilD)
-      -- "reach final result"
-    apply (simp add: invariant_def eval)
-      -- "check the invariant"
-    done
-qed
+    -- "evaluate all operations"
+  apply (drule transitions_nilD)
+    -- "reach final result"
+  apply (simp add: invariant_def eval)
+    -- "check the invariant"
+  done
 
 text {*
   \medskip At last we are left with the main effort to show that the
@@ -971,14 +946,12 @@
   required here.
 *}
 
-lemma (in invariant)
-  preserve_invariant: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow>
-    invariant root path \<Longrightarrow> uid_of x = user\<^isub>1 \<Longrightarrow> invariant root' path"
+lemma (in invariant) preserve_invariant:
+  assumes tr: "root \<midarrow>x\<rightarrow> root'"
+    and inv: "invariant root path"
+    and uid: "uid_of x = user\<^isub>1"
+  shows "invariant root' path"
 proof -
-  assume tr: "root \<midarrow>x\<rightarrow> root'"
-  assume inv: "invariant root path"
-  assume uid: "uid_of x = user\<^isub>1"
-
   from inv obtain att dir where
       inv1: "access root path user\<^isub>1 {} = Some (Env att dir)" and
       inv2: "dir \<noteq> empty" and
@@ -1019,7 +992,7 @@
         with tr uid inv2 inv3 lookup changed path and user\<^isub>1_not_root
         have False
           by cases (auto simp add: access_empty_lookup dest: access_some_lookup)
-        thus ?thesis ..
+        then show ?thesis ..
       next
         fix z zs assume ys: "ys = z # zs"
         have "lookup root' path = lookup root path"
@@ -1085,7 +1058,7 @@
               have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or>
                   lookup root ((path @ [y]) @ us) \<noteq> None"
                 by cases (auto dest: access_some_lookup)
-              thus ?thesis by (blast dest!: lookup_some_append)
+              then show ?thesis by (blast dest!: lookup_some_append)
             qed
             finally show ?thesis .
           qed
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/ZF/Induct/Brouwer.thy
--- a/src/ZF/Induct/Brouwer.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/ZF/Induct/Brouwer.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -22,24 +22,20 @@
   by (fast intro!: brouwer.intros [unfolded brouwer.con_defs]
     elim: brouwer.cases [unfolded brouwer.con_defs])
 
-lemma brouwer_induct2:
-  "[| b \<in> brouwer;
-      P(Zero);
-      !!b. [| b \<in> brouwer;  P(b) |] ==> P(Suc(b));
-      !!h. [| h \<in> nat -> brouwer;  \<forall>i \<in> nat. P(h`i)
-           |] ==> P(Lim(h))
-   |] ==> P(b)"
+lemma brouwer_induct2 [consumes 1, case_names Zero Suc Lim]:
+  assumes b: "b \<in> brouwer"
+    and cases:
+      "P(Zero)"
+      "!!b. [| b \<in> brouwer;  P(b) |] ==> P(Suc(b))"
+      "!!h. [| h \<in> nat -> brouwer;  \<forall>i \<in> nat. P(h`i) |] ==> P(Lim(h))"
+  shows "P(b)"
   -- {* A nicer induction rule than the standard one. *}
-proof -
-  case rule_context
-  assume "b \<in> brouwer"
-  thus ?thesis
-    apply induct
-    apply (assumption | rule rule_context)+
+  using b
+  apply induct
+    apply (assumption | rule cases)+
      apply (fast elim: fun_weaken_type)
     apply (fast dest: apply_type)
     done
-qed
 
 
 subsection {* The Martin-Löf wellordering type *}
@@ -58,22 +54,17 @@
     elim: Well.cases [unfolded Well.con_defs])
 
 
-lemma Well_induct2:
-  "[| w \<in> Well(A, B);
-      !!a f. [| a \<in> A;  f \<in> B(a) -> Well(A,B);  \<forall>y \<in> B(a). P(f`y)
-           |] ==> P(Sup(a,f))
-   |] ==> P(w)"
+lemma Well_induct2 [consumes 1, case_names step]:
+  assumes w: "w \<in> Well(A, B)"
+    and step: "!!a f. [| a \<in> A;  f \<in> B(a) -> Well(A,B);  \<forall>y \<in> B(a). P(f`y) |] ==> P(Sup(a,f))"
+  shows "P(w)"
   -- {* A nicer induction rule than the standard one. *}
-proof -
-  case rule_context
-  assume "w \<in> Well(A, B)"
-  thus ?thesis
-    apply induct
-    apply (assumption | rule rule_context)+
-     apply (fast elim: fun_weaken_type)
-    apply (fast dest: apply_type)
-    done
-qed
+  using w
+  apply induct
+  apply (assumption | rule step)+
+   apply (fast elim: fun_weaken_type)
+  apply (fast dest: apply_type)
+  done
 
 lemma Well_bool_unfold: "Well(bool, \<lambda>x. x) = 1 + (1 -> Well(bool, \<lambda>x. x))"
   -- {* In fact it's isomorphic to @{text nat}, but we need a recursion operator *}
diff -r d93fdf00f8a6 -r 2bffdf62fe7f src/ZF/Induct/Ntree.thy
--- a/src/ZF/Induct/Ntree.thy	Thu Dec 08 20:15:41 2005 +0100
+++ b/src/ZF/Induct/Ntree.thy	Thu Dec 08 20:15:50 2005 +0100
@@ -49,42 +49,36 @@
   by (blast intro: ntree.intros [unfolded ntree.con_defs]
     elim: ntree.cases [unfolded ntree.con_defs])
 
-lemma ntree_induct [induct set: ntree]:
-  "[| t \<in> ntree(A);
-      !!x n h. [| x \<in> A;  n \<in> nat;  h \<in> n -> ntree(A);  \<forall>i \<in> n. P(h`i)
-               |] ==> P(Branch(x,h))
-   |] ==> P(t)"
+lemma ntree_induct [consumes 1, case_names Branch, induct set: ntree]:
+  assumes t: "t \<in> ntree(A)"
+    and step: "!!x n h. [| x \<in> A;  n \<in> nat;  h \<in> n -> ntree(A);  \<forall>i \<in> n. P(h`i)
+      |] ==> P(Branch(x,h))"
+  shows "P(t)"
   -- {* A nicer induction rule than the standard one. *}
-proof -
-  case rule_context
-  assume "t \<in> ntree(A)"
-  thus ?thesis
-    apply induct
-    apply (erule UN_E)
-    apply (assumption | rule rule_context)+
-     apply (fast elim: fun_weaken_type)
-    apply (fast dest: apply_type)
-    done
-qed
+  using t
+  apply induct
+  apply (erule UN_E)
+  apply (assumption | rule step)+
+   apply (fast elim: fun_weaken_type)
+  apply (fast dest: apply_type)
+  done
 
-lemma ntree_induct_eqn:
-  "[| t \<in> ntree(A);  f \<in> ntree(A)->B;  g \<in> ntree(A)->B;
-      !!x n h. [| x \<in> A;  n \<in> nat;  h \<in> n -> ntree(A);  f O h = g O h |] ==>
-               f ` Branch(x,h) = g ` Branch(x,h)
-   |] ==> f`t=g`t"
+lemma ntree_induct_eqn [consumes 1]:
+  assumes t: "t \<in> ntree(A)"
+    and f: "f \<in> ntree(A)->B"
+    and g: "g \<in> ntree(A)->B"
+    and step: "!!x n h. [| x \<in> A;  n \<in> nat;  h \<in> n -> ntree(A);  f O h = g O h |] ==>
+      f ` Branch(x,h) = g ` Branch(x,h)"
+  shows "f`t=g`t"
   -- {* Induction on @{term "ntree(A)"} to prove an equation *}
-proof -
-  case rule_context
-  assume "t \<in> ntree(A)"
-  thus ?thesis
-    apply induct
-    apply (assumption | rule rule_context)+
-    apply (insert rule_context)
-    apply (rule fun_extension)
-      apply (assumption | rule comp_fun)+
-    apply (simp add: comp_fun_apply)
+  using t
+  apply induct
+  apply (assumption | rule step)+
+  apply (insert f g)
+  apply (rule fun_extension)
+  apply (assumption | rule comp_fun)+
+  apply (simp add: comp_fun_apply)
   done
-qed
 
 text {*
   \medskip Lemmas to justify using @{text Ntree} in other recursive
@@ -127,9 +121,8 @@
   by (simp add: ntree_copy_def ntree_rec_Branch)
 
 lemma ntree_copy_is_ident: "z \<in> ntree(A) ==> ntree_copy(z) = z"
-  apply (induct_tac z)
-  apply (auto simp add: domain_of_fun Pi_Collect_iff fun_is_function)
-  done
+  by (induct z set: ntree)
+    (auto simp add: domain_of_fun Pi_Collect_iff fun_is_function)
 
 
 text {*
@@ -140,25 +133,21 @@
   by (fast intro!: maptree.intros [unfolded maptree.con_defs]
     elim: maptree.cases [unfolded maptree.con_defs])
 
-lemma maptree_induct [induct set: maptree]:
-  "[| t \<in> maptree(A);
-      !!x n h. [| x \<in> A;  h \<in> maptree(A) -||> maptree(A);
+lemma maptree_induct [consumes 1, induct set: maptree]:
+  assumes t: "t \<in> maptree(A)"
+    and step: "!!x n h. [| x \<in> A;  h \<in> maptree(A) -||> maptree(A);
                   \<forall>y \<in> field(h). P(y)
-               |] ==> P(Sons(x,h))
-   |] ==> P(t)"
+               |] ==> P(Sons(x,h))"
+  shows "P(t)"
   -- {* A nicer induction rule than the standard one. *}
-proof -
-  case rule_context
-  assume "t \<in> maptree(A)"
-  thus ?thesis
-    apply induct
-    apply (assumption | rule rule_context)+
-     apply (erule Collect_subset [THEN FiniteFun_mono1, THEN subsetD])
-    apply (drule FiniteFun.dom_subset [THEN subsetD])
-    apply (drule Fin.dom_subset [THEN subsetD])
-    apply fast
-    done
-qed
+  using t
+  apply induct
+  apply (assumption | rule step)+
+  apply (erule Collect_subset [THEN FiniteFun_mono1, THEN subsetD])
+  apply (drule FiniteFun.dom_subset [THEN subsetD])
+  apply (drule Fin.dom_subset [THEN subsetD])
+  apply fast
+  done
 
 
 text {*
@@ -169,22 +158,18 @@
   by (fast intro!: maptree2.intros [unfolded maptree2.con_defs]
     elim: maptree2.cases [unfolded maptree2.con_defs])
 
-lemma maptree2_induct [induct set: maptree2]:
-  "[| t \<in> maptree2(A, B);
-      !!x n h. [| x \<in> A;  h \<in> B -||> maptree2(A,B);  \<forall>y \<in> range(h). P(y)
-               |] ==> P(Sons2(x,h))
-   |] ==> P(t)"
-proof -
-  case rule_context
-  assume "t \<in> maptree2(A, B)"
-  thus ?thesis
-    apply induct
-    apply (assumption | rule rule_context)+
-     apply (erule FiniteFun_mono [OF subset_refl Collect_subset, THEN subsetD])
-    apply (drule FiniteFun.dom_subset [THEN subsetD])
-    apply (drule Fin.dom_subset [THEN subsetD])
-    apply fast
-    done
-qed
+lemma maptree2_induct [consumes 1, induct set: maptree2]:
+  assumes t: "t \<in> maptree2(A, B)"
+    and step: "!!x n h. [| x \<in> A;  h \<in> B -||> maptree2(A,B);  \<forall>y \<in> range(h). P(y)
+               |] ==> P(Sons2(x,h))"
+  shows "P(t)"
+  using t
+  apply induct
+  apply (assumption | rule step)+
+   apply (erule FiniteFun_mono [OF subset_refl Collect_subset, THEN subsetD])
+   apply (drule FiniteFun.dom_subset [THEN subsetD])
+   apply (drule Fin.dom_subset [THEN subsetD])
+   apply fast
+   done
 
 end