equal
deleted
inserted
replaced
1 (* Title: HOL/TLA/Buffer/DBuffer.thy |
1 (* Title: HOL/TLA/Buffer/DBuffer.thy |
2 Author: Stephan Merz, University of Munich |
2 Author: Stephan Merz, University of Munich |
3 *) |
3 *) |
4 |
4 |
5 section {* Two FIFO buffers in a row, with interleaving assumption *} |
5 section \<open>Two FIFO buffers in a row, with interleaving assumption\<close> |
6 |
6 |
7 theory DBuffer |
7 theory DBuffer |
8 imports Buffer |
8 imports Buffer |
9 begin |
9 begin |
10 |
10 |
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 {* action_simp_tac (@{context} addsimps (@{thm hd_append} :: @{thms db_defs})) [] [] 1 *}) |
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 |