19 IBuffer :: "'a stfun => 'a list stfun => 'a stfun => temporal" |
19 IBuffer :: "'a stfun => 'a list stfun => 'a stfun => temporal" |
20 Buffer :: "'a stfun => 'a stfun => temporal" |
20 Buffer :: "'a stfun => 'a stfun => 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$ ~= $ic) |
24 Enq_def: "Enq ic q oc == ACT (ic$ \<noteq> $ic) |
25 & (q$ = $q @ [ ic$ ]) |
25 & (q$ = $q @ [ ic$ ]) |
26 & (oc$ = $oc)" |
26 & (oc$ = $oc)" |
27 Deq_def: "Deq ic q oc == ACT ($q ~= #[]) |
27 Deq_def: "Deq ic q oc == ACT ($q \<noteq> #[]) |
28 & (oc$ = hd< $q >) |
28 & (oc$ = hd< $q >) |
29 & (q$ = tl< $q >) |
29 & (q$ = tl< $q >) |
30 & (ic$ = $ic)" |
30 & (ic$ = $ic)" |
31 Next_def: "Next ic q oc == ACT (Enq ic q oc | Deq ic q oc)" |
31 Next_def: "Next ic q oc == ACT (Enq ic q oc | Deq ic q oc)" |
32 IBuffer_def: "IBuffer ic q oc == TEMP Init (BInit ic q oc) |
32 IBuffer_def: "IBuffer ic q oc == TEMP Init (BInit ic q oc) |
33 & [][Next ic q oc]_(ic,q,oc) |
33 & \<box>[Next ic q oc]_(ic,q,oc) |
34 & WF(Deq ic q oc)_(ic,q,oc)" |
34 & WF(Deq ic q oc)_(ic,q,oc)" |
35 Buffer_def: "Buffer ic oc == TEMP (EEX q. IBuffer ic q oc)" |
35 Buffer_def: "Buffer ic oc == TEMP (\<exists>\<exists>q. IBuffer ic q oc)" |
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 ~= [] ==> tl xs ~= xs" |
41 lemma tl_not_self [simp]: "xs \<noteq> [] ==> 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 |
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 "!!q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q ~= #[])" |
55 "\<And>q. basevars (ic,q,oc) ==> |- 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 ~= #[])" |
62 "|- Enabled (<Deq ic q oc>_(ic,q,oc)) --> (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 |