src/HOL/TLA/Buffer/Buffer.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TLA/Buffer/Buffer.ML	Wed Oct 08 11:50:33 1997 +0200
@@ -0,0 +1,48 @@
+(* 
+    File:        Buffer.ML
+    Author:      Stephan Merz
+    Copyright:   1997 University of Munich
+
+    Simple FIFO buffer (theorems and proofs)
+*)
+
+(* ---------------------------- Data lemmas ---------------------------- *)
+
+goal List.thy "xs ~= [] --> tl(xs @ ys) = (tl xs) @ ys";
+by (auto_tac (!claset, !simpset addsimps [tl_append,neq_Nil_conv]));
+qed_spec_mp "tl_append2";
+Addsimps [tl_append2];
+
+goal List.thy "xs ~= [] --> tl xs ~= xs";
+by (auto_tac (!claset, !simpset addsimps [neq_Nil_conv]));
+qed_spec_mp "tl_not_self";
+Addsimps [tl_not_self];
+
+goal List.thy "!ys zs. (ys @ xs = zs @ xs) = (ys=zs)";
+by (induct_tac "xs" 1);
+by (Simp_tac 1);
+by (REPEAT (rtac allI 1));
+by (subgoal_tac "((ys @ [a]) @ list = (zs @ [a]) @ list) = (ys=zs)" 1);
+by (Asm_full_simp_tac 1);
+by (Blast_tac 1);
+qed_spec_mp "append_same_eq";
+AddIffs [append_same_eq];
+
+(* ---------------------------- Action lemmas ---------------------------- *)
+
+(* Dequeue is visible *)
+goal Buffer.thy "<Deq ic q oc>_<ic,q,oc> .= Deq ic q oc";
+by (auto_tac (!claset, !simpset addsimps [angle_def,Deq_def]));
+qed "Deq_visible";
+
+(* Enabling condition for dequeue -- NOT NEEDED *)
+goalw Buffer.thy [temp_rewrite Deq_visible]
+   "!!q. base_var <ic,q,oc> ==> $Enabled (<Deq ic q oc>_<ic,q,oc>) .= ($q .~= .[])";
+by (auto_tac (!claset addSEs [base_enabled,enabledE], !simpset addsimps [Deq_def]));
+qed "Deq_enabled";
+
+(* For the left-to-right implication, we don't need the base variable stuff *)
+goalw Buffer.thy [temp_rewrite Deq_visible] 
+   "$Enabled (<Deq ic q oc>_<ic,q,oc>) .-> ($q .~= .[])";
+by (auto_tac (!claset addSEs [enabledE], !simpset addsimps [Deq_def]));
+qed "Deq_enabledE";