1 header {* 

     1 header {* 

     2  {\em abacus} a kind of register machine

     2  {\em abacus} a kind of register machine

     3 *}

     3 *}

     4 

     4 

     5 theory abacus

     5 theory abacus

     7 begin

     7 begin

     8 

     8 

     9 text {*

     9 text {*

    10   {\em Abacus} instructions:

    10   {\em Abacus} instructions:

    11 *}

    11 *}

   157 *)

   157 *)

   158 

   158 

   159 lemma frame: "{p} c {q} \<Longrightarrow> \<forall> r. {p * r} c {q * r}"

   159 lemma frame: "{p} c {q} \<Longrightarrow> \<forall> r. {p * r} c {q * r}"

   160 apply (unfold Hoare_abc_def, clarify)

   160 apply (unfold Hoare_abc_def, clarify)

   161 apply (erule_tac x = "(a, aa, ab, b)" in allE)

   161 apply (erule_tac x = "(a, aa, ab, b)" in allE)

   163 apply(simp add: stimes_ac)

   163 apply(simp add: stimes_ac)

   164 done

   164 done

   165 

   165 

   166 lemma code_extension: "\<lbrakk>{p} c {q}\<rbrakk> \<Longrightarrow> (\<forall> e. {p} c * e {q})"

   166 lemma code_extension: "\<lbrakk>{p} c {q}\<rbrakk> \<Longrightarrow> (\<forall> e. {p} c * e {q})"

   167   apply (unfold Hoare_abc_def, clarify)

   167   apply (unfold Hoare_abc_def, clarify)