Quelle DBuffer.thy Sprache: Isabelle

(*  Title:      HOL/TLA/Buffer/DBuffer.thy
    Author:     Stephan Merz, University of Munich
*)

section \<open>Two FIFO buffers in a row, with interleaving assumption\<close>

theory DBuffer
imports Buffer
begin

axiomatization
  (* implementation variables *)
  inp  :: "nat stfun" and
  mid  :: "nat stfun" and
  out  :: "nat stfun" and
  q1   :: "nat list stfun" and
  q2   :: "nat list stfun" and
  qc   :: "nat list stfun" and

  DBInit :: stpred and
  DBEnq :: action and
  DBDeq :: action and
  DBPass :: action and
  DBNext :: action and
  DBuffer :: temporal
where
  DB_base:        "basevars (inp,mid,out,q1,q2)" and

  (* the concatenation of the two buffers *)
  qc_def:         "PRED qc == PRED (q2 @ q1)" and

  DBInit_def:     "DBInit == PRED (BInit inp q1 mid \ BInit mid q2 out)" and
  DBEnq_def:      "DBEnq == ACT Enq inp q1 mid \ unchanged (q2,out)" and
  DBDeq_def:      "DBDeq == ACT Deq mid q2 out \ unchanged (inp,q1)" and
  DBPass_def:     "DBPass == ACT Deq inp q1 mid
                                 \<and> (q2$ = $q2 @ [ mid$ ])
                                 \<and> (out$ = $out)" and
  DBNext_def:     "DBNext == ACT (DBEnq \ DBDeq \ DBPass)" and
  DBuffer_def:    "DBuffer == TEMP Init DBInit
                                 \<and> \<box>[DBNext]_(inp,mid,out,q1,q2)
                                 \<and> WF(DBDeq)_(inp,mid,out,q1,q2)
                                 \<and> WF(DBPass)_(inp,mid,out,q1,q2)"

declare qc_def [simp]

lemmas db_defs =
  BInit_def Enq_def Deq_def Next_def IBuffer_def Buffer_def
  DBInit_def DBEnq_def DBDeq_def DBPass_def DBNext_def DBuffer_def

(*** Proper initialization ***)
lemma DBInit: "\ Init DBInit \ Init (BInit inp qc out)"
  by (auto simp: Init_def DBInit_def BInit_def)

(*** Step simulation ***)
lemma DB_step_simulation: "\ [DBNext]_(inp,mid,out,q1,q2) \ [Next inp qc out]_(inp,qc,out)"
  apply (rule square_simulation)
   apply clarsimp
  apply (tactic
    \<open>action_simp_tac (\<^context> addsimps (@{thm hd_append} :: @{thms db_defs})) [] [] 1\<close>)
  done

(*** Simulation of fairness ***)

(* Compute enabledness predicates for DBDeq and DBPass actions *)
lemma DBDeq_visible: "\ _(inp,mid,out,q1,q2) = DBDeq"
  apply (unfold angle_def DBDeq_def Deq_def)
  apply (safe, simp (asm_lr))+
  done

lemma DBDeq_enabled:
    "\ Enabled (_(inp,mid,out,q1,q2)) = (q2 \ #[])"
  apply (unfold DBDeq_visible [action_rewrite])
  apply (force intro!: DB_base [THEN base_enabled, temp_use]
    elim!: enabledE simp: angle_def DBDeq_def Deq_def)
  done

lemma DBPass_visible: "\ _(inp,mid,out,q1,q2) = DBPass"
  by (auto simp: angle_def DBPass_def Deq_def)

lemma DBPass_enabled:
    "\ Enabled (_(inp,mid,out,q1,q2)) = (q1 \ #[])"
  apply (unfold DBPass_visible [action_rewrite])
  apply (force intro!: DB_base [THEN base_enabled, temp_use]
    elim!: enabledE simp: angle_def DBPass_def Deq_def)
  done

(* The plan for proving weak fairness at the higher level is to prove
   (0)  DBuffer => (Enabled (Deq inp qc out) \<leadsto> (Deq inp qc out))
   which is in turn reduced to the two leadsto conditions
   (1)  DBuffer => (Enabled (Deq inp qc out) \<leadsto> q2 \<noteq> [])
   (2)  DBuffer => (q2 \<noteq> [] \<leadsto> DBDeq)
   and the fact that DBDeq implies <Deq inp qc out>_(inp,qc,out)
   (and therefore DBDeq \<leadsto> <Deq inp qc out>_(inp,qc,out) trivially holds).

   Condition (1) is reduced to
   (1a) DBuffer => (qc \<noteq> [] /\ q2 = [] \<leadsto> q2 \<noteq> [])
   by standard leadsto rules (leadsto_classical) and rule Deq_enabledE.

   Both (1a) and (2) are proved from DBuffer's WF conditions by standard
   WF reasoning (Lamport's WF1 and WF_leadsto).
   The condition WF(Deq inp qc out) follows from (0) by rule leadsto_WF.

   One could use Lamport's WF2 instead.
*)

(* Condition (1a) *)
lemma DBFair_1a: "\ \[DBNext]_(inp,mid,out,q1,q2) \ WF(DBPass)_(inp,mid,out,q1,q2)
         \<longrightarrow> (qc \<noteq> #[] \<and> q2 = #[] \<leadsto> q2 \<noteq> #[])"
  apply (rule WF1)
    apply (force simp: db_defs)
   apply (force simp: angle_def DBPass_def)
  apply (force simp: DBPass_enabled [temp_use])
  done

(* Condition (1) *)
lemma DBFair_1: "\ \[DBNext]_(inp,mid,out,q1,q2) \ WF(DBPass)_(inp,mid,out,q1,q2)
         \<longrightarrow> (Enabled (<Deq inp qc out>_(inp,qc,out)) \<leadsto> q2 \<noteq> #[])"
  apply clarsimp
  apply (rule leadsto_classical [temp_use])
  apply (rule DBFair_1a [temp_use, THEN LatticeTransitivity [temp_use]])
  apply assumption+
  apply (rule ImplLeadsto_gen [temp_use])
  apply (force intro!: necT [temp_use] dest!: STL2_gen [temp_use] Deq_enabledE [temp_use]
    simp add: Init_defs)
  done

(* Condition (2) *)
lemma DBFair_2: "\ \[DBNext]_(inp,mid,out,q1,q2) \ WF(DBDeq)_(inp,mid,out,q1,q2)
         \<longrightarrow> (q2 \<noteq> #[] \<leadsto> DBDeq)"
  apply (rule WF_leadsto)
    apply (force simp: DBDeq_enabled [temp_use])
   apply (force simp: angle_def)
  apply (force simp: db_defs elim!: Stable [temp_use])
  done

(* High-level fairness *)
lemma DBFair: "\ \[DBNext]_(inp,mid,out,q1,q2) \ WF(DBPass)_(inp,mid,out,q1,q2)
                                        \<and> WF(DBDeq)_(inp,mid,out,q1,q2)
         \<longrightarrow> WF(Deq inp qc out)_(inp,qc,out)"
  apply (auto simp del: qc_def intro!: leadsto_WF [temp_use]
    DBFair_1 [temp_use, THEN [2] LatticeTransitivity [temp_use]]
    DBFair_2 [temp_use, THEN [2] LatticeTransitivity [temp_use]])
  apply (auto intro!: ImplLeadsto_simple [temp_use]
    simp: angle_def DBDeq_def Deq_def hd_append [try_rewrite])
  done

(*** Main theorem ***)
lemma DBuffer_impl_Buffer: "\ DBuffer \ Buffer inp out"
  apply (unfold DBuffer_def Buffer_def IBuffer_def)
  apply (force intro!: eexI [temp_use] DBInit [temp_use]
    DB_step_simulation [THEN STL4, temp_use] DBFair [temp_use])
  done

end

quality100%

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.