21 dummy :: 'a --{*new variables*} |
21 dummy :: 'a --{*new variables*} |
22 |
22 |
23 |
23 |
24 (*Array indexing is translated to list indexing as A[n] == A!(n-1). *) |
24 (*Array indexing is translated to list indexing as A[n] == A!(n-1). *) |
25 |
25 |
26 constdefs |
|
27 |
26 |
28 (** Release some tokens **) |
27 (** Release some tokens **) |
29 |
28 |
|
29 definition |
30 rel_act :: "('a state_d * 'a state_d) set" |
30 rel_act :: "('a state_d * 'a state_d) set" |
31 "rel_act == {(s,s'). |
31 where "rel_act = {(s,s'). |
32 \<exists>nrel. nrel = size (rel s) & |
32 \<exists>nrel. nrel = size (rel s) & |
33 s' = s (| rel := rel s @ [giv s!nrel] |) & |
33 s' = s (| rel := rel s @ [giv s!nrel] |) & |
34 nrel < size (giv s) & |
34 nrel < size (giv s) & |
35 ask s!nrel \<le> giv s!nrel}" |
35 ask s!nrel \<le> giv s!nrel}" |
36 |
36 |
37 (** Choose a new token requirement **) |
37 (** Choose a new token requirement **) |
38 |
38 |
39 (** Including s'=s suppresses fairness, allowing the non-trivial part |
39 (** Including s'=s suppresses fairness, allowing the non-trivial part |
40 of the action to be ignored **) |
40 of the action to be ignored **) |
41 |
41 |
|
42 definition |
42 tok_act :: "('a state_d * 'a state_d) set" |
43 tok_act :: "('a state_d * 'a state_d) set" |
43 "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}" |
44 where "tok_act = {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}" |
44 |
45 |
|
46 definition |
45 ask_act :: "('a state_d * 'a state_d) set" |
47 ask_act :: "('a state_d * 'a state_d) set" |
46 "ask_act == {(s,s'). s'=s | |
48 where "ask_act = {(s,s'). s'=s | |
47 (s' = s (|ask := ask s @ [tok s]|))}" |
49 (s' = s (|ask := ask s @ [tok s]|))}" |
48 |
50 |
|
51 definition |
49 Client :: "'a state_d program" |
52 Client :: "'a state_d program" |
50 "Client == |
53 where "Client = |
51 mk_total_program |
54 mk_total_program |
52 ({s. tok s \<in> atMost NbT & |
55 ({s. tok s \<in> atMost NbT & |
53 giv s = [] & ask s = [] & rel s = []}, |
56 giv s = [] & ask s = [] & rel s = []}, |
54 {rel_act, tok_act, ask_act}, |
57 {rel_act, tok_act, ask_act}, |
55 \<Union>G \<in> preserves rel Int preserves ask Int preserves tok. |
58 \<Union>G \<in> preserves rel Int preserves ask Int preserves tok. |
56 Acts G)" |
59 Acts G)" |
57 |
60 |
|
61 definition |
58 (*Maybe want a special theory section to declare such maps*) |
62 (*Maybe want a special theory section to declare such maps*) |
59 non_dummy :: "'a state_d => state" |
63 non_dummy :: "'a state_d => state" |
60 "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)" |
64 where "non_dummy s = (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)" |
61 |
65 |
|
66 definition |
62 (*Renaming map to put a Client into the standard form*) |
67 (*Renaming map to put a Client into the standard form*) |
63 client_map :: "'a state_d => state*'a" |
68 client_map :: "'a state_d => state*'a" |
64 "client_map == funPair non_dummy dummy" |
69 where "client_map = funPair non_dummy dummy" |
65 |
70 |
66 |
71 |
67 declare Client_def [THEN def_prg_Init, simp] |
72 declare Client_def [THEN def_prg_Init, simp] |
68 declare Client_def [THEN def_prg_AllowedActs, simp] |
73 declare Client_def [THEN def_prg_AllowedActs, simp] |
69 declare rel_act_def [THEN def_act_simp, simp] |
74 declare rel_act_def [THEN def_act_simp, simp] |