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 {*