author  haftmann 
Sat, 22 Mar 2014 08:37:43 +0100  
changeset 56248  67dc9549fa15 
parent 46911  6d2a2f0e904e 
child 58889  5b7a9633cfa8 
permissions  rwrr 
37936  1 
(* Title: HOL/UNITY/Transformers.thy 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

3 
Copyright 2003 University of Cambridge 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

4 

13866  5 
Predicate Transformers. From 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

6 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

7 
David Meier and Beverly Sanders, 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

8 
Composing Leadsto Properties 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

9 
Theoretical Computer Science 243:12 (2000), 339361. 
13866  10 

11 
David Meier, 

12 
Progress Properties in Program Refinement and Parallel Composition 

13 
Swiss Federal Institute of Technology Zurich (1997) 

13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

14 
*) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

15 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

16 
header{*Predicate Transformers*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

17 

16417  18 
theory Transformers imports Comp begin 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

19 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

20 
subsection{*Defining the Predicate Transformers @{term wp}, 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

21 
@{term awp} and @{term wens}*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

22 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32693
diff
changeset

23 
definition wp :: "[('a*'a) set, 'a set] => 'a set" where 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

24 
{*Dijkstra's weakestprecondition operator (for an individual command)*} 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

25 
"wp act B ==  (act^1 `` (B))" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

26 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32693
diff
changeset

27 
definition awp :: "['a program, 'a set] => 'a set" where 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

28 
{*Dijkstra's weakestprecondition operator (for a program)*} 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

29 
"awp F B == (\<Inter>act \<in> Acts F. wp act B)" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

30 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32693
diff
changeset

31 
definition wens :: "['a program, ('a*'a) set, 'a set] => 'a set" where 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

32 
{*The weakestensures transformer*} 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

33 
"wens F act B == gfp(\<lambda>X. (wp act B \<inter> awp F (B \<union> X)) \<union> B)" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

34 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

35 
text{*The fundamental theorem for wp*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

36 
theorem wp_iff: "(A <= wp act B) = (act `` A <= B)" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

37 
by (force simp add: wp_def) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

38 

13874  39 
text{*This lemma is a good deal more intuitive than the definition!*} 
40 
lemma in_wp_iff: "(a \<in> wp act B) = (\<forall>x. (a,x) \<in> act > x \<in> B)" 

41 
by (simp add: wp_def, blast) 

42 

13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

43 
lemma Compl_Domain_subset_wp: " (Domain act) \<subseteq> wp act B" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

44 
by (force simp add: wp_def) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

45 

13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

46 
lemma wp_empty [simp]: "wp act {} =  (Domain act)" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

47 
by (force simp add: wp_def) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

48 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

49 
text{*The identity relation is the skip action*} 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

50 
lemma wp_Id [simp]: "wp Id B = B" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

51 
by (simp add: wp_def) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

52 

13851  53 
lemma wp_totalize_act: 
54 
"wp (totalize_act act) B = (wp act B \<inter> Domain act) \<union> (B  Domain act)" 

55 
by (simp add: wp_def totalize_act_def, blast) 

56 

13861  57 
lemma awp_subset: "(awp F A \<subseteq> A)" 
58 
by (force simp add: awp_def wp_def) 

59 

13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

60 
lemma awp_Int_eq: "awp F (A\<inter>B) = awp F A \<inter> awp F B" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

61 
by (simp add: awp_def wp_def, blast) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

62 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

63 
text{*The fundamental theorem for awp*} 
13861  64 
theorem awp_iff_constrains: "(A <= awp F B) = (F \<in> A co B)" 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

65 
by (simp add: awp_def constrains_def wp_iff INT_subset_iff) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

66 

13861  67 
lemma awp_iff_stable: "(A \<subseteq> awp F A) = (F \<in> stable A)" 
68 
by (simp add: awp_iff_constrains stable_def) 

69 

70 
lemma stable_imp_awp_ident: "F \<in> stable A ==> awp F A = A" 

71 
apply (rule equalityI [OF awp_subset]) 

72 
apply (simp add: awp_iff_stable) 

73 
done 

13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

74 

13874  75 
lemma wp_mono: "(A \<subseteq> B) ==> wp act A \<subseteq> wp act B" 
76 
by (simp add: wp_def, blast) 

77 

13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

78 
lemma awp_mono: "(A \<subseteq> B) ==> awp F A \<subseteq> awp F B" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

79 
by (simp add: awp_def wp_def, blast) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

80 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

81 
lemma wens_unfold: 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

82 
"wens F act B = (wp act B \<inter> awp F (B \<union> wens F act B)) \<union> B" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

83 
apply (simp add: wens_def) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

84 
apply (rule gfp_unfold) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

85 
apply (simp add: mono_def wp_def awp_def, blast) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

86 
done 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

87 

13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

88 
lemma wens_Id [simp]: "wens F Id B = B" 
32587
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
30971
diff
changeset

89 
by (simp add: wens_def gfp_def wp_def awp_def, blast) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

90 

13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

91 
text{*These two theorems justify the claim that @{term wens} returns the 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

92 
weakest assertion satisfying the ensures property*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

93 
lemma ensures_imp_wens: "F \<in> A ensures B ==> \<exists>act \<in> Acts F. A \<subseteq> wens F act B" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

94 
apply (simp add: wens_def ensures_def transient_def, clarify) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

95 
apply (rule rev_bexI, assumption) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

96 
apply (rule gfp_upperbound) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

97 
apply (simp add: constrains_def awp_def wp_def, blast) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

98 
done 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

99 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

100 
lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

101 
by (simp add: wens_def gfp_def constrains_def awp_def wp_def 
32587
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
30971
diff
changeset

102 
ensures_def transient_def, blast) 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

103 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

104 
text{*These two results constitute assertion (4.13) of the thesis*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

105 
lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

106 
apply (simp add: wens_def wp_def awp_def) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

107 
apply (rule gfp_mono, blast) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

108 
done 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

109 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

110 
lemma wens_weakening: "B \<subseteq> wens F act B" 
32587
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
30971
diff
changeset

111 
by (simp add: wens_def gfp_def, blast) 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

112 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

113 
text{*Assertion (6), or 4.16 in the thesis*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

114 
lemma subset_wens: "AB \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

115 
apply (simp add: wens_def wp_def awp_def) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

116 
apply (rule gfp_upperbound, blast) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

117 
done 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

118 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

119 
text{*Assertion 4.17 in the thesis*} 
21312  120 
lemma Diff_wens_constrains: "F \<in> (wens F act A  A) co wens F act A" 
32587
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
30971
diff
changeset

121 
by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast) 
15102  122 
{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff} 
123 
is declared as an iffrule, then it's almost impossible to prove. 

124 
One proof is via @{text meson} after expanding all definitions, but it's 

125 
slow!*} 

13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

126 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

127 
text{*Assertion (7): 4.18 in the thesis. NOTE that many of these results 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

128 
hold for an arbitrary action. We often do not require @{term "act \<in> Acts F"}*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

129 
lemma stable_wens: "F \<in> stable A ==> F \<in> stable (wens F act A)" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

130 
apply (simp add: stable_def) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

131 
apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

132 
apply (simp add: Un_Int_distrib2 Compl_partition2) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

133 
apply (erule constrains_weaken, blast) 
32693  134 
apply (simp add: wens_weakening) 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

135 
done 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

136 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

137 
text{*Assertion 4.20 in the thesis.*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

138 
lemma wens_Int_eq_lemma: 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

139 
"[TB \<subseteq> awp F T; act \<in> Acts F] 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

140 
==> T \<inter> wens F act B \<subseteq> wens F act (T\<inter>B)" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

141 
apply (rule subset_wens) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

142 
apply (rule_tac P="\<lambda>x. ?f x \<subseteq> ?b" in ssubst [OF wens_unfold]) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

143 
apply (simp add: wp_def awp_def, blast) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

144 
done 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

145 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

146 
text{*Assertion (8): 4.21 in the thesis. Here we indeed require 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

147 
@{term "act \<in> Acts F"}*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

148 
lemma wens_Int_eq: 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

149 
"[TB \<subseteq> awp F T; act \<in> Acts F] 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

150 
==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

151 
apply (rule equalityI) 
32693  152 
apply (simp_all add: Int_lower1) 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

153 
apply (rule wens_Int_eq_lemma, assumption+) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

154 
apply (rule subset_trans [OF _ wens_mono [of "T\<inter>B" B]], auto) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

155 
done 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

156 

13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

157 

13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

158 
subsection{*Defining the Weakest Ensures Set*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

159 

23767  160 
inductive_set 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

161 
wens_set :: "['a program, 'a set] => 'a set set" 
23767  162 
for F :: "'a program" and B :: "'a set" 
163 
where 

13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

164 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

165 
Basis: "B \<in> wens_set F B" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

166 

23767  167 
 Wens: "[X \<in> wens_set F B; act \<in> Acts F] ==> wens F act X \<in> wens_set F B" 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

168 

23767  169 
 Union: "W \<noteq> {} ==> \<forall>U \<in> W. U \<in> wens_set F B ==> \<Union>W \<in> wens_set F B" 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

170 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

171 
lemma wens_set_imp_co: "A \<in> wens_set F B ==> F \<in> (AB) co A" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

172 
apply (erule wens_set.induct) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

173 
apply (simp add: constrains_def) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

174 
apply (drule_tac act1=act and A1=X 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

175 
in constrains_Un [OF Diff_wens_constrains]) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

176 
apply (erule constrains_weaken, blast) 
32693  177 
apply (simp add: wens_weakening) 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

178 
apply (rule constrains_weaken) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

179 
apply (rule_tac I=W and A="\<lambda>v. vB" and A'="\<lambda>v. v" in constrains_UN, blast+) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

180 
done 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

181 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

182 
lemma wens_set_imp_leadsTo: "A \<in> wens_set F B ==> F \<in> A leadsTo B" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

183 
apply (erule wens_set.induct) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

184 
apply (rule leadsTo_refl) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

185 
apply (blast intro: wens_ensures leadsTo_Trans) 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

186 
apply (blast intro: leadsTo_Union) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

187 
done 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

188 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

189 
lemma leadsTo_imp_wens_set: "F \<in> A leadsTo B ==> \<exists>C \<in> wens_set F B. A \<subseteq> C" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

190 
apply (erule leadsTo_induct_pre) 
13861  191 
apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens) 
192 
apply (clarify, drule ensures_weaken_R, assumption) 

13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

193 
apply (blast dest!: ensures_imp_wens intro: wens_set.Wens) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

194 
apply (case_tac "S={}") 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

195 
apply (simp, blast intro: wens_set.Basis) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

196 
apply (clarsimp dest!: bchoice simp: ball_conj_distrib Bex_def) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

197 
apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>S. Z = f U}" in exI) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

198 
apply (blast intro: wens_set.Union) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

199 
done 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

200 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

201 
text{*Assertion (9): 4.27 in the thesis.*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

202 
lemma leadsTo_iff_wens_set: "(F \<in> A leadsTo B) = (\<exists>C \<in> wens_set F B. A \<subseteq> C)" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

203 
by (blast intro: leadsTo_imp_wens_set leadsTo_weaken_L wens_set_imp_leadsTo) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

204 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

205 
text{*This is the result that requires the definition of @{term wens_set} to 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

206 
require @{term W} to be nonempty in the Unio case, for otherwise we should 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

207 
always have @{term "{} \<in> wens_set F B"}.*} 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

208 
lemma wens_set_imp_subset: "A \<in> wens_set F B ==> B \<subseteq> A" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

209 
apply (erule wens_set.induct) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

210 
apply (blast intro: wens_weakening [THEN subsetD])+ 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

211 
done 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

212 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

213 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

214 
subsection{*Properties Involving Program Union*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

215 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

216 
text{*Assertion (4.30) of thesis, reoriented*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

217 
lemma awp_Join_eq: "awp (F\<squnion>G) B = awp F B \<inter> awp G B" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

218 
by (simp add: awp_def wp_def, blast) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

219 

13861  220 
lemma wens_subset: "wens F act B  B \<subseteq> wp act B \<inter> awp F (B \<union> wens F act B)" 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

221 
by (subst wens_unfold, fast) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

222 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

223 
text{*Assertion (4.31)*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

224 
lemma subset_wens_Join: 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

225 
"[A = T \<inter> wens F act B; TB \<subseteq> awp F T; AB \<subseteq> awp G (A \<union> B)] 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

226 
==> A \<subseteq> wens (F\<squnion>G) act B" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

227 
apply (subgoal_tac "(T \<inter> wens F act B)  B \<subseteq> 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

228 
wp act B \<inter> awp F (B \<union> wens F act B) \<inter> awp F T") 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

229 
apply (rule subset_wens) 
32693  230 
apply (simp add: awp_Join_eq awp_Int_eq Un_commute) 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

231 
apply (simp add: awp_def wp_def, blast) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

232 
apply (insert wens_subset [of F act B], blast) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

233 
done 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

234 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

235 
text{*Assertion (4.32)*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

236 
lemma wens_Join_subset: "wens (F\<squnion>G) act B \<subseteq> wens F act B" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

237 
apply (simp add: wens_def) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

238 
apply (rule gfp_mono) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

239 
apply (auto simp add: awp_Join_eq) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

240 
done 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

241 

0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

242 
text{*Lemma, because the inductive step is just too messy.*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

243 
lemma wens_Union_inductive_step: 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

244 
assumes awpF: "TB \<subseteq> awp F T" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

245 
and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X)  B \<subseteq> awp G (T\<inter>X)" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

246 
shows "[X \<in> wens_set F B; act \<in> Acts F; Y \<subseteq> X; T\<inter>X = T\<inter>Y] 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

247 
==> wens (F\<squnion>G) act Y \<subseteq> wens F act X \<and> 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

248 
T \<inter> wens F act X = T \<inter> wens (F\<squnion>G) act Y" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

249 
apply (subgoal_tac "wens (F\<squnion>G) act Y \<subseteq> wens F act X") 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

250 
prefer 2 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

251 
apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

252 
apply (rule equalityI) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

253 
prefer 2 apply blast 
32693  254 
apply (simp add: Int_lower1) 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

255 
apply (frule wens_set_imp_subset) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

256 
apply (subgoal_tac "TX \<subseteq> awp F T") 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

257 
prefer 2 apply (blast intro: awpF [THEN subsetD]) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

258 
apply (rule_tac B = "wens (F\<squnion>G) act (T\<inter>X)" in subset_trans) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

259 
prefer 2 apply (blast intro!: wens_mono) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

260 
apply (subst wens_Int_eq, assumption+) 
13861  261 
apply (rule subset_wens_Join [of _ T], simp, blast) 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

262 
apply (subgoal_tac "T \<inter> wens F act (T\<inter>X) \<union> T\<inter>X = T \<inter> wens F act X") 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

263 
prefer 2 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

264 
apply (subst wens_Int_eq [symmetric], assumption+) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

265 
apply (blast intro: wens_weakening [THEN subsetD], simp) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

266 
apply (blast intro: awpG [THEN subsetD] wens_set.Wens) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

267 
done 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

268 

13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

269 
theorem wens_Union: 
13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

270 
assumes awpF: "TB \<subseteq> awp F T" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

271 
and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X)  B \<subseteq> awp G (T\<inter>X)" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

272 
and major: "X \<in> wens_set F B" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

273 
shows "\<exists>Y \<in> wens_set (F\<squnion>G) B. Y \<subseteq> X & T\<inter>X = T\<inter>Y" 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

274 
apply (rule wens_set.induct [OF major]) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

275 
txt{*Basis: trivial*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

276 
apply (blast intro: wens_set.Basis) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

277 
txt{*Inductive step*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

278 
apply clarify 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

279 
apply (rule_tac x = "wens (F\<squnion>G) act Y" in rev_bexI) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

280 
apply (force intro: wens_set.Wens) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

281 
apply (simp add: wens_Union_inductive_step [OF awpF awpG]) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

282 
txt{*Union: by Axiom of Choice*} 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

283 
apply (simp add: ball_conj_distrib Bex_def) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

284 
apply (clarify dest!: bchoice) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

285 
apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>W. Z = f U}" in exI) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

286 
apply (blast intro: wens_set.Union) 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

287 
done 
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

288 

13866  289 
theorem leadsTo_Join: 
290 
assumes leadsTo: "F \<in> A leadsTo B" 

291 
and awpF: "TB \<subseteq> awp F T" 

13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

292 
and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X)  B \<subseteq> awp G (T\<inter>X)" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

293 
shows "F\<squnion>G \<in> T\<inter>A leadsTo B" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

294 
apply (rule leadsTo [THEN leadsTo_imp_wens_set, THEN bexE]) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

295 
apply (rule wens_Union [THEN bexE]) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

296 
apply (rule awpF) 
13851  297 
apply (erule awpG, assumption) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

298 
apply (blast intro: wens_set_imp_leadsTo [THEN leadsTo_weaken_L]) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

299 
done 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

300 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

301 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

302 
subsection {*The Set @{term "wens_set F B"} for a SingleAssignment Program*} 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

303 
text{*Thesis Section 4.3.3*} 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

304 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

305 
text{*We start by proving laws about singleassignment programs*} 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

306 
lemma awp_single_eq [simp]: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

307 
"awp (mk_program (init, {act}, allowed)) B = B \<inter> wp act B" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

308 
by (force simp add: awp_def wp_def) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

309 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

310 
lemma wp_Un_subset: "wp act A \<union> wp act B \<subseteq> wp act (A \<union> B)" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

311 
by (force simp add: wp_def) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

312 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

313 
lemma wp_Un_eq: "single_valued act ==> wp act (A \<union> B) = wp act A \<union> wp act B" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

314 
apply (rule equalityI) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

315 
apply (force simp add: wp_def single_valued_def) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

316 
apply (rule wp_Un_subset) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

317 
done 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

318 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

319 
lemma wp_UN_subset: "(\<Union>i\<in>I. wp act (A i)) \<subseteq> wp act (\<Union>i\<in>I. A i)" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

320 
by (force simp add: wp_def) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

321 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

322 
lemma wp_UN_eq: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

323 
"[single_valued act; I\<noteq>{}] 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

324 
==> wp act (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. wp act (A i))" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

325 
apply (rule equalityI) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

326 
prefer 2 apply (rule wp_UN_subset) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

327 
apply (simp add: wp_def Image_INT_eq) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

328 
done 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

329 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

330 
lemma wens_single_eq: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

331 
"wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B" 
32587
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
30971
diff
changeset

332 
by (simp add: wens_def gfp_def wp_def, blast) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

333 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

334 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

335 
text{*Next, we express the @{term "wens_set"} for singleassignment programs*} 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

336 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32693
diff
changeset

337 
definition wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set" where 
30971  338 
"wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act ^^ i) B" 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

339 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32693
diff
changeset

340 
definition wens_single :: "[('a*'a) set, 'a set] => 'a set" where 
30971  341 
"wens_single act B == \<Union>i. (wp act ^^ i) B" 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

342 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

343 
lemma wens_single_Un_eq: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

344 
"single_valued act 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

345 
==> wens_single act B \<union> wp act (wens_single act B) = wens_single act B" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

346 
apply (rule equalityI) 
32693  347 
apply (simp_all add: Un_upper1) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

348 
apply (simp add: wens_single_def wp_UN_eq, clarify) 
56248
67dc9549fa15
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
haftmann
parents:
46911
diff
changeset

349 
apply (rule_tac a="Suc xa" in UN_I, auto) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

350 
done 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

351 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

352 
lemma atMost_nat_nonempty: "atMost (k::nat) \<noteq> {}" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

353 
by force 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

354 

13851  355 
lemma wens_single_finite_0 [simp]: "wens_single_finite act B 0 = B" 
356 
by (simp add: wens_single_finite_def) 

357 

13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

358 
lemma wens_single_finite_Suc: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

359 
"single_valued act 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

360 
==> wens_single_finite act B (Suc k) = 
13851  361 
wens_single_finite act B k \<union> wp act (wens_single_finite act B k)" 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

362 
apply (simp add: wens_single_finite_def image_def 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

363 
wp_UN_eq [OF _ atMost_nat_nonempty]) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

364 
apply (force elim!: le_SucE) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

365 
done 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

366 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

367 
lemma wens_single_finite_Suc_eq_wens: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

368 
"single_valued act 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

369 
==> wens_single_finite act B (Suc k) = 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

370 
wens (mk_program (init, {act}, allowed)) act 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

371 
(wens_single_finite act B k)" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

372 
by (simp add: wens_single_finite_Suc wens_single_eq) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

373 

13851  374 
lemma def_wens_single_finite_Suc_eq_wens: 
375 
"[F = mk_program (init, {act}, allowed); single_valued act] 

376 
==> wens_single_finite act B (Suc k) = 

377 
wens F act (wens_single_finite act B k)" 

378 
by (simp add: wens_single_finite_Suc_eq_wens) 

379 

13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

380 
lemma wens_single_finite_Un_eq: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

381 
"single_valued act 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

382 
==> wens_single_finite act B k \<union> wp act (wens_single_finite act B k) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

383 
\<in> range (wens_single_finite act B)" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

384 
by (simp add: wens_single_finite_Suc [symmetric]) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

385 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

386 
lemma wens_single_eq_Union: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

387 
"wens_single act B = \<Union>range (wens_single_finite act B)" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

388 
by (simp add: wens_single_finite_def wens_single_def, blast) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

389 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

390 
lemma wens_single_finite_eq_Union: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

391 
"wens_single_finite act B n = (\<Union>k\<in>atMost n. wens_single_finite act B k)" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

392 
apply (auto simp add: wens_single_finite_def) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

393 
apply (blast intro: le_trans) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

394 
done 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

395 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

396 
lemma wens_single_finite_mono: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

397 
"m \<le> n ==> wens_single_finite act B m \<subseteq> wens_single_finite act B n" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

398 
by (force simp add: wens_single_finite_eq_Union [of act B n]) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

399 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

400 
lemma wens_single_finite_subset_wens_single: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

401 
"wens_single_finite act B k \<subseteq> wens_single act B" 
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15102
diff
changeset

402 
by (simp add: wens_single_eq_Union, blast) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

403 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

404 
lemma subset_wens_single_finite: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

405 
"[W \<subseteq> wens_single_finite act B ` (atMost k); single_valued act; W\<noteq>{}] 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

406 
==> \<exists>m. \<Union>W = wens_single_finite act B m" 
13851  407 
apply (induct k) 
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15102
diff
changeset

408 
apply (rule_tac x=0 in exI, simp, blast) 
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15102
diff
changeset

409 
apply (auto simp add: atMost_Suc) 
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15102
diff
changeset

410 
apply (case_tac "wens_single_finite act B (Suc k) \<in> W") 
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15102
diff
changeset

411 
prefer 2 apply blast 
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15102
diff
changeset

412 
apply (drule_tac x="Suc k" in spec) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

413 
apply (erule notE, rule equalityI) 
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15102
diff
changeset

414 
prefer 2 apply blast 
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15102
diff
changeset

415 
apply (subst wens_single_finite_eq_Union) 
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15102
diff
changeset

416 
apply (simp add: atMost_Suc, blast) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

417 
done 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

418 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

419 
text{*lemma for Union case*} 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

420 
lemma Union_eq_wens_single: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

421 
"\<lbrakk>\<forall>k. \<not> W \<subseteq> wens_single_finite act B ` {..k}; 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

422 
W \<subseteq> insert (wens_single act B) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

423 
(range (wens_single_finite act B))\<rbrakk> 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

424 
\<Longrightarrow> \<Union>W = wens_single act B" 
46911  425 
apply (cases "wens_single act B \<in> W") 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

426 
apply (blast dest: wens_single_finite_subset_wens_single [THEN subsetD]) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

427 
apply (simp add: wens_single_eq_Union) 
13851  428 
apply (rule equalityI, blast) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

429 
apply (simp add: UN_subset_iff, clarify) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

430 
apply (subgoal_tac "\<exists>y\<in>W. \<exists>n. y = wens_single_finite act B n & i\<le>n") 
13851  431 
apply (blast intro: wens_single_finite_mono [THEN subsetD]) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

432 
apply (drule_tac x=i in spec) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

433 
apply (force simp add: atMost_def) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

434 
done 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

435 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

436 
lemma wens_set_subset_single: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

437 
"single_valued act 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

438 
==> wens_set (mk_program (init, {act}, allowed)) B \<subseteq> 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

439 
insert (wens_single act B) (range (wens_single_finite act B))" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

440 
apply (rule subsetI) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

441 
apply (erule wens_set.induct) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

442 
txt{*Basis*} 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44106
diff
changeset

443 
apply (fastforce simp add: wens_single_finite_def) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

444 
txt{*Wens inductive step*} 
21733  445 
apply (case_tac "acta = Id", simp) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

446 
apply (simp add: wens_single_eq) 
21733  447 
apply (elim disjE) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

448 
apply (simp add: wens_single_Un_eq) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

449 
apply (force simp add: wens_single_finite_Un_eq) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

450 
txt{*Union inductive step*} 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

451 
apply (case_tac "\<exists>k. W \<subseteq> wens_single_finite act B ` (atMost k)") 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

452 
apply (blast dest!: subset_wens_single_finite, simp) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

453 
apply (rule disjI1 [OF Union_eq_wens_single], blast+) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

454 
done 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

455 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

456 
lemma wens_single_finite_in_wens_set: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

457 
"single_valued act \<Longrightarrow> 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

458 
wens_single_finite act B k 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

459 
\<in> wens_set (mk_program (init, {act}, allowed)) B" 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

460 
apply (induct_tac k) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

461 
apply (simp add: wens_single_finite_def wens_set.Basis) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

462 
apply (simp add: wens_set.Wens 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

463 
wens_single_finite_Suc_eq_wens [of act B _ init allowed]) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

464 
done 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

465 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

466 
lemma single_subset_wens_set: 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

467 
"single_valued act 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

468 
==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq> 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

469 
wens_set (mk_program (init, {act}, allowed)) B" 
44106  470 
apply (simp add: SUP_def image_def wens_single_eq_Union) 
13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

471 
apply (blast intro: wens_set.Union wens_single_finite_in_wens_set) 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

472 
done 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

473 

e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

474 
text{*Theorem (4.29)*} 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

475 
theorem wens_set_single_eq: 
13851  476 
"[F = mk_program (init, {act}, allowed); single_valued act] 
477 
==> wens_set F B = 

478 
insert (wens_single act B) (range (wens_single_finite act B))" 

13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

479 
apply (rule equalityI) 
13851  480 
apply (simp add: wens_set_subset_single) 
481 
apply (erule ssubst, erule single_subset_wens_set) 

13832
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

482 
done 
e7649436869c
completed proofs for programs consisting of a single assignment
paulson
parents:
13821
diff
changeset

483 

13853
89131afa9f01
New theory ProgressSets. Definition of closure sets
paulson
parents:
13851
diff
changeset

484 
text{*Generalizing Misra's Fixed Point Union Theorem (4.41)*} 
89131afa9f01
New theory ProgressSets. Definition of closure sets
paulson
parents:
13851
diff
changeset

485 

13866  486 
lemma fp_leadsTo_Join: 
13853
89131afa9f01
New theory ProgressSets. Definition of closure sets
paulson
parents:
13851
diff
changeset

487 
"[TB \<subseteq> awp F T; TB \<subseteq> FP G; F \<in> A leadsTo B] ==> F\<squnion>G \<in> T\<inter>A leadsTo B" 
13866  488 
apply (rule leadsTo_Join, assumption, blast) 
489 
apply (simp add: FP_def awp_iff_constrains stable_def constrains_def, blast) 

13853
89131afa9f01
New theory ProgressSets. Definition of closure sets
paulson
parents:
13851
diff
changeset

490 
done 
89131afa9f01
New theory ProgressSets. Definition of closure sets
paulson
parents:
13851
diff
changeset

491 

13821
0fd39aa77095
new theory Transformers: MeierSanders noninterference theory
paulson
parents:
diff
changeset

492 
end 