author  wenzelm 
Tue, 29 Mar 2011 17:47:11 +0200  
changeset 42151  4da4fc77664b 
parent 40945  b8703f63bfb2 
child 60754  02924903a6fd 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy 
40945  2 
Author: Olaf MÃ¼ller 
17256  3 
*) 
3071  4 

17256  5 
theory ShortExecutions 
6 
imports Traces 

7 
begin 

3071  8 

17256  9 
text {* 
10 
Some properties about @{text "Cut ex"}, defined as follows: 

3071  11 

17256  12 
For every execution ex there is another shorter execution @{text "Cut ex"} 
13 
that has the same trace as ex, but its schedule ends with an external action. 

14 
*} 

3071  15 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

16 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

17 
oraclebuild :: "('a => bool) => 'a Seq > 'a Seq > 'a Seq" where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

18 
"oraclebuild P = (fix$(LAM h s t. case t of 
3275  19 
nil => nil 
17256  20 
 x##xs => 
21 
(case x of 

12028  22 
UU => UU 
10835  23 
 Def y => (Takewhile (%x.~P x)$s) 
24 
@@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs)) 

3275  25 
) 
26 
))" 

27 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

28 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

29 
Cut :: "('a => bool) => 'a Seq => 'a Seq" where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

30 
"Cut P s = oraclebuild P$s$(Filter P$s)" 
3071  31 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

32 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

33 
LastActExtsch :: "('a,'s)ioa => 'a Seq => bool" where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

34 
"LastActExtsch A sch = (Cut (%x. x: ext A) sch = sch)" 
3071  35 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

36 
(* LastActExtex ::"('a,'s)ioa => ('a,'s) pairs => bool"*) 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

37 
(* LastActExtex_def: 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

38 
"LastActExtex A ex == LastActExtsch A (filter_act$ex)" *) 
3071  39 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

40 
axiomatization where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

41 
Cut_prefixcl_Finite: "Finite s ==> (? y. s = Cut P s @@ y)" 
3071  42 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

43 
axiomatization where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

44 
LastActExtsmall1: "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))" 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

45 

4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

46 
axiomatization where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

47 
LastActExtsmall2: "[ Finite sch1; LastActExtsch A (sch1 @@ sch2) ] ==> LastActExtsch A sch2" 
19741  48 

49 

50 
ML {* 

51 
fun thin_tac' j = 

52 
rotate_tac (j  1) THEN' 

53 
etac thin_rl THEN' 

54 
rotate_tac (~ (j  1)) 

55 
*} 

56 

57 

58 
subsection "oraclebuild rewrite rules" 

59 

60 

61 
lemma oraclebuild_unfold: 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

62 
"oraclebuild P = (LAM s t. case t of 
19741  63 
nil => nil 
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

64 
 x##xs => 
19741  65 
(case x of 
66 
UU => UU 

67 
 Def y => (Takewhile (%a.~ P a)$s) 

68 
@@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs)) 

69 
) 

70 
)" 

71 
apply (rule trans) 

72 
apply (rule fix_eq2) 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

73 
apply (simp only: oraclebuild_def) 
19741  74 
apply (rule beta_cfun) 
75 
apply simp 

76 
done 

77 

78 
lemma oraclebuild_UU: "oraclebuild P$sch$UU = UU" 

79 
apply (subst oraclebuild_unfold) 

80 
apply simp 

81 
done 

82 

83 
lemma oraclebuild_nil: "oraclebuild P$sch$nil = nil" 

84 
apply (subst oraclebuild_unfold) 

85 
apply simp 

86 
done 

87 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

88 
lemma oraclebuild_cons: "oraclebuild P$s$(x>>t) = 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

89 
(Takewhile (%a.~ P a)$s) 
19741  90 
@@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))" 
91 
apply (rule trans) 

92 
apply (subst oraclebuild_unfold) 

93 
apply (simp add: Consq_def) 

94 
apply (simp add: Consq_def) 

95 
done 

96 

97 

98 
subsection "Cut rewrite rules" 

99 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

100 
lemma Cut_nil: 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

101 
"[ Forall (%a.~ P a) s; Finite s] 
19741  102 
==> Cut P s =nil" 
103 
apply (unfold Cut_def) 

104 
apply (subgoal_tac "Filter P$s = nil") 

105 
apply (simp (no_asm_simp) add: oraclebuild_nil) 

106 
apply (rule ForallQFilterPnil) 

107 
apply assumption+ 

108 
done 

109 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

110 
lemma Cut_UU: 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

111 
"[ Forall (%a.~ P a) s; ~Finite s] 
19741  112 
==> Cut P s =UU" 
113 
apply (unfold Cut_def) 

114 
apply (subgoal_tac "Filter P$s= UU") 

115 
apply (simp (no_asm_simp) add: oraclebuild_UU) 

116 
apply (rule ForallQFilterPUU) 

117 
apply assumption+ 

118 
done 

119 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

120 
lemma Cut_Cons: 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

121 
"[ P t; Forall (%x.~ P x) ss; Finite ss] 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

122 
==> Cut P (ss @@ (t>> rs)) 
19741  123 
= ss @@ (t >> Cut P rs)" 
124 
apply (unfold Cut_def) 

125 
apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc) 

126 
done 

127 

128 

129 
subsection "Cut lemmas for main theorem" 

130 

131 
lemma FilterCut: "Filter P$s = Filter P$(Cut P s)" 

132 
apply (rule_tac A1 = "%x. True" and Q1 = "%x.~ P x" and x1 = "s" in take_lemma_induct [THEN mp]) 

133 
prefer 3 apply (fast) 

134 
apply (case_tac "Finite s") 

135 
apply (simp add: Cut_nil ForallQFilterPnil) 

136 
apply (simp add: Cut_UU ForallQFilterPUU) 

137 
(* main case *) 

138 
apply (simp add: Cut_Cons ForallQFilterPnil) 

139 
done 

140 

141 

142 
lemma Cut_idemp: "Cut P (Cut P s) = (Cut P s)" 

143 
apply (rule_tac A1 = "%x. True" and Q1 = "%x.~ P x" and x1 = "s" in 

144 
take_lemma_less_induct [THEN mp]) 

145 
prefer 3 apply (fast) 

146 
apply (case_tac "Finite s") 

147 
apply (simp add: Cut_nil ForallQFilterPnil) 

148 
apply (simp add: Cut_UU ForallQFilterPUU) 

149 
(* main case *) 

150 
apply (simp add: Cut_Cons ForallQFilterPnil) 

151 
apply (rule take_reduction) 

152 
apply auto 

153 
done 

154 

155 

156 
lemma MapCut: "Map f$(Cut (P o f) s) = Cut P (Map f$s)" 

157 
apply (rule_tac A1 = "%x. True" and Q1 = "%x.~ P (f x) " and x1 = "s" in 

158 
take_lemma_less_induct [THEN mp]) 

159 
prefer 3 apply (fast) 

160 
apply (case_tac "Finite s") 

161 
apply (simp add: Cut_nil) 

162 
apply (rule Cut_nil [symmetric]) 

163 
apply (simp add: ForallMap o_def) 

164 
apply (simp add: Map2Finite) 

165 
(* csae ~ Finite s *) 

166 
apply (simp add: Cut_UU) 

167 
apply (rule Cut_UU) 

168 
apply (simp add: ForallMap o_def) 

169 
apply (simp add: Map2Finite) 

170 
(* main case *) 

171 
apply (simp add: Cut_Cons MapConc ForallMap FiniteMap1 o_def) 

172 
apply (rule take_reduction) 

173 
apply auto 

174 
done 

175 

176 

177 
lemma Cut_prefixcl_nFinite [rule_format (no_asm)]: "~Finite s > Cut P s << s" 

178 
apply (intro strip) 

179 
apply (rule take_lemma_less [THEN iffD1]) 

180 
apply (intro strip) 

181 
apply (rule mp) 

182 
prefer 2 apply (assumption) 

183 
apply (tactic "thin_tac' 1 1") 

184 
apply (rule_tac x = "s" in spec) 

185 
apply (rule nat_less_induct) 

186 
apply (intro strip) 

187 
apply (rename_tac na n s) 

188 
apply (case_tac "Forall (%x. ~ P x) s") 

189 
apply (rule take_lemma_less [THEN iffD2, THEN spec]) 

190 
apply (simp add: Cut_UU) 

191 
(* main case *) 

192 
apply (drule divide_Seq3) 

193 
apply (erule exE)+ 

194 
apply (erule conjE)+ 

195 
apply hypsubst 

196 
apply (simp add: Cut_Cons) 

197 
apply (rule take_reduction_less) 

198 
(* auto makes also reasoning about Finiteness of parts of s ! *) 

199 
apply auto 

200 
done 

201 

202 

203 
lemma execThruCut: "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)" 

204 
apply (case_tac "Finite ex") 

205 
apply (cut_tac s = "ex" and P = "P" in Cut_prefixcl_Finite) 

206 
apply assumption 

207 
apply (erule exE) 

208 
apply (rule exec_prefix2closed) 

209 
apply (erule_tac s = "ex" and t = "Cut P ex @@ y" in subst) 

210 
apply assumption 

211 
apply (erule exec_prefixclosed) 

212 
apply (erule Cut_prefixcl_nFinite) 

213 
done 

214 

215 

216 
subsection "Main Cut Theorem" 

217 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

218 
lemma exists_LastActExtsch: 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

219 
"[sch : schedules A ; tr = Filter (%a. a:ext A)$sch] 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

220 
==> ? sch. sch : schedules A & 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

221 
tr = Filter (%a. a:ext A)$sch & 
19741  222 
LastActExtsch A sch" 
223 

224 
apply (unfold schedules_def has_schedule_def) 

26359  225 
apply auto 
19741  226 
apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI) 
227 
apply (simp add: executions_def) 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset

228 
apply (tactic {* pair_tac @{context} "ex" 1 *}) 
26359  229 
apply auto 
19741  230 
apply (rule_tac x = " (x,Cut (%a. fst a:ext A) y) " in exI) 
231 
apply (simp (no_asm_simp)) 

232 

233 
(* Subgoal 1: Lemma: propagation of execution through Cut *) 

234 

235 
apply (simp add: execThruCut) 

236 

237 
(* Subgoal 2: Lemma: Filter P s = Filter P (Cut P s) *) 

238 

239 
apply (simp (no_asm) add: filter_act_def) 

240 
apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) y) = Cut (%a. a:ext A) (Map fst$y) ") 

241 

242 
apply (rule_tac [2] MapCut [unfolded o_def]) 

243 
apply (simp add: FilterCut [symmetric]) 

244 

245 
(* Subgoal 3: Lemma: Cut idempotent *) 

246 

247 
apply (simp (no_asm) add: LastActExtsch_def filter_act_def) 

248 
apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) y) = Cut (%a. a:ext A) (Map fst$y) ") 

249 
apply (rule_tac [2] MapCut [unfolded o_def]) 

250 
apply (simp add: Cut_idemp) 

251 
done 

252 

253 

254 
subsection "Further Cut lemmas" 

255 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

256 
lemma LastActExtimplnil: 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

257 
"[ LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil ] 
19741  258 
==> sch=nil" 
259 
apply (unfold LastActExtsch_def) 

260 
apply (drule FilternPnilForallP) 

261 
apply (erule conjE) 

262 
apply (drule Cut_nil) 

263 
apply assumption 

264 
apply simp 

265 
done 

266 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

267 
lemma LastActExtimplUU: 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset

268 
"[ LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU ] 
19741  269 
==> sch=UU" 
270 
apply (unfold LastActExtsch_def) 

271 
apply (drule FilternPUUForallP) 

272 
apply (erule conjE) 

273 
apply (drule Cut_UU) 

274 
apply assumption 

275 
apply simp 

276 
done 

17256  277 

3071  278 
end 