src/HOL/TLA/Buffer/DBuffer.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477 b3e5857d8d99
parent 4089 96fba19bcbe2
child 5069 3ea049f7979d
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
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@4089
     9
val db_css = (claset(), simpset() addsimps [qc_def]);
wenzelm@3807
    10
Addsimps [qc_def];
wenzelm@3807
    11
wenzelm@3807
    12
val db_defs = [BInit_def, Enq_def, Deq_def, Next_def, IBuffer_def, Buffer_def,
wenzelm@3807
    13
               DBInit_def,DBEnq_def,DBDeq_def,DBPass_def,DBNext_def,DBuffer_def];
wenzelm@3807
    14
wenzelm@3807
    15
wenzelm@3807
    16
(*** Proper initialization ***)
wenzelm@3807
    17
goal DBuffer.thy "Init DBInit .-> Init (BInit inp qc out)";
wenzelm@3807
    18
by (auto_tac (db_css addsimps2 [Init_def,DBInit_def,BInit_def]));
wenzelm@3807
    19
qed "DBInit";
wenzelm@3807
    20
wenzelm@3807
    21
wenzelm@3807
    22
(*** Step simulation ***)
wenzelm@3807
    23
goal DBuffer.thy "[DBNext]_<inp,mid,out,q1,q2> .-> [Next inp qc out]_<inp,qc,out>";
wenzelm@3807
    24
by (rtac square_simulation 1);
wenzelm@3807
    25
by (Action_simp_tac 1);
wenzelm@4089
    26
by (action_simp_tac (simpset() addsimps hd_append::db_defs) [] [] 1);
wenzelm@3807
    27
qed "DB_step_simulation";
wenzelm@3807
    28
wenzelm@3807
    29
wenzelm@3807
    30
(*** Simulation of fairness ***)
wenzelm@3807
    31
wenzelm@3807
    32
(* Compute enabledness predicates for DBDeq and DBPass actions *)
wenzelm@3807
    33
goal DBuffer.thy "<DBDeq>_<inp,mid,out,q1,q2> .= DBDeq";
wenzelm@3807
    34
by (auto_tac (db_css addsimps2 [angle_def,DBDeq_def,Deq_def]));
wenzelm@3807
    35
qed "DBDeq_visible";
wenzelm@3807
    36
wenzelm@3807
    37
goal DBuffer.thy "$Enabled (<DBDeq>_<inp,mid,out,q1,q2>) .= ($q2 .~= .[])";
wenzelm@3807
    38
by (rewtac (action_rewrite DBDeq_visible));
wenzelm@3807
    39
by (cut_facts_tac [DB_base] 1);
paulson@4477
    40
by (old_auto_tac (db_css addSEs2 [base_enabled,enabledE] 
paulson@4477
    41
                         addsimps2 [angle_def,DBDeq_def,Deq_def]));
wenzelm@3807
    42
qed "DBDeq_enabled";
wenzelm@3807
    43
wenzelm@3807
    44
goal DBuffer.thy "<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@3807
    48
goal DBuffer.thy "$Enabled (<DBPass>_<inp,mid,out,q1,q2>) .= ($q1 .~= .[])";
wenzelm@3807
    49
by (rewtac (action_rewrite DBPass_visible));
wenzelm@3807
    50
by (cut_facts_tac [DB_base] 1);
wenzelm@3807
    51
by (auto_tac (db_css addSEs2 [base_enabled,enabledE] 
wenzelm@3807
    52
                     addsimps2 [angle_def,DBPass_def,Deq_def]));
wenzelm@3807
    53
qed "DBPass_enabled";
wenzelm@3807
    54
wenzelm@3807
    55
wenzelm@3807
    56
(* The plan for proving weak fairness at the higher level is to prove
wenzelm@3807
    57
   (0)  DBuffer => (Enabled (Deq inp qc out) ~> (Deq inp qc out))
wenzelm@3807
    58
   which is in turn reduced to the two leadsto conditions
wenzelm@3807
    59
   (1)  DBuffer => (Enabled (Deq inp qc out) ~> q2 ~= [])
wenzelm@3807
    60
   (2)  DBuffer => (q2 ~= [] ~> DBDeq)
wenzelm@3807
    61
   and the fact that DBDeq implies <Deq inp qc out>_<inp,qc,out>
wenzelm@3807
    62
   (and therefore DBDeq ~> <Deq inp qc out>_<inp,qc,out> trivially holds).
wenzelm@3807
    63
wenzelm@3807
    64
   Condition (1) is reduced to
wenzelm@3807
    65
   (1a) DBuffer => (qc ~= [] /\ q2 = [] ~> q2 ~= [])
wenzelm@3807
    66
   by standard leadsto rules (leadsto_classical) and rule Deq_enabledE.
wenzelm@3807
    67
wenzelm@3807
    68
   Both (1a) and (2) are proved from DBuffer's WF conditions by standard
wenzelm@3807
    69
   WF reasoning (Lamport's WF1 and WF_leadsto).
wenzelm@3807
    70
   The condition WF(Deq inp qc out) follows from (0) by rule leadsto_WF.
wenzelm@3807
    71
wenzelm@3807
    72
   One could use Lamport's WF2 instead.
wenzelm@3807
    73
*)
wenzelm@3807
    74
wenzelm@3807
    75
(* Condition (1a) *)
wenzelm@3807
    76
goal DBuffer.thy 
wenzelm@3807
    77
  "[][DBNext]_<inp,mid,out,q1,q2> .& WF(DBPass)_<inp,mid,out,q1,q2> \
wenzelm@3807
    78
\  .-> ($qc .~= .[] .& $q2 .= .[] ~> $q2 .~= .[])";
wenzelm@3807
    79
by (rtac WF1 1);
wenzelm@4089
    80
by (action_simp_tac (simpset() addsimps square_def::db_defs) [] [] 1);
wenzelm@4089
    81
by (action_simp_tac (simpset() addsimps [angle_def,DBPass_def]) [] [] 1);
wenzelm@4089
    82
by (action_simp_tac (simpset() addsimps [DBPass_enabled]) [] [] 1);
wenzelm@3807
    83
qed "DBFair_1a";
wenzelm@3807
    84
wenzelm@3807
    85
(* Condition (1) *)
wenzelm@3807
    86
goal DBuffer.thy
wenzelm@3807
    87
  "[][DBNext]_<inp,mid,out,q1,q2> .& WF(DBPass)_<inp,mid,out,q1,q2> \
wenzelm@3807
    88
\  .-> ($Enabled (<Deq inp qc out>_<inp,qc,out>) ~> $q2 .~= .[])";
wenzelm@3807
    89
by (auto_tac (temp_css addSIs2 [leadsto_classical] addSEs2 [temp_conjimpE DBFair_1a]));
wenzelm@3807
    90
by (auto_tac (temp_css addsimps2 [leadsto,Init_def] addDs2 [STL2bD]
wenzelm@3807
    91
                       addSDs2 [action_mp Deq_enabledE] addSEs2 [STL4E]));
wenzelm@3807
    92
qed "DBFair_1";
wenzelm@3807
    93
wenzelm@3807
    94
(* Condition (2) *)
wenzelm@3807
    95
goal DBuffer.thy
wenzelm@3807
    96
  "[][DBNext]_<inp,mid,out,q1,q2> .& WF(DBDeq)_<inp,mid,out,q1,q2> \
wenzelm@3807
    97
\  .-> ($q2 .~= .[] ~> DBDeq)";
wenzelm@3807
    98
by (rtac WF_leadsto 1);
wenzelm@4089
    99
by (action_simp_tac (simpset() addsimps [DBDeq_visible,DBDeq_enabled]) [] [] 1);
wenzelm@4089
   100
by (action_simp_tac (simpset() addsimps [angle_def]) [] [] 1);
wenzelm@4089
   101
by (action_simp_tac (simpset() addsimps square_def::db_defs) [tempI] [Stable] 1);
wenzelm@3807
   102
qed "DBFair_2";
wenzelm@3807
   103
wenzelm@3807
   104
(* High-level fairness *)
wenzelm@3807
   105
goal DBuffer.thy
wenzelm@3807
   106
  "[][DBNext]_<inp,mid,out,q1,q2> .& WF(DBPass)_<inp,mid,out,q1,q2> \
wenzelm@3807
   107
\                                 .& WF(DBDeq)_<inp,mid,out,q1,q2>  \ 
wenzelm@3807
   108
\  .-> WF(Deq inp qc out)_<inp,qc,out>";
wenzelm@3807
   109
by (auto_tac (db_css addSIs2 [leadsto_WF]));
wenzelm@3807
   110
by (auto_tac (db_css addSIs2 [(temp_mp DBFair_1) RSN(2,LatticeTransitivity)]));
wenzelm@3807
   111
by (auto_tac (db_css addSIs2 [(temp_mp DBFair_2) RSN(2,LatticeTransitivity)]));
wenzelm@3807
   112
by (auto_tac (db_css addSIs2 [ImplLeadsto] addSEs2 [STL4E]
wenzelm@3807
   113
                     addsimps2 [angle_def,DBDeq_def,Deq_def,hd_append]));
wenzelm@3807
   114
qed "DBFair";
wenzelm@3807
   115
wenzelm@3807
   116
(*** Main theorem ***)
wenzelm@3807
   117
goalw DBuffer.thy [DBuffer_def,Buffer_def,IBuffer_def] "DBuffer .-> Buffer inp out";
wenzelm@3807
   118
by (auto_tac (db_css addSIs2 (map temp_mp [eexI,DBInit,DB_step_simulation RS STL4,DBFair])));
wenzelm@3807
   119
qed "DBuffer_impl_Buffer";