8 imports TLA |
8 imports TLA |
9 begin |
9 begin |
10 |
10 |
11 consts |
11 consts |
12 (* actions *) |
12 (* actions *) |
13 BInit :: "'a stfun => 'a list stfun => 'a stfun => stpred" |
13 BInit :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> stpred" |
14 Enq :: "'a stfun => 'a list stfun => 'a stfun => action" |
14 Enq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action" |
15 Deq :: "'a stfun => 'a list stfun => 'a stfun => action" |
15 Deq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action" |
16 Next :: "'a stfun => 'a list stfun => 'a stfun => action" |
16 Next :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action" |
17 |
17 |
18 (* temporal formulas *) |
18 (* temporal formulas *) |
19 IBuffer :: "'a stfun => 'a list stfun => 'a stfun => temporal" |
19 IBuffer :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal" |
20 Buffer :: "'a stfun => 'a stfun => temporal" |
20 Buffer :: "'a stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal" |
21 |
21 |
22 defs |
22 defs |
23 BInit_def: "BInit ic q oc == PRED q = #[]" |
23 BInit_def: "BInit ic q oc == PRED q = #[]" |
24 Enq_def: "Enq ic q oc == ACT (ic$ \<noteq> $ic) |
24 Enq_def: "Enq ic q oc == ACT (ic$ \<noteq> $ic) |
25 & (q$ = $q @ [ ic$ ]) |
25 & (q$ = $q @ [ ic$ ]) |
36 |
36 |
37 |
37 |
38 (* ---------------------------- Data lemmas ---------------------------- *) |
38 (* ---------------------------- Data lemmas ---------------------------- *) |
39 |
39 |
40 (*FIXME: move to theory List? Maybe as (tl xs = xs) = (xs = [])"?*) |
40 (*FIXME: move to theory List? Maybe as (tl xs = xs) = (xs = [])"?*) |
41 lemma tl_not_self [simp]: "xs \<noteq> [] ==> tl xs \<noteq> xs" |
41 lemma tl_not_self [simp]: "xs \<noteq> [] \<Longrightarrow> tl xs \<noteq> xs" |
42 by (auto simp: neq_Nil_conv) |
42 by (auto simp: neq_Nil_conv) |
43 |
43 |
44 |
44 |
45 (* ---------------------------- Action lemmas ---------------------------- *) |
45 (* ---------------------------- Action lemmas ---------------------------- *) |
46 |
46 |
47 (* Dequeue is visible *) |
47 (* Dequeue is visible *) |
48 lemma Deq_visible: "|- <Deq ic q oc>_(ic,q,oc) = Deq ic q oc" |
48 lemma Deq_visible: "\<turnstile> <Deq ic q oc>_(ic,q,oc) = Deq ic q oc" |
49 apply (unfold angle_def Deq_def) |
49 apply (unfold angle_def Deq_def) |
50 apply (safe, simp (asm_lr))+ |
50 apply (safe, simp (asm_lr))+ |
51 done |
51 done |
52 |
52 |
53 (* Enabling condition for dequeue -- NOT NEEDED *) |
53 (* Enabling condition for dequeue -- NOT NEEDED *) |
54 lemma Deq_enabled: |
54 lemma Deq_enabled: |
55 "\<And>q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q \<noteq> #[])" |
55 "\<And>q. basevars (ic,q,oc) \<Longrightarrow> \<turnstile> Enabled (<Deq ic q oc>_(ic,q,oc)) = (q \<noteq> #[])" |
56 apply (unfold Deq_visible [temp_rewrite]) |
56 apply (unfold Deq_visible [temp_rewrite]) |
57 apply (force elim!: base_enabled [temp_use] enabledE [temp_use] simp: Deq_def) |
57 apply (force elim!: base_enabled [temp_use] enabledE [temp_use] simp: Deq_def) |
58 done |
58 done |
59 |
59 |
60 (* For the left-to-right implication, we don't need the base variable stuff *) |
60 (* For the left-to-right implication, we don't need the base variable stuff *) |
61 lemma Deq_enabledE: |
61 lemma Deq_enabledE: |
62 "|- Enabled (<Deq ic q oc>_(ic,q,oc)) --> (q \<noteq> #[])" |
62 "\<turnstile> Enabled (<Deq ic q oc>_(ic,q,oc)) \<longrightarrow> (q \<noteq> #[])" |
63 apply (unfold Deq_visible [temp_rewrite]) |
63 apply (unfold Deq_visible [temp_rewrite]) |
64 apply (auto elim!: enabledE simp add: Deq_def) |
64 apply (auto elim!: enabledE simp add: Deq_def) |
65 done |
65 done |
66 |
66 |
67 end |
67 end |