src/HOL/TLA/Buffer/DBuffer.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 13601 fd3e3d6b37b2
child 17309 c43ed29bd197
permissions -rw-r--r--
import -> imports
     1 (* 
     2     File:        DBuffer.ML
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6     Double FIFO buffer implements simple FIFO buffer.
     7 *)
     8 
     9 
    10 val db_css = (claset(), simpset() addsimps [qc_def]);
    11 Addsimps [qc_def];
    12 
    13 val db_defs = [BInit_def, Enq_def, Deq_def, Next_def, IBuffer_def, Buffer_def,
    14                DBInit_def,DBEnq_def,DBDeq_def,DBPass_def,DBNext_def,DBuffer_def];
    15 
    16 
    17 (*** Proper initialization ***)
    18 Goal "|- Init DBInit --> Init (BInit inp qc out)";
    19 by (auto_tac (db_css addsimps2 [Init_def,DBInit_def,BInit_def]));
    20 qed "DBInit";
    21 
    22 
    23 (*** Step simulation ***)
    24 Goal "|- [DBNext]_(inp,mid,out,q1,q2) --> [Next inp qc out]_(inp,qc,out)";
    25 by (rtac square_simulation 1);
    26 by (Clarsimp_tac 1);
    27 by (action_simp_tac (simpset() addsimps hd_append::db_defs) [] [] 1);
    28 qed "DB_step_simulation";
    29 
    30 
    31 (*** Simulation of fairness ***)
    32 
    33 (* Compute enabledness predicates for DBDeq and DBPass actions *)
    34 Goalw [angle_def,DBDeq_def,Deq_def] "|- <DBDeq>_(inp,mid,out,q1,q2) = DBDeq";
    35 by (REPEAT (Safe_tac THEN Asm_lr_simp_tac 1));
    36 qed "DBDeq_visible";
    37 
    38 Goalw [action_rewrite DBDeq_visible]
    39   "|- Enabled (<DBDeq>_(inp,mid,out,q1,q2)) = (q2 ~= #[])";
    40 by (force_tac (db_css addSIs2 [DB_base RS base_enabled] addSEs2 [enabledE] 
    41                      addsimps2 [angle_def,DBDeq_def,Deq_def]) 1);
    42 qed "DBDeq_enabled";
    43 
    44 Goal "|- <DBPass>_(inp,mid,out,q1,q2) = DBPass";
    45 by (auto_tac (db_css addsimps2 [angle_def,DBPass_def,Deq_def]));
    46 qed "DBPass_visible";
    47 
    48 Goalw [action_rewrite DBPass_visible]
    49    "|- Enabled (<DBPass>_(inp,mid,out,q1,q2)) = (q1 ~= #[])";
    50 by (force_tac (db_css addSIs2 [DB_base RS base_enabled] addSEs2 [enabledE] 
    51                      addsimps2 [angle_def,DBPass_def,Deq_def]) 1);
    52 qed "DBPass_enabled";
    53 
    54 
    55 (* The plan for proving weak fairness at the higher level is to prove
    56    (0)  DBuffer => (Enabled (Deq inp qc out) ~> (Deq inp qc out))
    57    which is in turn reduced to the two leadsto conditions
    58    (1)  DBuffer => (Enabled (Deq inp qc out) ~> q2 ~= [])
    59    (2)  DBuffer => (q2 ~= [] ~> DBDeq)
    60    and the fact that DBDeq implies <Deq inp qc out>_(inp,qc,out)
    61    (and therefore DBDeq ~> <Deq inp qc out>_(inp,qc,out) trivially holds).
    62 
    63    Condition (1) is reduced to
    64    (1a) DBuffer => (qc ~= [] /\ q2 = [] ~> q2 ~= [])
    65    by standard leadsto rules (leadsto_classical) and rule Deq_enabledE.
    66 
    67    Both (1a) and (2) are proved from DBuffer's WF conditions by standard
    68    WF reasoning (Lamport's WF1 and WF_leadsto).
    69    The condition WF(Deq inp qc out) follows from (0) by rule leadsto_WF.
    70 
    71    One could use Lamport's WF2 instead.
    72 *)
    73 
    74 (* Condition (1a) *)
    75 Goal "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2) \
    76 \        --> (qc ~= #[] & q2 = #[] ~> q2 ~= #[])";
    77 by (rtac WF1 1);
    78 by (force_tac (db_css addsimps2 db_defs) 1);
    79 by (force_tac (db_css addsimps2 [angle_def,DBPass_def]) 1);
    80 by (force_tac (db_css addsimps2 [DBPass_enabled]) 1);
    81 qed "DBFair_1a";
    82 
    83 (* Condition (1) *)
    84 Goal "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2) \
    85 \        --> (Enabled (<Deq inp qc out>_(inp,qc,out)) ~> q2 ~= #[])";
    86 by (Clarsimp_tac 1);
    87 by (rtac (temp_use leadsto_classical) 1);
    88 by (rtac ((temp_use DBFair_1a) RS (temp_use LatticeTransitivity)) 1);
    89 by (TRYALL atac);
    90 by (rtac (temp_use ImplLeadsto_gen) 1);
    91 by (force_tac (db_css addSIs2 [necT] addSDs2 [STL2_gen, Deq_enabledE]
    92                       addsimps2 Init_defs) 1);
    93 qed "DBFair_1";
    94 
    95 (* Condition (2) *)
    96 Goal "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2) \
    97 \        --> (q2 ~= #[] ~> DBDeq)";
    98 by (rtac WF_leadsto 1);
    99 by (force_tac (db_css addsimps2 [DBDeq_enabled]) 1);
   100 by (force_tac (db_css addsimps2 [angle_def]) 1);
   101 by (force_tac (db_css addsimps2 db_defs addSEs2 [Stable]) 1);
   102 qed "DBFair_2";
   103 
   104 (* High-level fairness *)
   105 Goal "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2) \
   106 \                                       & WF(DBDeq)_(inp,mid,out,q1,q2)  \ 
   107 \        --> WF(Deq inp qc out)_(inp,qc,out)";
   108 by (auto_tac (temp_css addSIs2 [leadsto_WF,
   109                                 (temp_use DBFair_1) RSN(2,(temp_use LatticeTransitivity)),
   110                                 (temp_use DBFair_2) RSN(2,(temp_use LatticeTransitivity))]));
   111 by (auto_tac (db_css addSIs2 [ImplLeadsto_simple]
   112                      addsimps2 [angle_def,DBDeq_def,Deq_def,hd_append]));
   113 qed "DBFair";
   114 
   115 (*** Main theorem ***)
   116 Goalw [DBuffer_def,Buffer_def,IBuffer_def] "|- DBuffer --> Buffer inp out";
   117 by (force_tac (temp_css addSIs2 [eexI,DBInit,DB_step_simulation RS STL4,DBFair]) 1);
   118 qed "DBuffer_impl_Buffer";