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