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