379 done

   379 done

   380 

   380 

   381 lemma abc_step_red: 

   381 lemma abc_step_red: 

   382  "abc_steps_l ac aprog stp = (as, am) \<Longrightarrow> 

   382  "abc_steps_l ac aprog stp = (as, am) \<Longrightarrow> 

   383    abc_steps_l ac aprog (Suc stp) = abc_step_l (as, am) (abc_fetch as aprog) "

   383    abc_steps_l ac aprog (Suc stp) = abc_step_l (as, am) (abc_fetch as aprog) "

   385 

   385 

   386 lemma tm_shift_fetch: 

   386 lemma tm_shift_fetch: 

   387   "\<lbrakk>fetch A s b = (ac, ns); ns \<noteq> 0 \<rbrakk>

   387   "\<lbrakk>fetch A s b = (ac, ns); ns \<noteq> 0 \<rbrakk>

   388   \<Longrightarrow> fetch (shift A off) s b = (ac, ns + off)"

   388   \<Longrightarrow> fetch (shift A off) s b = (ac, ns + off)"

   389 apply(case_tac b)

   389 apply(case_tac b)

   443   and abc_fetch: "abc_fetch as ap = Some ins" 

   443   and abc_fetch: "abc_fetch as ap = Some ins" 

   444   and fetch: "fetch (ci ly (start_of ly as) ins)

   444   and fetch: "fetch (ci ly (start_of ly as) ins)

   445        (Suc s - start_of ly as) b = (ac, ns)"

   445        (Suc s - start_of ly as) b = (ac, ns)"

   446   and notfinal: "ns \<noteq> 0"

   446   and notfinal: "ns \<noteq> 0"

   447   shows "fetch tp s b = (ac, ns)"

   447   shows "fetch tp s b = (ac, ns)"

   454   

   449   

   455 lemma step_eq_in:

   450 lemma step_eq_in:

   456   assumes layout: "ly = layout_of ap"

   451   assumes layout: "ly = layout_of ap"

   457   and compile: "tp = tm_of ap"

   452   and compile: "tp = tm_of ap"

   458   and fetch: "abc_fetch as ap = Some ins"    

   453   and fetch: "abc_fetch as ap = Some ins"