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