# HG changeset patch
# User nipkow
# Date 1019814421 -7200
# Node ID 8ed413a57bdcec8045db7b025401157907ae1de3
# Parent  643fce75f6cddb9e3ea91968a73a7988cc8540cc
New machine architecture and other direction of compiler proof.

diff -r 643fce75f6cd -r 8ed413a57bdc src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Thu Apr 25 17:36:29 2002 +0200
+++ b/src/HOL/IMP/Compiler.thy	Fri Apr 26 11:47:01 2002 +0200
@@ -4,46 +4,7 @@
     Copyright   1996 TUM
 *)
 
-header "A Simple Compiler"
-
-theory Compiler = Natural:
-
-subsection "An abstract, simplistic machine"
-
-text {* There are only three instructions: *}
-datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat
-
-text {* We describe execution of programs in the machine by
-  an operational (small step) semantics:
-*}
-consts  stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
-
-syntax
-  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
-               ("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50)
-  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
-               ("_ |-/ <_,_>/ -*-> <_,_>" [50,0,0,0,0] 50)
-
-syntax (xsymbols)
-  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
-               ("_ \<turnstile> \<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)
-  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
-               ("_ \<turnstile>/ \<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)
-
-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)^*)"
-
-inductive "stepa1 P"
-intros
-ASIN[simp]:
-  "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s[x\<mapsto> a s],Suc n\<rangle>"
-JMPFT[simp,intro]:
-  "\<lbrakk> n<size P; P!n = JMPF b i;  b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,Suc n\<rangle>"
-JMPFF[simp,intro]:
-  "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,m\<rangle>"
-JMPB[simp]:
-  "\<lbrakk> n<size P; P!n = JMPB i; i <= n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,j\<rangle>"
+theory Compiler = Machines:
 
 subsection "The compiler"
 
@@ -53,216 +14,287 @@
 "compile (x:==a) = [ASIN x a]"
 "compile (c1;c2) = compile c1 @ compile c2"
 "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
- [JMPF b (length(compile c1) + 2)] @ compile c1 @
- [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
-"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 2)] @ compile c @
+ [JMPF b (length(compile c1) + 1)] @ compile c1 @
+ [JMPF (%x. False) (length(compile c2))] @ compile c2"
+"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
  [JMPB (length(compile c)+1)]"
 
-declare nth_append[simp]
-
-subsection "Context lifting lemmas"
-
-text {* 
-  Some lemmas for lifting an execution into a prefix and suffix
-  of instructions; only needed for the first proof.
-*}
-lemma app_right_1:
-  "is1 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow> is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
-  (is "?P \<Longrightarrow> _")
-proof -
- assume ?P
- then show ?thesis
- by induct force+
-qed
-
-lemma app_left_1:
-  "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
-   is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -1\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
-  (is "?P \<Longrightarrow> _")
-proof -
- assume ?P
- then show ?thesis
- by induct force+
-qed
-
-declare rtrancl_induct2 [induct set: rtrancl]
-
-lemma app_right:
-  "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow> is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
-  (is "?P \<Longrightarrow> _")
-proof -
- assume ?P
- then 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
-qed
-
-lemma app_left:
-  "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
-   is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
-  (is "?P \<Longrightarrow> _")
-proof -
- assume ?P
- then 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
-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)
-
-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])
-
 subsection "Compiler correctness"
 
-declare rtrancl_into_rtrancl[trans]
-        converse_rtrancl_into_rtrancl[trans]
-        rtrancl_trans[trans]
-
-text {*
-  The first proof; The statement is very intuitive,
-  but application of induction hypothesis requires the above lifting lemmas
-*}
-theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> compile c \<turnstile> \<langle>s,0\<rangle> -*\<rightarrow> \<langle>t,length(compile c)\<rangle>"
-        (is "?P \<Longrightarrow> ?Q c s t")
+theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+shows "\<And>p q. \<langle>compile c @ p,q,s\<rangle> -*\<rightarrow> \<langle>p,rev(compile c)@q,t\<rangle>"
+  (is "\<And>p q. ?P c s t p q")
 proof -
-  assume ?P
-  then show ?thesis
+  from A show "\<And>p q. ?thesis p q"
   proof induct
-    show "\<And>s. ?Q \<SKIP> s s" by simp
+    case Skip thus ?case by simp
   next
-    show "\<And>a s x. ?Q (x :== a) s (s[x\<mapsto> a s])" by force
+    case Assign thus ?case by force
+  next
+    case Semi thus ?case by simp (blast intro:rtrancl_trans)
   next
-    fix c0 c1 s0 s1 s2
-    assume "?Q 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 "?Q 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 -
-      note app_left[of _ 0]
-      thus
-	      "\<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>"
-	      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 "?Q (c0; c1) s0 s2" by simp
+    fix b c0 c1 s0 s1 p q
+    assume IH: "\<And>p q. ?P c0 s0 s1 p q"
+    assume "b s0"
+    thus "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1 p q"
+      by(simp add: IH[THEN rtrancl_trans])
+  next
+    case IfFalse thus ?case by(simp)
   next
-    fix b c0 c1 s0 s1
-    let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
-    assume "b s0" and IH: "?Q 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 "?Q (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
+    case WhileFalse thus ?case by simp
   next
-    fix b c0 c1 s0 s1
-    let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
-    assume "\<not>b s0" and IH: "?Q 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 "?Q (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
-  next
-    fix b c and s::state
-    assume "\<not>b s"
-    thus "?Q (\<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: "?Q c s0 s1" and IHw: "?Q (\<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 "?Q (\<WHILE> b \<DO> c) s0 s2".
+    fix b c and s0::state and s1 s2 p q
+    assume b: "b s0" and
+      IHc: "\<And>p q. ?P c s0 s1 p q" and
+      IHw: "\<And>p q. ?P (\<WHILE> b \<DO> c) s1 s2 p q"
+    show "?P (\<WHILE> b \<DO> c) s0 s2 p q"
+      using b  IHc[THEN rtrancl_trans] IHw by(simp)
   qed
 qed
 
-text {*
-  Second proof; statement is generalized to cater for prefixes and suffixes;
-  needs none of the lifting lemmas, but instantiations of pre/suffix.
-  *}
-theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> 
-  !a z. a@compile c@z \<turnstile> \<langle>s,length a\<rangle> -*\<rightarrow> \<langle>t,length a + length(compile c)\<rangle>";
-apply(erule evalc.induct)
-      apply simp
-     apply(force intro!: ASIN)
-    apply(intro strip)
-    apply(erule_tac x = a in allE)
-    apply(erule_tac x = "a@compile c0" in allE)
-    apply(erule_tac x = "compile c1@z" in allE)
-    apply(erule_tac x = z in allE)
-    apply(simp add:add_assoc[THEN sym])
-    apply(blast intro:rtrancl_trans)
-(* \<IF> b \<THEN> c0 \<ELSE> c1; case b is true *)
-   apply(intro strip)
-   (* instantiate assumption sufficiently for later: *)
-   apply(erule_tac x = "a@[?I]" in allE)
-   apply(simp)
-   (* execute JMPF: *)
-   apply(rule converse_rtrancl_into_rtrancl)
-    apply(force intro!: JMPFT)
-   (* execute compile c0: *)
-   apply(rule rtrancl_trans)
-    apply(erule allE)
-    apply assumption
-   (* execute JMPF: *)
-   apply(rule r_into_rtrancl)
-   apply(force intro!: JMPFF)
-(* end of case b is true *)
-  apply(intro strip)
-  apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
-  apply(simp add:add_assoc)
-  apply(rule converse_rtrancl_into_rtrancl)
-   apply(force intro!: JMPFF)
-  apply(blast)
- apply(force intro: JMPFF)
-apply(intro strip)
-apply(erule_tac x = "a@[?I]" in allE)
-apply(erule_tac x = a in allE)
-apply(simp)
-apply(rule converse_rtrancl_into_rtrancl)
- apply(force intro!: JMPFT)
-apply(rule rtrancl_trans)
- apply(erule allE)
- apply assumption
-apply(rule converse_rtrancl_into_rtrancl)
- apply(force intro!: JMPB)
-apply(simp)
+text {* The other direction! *}
+
+inductive_cases [elim!]: "(([],p,s),next) : stepa1"
+
+lemma [simp]: "(\<langle>[],q,s\<rangle> -n\<rightarrow> \<langle>p',q',t\<rangle>) = (n=0 \<and> p' = [] \<and> q' = q \<and> t = s)"
+apply(rule iffI)
+ apply(erule converse_rel_powE, simp, fast)
+apply simp
+done
+
+lemma [simp]: "(\<langle>[],q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>) = (p' = [] \<and> q' = q \<and> t = s)"
+by(simp add: rtrancl_is_UN_rel_pow)
+
+constdefs
+ forws :: "instr \<Rightarrow> nat set"
+"forws instr == case instr of
+ ASIN x a \<Rightarrow> {0} |
+ JMPF b n \<Rightarrow> {0,n} |
+ JMPB n \<Rightarrow> {}"
+ backws :: "instr \<Rightarrow> nat set"
+"backws instr == case instr of
+ ASIN x a \<Rightarrow> {} |
+ JMPF b n \<Rightarrow> {} |
+ JMPB n \<Rightarrow> {n}"
+
+consts closed :: "nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
+primrec
+"closed m n [] = True"
+"closed m n (instr#is) = ((\<forall>j \<in> forws instr. j \<le> size is+n) \<and>
+                        (\<forall>j \<in> backws instr. j \<le> m) \<and> closed (Suc m) n is)"
+
+lemma [simp]:
+ "\<And>m n. closed m n (C1@C2) =
+         (closed m (n+size C2) C1 \<and> closed (m+size C1) n C2)"
+by(induct C1, simp, simp add:plus_ac0)
+
+theorem [simp]: "\<And>m n. closed m n (compile c)"
+by(induct c, simp_all add:backws_def forws_def)
+
+lemma drop_lem: "n \<le> size(p1@p2)
+ \<Longrightarrow> (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) =
+    (n \<le> size p1 & p1' = drop n p1)"
+apply(rule iffI)
+ defer apply simp
+apply(subgoal_tac "n \<le> size p1")
+ apply(rotate_tac -1)
+ apply simp
+apply(rule ccontr)
+apply(rotate_tac -1)
+apply(drule_tac f = length in arg_cong)
+apply simp
+apply arith
+done
+
+lemma reduce_exec1:
+ "\<langle>i # p1 @ p2,q1 @ q2,s\<rangle> -1\<rightarrow> \<langle>p1' @ p2,q1' @ q2,s'\<rangle> \<Longrightarrow>
+  \<langle>i # p1,q1,s\<rangle> -1\<rightarrow> \<langle>p1',q1',s'\<rangle>"
+by(clarsimp simp add: drop_lem split:instr.split_asm split_if_asm)
+
+
+lemma closed_exec1:
+ "\<lbrakk> closed 0 0 (rev q1 @ instr # p1);
+    \<langle>instr # p1 @ p2, q1 @ q2,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle> \<rbrakk> \<Longrightarrow>
+  \<exists>p1' q1'. p' = p1'@p2 \<and> q' = q1'@q2 \<and> rev q1' @ p1' = rev q1 @ instr # p1"
+apply(clarsimp simp add:forws_def backws_def
+               split:instr.split_asm split_if_asm)
 done
 
-text {* Missing: the other direction! *}
+theorem closed_execn_decomp: "\<And>C1 C2 r.
+ \<lbrakk> closed 0 0 (rev C1 @ C2);
+   \<langle>C2 @ p1 @ p2, C1 @ q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<rbrakk>
+ \<Longrightarrow> \<exists>s n1 n2. \<langle>C2,C1,r\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle> \<and>
+     \<langle>p1@p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
+         n = n1+n2"
+(is "\<And>C1 C2 r. \<lbrakk>?CL C1 C2; ?H C1 C2 r n\<rbrakk> \<Longrightarrow> ?P C1 C2 r n")
+proof(induct n)
+  fix C1 C2 r
+  assume "?H C1 C2 r 0"
+  thus "?P C1 C2 r 0" by simp
+next
+  fix C1 C2 r n
+  assume IH: "\<And>C1 C2 r. ?CL C1 C2 \<Longrightarrow> ?H C1 C2 r n \<Longrightarrow> ?P C1 C2 r n"
+  assume CL: "?CL C1 C2" and H: "?H C1 C2 r (Suc n)"
+  show "?P C1 C2 r (Suc n)"
+  proof (cases C2)
+    assume "C2 = []" with H show ?thesis by simp
+  next
+    fix instr tlC2
+    assume C2: "C2 = instr # tlC2"
+    from H C2 obtain p' q' r'
+      where 1: "\<langle>instr # tlC2 @ p1 @ p2, C1 @ q,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle>"
+      and n: "\<langle>p',q',r'\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle>"
+      by(fastsimp simp add:R_O_Rn_commute)
+    from CL closed_exec1[OF _ 1] C2
+    obtain C2' C1' where pq': "p' = C2' @ p1 @ p2 \<and> q' = C1' @ q"
+      and same: "rev C1' @ C2' = rev C1 @ C2"
+      by fastsimp
+    have rev_same: "rev C2' @ C1' = rev C2 @ C1"
+    proof -
+      have "rev C2' @ C1' = rev(rev C1' @ C2')" by simp
+      also have "\<dots> = rev(rev C1 @ C2)" by(simp only:same)
+      also have "\<dots> =  rev C2 @ C1" by simp
+      finally show ?thesis .
+    qed
+    hence rev_same': "\<And>p. rev C2' @ C1' @ p = rev C2 @ C1 @ p" by simp
+    from n have n': "\<langle>C2' @ p1 @ p2,C1' @ q,r'\<rangle> -n\<rightarrow>
+                     \<langle>p2,rev p1 @ rev C2' @ C1' @ q,t\<rangle>"
+      by(simp add:pq' rev_same')
+    from IH[OF _ n'] CL
+    obtain s n1 n2 where n1: "\<langle>C2',C1',r'\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>" and
+      "\<langle>p1 @ p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
+       n = n1 + n2"
+      by(fastsimp simp add: same rev_same rev_same')
+    moreover
+    from 1 n1 pq' C2 have "\<langle>C2,C1,r\<rangle> -Suc n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>"
+      by (simp del:relpow.simps exec_simp) (fast dest:reduce_exec1)
+    ultimately show ?thesis by (fastsimp simp del:relpow.simps)
+  qed
+qed
+
+lemma execn_decomp:
+"\<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
+ \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
+     \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
+         n = n1+n2"
+using closed_execn_decomp[of "[]",simplified] by simp
+
+lemma exec_star_decomp:
+"\<langle>compile c @ p1 @ p2,q,r\<rangle> -*\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
+ \<Longrightarrow> \<exists>s. \<langle>compile c,[],r\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
+     \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -*\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle>"
+by(simp add:rtrancl_is_UN_rel_pow)(fast dest: execn_decomp)
+
+
+(* Alternative:
+lemma exec_comp_n:
+"\<And>p1 p2 q r t n.
+ \<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
+ \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
+     \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
+         n = n1+n2"
+ (is "\<And>p1 p2 q r t n. ?H c p1 p2 q r t n \<Longrightarrow> ?P c p1 p2 q r t n")
+proof (induct c)
+*)
+
+text{*Warning: 
+@{prop"\<langle>compile c @ p,q,s\<rangle> -*\<rightarrow> \<langle>p,rev(compile c)@q,t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"}
+is not true! *}
 
-end
+theorem "\<And>s t.
+ \<langle>compile c,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+proof (induct c)
+  fix s t
+  assume "\<langle>compile SKIP,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile SKIP),t\<rangle>"
+  thus "\<langle>SKIP,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
+next
+  fix s t v f
+  assume "\<langle>compile(v :== f),[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile(v :== f)),t\<rangle>"
+  thus "\<langle>v :== f,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
+next
+  fix s1 s3 c1 c2
+  let ?C1 = "compile c1" let ?C2 = "compile c2"
+  assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
+     and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
+  assume "\<langle>compile(c1;c2),[],s1\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
+  then obtain s2 where exec1: "\<langle>?C1,[],s1\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,s2\<rangle>" and
+             exec2: "\<langle>?C2,rev ?C1,s2\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
+    by(fastsimp dest:exec_star_decomp[of _ _ "[]" "[]",simplified])
+  from exec2 have exec2': "\<langle>?C2,[],s2\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,s3\<rangle>"
+    using exec_star_decomp[of _ "[]" "[]"] by fastsimp
+  have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>c s2" using IH1 exec1 by simp
+  moreover have "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>c s3" using IH2 exec2' by fastsimp
+  ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>c s3" ..
+next
+  fix s t b c1 c2
+  let ?if = "IF b THEN c1 ELSE c2" let ?C = "compile ?if"
+  let ?C1 = "compile c1" let ?C2 = "compile c2"
+  assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
+     and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
+     and H: "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle>"
+  show "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>c t"
+  proof cases
+    assume b: "b s"
+    with H have "\<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle>"
+      by (fastsimp dest:exec_star_decomp
+            [of _ "[JMPF (\<lambda>x. False) (size ?C2)]@?C2" "[]",simplified])
+    hence "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH1)
+    with b show ?thesis ..
+  next
+    assume b: "\<not> b s"
+    with H have "\<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle>"
+      using exec_star_decomp[of _ "[]" "[]"] by simp
+    hence "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH2)
+    with b show ?thesis ..
+  qed
+next
+  fix b c s t
+  let ?w = "WHILE b DO c" let ?W = "compile ?w" let ?C = "compile c"
+  let ?j1 = "JMPF b (size ?C + 1)" let ?j2 = "JMPB (size ?C + 1)"
+  assume IHc: "\<And>s t. \<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+     and H: "\<langle>?W,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
+  from H obtain k where ob:"\<langle>?W,[],s\<rangle> -k\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
+    by(simp add:rtrancl_is_UN_rel_pow) blast
+  { fix n have "\<And>s. \<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle> \<Longrightarrow> \<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
+    proof (induct n rule: less_induct)
+      fix n
+      assume IHm: "\<And>m s. \<lbrakk>m < n; \<langle>?W,[],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle> \<rbrakk> \<Longrightarrow> \<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
+      fix s
+      assume H: "\<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
+      show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
+      proof cases
+	assume b: "b s"
+	then obtain m where m: "n = Suc m"
+          and 1: "\<langle>?C @ [?j2],[?j1],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
+	  using H by fastsimp
+	then obtain r n1 n2 where n1: "\<langle>?C,[],s\<rangle> -n1\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
+          and n2: "\<langle>[?j2],rev ?C @ [?j1],r\<rangle> -n2\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
+          and n12: "m = n1+n2"
+	  using execn_decomp[of _ "[?j2]"]
+	  by(simp del: execn_simp) fast
+	have n2n: "n2 - 1 < n" using m n12 by arith
+	note b
+	moreover
+	{ from n1 have "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
+	    by (simp add:rtrancl_is_UN_rel_pow) fast
+	  hence "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c r" by(rule IHc)
+	}
+	moreover
+	{ have "n2 - 1 < n" using m n12 by arith
+	  moreover from n2 have "\<langle>?W,[],r\<rangle> -n2- 1\<rightarrow> \<langle>[],rev ?W,t\<rangle>" by fastsimp
+	  ultimately have "\<langle>?w,r\<rangle> \<longrightarrow>\<^sub>c t" by(rule IHm)
+	}
+	ultimately show ?thesis ..
+      next
+	assume b: "\<not> b s"
+	hence "t = s" using H by simp
+	with b show ?thesis by simp
+      qed
+    qed
+  }
+  with ob show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t" by fast
+qed
+
+(* To Do: connect with Machine 0 using M_equiv *)
+
+end
\ No newline at end of file
diff -r 643fce75f6cd -r 8ed413a57bdc src/HOL/IMP/Compiler0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Compiler0.thy	Fri Apr 26 11:47:01 2002 +0200
@@ -0,0 +1,272 @@
+(*  Title:      HOL/IMP/Compiler.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow, TUM
+    Copyright   1996 TUM
+
+This is an early version of the compiler, where the abstract machine
+has an explicit pc. This turned out to be awkward, and a second
+development was started. See Machines.thy and Compiler.thy.
+*)
+
+header "A Simple Compiler"
+
+theory Compiler0 = Natural:
+
+subsection "An abstract, simplistic machine"
+
+text {* There are only three instructions: *}
+datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat
+
+text {* We describe execution of programs in the machine by
+  an operational (small step) semantics:
+*}
+consts  stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
+
+syntax
+  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+               ("_ |- (3<_,_>/ -1-> <_,_>)" [50,0,0,0,0] 50)
+  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+               ("_ |-/ (3<_,_>/ -*-> <_,_>)" [50,0,0,0,0] 50)
+
+  "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
+               ("_ |-/ (3<_,_>/ -(_)-> <_,_>)" [50,0,0,0,0,0] 50)
+
+syntax (xsymbols)
+  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+               ("_ \<turnstile> (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
+  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+               ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
+  "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
+               ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
+
+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)"
+
+inductive "stepa1 P"
+intros
+ASIN[simp]:
+  "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s[x\<mapsto> a s],Suc n\<rangle>"
+JMPFT[simp,intro]:
+  "\<lbrakk> n<size P; P!n = JMPF b i;  b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,Suc n\<rangle>"
+JMPFF[simp,intro]:
+  "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,m\<rangle>"
+JMPB[simp]:
+  "\<lbrakk> n<size P; P!n = JMPB i; i <= n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,j\<rangle>"
+
+subsection "The compiler"
+
+consts compile :: "com \<Rightarrow> instr list"
+primrec
+"compile \<SKIP> = []"
+"compile (x:==a) = [ASIN x a]"
+"compile (c1;c2) = compile c1 @ compile c2"
+"compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
+ [JMPF b (length(compile c1) + 2)] @ compile c1 @
+ [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
+"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 2)] @ compile c @
+ [JMPB (length(compile c)+1)]"
+
+declare nth_append[simp]
+
+subsection "Context lifting lemmas"
+
+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>"
+  shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
+proof -
+ from A show ?thesis
+ by induct force+
+qed
+
+lemma app_left_1:
+  assumes A: "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
+
+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
+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
+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)
+
+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])
+
+subsection "Compiler correctness"
+
+declare rtrancl_into_rtrancl[trans]
+        converse_rtrancl_into_rtrancl[trans]
+        rtrancl_trans[trans]
+
+text {*
+  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".
+  qed
+qed
+
+text {*
+  Second proof; statement is generalized to cater for prefixes and suffixes;
+  needs none of the lifting lemmas, but instantiations of pre/suffix.
+  *}
+theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> 
+  !a z. a@compile c@z \<turnstile> \<langle>s,length a\<rangle> -*\<rightarrow> \<langle>t,length a + length(compile c)\<rangle>";
+apply(erule evalc.induct)
+      apply simp
+     apply(force intro!: ASIN)
+    apply(intro strip)
+    apply(erule_tac x = a in allE)
+    apply(erule_tac x = "a@compile c0" in allE)
+    apply(erule_tac x = "compile c1@z" in allE)
+    apply(erule_tac x = z in allE)
+    apply(simp add:add_assoc[THEN sym])
+    apply(blast intro:rtrancl_trans)
+(* \<IF> b \<THEN> c0 \<ELSE> c1; case b is true *)
+   apply(intro strip)
+   (* instantiate assumption sufficiently for later: *)
+   apply(erule_tac x = "a@[?I]" in allE)
+   apply(simp)
+   (* execute JMPF: *)
+   apply(rule converse_rtrancl_into_rtrancl)
+    apply(force intro!: JMPFT)
+   (* execute compile c0: *)
+   apply(rule rtrancl_trans)
+    apply(erule allE)
+    apply assumption
+   (* execute JMPF: *)
+   apply(rule r_into_rtrancl)
+   apply(force intro!: JMPFF)
+(* end of case b is true *)
+  apply(intro strip)
+  apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
+  apply(simp add:add_assoc)
+  apply(rule converse_rtrancl_into_rtrancl)
+   apply(force intro!: JMPFF)
+  apply(blast)
+ apply(force intro: JMPFF)
+apply(intro strip)
+apply(erule_tac x = "a@[?I]" in allE)
+apply(erule_tac x = a in allE)
+apply(simp)
+apply(rule converse_rtrancl_into_rtrancl)
+ apply(force intro!: JMPFT)
+apply(rule rtrancl_trans)
+ apply(erule allE)
+ apply assumption
+apply(rule converse_rtrancl_into_rtrancl)
+ apply(force intro!: JMPB)
+apply(simp)
+done
+
+text {* Missing: the other direction! I did much of it, and although
+the main lemma is very similar to the one in the new development, the
+lemmas surrounding it seemed much more complicated. In the end I gave
+up. *}
+
+end
diff -r 643fce75f6cd -r 8ed413a57bdc src/HOL/IMP/Machines.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Machines.thy	Fri Apr 26 11:47:01 2002 +0200
@@ -0,0 +1,242 @@
+theory Machines = Natural:
+
+lemma rtrancl_eq: "R^* = Id \<union> (R O R^*)"
+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)
+
+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])
+
+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))"
+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)
+
+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)
+
+subsection "Instructions"
+
+text {* There are only three instructions: *}
+datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat
+
+types instrs = "instr list"
+
+subsection "M0 with PC"
+
+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)
+  "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
+               ("(_/ |- (1<_,/_>)/ -*-> (1<_,/_>))" [50,0,0,0,0] 50)
+  "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
+               ("(_/ |- (1<_,/_>)/ -_-> (1<_,/_>))" [50,0,0,0,0] 50)
+
+syntax (xsymbols)
+  "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
+               ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
+  "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
+               ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
+  "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
+               ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
+
+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"
+
+inductive "exec01 P"
+intros
+ASIN: "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s[x\<mapsto> a s]\<rangle>"
+JMPFT: "\<lbrakk> n<size P; P!n = JMPF b i;  b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s\<rangle>"
+JMPFF: "\<lbrakk> n<size P; P!n = JMPF b i; \<not>b s; m=n+i+1; m \<le> size P \<rbrakk>
+        \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>m,s\<rangle>"
+JMPB:  "\<lbrakk> n<size P; P!n = JMPB i; i \<le> n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>j,s\<rangle>"
+
+subsection "M0 with lists"
+
+text {* We describe execution of programs in the machine by
+  an operational (small step) semantics:
+*}
+
+types config = "instrs \<times> instrs \<times> state"
+
+consts  stepa1 :: "(config \<times> config)set"
+
+syntax
+  "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
+               ("((1<_,/_,/_>)/ -1-> (1<_,/_,/_>))" 50)
+  "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
+               ("((1<_,/_,/_>)/ -*-> (1<_,/_,/_>))" 50)
+  "_stepan" :: "[state,instrs,instrs, nat, instrs,instrs,state] \<Rightarrow> bool"
+               ("((1<_,/_,/_>)/ -_-> (1<_,/_,/_>))" 50)
+
+syntax (xsymbols)
+  "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
+               ("((1\<langle>_,/_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
+  "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
+               ("((1\<langle>_,/_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
+  "_stepan" :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool"
+               ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
+
+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)"
+
+
+inductive "stepa1"
+intros
+  "\<langle>ASIN x a#p,q,s\<rangle> -1\<rightarrow> \<langle>p,ASIN x a#q,s[x\<mapsto> a s]\<rangle>"
+  "b s \<Longrightarrow> \<langle>JMPF b i#p,q,s\<rangle> -1\<rightarrow> \<langle>p,JMPF b i#q,s\<rangle>"
+  "\<lbrakk> \<not> b s; i \<le> size p \<rbrakk>
+   \<Longrightarrow> \<langle>JMPF b i # p, q, s\<rangle> -1\<rightarrow> \<langle>drop i p, rev(take i p) @ JMPF b i # q, s\<rangle>"
+  "i \<le> size q
+   \<Longrightarrow> \<langle>JMPB i # p, q, s\<rangle> -1\<rightarrow> \<langle>rev(take i q) @ JMPB i # p, drop i q, s\<rangle>"
+
+inductive_cases execE: "((i#is,p,s),next) : stepa1"
+
+lemma exec_simp[simp]:
+ "(\<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>) = (case i of
+ ASIN x a \<Rightarrow> t = s[x\<mapsto> a s] \<and> p' = p \<and> q' = i#q |
+ JMPF b n \<Rightarrow> t=s \<and> (if b s then p' = p \<and> q' = i#q
+            else n \<le> size p \<and> p' = drop n p \<and> q' = rev(take n p) @ i # q) |
+ JMPB n \<Rightarrow> n \<le> size q \<and> t=s \<and> p' = rev(take n q) @ i # p \<and> q' = drop n q)"
+apply(rule iffI)
+defer
+apply(clarsimp simp add: stepa1.intros split: instr.split_asm split_if_asm)
+apply(erule execE)
+apply(simp_all)
+done
+
+lemma execn_simp[simp]:
+"(\<langle>i#p,q,s\<rangle> -n\<rightarrow> \<langle>p'',q'',u\<rangle>) =
+ (n=0 \<and> p'' = i#p \<and> q'' = q \<and> u = s \<or>
+  ((\<exists>m p' q' t. n = Suc m \<and>
+                \<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> \<and> \<langle>p',q',t\<rangle> -m\<rightarrow> \<langle>p'',q'',u\<rangle>)))"
+by(subst converse_in_rel_pow_eq, simp)
+
+
+lemma exec_star_simp[simp]: "(\<langle>i#p,q,s\<rangle> -*\<rightarrow> \<langle>p'',q'',u\<rangle>) =
+ (p'' = i#p & q''=q & u=s |
+ (\<exists>p' q' t. \<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> \<and> \<langle>p',q',t\<rangle> -*\<rightarrow> \<langle>p'',q'',u\<rangle>))"
+apply(simp add: rtrancl_is_UN_rel_pow del:exec_simp)
+apply(blast)
+done
+
+declare nth_append[simp]
+
+lemma rev_revD: "rev xs = rev ys \<Longrightarrow> xs = ys"
+by simp
+
+lemma [simp]: "(rev xs @ rev ys = rev zs) = (ys @ xs = zs)"
+apply(rule iffI)
+ apply(rule rev_revD, simp)
+apply fastsimp
+done
+
+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(simp add:exec01.ASIN)
+  apply(fastsimp intro:exec01.JMPFT)
+ apply simp
+ apply(rule exec01.JMPFF)
+     apply simp
+    apply fastsimp
+   apply simp
+  apply simp
+  apply arith
+ apply simp
+ apply arith
+apply(fastsimp simp add:exec01.JMPB)
+done
+
+lemma drop_take_rev: "\<And>i. drop (length xs - i) (rev xs) = rev (take i xs)"
+apply(induct xs)
+ apply simp_all
+apply(case_tac i)
+apply simp_all
+done
+
+lemma take_drop_rev: "\<And>i. take (length xs - i) (rev xs) = rev (drop i xs)"
+apply(induct xs)
+ apply simp_all
+apply(case_tac i)
+apply simp_all
+done
+
+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>
+          rev p' @ q' = rev p @ q \<longrightarrow> \<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>"
+apply(erule exec01.induct)
+   apply(clarsimp simp add: neq_Nil_conv)
+   apply(rule conjI)
+    apply(drule_tac f = "drop (size p')" in arg_cong)
+    apply simp
+    apply(drule sym)
+    apply simp
+   apply(drule_tac f = "take (size p')" in arg_cong)
+   apply simp
+   apply(drule sym)
+   apply simp
+   apply(rule rev_revD)
+   apply simp
+  apply(clarsimp simp add: neq_Nil_conv)
+  apply(rule conjI)
+   apply(drule_tac f = "drop (size p')" in arg_cong)
+   apply simp
+   apply(drule sym)
+   apply simp
+  apply(drule_tac f = "take (size p')" in arg_cong)
+  apply simp
+  apply(drule sym)
+  apply simp
+  apply(rule rev_revD)
+  apply simp
+ apply(clarsimp simp add: neq_Nil_conv)
+ apply(rule conjI)
+  apply(drule_tac f = "drop (size p')" in arg_cong)
+  apply simp
+  apply(drule sym)
+  apply simp
+ apply(drule_tac f = "take (size p')" in arg_cong)
+ apply simp
+ apply(drule sym)
+ apply simp
+ apply(rule rev_revD)
+ apply simp
+apply(clarsimp simp add: neq_Nil_conv)
+apply(rule conjI)
+ apply(drule_tac f = "drop (size p')" in arg_cong)
+ apply simp
+ apply(drule sym)
+ apply(simp add:drop_take_rev)
+apply(drule_tac f = "take (size p')" in arg_cong)
+apply simp
+apply(drule sym)
+apply simp
+apply(rule rev_revD)
+apply(simp add:take_drop_rev)
+done
+
+
+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)
+
+end
diff -r 643fce75f6cd -r 8ed413a57bdc src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Thu Apr 25 17:36:29 2002 +0200
+++ b/src/HOL/IMP/ROOT.ML	Fri Apr 26 11:47:01 2002 +0200
@@ -10,4 +10,5 @@
 time_use_thy "Transition";
 time_use_thy "VC";
 time_use_thy "Examples";
+time_use_thy "Compiler0";
 time_use_thy "Compiler";