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