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