author | berghofe |
Mon, 30 Sep 2002 16:14:02 +0200 | |
changeset 13601 | fd3e3d6b37b2 |
parent 9517 | f58863b1406a |
child 14396 | 011a2a49d303 |
permissions | -rw-r--r-- |
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 |
||
6255 | 11 |
context List.thy; |
3807 | 12 |
goal List.thy "xs ~= [] --> tl xs ~= xs"; |
4089 | 13 |
by (auto_tac (claset(), simpset() addsimps [neq_Nil_conv])); |
3807 | 14 |
qed_spec_mp "tl_not_self"; |
6255 | 15 |
context Buffer.thy; |
3807 | 16 |
|
6255 | 17 |
Addsimps [tl_not_self]; |
3807 | 18 |
|
19 |
(* ---------------------------- Action lemmas ---------------------------- *) |
|
20 |
||
21 |
(* Dequeue is visible *) |
|
13601 | 22 |
Goalw [angle_def,Deq_def] "|- <Deq ic q oc>_(ic,q,oc) = Deq ic q oc"; |
23 |
by (REPEAT (Safe_tac THEN Asm_lr_simp_tac 1)); |
|
3807 | 24 |
qed "Deq_visible"; |
25 |
||
26 |
(* Enabling condition for dequeue -- NOT NEEDED *) |
|
5069 | 27 |
Goalw [temp_rewrite Deq_visible] |
6255 | 28 |
"!!q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q ~= #[])"; |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
29 |
by (force_tac (claset() addSEs [base_enabled,enabledE], |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
30 |
simpset() addsimps [Deq_def]) 1); |
3807 | 31 |
qed "Deq_enabled"; |
32 |
||
33 |
(* For the left-to-right implication, we don't need the base variable stuff *) |
|
5069 | 34 |
Goalw [temp_rewrite Deq_visible] |
6255 | 35 |
"|- Enabled (<Deq ic q oc>_(ic,q,oc)) --> (q ~= #[])"; |
4089 | 36 |
by (auto_tac (claset() addSEs [enabledE], simpset() addsimps [Deq_def])); |
3807 | 37 |
qed "Deq_enabledE"; |