src/HOL/TLA/Buffer/DBuffer.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 41589 bbd861837ebc
child 47968 3119ad2b5ad3
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41589
bbd861837ebc tuned headers;
wenzelm
parents: 26342
diff changeset
     1
(*  Title:      HOL/TLA/Buffer/DBuffer.thy
bbd861837ebc tuned headers;
wenzelm
parents: 26342
diff changeset
     2
    Author:     Stephan Merz, University of Munich
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
     3
*)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
     4
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
     5
header {* Two FIFO buffers in a row, with interleaving assumption *}
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
     6
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
     7
theory DBuffer
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
     8
imports Buffer
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
     9
begin
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    10
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    11
consts
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    12
  (* implementation variables *)
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    13
  inp  :: "nat stfun"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    14
  mid  :: "nat stfun"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    15
  out  :: "nat stfun"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    16
  q1   :: "nat list stfun"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    17
  q2   :: "nat list stfun"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    18
  qc   :: "nat list stfun"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    19
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    20
  DBInit :: stpred
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    21
  DBEnq :: action
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    22
  DBDeq :: action
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    23
  DBPass :: action
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    24
  DBNext :: action
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    25
  DBuffer :: temporal
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    26
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    27
axioms
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    28
  DB_base:        "basevars (inp,mid,out,q1,q2)"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    29
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    30
  (* the concatenation of the two buffers *)
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    31
  qc_def:         "PRED qc == PRED (q2 @ q1)"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    32
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    33
  DBInit_def:     "DBInit   == PRED (BInit inp q1 mid  &  BInit mid q2 out)"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    34
  DBEnq_def:      "DBEnq    == ACT  Enq inp q1 mid  &  unchanged (q2,out)"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    35
  DBDeq_def:      "DBDeq    == ACT  Deq mid q2 out  &  unchanged (inp,q1)"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    36
  DBPass_def:     "DBPass   == ACT  Deq inp q1 mid
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    37
                                 & (q2$ = $q2 @ [ mid$ ])
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    38
                                 & (out$ = $out)"
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    39
  DBNext_def:     "DBNext   == ACT  (DBEnq | DBDeq | DBPass)"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
    40
  DBuffer_def:    "DBuffer  == TEMP Init DBInit
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    41
                                 & [][DBNext]_(inp,mid,out,q1,q2)
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    42
                                 & WF(DBDeq)_(inp,mid,out,q1,q2)
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    43
                                 & WF(DBPass)_(inp,mid,out,q1,q2)"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    44
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    45
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    46
declare qc_def [simp]
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    47
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    48
lemmas db_defs =
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    49
  BInit_def Enq_def Deq_def Next_def IBuffer_def Buffer_def
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    50
  DBInit_def DBEnq_def DBDeq_def DBPass_def DBNext_def DBuffer_def
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    51
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    52
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    53
(*** Proper initialization ***)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    54
lemma DBInit: "|- Init DBInit --> Init (BInit inp qc out)"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    55
  by (auto simp: Init_def DBInit_def BInit_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    56
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    57
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    58
(*** Step simulation ***)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    59
lemma DB_step_simulation: "|- [DBNext]_(inp,mid,out,q1,q2) --> [Next inp qc out]_(inp,qc,out)"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    60
  apply (rule square_simulation)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    61
   apply clarsimp
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    62
  apply (tactic
26342
0f65fa163304 more antiquotations;
wenzelm
parents: 21624
diff changeset
    63
    {* action_simp_tac (@{simpset} addsimps (@{thm hd_append} :: @{thms db_defs})) [] [] 1 *})
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    64
  done
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    65
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    66
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    67
(*** Simulation of fairness ***)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    68
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    69
(* Compute enabledness predicates for DBDeq and DBPass actions *)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    70
lemma DBDeq_visible: "|- <DBDeq>_(inp,mid,out,q1,q2) = DBDeq"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    71
  apply (unfold angle_def DBDeq_def Deq_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    72
  apply (safe, simp (asm_lr))+
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    73
  done
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    74
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    75
lemma DBDeq_enabled: 
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    76
    "|- Enabled (<DBDeq>_(inp,mid,out,q1,q2)) = (q2 ~= #[])"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    77
  apply (unfold DBDeq_visible [action_rewrite])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    78
  apply (force intro!: DB_base [THEN base_enabled, temp_use]
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    79
    elim!: enabledE simp: angle_def DBDeq_def Deq_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    80
  done
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    81
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    82
lemma DBPass_visible: "|- <DBPass>_(inp,mid,out,q1,q2) = DBPass"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    83
  by (auto simp: angle_def DBPass_def Deq_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    84
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    85
lemma DBPass_enabled: 
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    86
    "|- Enabled (<DBPass>_(inp,mid,out,q1,q2)) = (q1 ~= #[])"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    87
  apply (unfold DBPass_visible [action_rewrite])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    88
  apply (force intro!: DB_base [THEN base_enabled, temp_use]
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    89
    elim!: enabledE simp: angle_def DBPass_def Deq_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    90
  done
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    91
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    92
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    93
(* The plan for proving weak fairness at the higher level is to prove
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    94
   (0)  DBuffer => (Enabled (Deq inp qc out) ~> (Deq inp qc out))
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    95
   which is in turn reduced to the two leadsto conditions
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    96
   (1)  DBuffer => (Enabled (Deq inp qc out) ~> q2 ~= [])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    97
   (2)  DBuffer => (q2 ~= [] ~> DBDeq)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    98
   and the fact that DBDeq implies <Deq inp qc out>_(inp,qc,out)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    99
   (and therefore DBDeq ~> <Deq inp qc out>_(inp,qc,out) trivially holds).
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 6255
diff changeset
   100
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   101
   Condition (1) is reduced to
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   102
   (1a) DBuffer => (qc ~= [] /\ q2 = [] ~> q2 ~= [])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   103
   by standard leadsto rules (leadsto_classical) and rule Deq_enabledE.
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   104
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   105
   Both (1a) and (2) are proved from DBuffer's WF conditions by standard
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   106
   WF reasoning (Lamport's WF1 and WF_leadsto).
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   107
   The condition WF(Deq inp qc out) follows from (0) by rule leadsto_WF.
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   108
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   109
   One could use Lamport's WF2 instead.
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   110
*)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   111
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   112
(* Condition (1a) *)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   113
lemma DBFair_1a: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   114
         --> (qc ~= #[] & q2 = #[] ~> q2 ~= #[])"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   115
  apply (rule WF1)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   116
    apply (force simp: db_defs)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   117
   apply (force simp: angle_def DBPass_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   118
  apply (force simp: DBPass_enabled [temp_use])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   119
  done
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   120
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   121
(* Condition (1) *)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   122
lemma DBFair_1: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   123
         --> (Enabled (<Deq inp qc out>_(inp,qc,out)) ~> q2 ~= #[])"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   124
  apply clarsimp
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   125
  apply (rule leadsto_classical [temp_use])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   126
  apply (rule DBFair_1a [temp_use, THEN LatticeTransitivity [temp_use]])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   127
  apply assumption+
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   128
  apply (rule ImplLeadsto_gen [temp_use])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   129
  apply (force intro!: necT [temp_use] dest!: STL2_gen [temp_use] Deq_enabledE [temp_use]
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   130
    simp add: Init_defs)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   131
  done
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   132
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   133
(* Condition (2) *)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   134
lemma DBFair_2: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2)  
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   135
         --> (q2 ~= #[] ~> DBDeq)"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   136
  apply (rule WF_leadsto)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   137
    apply (force simp: DBDeq_enabled [temp_use])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   138
   apply (force simp: angle_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   139
  apply (force simp: db_defs elim!: Stable [temp_use])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   140
  done
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   141
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   142
(* High-level fairness *)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   143
lemma DBFair: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   144
                                        & WF(DBDeq)_(inp,mid,out,q1,q2)   
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   145
         --> WF(Deq inp qc out)_(inp,qc,out)"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   146
  apply (auto simp del: qc_def intro!: leadsto_WF [temp_use]
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   147
    DBFair_1 [temp_use, THEN [2] LatticeTransitivity [temp_use]]
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   148
    DBFair_2 [temp_use, THEN [2] LatticeTransitivity [temp_use]])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   149
  apply (auto intro!: ImplLeadsto_simple [temp_use]
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   150
    simp: angle_def DBDeq_def Deq_def hd_append [try_rewrite])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   151
  done
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   152
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   153
(*** Main theorem ***)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   154
lemma DBuffer_impl_Buffer: "|- DBuffer --> Buffer inp out"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   155
  apply (unfold DBuffer_def Buffer_def IBuffer_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   156
  apply (force intro!: eexI [temp_use] DBInit [temp_use]
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   157
    DB_step_simulation [THEN STL4, temp_use] DBFair [temp_use])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   158
  done
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   159
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   160
end