src/ZF/UNITY/Distributor.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46823 57bf0cecb366
child 59788 6f7b6adac439
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 28232
diff changeset
     1
(*  Title:      ZF/UNITY/Distributor.thy
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     2
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     3
    Copyright   2002  University of Cambridge
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     4
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     5
A multiple-client allocator from a single-client allocator:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 28232
diff changeset
     6
Distributor specification.
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     7
*)
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
     8
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14095
diff changeset
     9
theory Distributor imports AllocBase Follows  Guar GenPrefix begin
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    10
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    11
text{*Distributor specification (the number of outputs is Nclients)*}
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    12
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    13
text{*spec (14)*}
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    14
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    15
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    16
  distr_follows :: "[i, i, i, i =>i] =>i"  where
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    17
    "distr_follows(A, In, iIn, Out) ==
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    18
     (lift(In) IncreasingWrt prefix(A)/list(A)) \<inter>
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    19
     (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) \<inter>
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    20
     Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iIn). elt < Nclients})
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    21
         guarantees
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    22
         (\<Inter>n \<in> Nclients.
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    23
          lift(Out(n))
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    24
              Fols
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    25
          (%s. sublist(s`In, {k \<in> nat. k<length(s`iIn) & nth(k, s`iIn) = n}))
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 28232
diff changeset
    26
          Wrt prefix(A)/list(A))"
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    27
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    28
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    29
  distr_allowed_acts :: "[i=>i]=>i"  where
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    30
    "distr_allowed_acts(Out) ==
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    31
     {D \<in> program. AllowedActs(D) =
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    32
     cons(id(state), \<Union>G \<in> (\<Inter>n\<in>nat. preserves(lift(Out(n)))). Acts(G))}"
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    33
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    34
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    35
  distr_spec :: "[i, i, i, i =>i]=>i"  where
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    36
    "distr_spec(A, In, iIn, Out) ==
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    37
     distr_follows(A, In, iIn, Out) \<inter> distr_allowed_acts(Out)"
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    38
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    39
locale distr =
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    40
  fixes In  --{*items to distribute*}
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    41
    and iIn --{*destinations of items to distribute*}
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    42
    and Out --{*distributed items*}
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    43
    and A   --{*the type of items being distributed *}
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    44
    and D
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    45
 assumes
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    46
     var_assumes [simp]:  "In \<in> var & iIn \<in> var & (\<forall>n. Out(n):var)"
28232
c1502be099a7 Fixed typo in locale declaration.
ballarin
parents: 24893
diff changeset
    47
 and all_distinct_vars:   "\<forall>n. all_distinct([In, iIn, Out(n)])"
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    48
 and type_assumes [simp]: "type_of(In)=list(A) &  type_of(iIn)=list(nat) &
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    49
                          (\<forall>n. type_of(Out(n))=list(A))"
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    50
 and default_val_assumes [simp]:
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    51
                         "default_val(In)=Nil &
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    52
                          default_val(iIn)=Nil &
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    53
                          (\<forall>n. default_val(Out(n))=Nil)"
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    54
 and distr_spec:  "D \<in> distr_spec(A, In, iIn, Out)"
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    55
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    56
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    57
lemma (in distr) In_value_type [simp,TC]: "s \<in> state ==> s`In \<in> list(A)"
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    58
apply (unfold state_def)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    59
apply (drule_tac a = In in apply_type, auto)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    60
done
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    61
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    62
lemma (in distr) iIn_value_type [simp,TC]:
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    63
     "s \<in> state ==> s`iIn \<in> list(nat)"
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    64
apply (unfold state_def)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    65
apply (drule_tac a = iIn in apply_type, auto)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    66
done
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    67
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    68
lemma (in distr) Out_value_type [simp,TC]:
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    69
     "s \<in> state ==> s`Out(n):list(A)"
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    70
apply (unfold state_def)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    71
apply (drule_tac a = "Out (n)" in apply_type)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    72
apply auto
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    73
done
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    74
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    75
lemma (in distr) D_in_program [simp,TC]: "D \<in> program"
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    76
apply (cut_tac distr_spec)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    77
apply (auto simp add: distr_spec_def distr_allowed_acts_def)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    78
done
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    79
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    80
lemma (in distr) D_ok_iff:
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    81
     "G \<in> program ==>
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    82
        D ok G \<longleftrightarrow> ((\<forall>n \<in> nat. G \<in> preserves(lift(Out(n)))) & D \<in> Allowed(G))"
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    83
apply (cut_tac distr_spec)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    84
apply (auto simp add: INT_iff distr_spec_def distr_allowed_acts_def
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    85
                      Allowed_def ok_iff_Allowed)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    86
apply (drule safety_prop_Acts_iff [THEN [2] rev_iffD1])
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    87
apply (auto intro: safety_prop_Inter)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    88
done
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    89
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    90
lemma (in distr) distr_Increasing_Out:
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    91
"D \<in> ((lift(In) IncreasingWrt prefix(A)/list(A)) \<inter>
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    92
      (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) \<inter>
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    93
      Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iIn). elt<Nclients}))
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    94
      guarantees
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    95
          (\<Inter>n \<in> Nclients. lift(Out(n)) IncreasingWrt
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    96
                            prefix(A)/list(A))"
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    97
apply (cut_tac D_in_program distr_spec)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    98
apply (simp (no_asm_use) add: distr_spec_def distr_follows_def)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
    99
apply (auto intro!: guaranteesI intro: Follows_imp_Increasing_left 
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   100
            dest!: guaranteesD)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   101
done
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   102
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   103
lemma (in distr) distr_bag_Follows_lemma:
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   104
"[| \<forall>n \<in> nat. G \<in> preserves(lift(Out(n)));
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   105
   D \<squnion> G \<in> Always({s \<in> state.
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   106
          \<forall>elt \<in> set_of_list(s`iIn). elt < Nclients}) |]
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   107
  ==> D \<squnion> G \<in> Always
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   108
          ({s \<in> state. msetsum(%n. bag_of (sublist(s`In,
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   109
                       {k \<in> nat. k < length(s`iIn) &
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   110
                          nth(k, s`iIn)= n})),
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   111
                         Nclients, A) =
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   112
              bag_of(sublist(s`In, length(s`iIn)))})"
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   113
apply (cut_tac D_in_program)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   114
apply (subgoal_tac "G \<in> program")
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   115
 prefer 2 apply (blast dest: preserves_type [THEN subsetD])
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   116
apply (erule Always_Diff_Un_eq [THEN iffD1])
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   117
apply (rule state_AlwaysI [THEN Always_weaken], auto)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   118
apply (rename_tac s)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   119
apply (subst bag_of_sublist_UN_disjoint [symmetric])
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   120
   apply (simp (no_asm_simp) add: nat_into_Finite)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   121
  apply blast
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   122
 apply (simp (no_asm_simp))
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   123
apply (simp add: set_of_list_conv_nth [of _ nat])
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   124
apply (subgoal_tac
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   125
       "(\<Union>i \<in> Nclients. {k\<in>nat. k < length(s`iIn) & nth(k, s`iIn) = i}) =
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   126
        length(s`iIn) ")
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   127
apply (simp (no_asm_simp))
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   128
apply (rule equalityI)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   129
apply (force simp add: ltD, safe)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   130
apply (rename_tac m)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   131
apply (subgoal_tac "length (s ` iIn) \<in> nat")
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   132
apply typecheck
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   133
apply (subgoal_tac "m \<in> nat")
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   134
apply (drule_tac x = "nth(m, s`iIn) " and P = "%elt. ?X (elt) \<longrightarrow> elt<Nclients" in bspec)
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   135
apply (simp add: ltI)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   136
apply (simp_all add: Ord_mem_iff_lt)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   137
apply (blast dest: ltD)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   138
apply (blast intro: lt_trans)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   139
done
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   140
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   141
theorem (in distr) distr_bag_Follows:
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   142
 "D \<in> ((lift(In) IncreasingWrt prefix(A)/list(A)) \<inter>
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   143
       (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) \<inter>
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   144
        Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iIn). elt < Nclients}))
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   145
      guarantees
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   146
       (\<Inter>n \<in> Nclients.
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   147
        (%s. msetsum(%i. bag_of(s`Out(i)),  Nclients, A))
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   148
        Fols
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   149
        (%s. bag_of(sublist(s`In, length(s`iIn))))
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   150
        Wrt MultLe(A, r)/Mult(A))"
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   151
apply (cut_tac distr_spec)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   152
apply (rule guaranteesI, clarify)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   153
apply (rule distr_bag_Follows_lemma [THEN Always_Follows2])
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   154
apply (simp add: D_ok_iff, auto)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   155
apply (rule Follows_state_ofD1)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   156
apply (rule Follows_msetsum_UN)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   157
   apply (simp_all add: nat_into_Finite bag_of_multiset [of _ A])
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   158
apply (auto simp add: distr_spec_def distr_follows_def)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   159
apply (drule guaranteesD, assumption)
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   160
apply (simp_all cong add: Follows_cong
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 28232
diff changeset
   161
                add: refl_prefix
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 28232
diff changeset
   162
                   mono_bag_of [THEN subset_Follows_comp, THEN subsetD, 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 28232
diff changeset
   163
                                unfolded metacomp_def])
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   164
done
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14057
diff changeset
   165
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
   166
end