src/HOL/IMP/Compiler.thy
author nipkow
Fri Aug 28 18:52:41 2009 +0200 (2009-08-28)
changeset 32436 10cd49e0c067
parent 31969 09524788a6b9
child 32960 69916a850301
permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow@10343
     1
(*  Title:      HOL/IMP/Compiler.thy
nipkow@10343
     2
    ID:         $Id$
nipkow@10343
     3
    Author:     Tobias Nipkow, TUM
nipkow@10343
     4
    Copyright   1996 TUM
kleing@12429
     5
*)
nipkow@10343
     6
haftmann@16417
     7
theory Compiler imports Machines begin
kleing@12429
     8
kleing@12429
     9
subsection "The compiler"
nipkow@10342
    10
wenzelm@27362
    11
primrec compile :: "com \<Rightarrow> instr list"
wenzelm@27362
    12
where
wenzelm@27362
    13
  "compile \<SKIP> = []"
wenzelm@27362
    14
| "compile (x:==a) = [SET x a]"
wenzelm@27362
    15
| "compile (c1;c2) = compile c1 @ compile c2"
wenzelm@27362
    16
| "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
wenzelm@27362
    17
    [JMPF b (length(compile c1) + 1)] @ compile c1 @
wenzelm@27362
    18
    [JMPF (\<lambda>x. False) (length(compile c2))] @ compile c2"
wenzelm@27362
    19
| "compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
wenzelm@27362
    20
    [JMPB (length(compile c)+1)]"
nipkow@10342
    21
kleing@12429
    22
subsection "Compiler correctness"
nipkow@11275
    23
nipkow@13095
    24
theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
nipkow@13095
    25
shows "\<And>p q. \<langle>compile c @ p,q,s\<rangle> -*\<rightarrow> \<langle>p,rev(compile c)@q,t\<rangle>"
nipkow@13095
    26
  (is "\<And>p q. ?P c s t p q")
nipkow@12275
    27
proof -
nipkow@13095
    28
  from A show "\<And>p q. ?thesis p q"
nipkow@12275
    29
  proof induct
nipkow@13095
    30
    case Skip thus ?case by simp
nipkow@12275
    31
  next
nipkow@13095
    32
    case Assign thus ?case by force
nipkow@13095
    33
  next
nipkow@13095
    34
    case Semi thus ?case by simp (blast intro:rtrancl_trans)
nipkow@12275
    35
  next
nipkow@13095
    36
    fix b c0 c1 s0 s1 p q
nipkow@13095
    37
    assume IH: "\<And>p q. ?P c0 s0 s1 p q"
nipkow@13095
    38
    assume "b s0"
nipkow@13095
    39
    thus "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1 p q"
nipkow@13095
    40
      by(simp add: IH[THEN rtrancl_trans])
nipkow@13095
    41
  next
nipkow@13095
    42
    case IfFalse thus ?case by(simp)
nipkow@12275
    43
  next
nipkow@13095
    44
    case WhileFalse thus ?case by simp
nipkow@12275
    45
  next
nipkow@13095
    46
    fix b c and s0::state and s1 s2 p q
nipkow@13095
    47
    assume b: "b s0" and
nipkow@13095
    48
      IHc: "\<And>p q. ?P c s0 s1 p q" and
nipkow@13095
    49
      IHw: "\<And>p q. ?P (\<WHILE> b \<DO> c) s1 s2 p q"
nipkow@13095
    50
    show "?P (\<WHILE> b \<DO> c) s0 s2 p q"
nipkow@13095
    51
      using b  IHc[THEN rtrancl_trans] IHw by(simp)
nipkow@12275
    52
  qed
nipkow@12275
    53
qed
nipkow@11275
    54
nipkow@13095
    55
text {* The other direction! *}
nipkow@13095
    56
berghofe@23746
    57
inductive_cases [elim!]: "(([],p,s),(is',p',s')) : stepa1"
nipkow@13095
    58
nipkow@13095
    59
lemma [simp]: "(\<langle>[],q,s\<rangle> -n\<rightarrow> \<langle>p',q',t\<rangle>) = (n=0 \<and> p' = [] \<and> q' = q \<and> t = s)"
nipkow@13095
    60
apply(rule iffI)
krauss@31969
    61
 apply(erule rel_pow_E2, simp, fast)
nipkow@13095
    62
apply simp
nipkow@13095
    63
done
nipkow@13095
    64
nipkow@13095
    65
lemma [simp]: "(\<langle>[],q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>) = (p' = [] \<and> q' = q \<and> t = s)"
nipkow@13095
    66
by(simp add: rtrancl_is_UN_rel_pow)
nipkow@13095
    67
wenzelm@27362
    68
definition
wenzelm@27362
    69
  forws :: "instr \<Rightarrow> nat set" where
wenzelm@27362
    70
  "forws instr = (case instr of
wenzelm@27362
    71
     SET x a \<Rightarrow> {0} |
wenzelm@27362
    72
     JMPF b n \<Rightarrow> {0,n} |
wenzelm@27362
    73
     JMPB n \<Rightarrow> {})"
nipkow@13095
    74
wenzelm@27362
    75
definition
wenzelm@27362
    76
  backws :: "instr \<Rightarrow> nat set" where
wenzelm@27362
    77
  "backws instr = (case instr of
wenzelm@27362
    78
     SET x a \<Rightarrow> {} |
wenzelm@27362
    79
     JMPF b n \<Rightarrow> {} |
wenzelm@27362
    80
     JMPB n \<Rightarrow> {n})"
wenzelm@27362
    81
wenzelm@27362
    82
primrec closed :: "nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
wenzelm@27362
    83
where
wenzelm@27362
    84
  "closed m n [] = True"
wenzelm@27362
    85
| "closed m n (instr#is) = ((\<forall>j \<in> forws instr. j \<le> size is+n) \<and>
wenzelm@27362
    86
                          (\<forall>j \<in> backws instr. j \<le> m) \<and> closed (Suc m) n is)"
nipkow@13095
    87
nipkow@13095
    88
lemma [simp]:
nipkow@13095
    89
 "\<And>m n. closed m n (C1@C2) =
nipkow@13095
    90
         (closed m (n+size C2) C1 \<and> closed (m+size C1) n C2)"
wenzelm@27362
    91
by(induct C1) (simp, simp add:add_ac)
nipkow@13095
    92
nipkow@13095
    93
theorem [simp]: "\<And>m n. closed m n (compile c)"
wenzelm@27362
    94
by(induct c) (simp_all add:backws_def forws_def)
nipkow@13095
    95
nipkow@13095
    96
lemma drop_lem: "n \<le> size(p1@p2)
nipkow@13095
    97
 \<Longrightarrow> (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) =
nipkow@13095
    98
    (n \<le> size p1 & p1' = drop n p1)"
nipkow@13095
    99
apply(rule iffI)
nipkow@13095
   100
 defer apply simp
nipkow@13095
   101
apply(subgoal_tac "n \<le> size p1")
nipkow@13095
   102
 apply simp
nipkow@13095
   103
apply(rule ccontr)
nipkow@13095
   104
apply(drule_tac f = length in arg_cong)
nipkow@13095
   105
apply simp
nipkow@13095
   106
done
nipkow@13095
   107
nipkow@13095
   108
lemma reduce_exec1:
nipkow@13095
   109
 "\<langle>i # p1 @ p2,q1 @ q2,s\<rangle> -1\<rightarrow> \<langle>p1' @ p2,q1' @ q2,s'\<rangle> \<Longrightarrow>
nipkow@13095
   110
  \<langle>i # p1,q1,s\<rangle> -1\<rightarrow> \<langle>p1',q1',s'\<rangle>"
nipkow@13095
   111
by(clarsimp simp add: drop_lem split:instr.split_asm split_if_asm)
nipkow@13095
   112
nipkow@13095
   113
nipkow@13095
   114
lemma closed_exec1:
nipkow@13095
   115
 "\<lbrakk> closed 0 0 (rev q1 @ instr # p1);
nipkow@13095
   116
    \<langle>instr # p1 @ p2, q1 @ q2,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle> \<rbrakk> \<Longrightarrow>
nipkow@13095
   117
  \<exists>p1' q1'. p' = p1'@p2 \<and> q' = q1'@q2 \<and> rev q1' @ p1' = rev q1 @ instr # p1"
nipkow@13095
   118
apply(clarsimp simp add:forws_def backws_def
nipkow@13095
   119
               split:instr.split_asm split_if_asm)
nipkow@10342
   120
done
nipkow@10342
   121
nipkow@13095
   122
theorem closed_execn_decomp: "\<And>C1 C2 r.
nipkow@13095
   123
 \<lbrakk> closed 0 0 (rev C1 @ C2);
nipkow@13095
   124
   \<langle>C2 @ p1 @ p2, C1 @ q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<rbrakk>
nipkow@13095
   125
 \<Longrightarrow> \<exists>s n1 n2. \<langle>C2,C1,r\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle> \<and>
nipkow@13095
   126
     \<langle>p1@p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
nipkow@13095
   127
         n = n1+n2"
nipkow@13095
   128
(is "\<And>C1 C2 r. \<lbrakk>?CL C1 C2; ?H C1 C2 r n\<rbrakk> \<Longrightarrow> ?P C1 C2 r n")
nipkow@13095
   129
proof(induct n)
nipkow@13095
   130
  fix C1 C2 r
nipkow@13095
   131
  assume "?H C1 C2 r 0"
nipkow@13095
   132
  thus "?P C1 C2 r 0" by simp
nipkow@13095
   133
next
nipkow@13095
   134
  fix C1 C2 r n
nipkow@13095
   135
  assume IH: "\<And>C1 C2 r. ?CL C1 C2 \<Longrightarrow> ?H C1 C2 r n \<Longrightarrow> ?P C1 C2 r n"
nipkow@13095
   136
  assume CL: "?CL C1 C2" and H: "?H C1 C2 r (Suc n)"
nipkow@13095
   137
  show "?P C1 C2 r (Suc n)"
nipkow@13095
   138
  proof (cases C2)
nipkow@13095
   139
    assume "C2 = []" with H show ?thesis by simp
nipkow@13095
   140
  next
nipkow@13095
   141
    fix instr tlC2
nipkow@13095
   142
    assume C2: "C2 = instr # tlC2"
nipkow@13095
   143
    from H C2 obtain p' q' r'
nipkow@13095
   144
      where 1: "\<langle>instr # tlC2 @ p1 @ p2, C1 @ q,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle>"
nipkow@13095
   145
      and n: "\<langle>p',q',r'\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle>"
krauss@31969
   146
      by(fastsimp simp add:rel_pow_commute)
nipkow@13095
   147
    from CL closed_exec1[OF _ 1] C2
nipkow@13095
   148
    obtain C2' C1' where pq': "p' = C2' @ p1 @ p2 \<and> q' = C1' @ q"
nipkow@13095
   149
      and same: "rev C1' @ C2' = rev C1 @ C2"
nipkow@13095
   150
      by fastsimp
nipkow@13095
   151
    have rev_same: "rev C2' @ C1' = rev C2 @ C1"
nipkow@13095
   152
    proof -
nipkow@13095
   153
      have "rev C2' @ C1' = rev(rev C1' @ C2')" by simp
nipkow@13095
   154
      also have "\<dots> = rev(rev C1 @ C2)" by(simp only:same)
nipkow@13095
   155
      also have "\<dots> =  rev C2 @ C1" by simp
nipkow@13095
   156
      finally show ?thesis .
nipkow@13095
   157
    qed
nipkow@13095
   158
    hence rev_same': "\<And>p. rev C2' @ C1' @ p = rev C2 @ C1 @ p" by simp
nipkow@13095
   159
    from n have n': "\<langle>C2' @ p1 @ p2,C1' @ q,r'\<rangle> -n\<rightarrow>
nipkow@13095
   160
                     \<langle>p2,rev p1 @ rev C2' @ C1' @ q,t\<rangle>"
nipkow@13095
   161
      by(simp add:pq' rev_same')
nipkow@13095
   162
    from IH[OF _ n'] CL
nipkow@13095
   163
    obtain s n1 n2 where n1: "\<langle>C2',C1',r'\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>" and
nipkow@13095
   164
      "\<langle>p1 @ p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
nipkow@13095
   165
       n = n1 + n2"
nipkow@13095
   166
      by(fastsimp simp add: same rev_same rev_same')
nipkow@13095
   167
    moreover
nipkow@13095
   168
    from 1 n1 pq' C2 have "\<langle>C2,C1,r\<rangle> -Suc n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>"
nipkow@13095
   169
      by (simp del:relpow.simps exec_simp) (fast dest:reduce_exec1)
nipkow@13095
   170
    ultimately show ?thesis by (fastsimp simp del:relpow.simps)
nipkow@13095
   171
  qed
nipkow@13095
   172
qed
nipkow@13095
   173
nipkow@13095
   174
lemma execn_decomp:
nipkow@13095
   175
"\<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
nipkow@13095
   176
 \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
nipkow@13095
   177
     \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
nipkow@13095
   178
         n = n1+n2"
nipkow@13095
   179
using closed_execn_decomp[of "[]",simplified] by simp
nipkow@13095
   180
nipkow@13095
   181
lemma exec_star_decomp:
nipkow@13095
   182
"\<langle>compile c @ p1 @ p2,q,r\<rangle> -*\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
nipkow@13095
   183
 \<Longrightarrow> \<exists>s. \<langle>compile c,[],r\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
nipkow@13095
   184
     \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -*\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle>"
nipkow@13095
   185
by(simp add:rtrancl_is_UN_rel_pow)(fast dest: execn_decomp)
nipkow@13095
   186
nipkow@13095
   187
nipkow@13095
   188
(* Alternative:
nipkow@13095
   189
lemma exec_comp_n:
nipkow@13095
   190
"\<And>p1 p2 q r t n.
nipkow@13095
   191
 \<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
nipkow@13095
   192
 \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
nipkow@13095
   193
     \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
nipkow@13095
   194
         n = n1+n2"
nipkow@13095
   195
 (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")
nipkow@13095
   196
proof (induct c)
nipkow@13095
   197
*)
nipkow@13095
   198
nipkow@13095
   199
text{*Warning: 
nipkow@13095
   200
@{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"}
nipkow@13095
   201
is not true! *}
nipkow@10342
   202
nipkow@13095
   203
theorem "\<And>s t.
nipkow@13095
   204
 \<langle>compile c,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
nipkow@13095
   205
proof (induct c)
nipkow@13095
   206
  fix s t
nipkow@13095
   207
  assume "\<langle>compile SKIP,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile SKIP),t\<rangle>"
nipkow@13095
   208
  thus "\<langle>SKIP,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
nipkow@13095
   209
next
nipkow@13095
   210
  fix s t v f
nipkow@13095
   211
  assume "\<langle>compile(v :== f),[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile(v :== f)),t\<rangle>"
nipkow@13095
   212
  thus "\<langle>v :== f,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
nipkow@13095
   213
next
nipkow@13095
   214
  fix s1 s3 c1 c2
nipkow@13095
   215
  let ?C1 = "compile c1" let ?C2 = "compile c2"
nipkow@13095
   216
  assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
nipkow@13095
   217
     and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
nipkow@13095
   218
  assume "\<langle>compile(c1;c2),[],s1\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
nipkow@13095
   219
  then obtain s2 where exec1: "\<langle>?C1,[],s1\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,s2\<rangle>" and
nipkow@13095
   220
             exec2: "\<langle>?C2,rev ?C1,s2\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
nipkow@13095
   221
    by(fastsimp dest:exec_star_decomp[of _ _ "[]" "[]",simplified])
nipkow@13095
   222
  from exec2 have exec2': "\<langle>?C2,[],s2\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,s3\<rangle>"
nipkow@13095
   223
    using exec_star_decomp[of _ "[]" "[]"] by fastsimp
nipkow@13095
   224
  have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>c s2" using IH1 exec1 by simp
nipkow@13095
   225
  moreover have "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>c s3" using IH2 exec2' by fastsimp
nipkow@13095
   226
  ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>c s3" ..
nipkow@13095
   227
next
nipkow@13095
   228
  fix s t b c1 c2
nipkow@13095
   229
  let ?if = "IF b THEN c1 ELSE c2" let ?C = "compile ?if"
nipkow@13095
   230
  let ?C1 = "compile c1" let ?C2 = "compile c2"
nipkow@13095
   231
  assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
nipkow@13095
   232
     and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
nipkow@13095
   233
     and H: "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle>"
nipkow@13095
   234
  show "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>c t"
nipkow@13095
   235
  proof cases
nipkow@13095
   236
    assume b: "b s"
nipkow@13095
   237
    with H have "\<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle>"
nipkow@13095
   238
      by (fastsimp dest:exec_star_decomp
nipkow@13095
   239
            [of _ "[JMPF (\<lambda>x. False) (size ?C2)]@?C2" "[]",simplified])
nipkow@13095
   240
    hence "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH1)
nipkow@13095
   241
    with b show ?thesis ..
nipkow@13095
   242
  next
nipkow@13095
   243
    assume b: "\<not> b s"
nipkow@13095
   244
    with H have "\<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle>"
nipkow@13095
   245
      using exec_star_decomp[of _ "[]" "[]"] by simp
nipkow@13095
   246
    hence "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH2)
nipkow@13095
   247
    with b show ?thesis ..
nipkow@13095
   248
  qed
nipkow@13095
   249
next
nipkow@13095
   250
  fix b c s t
nipkow@13095
   251
  let ?w = "WHILE b DO c" let ?W = "compile ?w" let ?C = "compile c"
nipkow@13095
   252
  let ?j1 = "JMPF b (size ?C + 1)" let ?j2 = "JMPB (size ?C + 1)"
nipkow@13095
   253
  assume IHc: "\<And>s t. \<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
nipkow@13095
   254
     and H: "\<langle>?W,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
nipkow@13095
   255
  from H obtain k where ob:"\<langle>?W,[],s\<rangle> -k\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
nipkow@13095
   256
    by(simp add:rtrancl_is_UN_rel_pow) blast
nipkow@13095
   257
  { 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"
nipkow@13095
   258
    proof (induct n rule: less_induct)
nipkow@13095
   259
      fix n
nipkow@13095
   260
      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"
nipkow@13095
   261
      fix s
nipkow@13095
   262
      assume H: "\<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
nipkow@13095
   263
      show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
nipkow@13095
   264
      proof cases
nipkow@13095
   265
	assume b: "b s"
nipkow@13095
   266
	then obtain m where m: "n = Suc m"
nipkow@13675
   267
          and "\<langle>?C @ [?j2],[?j1],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
nipkow@13095
   268
	  using H by fastsimp
nipkow@13095
   269
	then obtain r n1 n2 where n1: "\<langle>?C,[],s\<rangle> -n1\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
nipkow@13095
   270
          and n2: "\<langle>[?j2],rev ?C @ [?j1],r\<rangle> -n2\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
nipkow@13095
   271
          and n12: "m = n1+n2"
nipkow@13095
   272
	  using execn_decomp[of _ "[?j2]"]
nipkow@13095
   273
	  by(simp del: execn_simp) fast
nipkow@13095
   274
	have n2n: "n2 - 1 < n" using m n12 by arith
nipkow@13095
   275
	note b
nipkow@13095
   276
	moreover
nipkow@13095
   277
	{ from n1 have "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
nipkow@13095
   278
	    by (simp add:rtrancl_is_UN_rel_pow) fast
nipkow@13095
   279
	  hence "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c r" by(rule IHc)
nipkow@13095
   280
	}
nipkow@13095
   281
	moreover
nipkow@13095
   282
	{ have "n2 - 1 < n" using m n12 by arith
nipkow@13095
   283
	  moreover from n2 have "\<langle>?W,[],r\<rangle> -n2- 1\<rightarrow> \<langle>[],rev ?W,t\<rangle>" by fastsimp
nipkow@13095
   284
	  ultimately have "\<langle>?w,r\<rangle> \<longrightarrow>\<^sub>c t" by(rule IHm)
nipkow@13095
   285
	}
nipkow@13095
   286
	ultimately show ?thesis ..
nipkow@13095
   287
      next
nipkow@13095
   288
	assume b: "\<not> b s"
nipkow@13095
   289
	hence "t = s" using H by simp
nipkow@13095
   290
	with b show ?thesis by simp
nipkow@13095
   291
      qed
nipkow@13095
   292
    qed
nipkow@13095
   293
  }
nipkow@13095
   294
  with ob show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t" by fast
nipkow@13095
   295
qed
nipkow@13095
   296
webertj@20217
   297
(* TODO: connect with Machine 0 using M_equiv *)
nipkow@13095
   298
webertj@20217
   299
end