src/HOL/TLA/Buffer/Buffer.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 60592 c9bd1d902f04
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
eliminated old defs;
     1 (*  Title:      HOL/TLA/Buffer/Buffer.thy
     2     Author:     Stephan Merz, University of Munich
     3 *)
     4 
     5 section \<open>A simple FIFO buffer (synchronous communication, interleaving)\<close>
     6 
     7 theory Buffer
     8 imports "../TLA"
     9 begin
    10 
    11 (* actions *)
    12 
    13 definition BInit :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> stpred"
    14   where "BInit ic q oc == PRED q = #[]"
    15 
    16 definition Enq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
    17   where "Enq ic q oc == ACT (ic$ \<noteq> $ic)
    18                          \<and> (q$ = $q @ [ ic$ ])
    19                          \<and> (oc$ = $oc)"
    20 
    21 definition Deq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
    22   where "Deq ic q oc == ACT ($q \<noteq> #[])
    23                          \<and> (oc$ = hd< $q >)
    24                          \<and> (q$ = tl< $q >)
    25                          \<and> (ic$ = $ic)"
    26 
    27 definition Next :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
    28   where "Next ic q oc == ACT (Enq ic q oc \<or> Deq ic q oc)"
    29 
    30 
    31 (* temporal formulas *)
    32 
    33 definition IBuffer :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
    34   where "IBuffer ic q oc == TEMP Init (BInit ic q oc)
    35                                   \<and> \<box>[Next ic q oc]_(ic,q,oc)
    36                                   \<and> WF(Deq ic q oc)_(ic,q,oc)"
    37 
    38 definition Buffer :: "'a stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
    39   where "Buffer ic oc == TEMP (\<exists>\<exists>q. IBuffer ic q oc)"
    40 
    41 
    42 (* ---------------------------- Data lemmas ---------------------------- *)
    43 
    44 (*FIXME: move to theory List? Maybe as (tl xs = xs) = (xs = [])"?*)
    45 lemma tl_not_self [simp]: "xs \<noteq> [] \<Longrightarrow> tl xs \<noteq> xs"
    46   by (auto simp: neq_Nil_conv)
    47 
    48 
    49 (* ---------------------------- Action lemmas ---------------------------- *)
    50 
    51 (* Dequeue is visible *)
    52 lemma Deq_visible: "\<turnstile> <Deq ic q oc>_(ic,q,oc) = Deq ic q oc"
    53   apply (unfold angle_def Deq_def)
    54   apply (safe, simp (asm_lr))+
    55   done
    56 
    57 (* Enabling condition for dequeue -- NOT NEEDED *)
    58 lemma Deq_enabled: 
    59     "\<And>q. basevars (ic,q,oc) \<Longrightarrow> \<turnstile> Enabled (<Deq ic q oc>_(ic,q,oc)) = (q \<noteq> #[])"
    60   apply (unfold Deq_visible [temp_rewrite])
    61   apply (force elim!: base_enabled [temp_use] enabledE [temp_use] simp: Deq_def)
    62   done
    63 
    64 (* For the left-to-right implication, we don't need the base variable stuff *)
    65 lemma Deq_enabledE: 
    66     "\<turnstile> Enabled (<Deq ic q oc>_(ic,q,oc)) \<longrightarrow> (q \<noteq> #[])"
    67   apply (unfold Deq_visible [temp_rewrite])
    68   apply (auto elim!: enabledE simp add: Deq_def)
    69   done
    70 
    71 end