# Theory Distributor

Up to index of Isabelle/ZF/UNITY

theory Distributor
imports AllocBase Follows Guar GenPrefix
begin

    (*  Title: ZF/UNITY/Distributor
        ID:         $Id: Distributor.thy,v 1.6 2005/06/17 14:15:11 haftmann Exp $
        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)*}
    constdefs
      distr_follows :: "[i, i, i, i =>i] =>i"
        "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
             (\<Inter>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))"

      distr_allowed_acts :: "[i=>i]=>i"
        "distr_allowed_acts(Out) ==
         {D ∈ program. AllowedActs(D) =
         cons(id(state), \<Union>G ∈ (\<Inter>n∈nat. preserves(lift(Out(n)))). Acts(G))}"

      distr_spec :: "[i, i, i, i =>i]=>i"
        "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, iOut(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)"
    apply (unfold 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)"
    apply (unfold 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)"
    apply (unfold 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
              (\<Inter>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 \<squnion> G ∈ Always({s ∈ state.
              ∀elt ∈ set_of_list(s`iIn). elt < Nclients}) |]
      ==> D \<squnion> 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
           "(\<Union>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<Nclients" 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
           (\<Inter>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

lemma In_value_type:

      [| PROP distr(TYPE('a), In, iIn, Out, A, D); s ∈ state |] ==> s ` In ∈ list(A)

lemma iIn_value_type:

      [| PROP distr(TYPE('a), In, iIn, Out, A, D); s ∈ state |]
      ==> s ` iIn ∈ list(nat)

lemma Out_value_type:

      [| PROP distr(TYPE('a), In, iIn, Out, A, D); s ∈ state |]
      ==> s ` Out(n) ∈ list(A)

lemma D_in_program:

      PROP distr(TYPE('a), In, iIn, Out, A, D) ==> D ∈ program

lemma D_ok_iff:

      [| PROP distr(TYPE('a), In, iIn, Out, A, D); G ∈ program |]
      ==> D ok G <-> (∀n∈nat. G ∈ preserves(lift(Out(n)))) ∧ D ∈ Allowed(G)

lemma distr_Increasing_Out:

      PROP distr(TYPE('a), In, iIn, Out, A, D)
      ==> D ∈ Increasing[list(A)](prefix(A), lift(In)) ∩ Incr(lift(iIn)) ∩
              Always
               ({s ∈ state . ∀elt∈set_of_list(s ` iIn). elt < Nclients}) guarantees
              (\<Inter>n∈Nclients. Increasing[list(A)](prefix(A), lift(Out(n))))

lemma distr_bag_Follows_lemma:

      [| PROP distr(TYPE('a), In, iIn, Out, A, D);
         ∀n∈nat. G ∈ preserves(lift(Out(n)));
         D Join G ∈ Always({s ∈ state . ∀elt∈set_of_list(s ` iIn). elt < Nclients}) |]
      ==> D Join 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)))})

theorem distr_bag_Follows:

      PROP distr(TYPE('a), In, iIn, Out, A, D)
      ==> D ∈ Increasing[list(A)](prefix(A), lift(In)) ∩ Incr(lift(iIn)) ∩
              Always
               ({s ∈ state . ∀elt∈set_of_list(s ` iIn). elt < Nclients}) guarantees
              (\<Inter>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) / A -||> nat - {0})