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