--- a/src/HOL/TLA/Buffer/Buffer.thy Fri Dec 01 17:22:33 2006 +0100
+++ b/src/HOL/TLA/Buffer/Buffer.thy Sat Dec 02 02:52:02 2006 +0100
@@ -3,9 +3,6 @@
ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
-
- Theory Name: Buffer
- Logic Image: TLA
*)
header {* A simple FIFO buffer (synchronous communication, interleaving) *}
@@ -40,6 +37,34 @@
& WF(Deq ic q oc)_(ic,q,oc)"
Buffer_def: "Buffer ic oc == TEMP (EEX q. IBuffer ic q oc)"
-ML {* use_legacy_bindings (the_context ()) *}
+
+(* ---------------------------- Data lemmas ---------------------------- *)
+
+(*FIXME: move to theory List? Maybe as (tl xs = xs) = (xs = [])"?*)
+lemma tl_not_self [simp]: "xs ~= [] ==> tl xs ~= xs"
+ by (auto simp: neq_Nil_conv)
+
+
+(* ---------------------------- Action lemmas ---------------------------- *)
+
+(* Dequeue is visible *)
+lemma Deq_visible: "|- <Deq ic q oc>_(ic,q,oc) = Deq ic q oc"
+ apply (unfold angle_def Deq_def)
+ apply (safe, simp (asm_lr))+
+ done
+
+(* Enabling condition for dequeue -- NOT NEEDED *)
+lemma Deq_enabled:
+ "!!q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q ~= #[])"
+ apply (unfold Deq_visible [temp_rewrite])
+ apply (force elim!: base_enabled [temp_use] enabledE [temp_use] simp: Deq_def)
+ done
+
+(* For the left-to-right implication, we don't need the base variable stuff *)
+lemma Deq_enabledE:
+ "|- Enabled (<Deq ic q oc>_(ic,q,oc)) --> (q ~= #[])"
+ apply (unfold Deq_visible [temp_rewrite])
+ apply (auto elim!: enabledE simp add: Deq_def)
+ done
end