(* Title: ZF/UNITY/Distributor.thy
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
Copyright 2002 University of Cambridge
A multiple-client allocator from a single-client allocator:
Distributor specification.
*)
theory Distributor
imports AllocBase Follows Guar GenPrefix
begin
text‹Distributor
specification (the number of
outputs is Nclients)
›
text‹spec (14)
›
definition
distr_follows ::
"[i, i, i, i \i] \i" where
"distr_follows(A, In, iIn, Out) \
(lift(
In) IncreasingWrt prefix(A)/list(A))
∩
(lift(iIn) IncreasingWrt prefix(nat)/list(nat))
∩
Always({s
∈ state.
∀elt
∈ set_of_list(s`iIn). elt < Nclients})
guarantees
(
∩n
∈ Nclients.
lift(Out(n))
Fols
(λs. sublist(s`
In, {k
∈ nat. k<length(s`iIn)
∧ nth(k, s`iIn) = n}))
Wrt prefix(A)/list(A))
"
definition
distr_allowed_acts ::
"[i\i]\i" where
"distr_allowed_acts(Out) \
{D
∈ program. AllowedActs(D) =
cons(id(state),
∪G
∈ (
∩n
∈nat. preserves(lift(Out(n)))). Acts(G))}
"
definition
distr_spec ::
"[i, i, i, i \i]\i" where
"distr_spec(A, In, iIn, Out) \
distr_follows(A,
In, iIn, Out)
∩ distr_allowed_acts(Out)
"
locale distr =
fixes In 🍋 ‹items
to distribute
›
and iIn
🍋 ‹destinations of items
to distribute
›
and Out
🍋 ‹distributed items
›
and A
🍋 ‹the type of items being distributed
›
and D
assumes
var_assumes [simp]:
"In \ var \ iIn \ var \ (\n. Out(n):var)"
and all_distinct_vars:
"\n. all_distinct([In, iIn, Out(n)])"
and type_assumes [simp]:
"type_of(In)=list(A) \ type_of(iIn)=list(nat) \
(
∀n. type_of(Out(n))=list(A))
"
and default_val_assumes [simp]:
"default_val(In)=Nil \
default_val(iIn)=Nil
∧
(
∀n. default_val(Out(n))=Nil)
"
and distr_spec:
"D \ distr_spec(A, In, iIn, Out)"
lemma (
in distr) In_value_type [simp,TC]:
"s \ state \ s`In \ list(A)"
unfolding state_def
apply (drule_tac a =
In in apply_type, auto)
done
lemma (
in distr) iIn_value_type [simp,TC]:
"s \ state \ s`iIn \ list(nat)"
unfolding state_def
apply (drule_tac a = iIn
in apply_type, auto)
done
lemma (
in distr) Out_value_type [simp,TC]:
"s \ state \ s`Out(n):list(A)"
unfolding state_def
apply (drule_tac a =
"Out (n)" in apply_type)
apply auto
done
lemma (
in distr) D_in_program [simp,TC]:
"D \ program"
apply (cut_tac distr_spec)
apply (auto simp add: distr_spec_def distr_allowed_acts_def)
done
lemma (
in distr) D_ok_iff:
"G \ program \
D ok G
⟷ ((
∀n
∈ nat. G
∈ preserves(lift(Out(n))))
∧ D
∈ Allowed(G))
"
apply (cut_tac distr_spec)
apply (auto simp add: INT_iff distr_spec_def distr_allowed_acts_def
Allowed_def ok_iff_Allowed)
apply (drule safety_prop_Acts_iff [
THEN [2] rev_iffD1])
apply (auto intro: safety_prop_Inter)
done
lemma (
in distr) distr_Increasing_Out:
"D \ ((lift(In) IncreasingWrt prefix(A)/list(A)) \
(lift(iIn) IncreasingWrt prefix(nat)/list(nat))
∩
Always({s
∈ state.
∀elt
∈ set_of_list(s`iIn). elt<Nclients}))
guarantees
(
∩n
∈ Nclients. lift(Out(n)) IncreasingWrt
prefix(A)/list(A))
"
apply (cut_tac D_in_program distr_spec)
apply (simp (no_asm_use) add: distr_spec_def distr_follows_def)
apply (auto intro!: guaranteesI intro: Follows_imp_Increasing_left
dest!: guaranteesD)
done
lemma (
in distr) distr_bag_Follows_lemma:
"\\n \ nat. G \ preserves(lift(Out(n)));
D
⊔ G
∈ Always({s
∈ state.
∀elt
∈ set_of_list(s`iIn). elt < Nclients})
]
==> D
⊔ G
∈ Always
({s
∈ state. msetsum(λn. bag_of (sublist(s`
In,
{k
∈ nat. k < length(s`iIn)
∧
nth(k, s`iIn)= n})),
Nclients, A) =
bag_of(sublist(s`
In, length(s`iIn)))})
"
apply (cut_tac D_in_program)
apply (subgoal_tac
"G \ program")
prefer 2
apply (blast dest: preserves_type [
THEN subsetD])
apply (erule Always_Diff_Un_eq [
THEN iffD1])
apply (rule state_AlwaysI [
THEN Always_weaken], auto)
apply (rename_tac s)
apply (subst bag_of_sublist_UN_disjoint [symmetric])
apply (simp (no_asm_simp) add: nat_into_Finite)
apply blast
apply (simp (no_asm_simp))
apply (simp add: set_of_list_conv_nth [of _ nat])
apply (subgoal_tac
"(\i \ Nclients. {k\nat. k < length(s`iIn) \ nth(k, s`iIn) = i}) =
length(s`iIn)
")
apply (simp (no_asm_simp))
apply (rule equalityI)
apply (force simp add: ltD, safe)
apply (rename_tac m)
apply (subgoal_tac
"length (s ` iIn) \ nat")
apply typecheck
apply (subgoal_tac
"m \ nat")
apply (drule_tac x =
"nth(m, s`iIn) " and P =
"\elt. X (elt) \ elt for X in bspec)
apply (simp add: ltI)
apply (simp_all add: Ord_mem_iff_lt)
apply (blast dest: ltD)
apply (blast intro: lt_trans)
done
theorem (in distr) distr_bag_Follows:
"D \ ((lift(In) IncreasingWrt prefix(A)/list(A)) \
(lift(iIn) IncreasingWrt prefix(nat)/list(nat)) ∩
Always({s ∈ state. ∀elt ∈ set_of_list(s`iIn). elt < Nclients}))
guarantees
(∩n ∈ Nclients.
(λs. msetsum(λi. bag_of(s`Out(i)), Nclients, A))
Fols
(λs. bag_of(sublist(s`In, length(s`iIn))))
Wrt MultLe(A, r)/Mult(A))"
apply (cut_tac distr_spec)
apply (rule guaranteesI, clarify)
apply (rule distr_bag_Follows_lemma [THEN Always_Follows2])
apply (simp add: D_ok_iff, auto)
apply (rule Follows_state_ofD1)
apply (rule Follows_msetsum_UN)
apply (simp_all add: nat_into_Finite bag_of_multiset [of _ A])
apply (auto simp add: distr_spec_def distr_follows_def)
apply (drule guaranteesD, assumption)
apply (simp_all cong add: Follows_cong
add: refl_prefix
mono_bag_of [THEN subset_Follows_comp, THEN subsetD,
unfolded metacomp_def])
done
end
