1(*  Title:      HOL/TLA/Buffer/Buffer.thy
2    Author:     Stephan Merz, University of Munich
3*)
4
5section \<open>A simple FIFO buffer (synchronous communication, interleaving)\<close>
6
7theory Buffer
8imports "HOL-TLA.TLA"
9begin
10
11(* actions *)
12
13definition BInit :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> stpred"
14  where "BInit ic q oc == PRED q = #[]"
15
16definition 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
21definition 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
27definition 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
33definition 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
38definition 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 = [])"?*)
45lemma 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 *)
52lemma 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 *)
58lemma 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 *)
65lemma 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
71end
72