# HG changeset patch
# User kleing
# Date 1007904896 -3600
# Node ID 15c13bdc94c8f89aa003b0316205067f59d6851f
# Parent  f3033eed309a931a4ef85f9e80c93881b2ce9b33
tuned for latex output

diff -r f3033eed309a -r 15c13bdc94c8 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Sun Dec 09 14:34:18 2001 +0100
+++ b/src/HOL/IMP/Compiler.thy	Sun Dec 09 14:34:56 2001 +0100
@@ -2,55 +2,72 @@
     ID:         $Id$
     Author:     Tobias Nipkow, TUM
     Copyright   1996 TUM
+*)
 
-A simple compiler for a simplistic machine.
-*)
+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
 
-consts  stepa1 :: "instr list => ((state*nat) * (state*nat))set"
+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] => bool"
-                     ("_ \<turnstile> <_,_>/ -1\<rightarrow> <_,_>" [50,0,0,0,0] 50)
-        "@stepa" :: "[instr list,state,nat,state,nat] => bool"
-                     ("_ \<turnstile>/ <_,_>/ -*\<rightarrow> <_,_>" [50,0,0,0,0] 50)
+  "@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)
 
-translations  "P \<turnstile> <s,m> -1\<rightarrow> <t,n>" == "((s,m),t,n) : stepa1 P"
-              "P \<turnstile> <s,m> -*\<rightarrow> <t,n>" == "((s,m),t,n) : ((stepa1 P)^*)"
+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> <s,n> -1\<rightarrow> <s[x::= a s],Suc n>"
+  "\<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> <s,n> -1\<rightarrow> <s,Suc n>"
+  "\<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> <s,n> -1\<rightarrow> <s,m>"
+  "\<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> <s,n> -1\<rightarrow> <s,j>"
+  "\<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>"
 
-consts compile :: "com => instr list"
+subsection "The compiler"
+
+consts compile :: "com \<Rightarrow> instr list"
 primrec
-"compile SKIP = []"
+"compile \<SKIP> = []"
 "compile (x:==a) = [ASIN x a]"
 "compile (c1;c2) = compile c1 @ compile c2"
-"compile (IF b THEN c1 ELSE 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 @
+"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 2)] @ compile c @
  [JMPB (length(compile c)+1)]"
 
-declare nth_append[simp];
+declare nth_append[simp]
 
-(* Lemmas for lifting an execution into a prefix and suffix
-   of instructions; only needed for the first proof *)
+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> <s1,i1> -1\<rightarrow> <s2,i2> \<Longrightarrow> is1 @ is2 \<turnstile> <s1,i1> -1\<rightarrow> <s2,i2>"
+  "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
@@ -59,8 +76,8 @@
 qed
 
 lemma app_left_1:
-  "is2 \<turnstile> <s1,i1> -1\<rightarrow> <s2,i2> \<Longrightarrow>
-   is1 @ is2 \<turnstile> <s1,size is1+i1> -1\<rightarrow> <s2,size is1+i2>"
+  "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
@@ -71,176 +88,181 @@
 declare rtrancl_induct2 [induct set: rtrancl]
 
 lemma app_right:
-  "is1 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2> \<Longrightarrow> is1 @ is2 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2>"
+  "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> <s1,i1> -*\<rightarrow> <s1,i1>" by simp
+   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> <s1,i1> -*\<rightarrow> <s1',i1'>"
-          "is1 \<turnstile> <s1',i1'> -1\<rightarrow> <s2,i2>"
-   thus "is1 @ is2 \<turnstile> <s1,i1> -*\<rightarrow> <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> <s1,i1> -*\<rightarrow> <s2,i2> \<Longrightarrow>
-   is1 @ is2 \<turnstile> <s1,size is1+i1> -*\<rightarrow> <s2,size is1+i2>"
+  "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> <s1,length is1 + i1> -*\<rightarrow> <s1,length is1 + i1>" by simp
+   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> <s1,length is1 + i1> -*\<rightarrow> <s1',length is1 + i1'>"
-          "is2 \<turnstile> <s1',i1'> -1\<rightarrow> <s2,i2>"
-   thus "is1 @ is2 \<turnstile> <s1,length is1 + i1> -*\<rightarrow> <s2,length is1 + 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> <s1,i1> -*\<rightarrow> <s2,i2>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
-   is1 @ is2 \<turnstile> <s1,j1> -*\<rightarrow> <s2,j2>"
-by (simp add:app_left)
+  "\<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> <s1,i1> -*\<rightarrow> <s2,i2> \<Longrightarrow>
-   instr # is \<turnstile> <s1,Suc i1> -*\<rightarrow> <s2,Suc i2>"
-by(erule app_left[of _ _ _ _ _ "[instr]",simplified])
+  "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]
         rtrancl_into_rtrancl2[trans]
         rtrancl_trans[trans]
-(* The first proof; statement very intuitive,
-   but application of induction hypothesis requires the above lifting lemmas
-*)
-theorem "<c,s> -c-> t \<Longrightarrow> compile c \<turnstile> <s,0> -*\<rightarrow> <t,length(compile c)>"
+
+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")
 proof -
   assume ?P
   then show ?thesis
   proof induct
-    show "\<And>s. ?Q SKIP s s" by simp
+    show "\<And>s. ?Q \<SKIP> s s" by simp
   next
-    show "\<And>a s x. ?Q (x :== a) s (s[x::= a s])" by force
+    show "\<And>a s x. ?Q (x :== a) s (s[x\<mapsto> a s])" by force
   next
     fix c0 c1 s0 s1 s2
     assume "?Q c0 s0 s1"
-    hence "compile c0 @ compile c1 \<turnstile> <s0,0> -*\<rightarrow> <s1,length(compile c0)>"
+    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> <s1,length(compile c0)> -*\<rightarrow>
-           <s2,length(compile c0)+length(compile c1)>"
+    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> <s1,0> -*\<rightarrow> <s2,i2> \<Longrightarrow>
-	is1 @ is2 \<turnstile> <s1,size is1> -*\<rightarrow> <s2,size is1+i2>"
-	by simp
+	      "\<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> <s0,0> -*\<rightarrow>
-                       <s2,length(compile c0)+length(compile c1)>"
+    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
   next
     fix b c0 c1 s0 s1
-    let ?comp = "compile(IF b THEN c0 ELSE c1)"
+    let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
     assume "b s0" and IH: "?Q c0 s0 s1"
-    hence "?comp \<turnstile> <s0,0> -1\<rightarrow> <s0,1>" by auto
+    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
     also from IH
-    have "?comp \<turnstile> <s0,1> -*\<rightarrow> <s1,length(compile c0)+1>"
+    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> <s1,length(compile c0)+1> -1\<rightarrow> <s1,length ?comp>"
+    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" .
+    finally show "?Q (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
   next
     fix b c0 c1 s0 s1
-    let ?comp = "compile(IF b THEN c0 ELSE c1)"
+    let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
     assume "\<not>b s0" and IH: "?Q c1 s0 s1"
-    hence "?comp \<turnstile> <s0,0> -1\<rightarrow> <s0,length(compile c0) + 2>" by auto
+    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto
     also from IH
-    have "?comp \<turnstile> <s0,length(compile c0)+2> -*\<rightarrow> <s1,length ?comp>"
+    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" .
+    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
+    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)"
+    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> <s0,0> -1\<rightarrow> <s0,1>" by auto
+      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> <s0,1> -*\<rightarrow> <s1,length(compile c)+1>"
+    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> <s1,length(compile c)+1> -1\<rightarrow> <s1,0>" by simp
+    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".
+    finally show "?Q (\<WHILE> b \<DO> c) s0 s2".
   qed
 qed
 
-(* Second proof; statement is generalized to cater for prefixes and suffixes;
-   needs none of the lifting lemmas, but instantiations of pre/suffix.
-*)
-theorem "<c,s> -c-> t ==> 
- !a z. a@compile c@z \<turnstile> <s,length a> -*\<rightarrow> <t,length a + length(compile c)>";
-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);
+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);
+   apply(erule_tac x = "a@[?I]" in allE)
+   apply(simp)
    (* execute JMPF: *)
-   apply(rule rtrancl_into_rtrancl2);
-    apply(force intro!: JMPFT);
+   apply(rule rtrancl_into_rtrancl2)
+    apply(force intro!: JMPFT)
    (* execute compile c0: *)
-   apply(rule rtrancl_trans);
-    apply(erule allE);
-    apply assumption;
+   apply(rule rtrancl_trans)
+    apply(erule allE)
+    apply assumption
    (* execute JMPF: *)
-   apply(rule r_into_rtrancl);
-   apply(force intro!: JMPFF);
+   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 rtrancl_into_rtrancl2);
-   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 rtrancl_into_rtrancl2);
- apply(force intro!: JMPFT);
-apply(rule rtrancl_trans);
- apply(erule allE);
- apply assumption;
-apply(rule rtrancl_into_rtrancl2);
- apply(force intro!: JMPB);
-apply(simp);
+  apply(intro strip)
+  apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
+  apply(simp add:add_assoc)
+  apply(rule rtrancl_into_rtrancl2)
+   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 rtrancl_into_rtrancl2)
+ apply(force intro!: JMPFT)
+apply(rule rtrancl_trans)
+ apply(erule allE)
+ apply assumption
+apply(rule rtrancl_into_rtrancl2)
+ apply(force intro!: JMPB)
+apply(simp)
 done
 
-(* Missing: the other direction! *)
+text {* Missing: the other direction! *}
 
 end