6 Simple FIFO buffer (theorems and proofs) |
6 Simple FIFO buffer (theorems and proofs) |
7 *) |
7 *) |
8 |
8 |
9 (* ---------------------------- Data lemmas ---------------------------- *) |
9 (* ---------------------------- Data lemmas ---------------------------- *) |
10 |
10 |
11 (* "xs ~= [] --> tl(xs @ ys) = (tl xs) @ ys" *) |
11 context List.thy; |
12 Addsimps [tl_append2]; |
|
13 |
|
14 goal List.thy "xs ~= [] --> tl xs ~= xs"; |
12 goal List.thy "xs ~= [] --> tl xs ~= xs"; |
15 by (auto_tac (claset(), simpset() addsimps [neq_Nil_conv])); |
13 by (auto_tac (claset(), simpset() addsimps [neq_Nil_conv])); |
16 qed_spec_mp "tl_not_self"; |
14 qed_spec_mp "tl_not_self"; |
|
15 context Buffer.thy; |
|
16 |
17 Addsimps [tl_not_self]; |
17 Addsimps [tl_not_self]; |
18 |
|
19 (* "!ys zs. (ys @ xs = zs @ xs) = (ys=zs)" has been subsumed *) |
|
20 |
18 |
21 (* ---------------------------- Action lemmas ---------------------------- *) |
19 (* ---------------------------- Action lemmas ---------------------------- *) |
22 |
20 |
23 (* Dequeue is visible *) |
21 (* Dequeue is visible *) |
24 Goal "<Deq ic q oc>_<ic,q,oc> .= Deq ic q oc"; |
22 Goal "|- <Deq ic q oc>_(ic,q,oc) = Deq ic q oc"; |
25 by (auto_tac (claset(), simpset() addsimps [angle_def,Deq_def])); |
23 by (auto_tac (claset(), simpset() addsimps [angle_def,Deq_def])); |
26 qed "Deq_visible"; |
24 qed "Deq_visible"; |
27 |
25 |
28 (* Enabling condition for dequeue -- NOT NEEDED *) |
26 (* Enabling condition for dequeue -- NOT NEEDED *) |
29 Goalw [temp_rewrite Deq_visible] |
27 Goalw [temp_rewrite Deq_visible] |
30 "!!q. base_var <ic,q,oc> ==> $Enabled (<Deq ic q oc>_<ic,q,oc>) .= ($q .~= .[])"; |
28 "!!q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q ~= #[])"; |
31 by (force_tac (claset() addSEs [base_enabled,enabledE], simpset() addsimps [Deq_def]) 1); |
29 by (force_tac (claset() addSEs [base_enabled,enabledE], simpset() addsimps [Deq_def]) 1); |
32 qed "Deq_enabled"; |
30 qed "Deq_enabled"; |
33 |
31 |
34 (* For the left-to-right implication, we don't need the base variable stuff *) |
32 (* For the left-to-right implication, we don't need the base variable stuff *) |
35 Goalw [temp_rewrite Deq_visible] |
33 Goalw [temp_rewrite Deq_visible] |
36 "$Enabled (<Deq ic q oc>_<ic,q,oc>) .-> ($q .~= .[])"; |
34 "|- Enabled (<Deq ic q oc>_(ic,q,oc)) --> (q ~= #[])"; |
37 by (auto_tac (claset() addSEs [enabledE], simpset() addsimps [Deq_def])); |
35 by (auto_tac (claset() addSEs [enabledE], simpset() addsimps [Deq_def])); |
38 qed "Deq_enabledE"; |
36 qed "Deq_enabledE"; |