author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
child 58871  c399ae4b836f 
permissions  rwrr 
11479  1 
(* Title: ZF/UNITY/Comp.thy 
2 
Author: Sidi O Ehmety, Computer Laboratory 

3 
Copyright 1998 University of Cambridge 

4 

5 
From Chandy and Sanders, "Reasoning About Program Composition", 

6 
Technical Report 2000003, University of Florida, 2000. 

7 

8 
Revised by Sidi Ehmety on January 2001 

9 

10 
Added: a strong form of the order relation over component and localize 

11 

12 
Theory ported from HOL. 

13 

14 
*) 

15 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

16 
header{*Composition*} 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

17 

16417  18 
theory Comp imports Union Increasing begin 
11479  19 

24893  20 
definition 
21 
component :: "[i,i]=>o" (infixl "component" 65) where 

46823  22 
"F component H == (\<exists>G. F Join G = H)" 
11479  23 

24893  24 
definition 
25 
strict_component :: "[i,i]=>o" (infixl "strict'_component" 65) where 

46823  26 
"F strict_component H == F component H & F\<noteq>H" 
11479  27 

24893  28 
definition 
11479  29 
(* A stronger form of the component relation *) 
24893  30 
component_of :: "[i,i]=>o" (infixl "component'_of" 65) where 
46823  31 
"F component_of H == (\<exists>G. F ok G & F Join G = H)" 
11479  32 

24893  33 
definition 
34 
strict_component_of :: "[i,i]=>o" (infixl "strict'_component'_of" 65) where 

46823  35 
"F strict_component_of H == F component_of H & F\<noteq>H" 
11479  36 

24893  37 
definition 
12195  38 
(* Preserves a state function f, in particular a variable *) 
24893  39 
preserves :: "(i=>i)=>i" where 
46823  40 
"preserves(f) == {F:program. \<forall>z. F: stable({s:state. f(s) = z})}" 
11479  41 

24893  42 
definition 
43 
fun_pair :: "[i=>i, i =>i] =>(i=>i)" where 

14046  44 
"fun_pair(f, g) == %x. <f(x), g(x)>" 
45 

24893  46 
definition 
47 
localize :: "[i=>i, i] => i" where 

11479  48 
"localize(f,F) == mk_program(Init(F), Acts(F), 
46823  49 
AllowedActs(F) \<inter> (\<Union>G\<in>preserves(f). Acts(G)))" 
11479  50 

51 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

52 
(*** component and strict_component relations ***) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

53 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

54 
lemma componentI: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

55 
"H component F  H component G ==> H component (F Join G)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

56 
apply (unfold component_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

57 
apply (rule_tac x = "Ga Join G" in exI) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

58 
apply (rule_tac [2] x = "G Join F" in exI) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

59 
apply (auto simp add: Join_ac) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

60 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

61 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

62 
lemma component_eq_subset: 
46823  63 
"G \<in> program ==> (F component G) \<longleftrightarrow> 
64 
(Init(G) \<subseteq> Init(F) & Acts(F) \<subseteq> Acts(G) & AllowedActs(G) \<subseteq> AllowedActs(F))" 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

65 
apply (unfold component_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

66 
apply (rule exI) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

67 
apply (rule program_equalityI, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

68 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

69 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

70 
lemma component_SKIP [simp]: "F \<in> program ==> SKIP component F" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

71 
apply (unfold component_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

72 
apply (rule_tac x = F in exI) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

73 
apply (force intro: Join_SKIP_left) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

74 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

75 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

76 
lemma component_refl [simp]: "F \<in> program ==> F component F" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

77 
apply (unfold component_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

78 
apply (rule_tac x = F in exI) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

79 
apply (force intro: Join_SKIP_right) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

80 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

81 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

82 
lemma SKIP_minimal: "F component SKIP ==> programify(F) = SKIP" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

83 
apply (rule program_equalityI) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

84 
apply (simp_all add: component_eq_subset, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

85 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

86 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

87 
lemma component_Join1: "F component (F Join G)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

88 
by (unfold component_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

89 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

90 
lemma component_Join2: "G component (F Join G)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

91 
apply (unfold component_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

92 
apply (simp (no_asm) add: Join_commute) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

93 
apply blast 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

94 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

95 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

96 
lemma Join_absorb1: "F component G ==> F Join G = G" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

97 
by (auto simp add: component_def Join_left_absorb) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

98 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

99 
lemma Join_absorb2: "G component F ==> F Join G = F" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

100 
by (auto simp add: Join_ac component_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

101 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

102 
lemma JN_component_iff: 
46823  103 
"H \<in> program==>(JOIN(I,F) component H) \<longleftrightarrow> (\<forall>i \<in> I. F(i) component H)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

104 
apply (case_tac "I=0", force) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

105 
apply (simp (no_asm_simp) add: component_eq_subset) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

106 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

107 
apply blast 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

108 
apply (rename_tac "y") 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

109 
apply (drule_tac c = y and A = "AllowedActs (H)" in subsetD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

110 
apply (blast elim!: not_emptyE)+ 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

111 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

112 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

113 
lemma component_JN: "i \<in> I ==> F(i) component (\<Squnion>i \<in> I. (F(i)))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

114 
apply (unfold component_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

115 
apply (blast intro: JN_absorb) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

116 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

117 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

118 
lemma component_trans: "[ F component G; G component H ] ==> F component H" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

119 
apply (unfold component_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

120 
apply (blast intro: Join_assoc [symmetric]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

121 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

122 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

123 
lemma component_antisym: 
46823  124 
"[ F \<in> program; G \<in> program ] ==>(F component G & G component F) \<longrightarrow> F = G" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

125 
apply (simp (no_asm_simp) add: component_eq_subset) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

126 
apply clarify 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

127 
apply (rule program_equalityI, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

128 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

129 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

130 
lemma Join_component_iff: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

131 
"H \<in> program ==> 
46823  132 
((F Join G) component H) \<longleftrightarrow> (F component H & G component H)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

133 
apply (simp (no_asm_simp) add: component_eq_subset) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

134 
apply blast 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

135 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

136 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

137 
lemma component_constrains: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

138 
"[ F component G; G \<in> A co B; F \<in> program ] ==> F \<in> A co B" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

139 
apply (frule constrainsD2) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

140 
apply (auto simp add: constrains_def component_eq_subset) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

141 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

142 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

143 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

144 
(*** preserves ***) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

145 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

146 
lemma preserves_is_safety_prop [simp]: "safety_prop(preserves(f))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

147 
apply (unfold preserves_def safety_prop_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

148 
apply (auto dest: ActsD simp add: stable_def constrains_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

149 
apply (drule_tac c = act in subsetD, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

150 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

151 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

152 
lemma preservesI [rule_format]: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

153 
"\<forall>z. F \<in> stable({s \<in> state. f(s) = z}) ==> F \<in> preserves(f)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

154 
apply (auto simp add: preserves_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

155 
apply (blast dest: stableD2) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

156 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

157 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

158 
lemma preserves_imp_eq: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

159 
"[ F \<in> preserves(f); act \<in> Acts(F); <s,t> \<in> act ] ==> f(s) = f(t)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

160 
apply (unfold preserves_def stable_def constrains_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

161 
apply (subgoal_tac "s \<in> state & t \<in> state") 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

162 
prefer 2 apply (blast dest!: Acts_type [THEN subsetD], force) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

163 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

164 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

165 
lemma Join_preserves [iff]: 
46823  166 
"(F Join G \<in> preserves(v)) \<longleftrightarrow> 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

167 
(programify(F) \<in> preserves(v) & programify(G) \<in> preserves(v))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

168 
by (auto simp add: preserves_def INT_iff) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

169 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

170 
lemma JN_preserves [iff]: 
46823  171 
"(JOIN(I,F): preserves(v)) \<longleftrightarrow> (\<forall>i \<in> I. programify(F(i)):preserves(v))" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

172 
by (auto simp add: JN_stable preserves_def INT_iff) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

173 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

174 
lemma SKIP_preserves [iff]: "SKIP \<in> preserves(v)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

175 
by (auto simp add: preserves_def INT_iff) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

176 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

177 
lemma fun_pair_apply [simp]: "fun_pair(f,g,x) = <f(x), g(x)>" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

178 
apply (unfold fun_pair_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

179 
apply (simp (no_asm)) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

180 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

181 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

182 
lemma preserves_fun_pair: 
46823  183 
"preserves(fun_pair(v,w)) = preserves(v) \<inter> preserves(w)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

184 
apply (rule equalityI) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

185 
apply (auto simp add: preserves_def stable_def constrains_def, blast+) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

186 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

187 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

188 
lemma preserves_fun_pair_iff [iff]: 
46823  189 
"F \<in> preserves(fun_pair(v, w)) \<longleftrightarrow> F \<in> preserves(v) \<inter> preserves(w)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

190 
by (simp add: preserves_fun_pair) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

191 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

192 
lemma fun_pair_comp_distrib: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

193 
"(fun_pair(f, g) comp h)(x) = fun_pair(f comp h, g comp h, x)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

194 
by (simp add: fun_pair_def metacomp_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

195 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

196 
lemma comp_apply [simp]: "(f comp g)(x) = f(g(x))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

197 
by (simp add: metacomp_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

198 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

199 
lemma preserves_type: "preserves(v)<=program" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

200 
by (unfold preserves_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

201 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

202 
lemma preserves_into_program [TC]: "F \<in> preserves(f) ==> F \<in> program" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

203 
by (blast intro: preserves_type [THEN subsetD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

204 

46823  205 
lemma subset_preserves_comp: "preserves(f) \<subseteq> preserves(g comp f)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

206 
apply (auto simp add: preserves_def stable_def constrains_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

207 
apply (drule_tac x = "f (xb)" in spec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

208 
apply (drule_tac x = act in bspec, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

209 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

210 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

211 
lemma imp_preserves_comp: "F \<in> preserves(f) ==> F \<in> preserves(g comp f)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

212 
by (blast intro: subset_preserves_comp [THEN subsetD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

213 

46823  214 
lemma preserves_subset_stable: "preserves(f) \<subseteq> stable({s \<in> state. P(f(s))})" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

215 
apply (auto simp add: preserves_def stable_def constrains_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

216 
apply (rename_tac s' s) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

217 
apply (subgoal_tac "f (s) = f (s') ") 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

218 
apply (force+) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

219 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

220 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

221 
lemma preserves_imp_stable: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

222 
"F \<in> preserves(f) ==> F \<in> stable({s \<in> state. P(f(s))})" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

223 
by (blast intro: preserves_subset_stable [THEN subsetD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

224 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

225 
lemma preserves_imp_increasing: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

226 
"[ F \<in> preserves(f); \<forall>x \<in> state. f(x):A ] ==> F \<in> Increasing.increasing(A, r, f)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

227 
apply (unfold Increasing.increasing_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

228 
apply (auto intro: preserves_into_program) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

229 
apply (rule_tac P = "%x. <k, x>:r" in preserves_imp_stable, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

230 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

231 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

232 
lemma preserves_id_subset_stable: 
46823  233 
"st_set(A) ==> preserves(%x. x) \<subseteq> stable(A)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

234 
apply (unfold preserves_def stable_def constrains_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

235 
apply (drule_tac x = xb in spec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

236 
apply (drule_tac x = act in bspec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

237 
apply (auto dest: ActsD) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

238 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

239 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

240 
lemma preserves_id_imp_stable: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

241 
"[ F \<in> preserves(%x. x); st_set(A) ] ==> F \<in> stable(A)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

242 
by (blast intro: preserves_id_subset_stable [THEN subsetD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

243 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

244 
(** Added by Sidi **) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

245 
(** component_of **) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

246 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

247 
(* component_of is stronger than component *) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

248 
lemma component_of_imp_component: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

249 
"F component_of H ==> F component H" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

250 
apply (unfold component_def component_of_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

251 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

252 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

253 
(* component_of satisfies many of component's properties *) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

254 
lemma component_of_refl [simp]: "F \<in> program ==> F component_of F" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

255 
apply (unfold component_of_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

256 
apply (rule_tac x = SKIP in exI, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

257 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

258 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

259 
lemma component_of_SKIP [simp]: "F \<in> program ==>SKIP component_of F" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

260 
apply (unfold component_of_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

261 
apply (rule_tac x = F in exI, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

262 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

263 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

264 
lemma component_of_trans: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

265 
"[ F component_of G; G component_of H ] ==> F component_of H" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

266 
apply (unfold component_of_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

267 
apply (blast intro: Join_assoc [symmetric]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

268 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

269 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

270 
(** localize **) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

271 
lemma localize_Init_eq [simp]: "Init(localize(v,F)) = Init(F)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

272 
by (unfold localize_def, simp) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

273 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

274 
lemma localize_Acts_eq [simp]: "Acts(localize(v,F)) = Acts(F)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

275 
by (unfold localize_def, simp) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

276 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

277 
lemma localize_AllowedActs_eq [simp]: 
46823  278 
"AllowedActs(localize(v,F)) = AllowedActs(F) \<inter> (\<Union>G \<in> preserves(v). Acts(G))" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

279 
apply (unfold localize_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

280 
apply (rule equalityI) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

281 
apply (auto dest: Acts_type [THEN subsetD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

282 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

283 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

284 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

285 
(** Theorems used in ClientImpl **) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

286 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

287 
lemma stable_localTo_stable2: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

288 
"[ F \<in> stable({s \<in> state. P(f(s), g(s))}); G \<in> preserves(f); G \<in> preserves(g) ] 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

289 
==> F Join G \<in> stable({s \<in> state. P(f(s), g(s))})" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

290 
apply (auto dest: ActsD preserves_into_program simp add: stable_def constrains_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

291 
apply (case_tac "act \<in> Acts (F) ") 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

292 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

293 
apply (drule preserves_imp_eq) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

294 
apply (drule_tac [3] preserves_imp_eq, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

295 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

296 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

297 
lemma Increasing_preserves_Stable: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

298 
"[ F \<in> stable({s \<in> state. <f(s), g(s)>:r}); G \<in> preserves(f); 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

299 
F Join G \<in> Increasing(A, r, g); 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

300 
\<forall>x \<in> state. f(x):A & g(x):A ] 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

301 
==> F Join G \<in> Stable({s \<in> state. <f(s), g(s)>:r})" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

302 
apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

303 
apply (simp_all add: constrains_type [THEN subsetD] preserves_type [THEN subsetD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

304 
apply (blast intro: constrains_weaken) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

305 
(*The G case remains*) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

306 
apply (auto dest: ActsD simp add: preserves_def stable_def constrains_def ball_conj_distrib all_conj_distrib) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

307 
(*We have a Gaction, so delete assumptions about Factions*) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

308 
apply (erule_tac V = "\<forall>act \<in> Acts (F) . ?P (act)" in thin_rl) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

309 
apply (erule_tac V = "\<forall>k\<in>A. \<forall>act \<in> Acts (F) . ?P (k,act)" in thin_rl) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

310 
apply (subgoal_tac "f (x) = f (xa) ") 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

311 
apply (auto dest!: bspec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

312 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

313 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

314 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

315 
(** Lemma used in AllocImpl **) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

316 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

317 
lemma Constrains_UN_left: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

318 
"[ \<forall>x \<in> I. F \<in> A(x) Co B; F \<in> program ] ==> F:(\<Union>x \<in> I. A(x)) Co B" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

319 
by (unfold Constrains_def constrains_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

320 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

321 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

322 
lemma stable_Join_Stable: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

323 
"[ F \<in> stable({s \<in> state. P(f(s), g(s))}); 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

324 
\<forall>k \<in> A. F Join G \<in> Stable({s \<in> state. P(k, g(s))}); 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

325 
G \<in> preserves(f); \<forall>s \<in> state. f(s):A] 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

326 
==> F Join G \<in> Stable({s \<in> state. P(f(s), g(s))})" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

327 
apply (unfold stable_def Stable_def preserves_def) 
46823  328 
apply (rule_tac A = "(\<Union>k \<in> A. {s \<in> state. f(s)=k} \<inter> {s \<in> state. P (f (s), g (s))})" in Constrains_weaken_L) 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

329 
prefer 2 apply blast 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

330 
apply (rule Constrains_UN_left, auto) 
46823  331 
apply (rule_tac A = "{s \<in> state. f(s)=k} \<inter> {s \<in> state. P (f (s), g (s))} \<inter> {s \<in> state. P (k, g (s))}" and A' = "({s \<in> state. f(s)=k} \<union> {s \<in> state. P (f (s), g (s))}) \<inter> {s \<in> state. P (k, g (s))}" in Constrains_weaken) 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

332 
prefer 2 apply blast 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

333 
prefer 2 apply blast 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

334 
apply (rule Constrains_Int) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

335 
apply (rule constrains_imp_Constrains) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

336 
apply (auto simp add: constrains_type [THEN subsetD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

337 
apply (blast intro: constrains_weaken) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

338 
apply (drule_tac x = k in spec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

339 
apply (blast intro: constrains_weaken) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

340 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

341 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
14046
diff
changeset

342 
end 