author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
child 59788  6f7b6adac439 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28232
diff
changeset

1 
(* Title: ZF/UNITY/Distributor.thy 
14052  2 
Author: Sidi O Ehmety, Cambridge University Computer Laboratory 
3 
Copyright 2002 University of Cambridge 

4 

5 
A multipleclient allocator from a singleclient allocator: 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28232
diff
changeset

6 
Distributor specification. 
14052  7 
*) 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

8 

16417  9 
theory Distributor imports AllocBase Follows Guar GenPrefix begin 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

10 

f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

11 
text{*Distributor specification (the number of outputs is Nclients)*} 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

12 

f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

13 
text{*spec (14)*} 
24893  14 

15 
definition 

16 
distr_follows :: "[i, i, i, i =>i] =>i" where 

14052  17 
"distr_follows(A, In, iIn, Out) == 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

18 
(lift(In) IncreasingWrt prefix(A)/list(A)) \<inter> 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

19 
(lift(iIn) IncreasingWrt prefix(nat)/list(nat)) \<inter> 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

20 
Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iIn). elt < Nclients}) 
14052  21 
guarantees 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

22 
(\<Inter>n \<in> Nclients. 
14052  23 
lift(Out(n)) 
24 
Fols 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tabwidth;
wenzelm
parents:
28232
diff
changeset

26 
Wrt prefix(A)/list(A))" 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

27 

24893  28 
definition 
29 
distr_allowed_acts :: "[i=>i]=>i" where 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

30 
"distr_allowed_acts(Out) == 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

31 
{D \<in> program. AllowedActs(D) = 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

33 

24893  34 
definition 
35 
distr_spec :: "[i, i, i, i =>i]=>i" where 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

36 
"distr_spec(A, In, iIn, Out) == 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

38 

f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

39 
locale distr = 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

40 
fixes In {*items to distribute*} 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

41 
and iIn {*destinations of items to distribute*} 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

42 
and Out {*distributed items*} 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

43 
and A {*the type of items being distributed *} 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

44 
and D 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

45 
assumes 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

46 
var_assumes [simp]: "In \<in> var & iIn \<in> var & (\<forall>n. Out(n):var)" 
28232  47 
and all_distinct_vars: "\<forall>n. all_distinct([In, iIn, Out(n)])" 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

49 
(\<forall>n. type_of(Out(n))=list(A))" 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

50 
and default_val_assumes [simp]: 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

51 
"default_val(In)=Nil & 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

52 
default_val(iIn)=Nil & 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

53 
(\<forall>n. default_val(Out(n))=Nil)" 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

55 

14052  56 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

58 
apply (unfold state_def) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

59 
apply (drule_tac a = In in apply_type, auto) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

60 
done 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

61 

f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

62 
lemma (in distr) iIn_value_type [simp,TC]: 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

63 
"s \<in> state ==> s`iIn \<in> list(nat)" 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

64 
apply (unfold state_def) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

65 
apply (drule_tac a = iIn in apply_type, auto) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

66 
done 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

67 

f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

68 
lemma (in distr) Out_value_type [simp,TC]: 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

69 
"s \<in> state ==> s`Out(n):list(A)" 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

70 
apply (unfold state_def) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

71 
apply (drule_tac a = "Out (n)" in apply_type) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

72 
apply auto 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

73 
done 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

74 

f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

76 
apply (cut_tac distr_spec) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

78 
done 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

79 

f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

80 
lemma (in distr) D_ok_iff: 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

81 
"G \<in> program ==> 
46823  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 tidyup.
paulson
parents:
14057
diff
changeset

83 
apply (cut_tac distr_spec) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

85 
Allowed_def ok_iff_Allowed) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

87 
apply (auto intro: safety_prop_Inter) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

88 
done 
14052  89 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

90 
lemma (in distr) distr_Increasing_Out: 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

92 
(lift(iIn) IncreasingWrt prefix(nat)/list(nat)) \<inter> 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

94 
guarantees 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

95 
(\<Inter>n \<in> Nclients. lift(Out(n)) IncreasingWrt 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

96 
prefix(A)/list(A))" 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

97 
apply (cut_tac D_in_program distr_spec) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

99 
apply (auto intro!: guaranteesI intro: Follows_imp_Increasing_left 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

100 
dest!: guaranteesD) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

101 
done 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

102 

f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

103 
lemma (in distr) distr_bag_Follows_lemma: 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

105 
D \<squnion> G \<in> Always({s \<in> state. 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

107 
==> D \<squnion> G \<in> Always 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

109 
{k \<in> nat. k < length(s`iIn) & 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

110 
nth(k, s`iIn)= n})), 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

111 
Nclients, A) = 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

112 
bag_of(sublist(s`In, length(s`iIn)))})" 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

113 
apply (cut_tac D_in_program) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

114 
apply (subgoal_tac "G \<in> program") 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

115 
prefer 2 apply (blast dest: preserves_type [THEN subsetD]) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

116 
apply (erule Always_Diff_Un_eq [THEN iffD1]) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

117 
apply (rule state_AlwaysI [THEN Always_weaken], auto) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

118 
apply (rename_tac s) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

119 
apply (subst bag_of_sublist_UN_disjoint [symmetric]) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

120 
apply (simp (no_asm_simp) add: nat_into_Finite) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

121 
apply blast 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

122 
apply (simp (no_asm_simp)) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

124 
apply (subgoal_tac 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

126 
length(s`iIn) ") 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

127 
apply (simp (no_asm_simp)) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

128 
apply (rule equalityI) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

129 
apply (force simp add: ltD, safe) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

130 
apply (rename_tac m) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

131 
apply (subgoal_tac "length (s ` iIn) \<in> nat") 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

132 
apply typecheck 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

133 
apply (subgoal_tac "m \<in> nat") 
46823  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 tidyup.
paulson
parents:
14057
diff
changeset

135 
apply (simp add: ltI) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

136 
apply (simp_all add: Ord_mem_iff_lt) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

137 
apply (blast dest: ltD) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

138 
apply (blast intro: lt_trans) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

139 
done 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

140 

f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

141 
theorem (in distr) distr_bag_Follows: 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

143 
(lift(iIn) IncreasingWrt prefix(nat)/list(nat)) \<inter> 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

145 
guarantees 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

146 
(\<Inter>n \<in> Nclients. 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

148 
Fols 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

149 
(%s. bag_of(sublist(s`In, length(s`iIn)))) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

150 
Wrt MultLe(A, r)/Mult(A))" 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

151 
apply (cut_tac distr_spec) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

152 
apply (rule guaranteesI, clarify) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

153 
apply (rule distr_bag_Follows_lemma [THEN Always_Follows2]) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

154 
apply (simp add: D_ok_iff, auto) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

155 
apply (rule Follows_state_ofD1) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

156 
apply (rule Follows_msetsum_UN) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
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 tidyup.
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 tidyup.
paulson
parents:
14057
diff
changeset

159 
apply (drule guaranteesD, assumption) 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

160 
apply (simp_all cong add: Follows_cong 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28232
diff
changeset

161 
add: refl_prefix 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
28232
diff
changeset

163 
unfolded metacomp_def]) 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

164 
done 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14057
diff
changeset

165 

14052  166 
end 