src/HOL/IMP/Compiler.thy

   by(erule app_left[of _ _ _ _ _ "[instr]",simplified])
 
 subsection "Compiler correctness"
 
 declare rtrancl_into_rtrancl[trans]
-        rtrancl_into_rtrancl2[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

    apply(intro strip)
    (* instantiate assumption sufficiently for later: *)
    apply(erule_tac x = "a@[?I]" in allE)
    apply(simp)
    (* execute JMPF: *)
-   apply(rule rtrancl_into_rtrancl2)
+   apply(rule converse_rtrancl_into_rtrancl)
     apply(force intro!: JMPFT)
    (* execute compile c0: *)
    apply(rule rtrancl_trans)
     apply(erule allE)
     apply assumption

    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(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 rtrancl_into_rtrancl2)
+apply(rule converse_rtrancl_into_rtrancl)
  apply(force intro!: JMPFT)
 apply(rule rtrancl_trans)
  apply(erule allE)
  apply assumption
-apply(rule rtrancl_into_rtrancl2)
+apply(rule converse_rtrancl_into_rtrancl)
  apply(force intro!: JMPB)
 apply(simp)
 done
 
 text {* Missing: the other direction! *}