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