|
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 |
|
11 goal List.thy "xs ~= [] --> tl(xs @ ys) = (tl xs) @ ys"; |
|
12 by (auto_tac (!claset, !simpset addsimps [tl_append,neq_Nil_conv])); |
|
13 qed_spec_mp "tl_append2"; |
|
14 Addsimps [tl_append2]; |
|
15 |
|
16 goal List.thy "xs ~= [] --> tl xs ~= xs"; |
|
17 by (auto_tac (!claset, !simpset addsimps [neq_Nil_conv])); |
|
18 qed_spec_mp "tl_not_self"; |
|
19 Addsimps [tl_not_self]; |
|
20 |
|
21 goal List.thy "!ys zs. (ys @ xs = zs @ xs) = (ys=zs)"; |
|
22 by (induct_tac "xs" 1); |
|
23 by (Simp_tac 1); |
|
24 by (REPEAT (rtac allI 1)); |
|
25 by (subgoal_tac "((ys @ [a]) @ list = (zs @ [a]) @ list) = (ys=zs)" 1); |
|
26 by (Asm_full_simp_tac 1); |
|
27 by (Blast_tac 1); |
|
28 qed_spec_mp "append_same_eq"; |
|
29 AddIffs [append_same_eq]; |
|
30 |
|
31 (* ---------------------------- Action lemmas ---------------------------- *) |
|
32 |
|
33 (* Dequeue is visible *) |
|
34 goal Buffer.thy "<Deq ic q oc>_<ic,q,oc> .= Deq ic q oc"; |
|
35 by (auto_tac (!claset, !simpset addsimps [angle_def,Deq_def])); |
|
36 qed "Deq_visible"; |
|
37 |
|
38 (* Enabling condition for dequeue -- NOT NEEDED *) |
|
39 goalw Buffer.thy [temp_rewrite Deq_visible] |
|
40 "!!q. base_var <ic,q,oc> ==> $Enabled (<Deq ic q oc>_<ic,q,oc>) .= ($q .~= .[])"; |
|
41 by (auto_tac (!claset addSEs [base_enabled,enabledE], !simpset addsimps [Deq_def])); |
|
42 qed "Deq_enabled"; |
|
43 |
|
44 (* For the left-to-right implication, we don't need the base variable stuff *) |
|
45 goalw Buffer.thy [temp_rewrite Deq_visible] |
|
46 "$Enabled (<Deq ic q oc>_<ic,q,oc>) .-> ($q .~= .[])"; |
|
47 by (auto_tac (!claset addSEs [enabledE], !simpset addsimps [Deq_def])); |
|
48 qed "Deq_enabledE"; |