35 distr_spec :: "[i, i, i, i =>i]=>i" where |
35 distr_spec :: "[i, i, i, i =>i]=>i" where |
36 "distr_spec(A, In, iIn, Out) == |
36 "distr_spec(A, In, iIn, Out) == |
37 distr_follows(A, In, iIn, Out) \<inter> distr_allowed_acts(Out)" |
37 distr_follows(A, In, iIn, Out) \<inter> distr_allowed_acts(Out)" |
38 |
38 |
39 locale distr = |
39 locale distr = |
40 fixes In --\<open>items to distribute\<close> |
40 fixes In \<comment>\<open>items to distribute\<close> |
41 and iIn --\<open>destinations of items to distribute\<close> |
41 and iIn \<comment>\<open>destinations of items to distribute\<close> |
42 and Out --\<open>distributed items\<close> |
42 and Out \<comment>\<open>distributed items\<close> |
43 and A --\<open>the type of items being distributed\<close> |
43 and A \<comment>\<open>the type of items being distributed\<close> |
44 and D |
44 and D |
45 assumes |
45 assumes |
46 var_assumes [simp]: "In \<in> var & iIn \<in> var & (\<forall>n. Out(n):var)" |
46 var_assumes [simp]: "In \<in> var & iIn \<in> var & (\<forall>n. Out(n):var)" |
47 and all_distinct_vars: "\<forall>n. all_distinct([In, iIn, Out(n)])" |
47 and all_distinct_vars: "\<forall>n. all_distinct([In, iIn, Out(n)])" |
48 and type_assumes [simp]: "type_of(In)=list(A) & type_of(iIn)=list(nat) & |
48 and type_assumes [simp]: "type_of(In)=list(A) & type_of(iIn)=list(nat) & |