src/HOL/TLA/Buffer/DBuffer.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TLA/Buffer/DBuffer.ML	Wed Oct 08 11:50:33 1997 +0200
@@ -0,0 +1,119 @@
+(* 
+    File:        DBuffer.ML
+    Author:      Stephan Merz
+    Copyright:   1997 University of Munich
+
+    Double FIFO buffer implements simple FIFO buffer.
+*)
+
+val db_css = (!claset, !simpset addsimps [qc_def]);
+Addsimps [qc_def];
+
+val db_defs = [BInit_def, Enq_def, Deq_def, Next_def, IBuffer_def, Buffer_def,
+               DBInit_def,DBEnq_def,DBDeq_def,DBPass_def,DBNext_def,DBuffer_def];
+
+
+(*** Proper initialization ***)
+goal DBuffer.thy "Init DBInit .-> Init (BInit inp qc out)";
+by (auto_tac (db_css addsimps2 [Init_def,DBInit_def,BInit_def]));
+qed "DBInit";
+
+
+(*** Step simulation ***)
+goal DBuffer.thy "[DBNext]_<inp,mid,out,q1,q2> .-> [Next inp qc out]_<inp,qc,out>";
+by (rtac square_simulation 1);
+by (Action_simp_tac 1);
+by (action_simp_tac (!simpset addsimps hd_append::db_defs) [] [] 1);
+qed "DB_step_simulation";
+
+
+(*** Simulation of fairness ***)
+
+(* Compute enabledness predicates for DBDeq and DBPass actions *)
+goal DBuffer.thy "<DBDeq>_<inp,mid,out,q1,q2> .= DBDeq";
+by (auto_tac (db_css addsimps2 [angle_def,DBDeq_def,Deq_def]));
+qed "DBDeq_visible";
+
+goal DBuffer.thy "$Enabled (<DBDeq>_<inp,mid,out,q1,q2>) .= ($q2 .~= .[])";
+by (rewtac (action_rewrite DBDeq_visible));
+by (cut_facts_tac [DB_base] 1);
+by (auto_tac (db_css addSEs2 [base_enabled,enabledE] 
+                     addsimps2 [angle_def,DBDeq_def,Deq_def]));
+qed "DBDeq_enabled";
+
+goal DBuffer.thy "<DBPass>_<inp,mid,out,q1,q2> .= DBPass";
+by (auto_tac (db_css addsimps2 [angle_def,DBPass_def,Deq_def]));
+qed "DBPass_visible";
+
+goal DBuffer.thy "$Enabled (<DBPass>_<inp,mid,out,q1,q2>) .= ($q1 .~= .[])";
+by (rewtac (action_rewrite DBPass_visible));
+by (cut_facts_tac [DB_base] 1);
+by (auto_tac (db_css addSEs2 [base_enabled,enabledE] 
+                     addsimps2 [angle_def,DBPass_def,Deq_def]));
+qed "DBPass_enabled";
+
+
+(* The plan for proving weak fairness at the higher level is to prove
+   (0)  DBuffer => (Enabled (Deq inp qc out) ~> (Deq inp qc out))
+   which is in turn reduced to the two leadsto conditions
+   (1)  DBuffer => (Enabled (Deq inp qc out) ~> q2 ~= [])
+   (2)  DBuffer => (q2 ~= [] ~> DBDeq)
+   and the fact that DBDeq implies <Deq inp qc out>_<inp,qc,out>
+   (and therefore DBDeq ~> <Deq inp qc out>_<inp,qc,out> trivially holds).
+
+   Condition (1) is reduced to
+   (1a) DBuffer => (qc ~= [] /\ q2 = [] ~> q2 ~= [])
+   by standard leadsto rules (leadsto_classical) and rule Deq_enabledE.
+
+   Both (1a) and (2) are proved from DBuffer's WF conditions by standard
+   WF reasoning (Lamport's WF1 and WF_leadsto).
+   The condition WF(Deq inp qc out) follows from (0) by rule leadsto_WF.
+
+   One could use Lamport's WF2 instead.
+*)
+
+(* Condition (1a) *)
+goal DBuffer.thy 
+  "[][DBNext]_<inp,mid,out,q1,q2> .& WF(DBPass)_<inp,mid,out,q1,q2> \
+\  .-> ($qc .~= .[] .& $q2 .= .[] ~> $q2 .~= .[])";
+by (rtac WF1 1);
+by (action_simp_tac (!simpset addsimps square_def::db_defs) [] [] 1);
+by (action_simp_tac (!simpset addsimps [angle_def,DBPass_def]) [] [] 1);
+by (action_simp_tac (!simpset addsimps [DBPass_enabled]) [] [] 1);
+qed "DBFair_1a";
+
+(* Condition (1) *)
+goal DBuffer.thy
+  "[][DBNext]_<inp,mid,out,q1,q2> .& WF(DBPass)_<inp,mid,out,q1,q2> \
+\  .-> ($Enabled (<Deq inp qc out>_<inp,qc,out>) ~> $q2 .~= .[])";
+by (auto_tac (temp_css addSIs2 [leadsto_classical] addSEs2 [temp_conjimpE DBFair_1a]));
+by (auto_tac (temp_css addsimps2 [leadsto,Init_def] addDs2 [STL2bD]
+                       addSDs2 [action_mp Deq_enabledE] addSEs2 [STL4E]));
+qed "DBFair_1";
+
+(* Condition (2) *)
+goal DBuffer.thy
+  "[][DBNext]_<inp,mid,out,q1,q2> .& WF(DBDeq)_<inp,mid,out,q1,q2> \
+\  .-> ($q2 .~= .[] ~> DBDeq)";
+by (rtac WF_leadsto 1);
+by (action_simp_tac (!simpset addsimps [DBDeq_visible,DBDeq_enabled]) [] [] 1);
+by (action_simp_tac (!simpset addsimps [angle_def]) [] [] 1);
+by (action_simp_tac (!simpset addsimps square_def::db_defs) [tempI] [Stable] 1);
+qed "DBFair_2";
+
+(* High-level fairness *)
+goal DBuffer.thy
+  "[][DBNext]_<inp,mid,out,q1,q2> .& WF(DBPass)_<inp,mid,out,q1,q2> \
+\                                 .& WF(DBDeq)_<inp,mid,out,q1,q2>  \ 
+\  .-> WF(Deq inp qc out)_<inp,qc,out>";
+by (auto_tac (db_css addSIs2 [leadsto_WF]));
+by (auto_tac (db_css addSIs2 [(temp_mp DBFair_1) RSN(2,LatticeTransitivity)]));
+by (auto_tac (db_css addSIs2 [(temp_mp DBFair_2) RSN(2,LatticeTransitivity)]));
+by (auto_tac (db_css addSIs2 [ImplLeadsto] addSEs2 [STL4E]
+                     addsimps2 [angle_def,DBDeq_def,Deq_def,hd_append]));
+qed "DBFair";
+
+(*** Main theorem ***)
+goalw DBuffer.thy [DBuffer_def,Buffer_def,IBuffer_def] "DBuffer .-> Buffer inp out";
+by (auto_tac (db_css addSIs2 (map temp_mp [eexI,DBInit,DB_step_simulation RS STL4,DBFair])));
+qed "DBuffer_impl_Buffer";