equal
deleted
inserted
replaced
57 (*** Step simulation ***) |
57 (*** Step simulation ***) |
58 lemma DB_step_simulation: "\<turnstile> [DBNext]_(inp,mid,out,q1,q2) \<longrightarrow> [Next inp qc out]_(inp,qc,out)" |
58 lemma DB_step_simulation: "\<turnstile> [DBNext]_(inp,mid,out,q1,q2) \<longrightarrow> [Next inp qc out]_(inp,qc,out)" |
59 apply (rule square_simulation) |
59 apply (rule square_simulation) |
60 apply clarsimp |
60 apply clarsimp |
61 apply (tactic |
61 apply (tactic |
62 \<open>action_simp_tac (@{context} addsimps (@{thm hd_append} :: @{thms db_defs})) [] [] 1\<close>) |
62 \<open>action_simp_tac (\<^context> addsimps (@{thm hd_append} :: @{thms db_defs})) [] [] 1\<close>) |
63 done |
63 done |
64 |
64 |
65 |
65 |
66 (*** Simulation of fairness ***) |
66 (*** Simulation of fairness ***) |
67 |
67 |