author | paulson |
Wed, 24 Dec 1997 10:02:30 +0100 | |
changeset 4477 | b3e5857d8d99 |
parent 4283 | 92707e24b62b |
child 5068 | fb28eaa07e01 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy |
3275 | 2 |
ID: $Id$ |
3071 | 3 |
Author: Olaf M"uller |
4 |
Copyright 1997 TU Muenchen |
|
5 |
||
3275 | 6 |
Some properties about (Cut ex), defined as follows: |
3071 | 7 |
|
3275 | 8 |
For every execution ex there is another shorter execution (Cut ex) |
3071 | 9 |
that has the same trace as ex, but its schedule ends with an external action. |
10 |
||
3275 | 11 |
*) |
12 |
||
13 |
||
3361 | 14 |
fun thin_tac' j = |
15 |
rotate_tac (j - 1) THEN' |
|
16 |
etac thin_rl THEN' |
|
17 |
rotate_tac (~ (j - 1)); |
|
18 |
||
3275 | 19 |
|
20 |
||
21 |
(* ---------------------------------------------------------------- *) |
|
22 |
section "oraclebuild rewrite rules"; |
|
23 |
(* ---------------------------------------------------------------- *) |
|
24 |
||
25 |
||
26 |
bind_thm ("oraclebuild_unfold", fix_prover2 thy oraclebuild_def |
|
27 |
"oraclebuild P = (LAM s t. case t of \ |
|
28 |
\ nil => nil\ |
|
29 |
\ | x##xs => \ |
|
30 |
\ (case x of\ |
|
31 |
\ Undef => UU\ |
|
32 |
\ | Def y => (Takewhile (%a.~ P a)`s)\ |
|
33 |
\ @@ (y>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`xs))\ |
|
34 |
\ )\ |
|
35 |
\ )"); |
|
36 |
||
37 |
goal thy "oraclebuild P`sch`UU = UU"; |
|
38 |
by (stac oraclebuild_unfold 1); |
|
39 |
by (Simp_tac 1); |
|
40 |
qed"oraclebuild_UU"; |
|
41 |
||
42 |
goal thy "oraclebuild P`sch`nil = nil"; |
|
43 |
by (stac oraclebuild_unfold 1); |
|
44 |
by (Simp_tac 1); |
|
45 |
qed"oraclebuild_nil"; |
|
46 |
||
47 |
goal thy "oraclebuild P`s`(x>>t) = \ |
|
48 |
\ (Takewhile (%a.~ P a)`s) \ |
|
49 |
\ @@ (x>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`t))"; |
|
3457 | 50 |
by (rtac trans 1); |
3275 | 51 |
by (stac oraclebuild_unfold 1); |
4098 | 52 |
by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1); |
53 |
by (simp_tac (simpset() addsimps [Cons_def]) 1); |
|
3275 | 54 |
qed"oraclebuild_cons"; |
55 |
||
56 |
||
57 |
||
58 |
||
59 |
(* ---------------------------------------------------------------- *) |
|
60 |
section "Cut rewrite rules"; |
|
61 |
(* ---------------------------------------------------------------- *) |
|
62 |
||
63 |
goalw thy [Cut_def] |
|
64 |
"!! s. [| Forall (%a.~ P a) s; Finite s|] \ |
|
65 |
\ ==> Cut P s =nil"; |
|
66 |
by (subgoal_tac "Filter P`s = nil" 1); |
|
4098 | 67 |
by (asm_simp_tac (simpset() addsimps [oraclebuild_nil]) 1); |
3457 | 68 |
by (rtac ForallQFilterPnil 1); |
3275 | 69 |
by (REPEAT (atac 1)); |
70 |
qed"Cut_nil"; |
|
71 |
||
72 |
goalw thy [Cut_def] |
|
73 |
"!! s. [| Forall (%a.~ P a) s; ~Finite s|] \ |
|
74 |
\ ==> Cut P s =UU"; |
|
75 |
by (subgoal_tac "Filter P`s= UU" 1); |
|
4098 | 76 |
by (asm_simp_tac (simpset() addsimps [oraclebuild_UU]) 1); |
3457 | 77 |
by (rtac ForallQFilterPUU 1); |
3275 | 78 |
by (REPEAT (atac 1)); |
79 |
qed"Cut_UU"; |
|
80 |
||
81 |
goalw thy [Cut_def] |
|
82 |
"!! s. [| P t; Forall (%x.~ P x) ss; Finite ss|] \ |
|
83 |
\ ==> Cut P (ss @@ (t>> rs)) \ |
|
84 |
\ = ss @@ (t >> Cut P rs)"; |
|
85 |
||
4098 | 86 |
by (asm_full_simp_tac (simpset() addsimps [ForallQFilterPnil,oraclebuild_cons, |
3275 | 87 |
TakewhileConc,DropwhileConc]) 1); |
88 |
qed"Cut_Cons"; |
|
89 |
||
90 |
||
91 |
(* ---------------------------------------------------------------- *) |
|
92 |
section "Cut lemmas for main theorem"; |
|
93 |
(* ---------------------------------------------------------------- *) |
|
94 |
||
95 |
||
96 |
goal thy "Filter P`s = Filter P`(Cut P s)"; |
|
97 |
||
3847 | 98 |
by (res_inst_tac [("A1","%x. True") |
3275 | 99 |
,("Q1","%x.~ P x"), ("x1","s")] |
100 |
(take_lemma_induct RS mp) 1); |
|
101 |
by (Fast_tac 3); |
|
102 |
by (case_tac "Finite s" 1); |
|
4098 | 103 |
by (asm_full_simp_tac (simpset() addsimps [Cut_nil, |
3275 | 104 |
ForallQFilterPnil]) 1); |
4098 | 105 |
by (asm_full_simp_tac (simpset() addsimps [Cut_UU, |
3275 | 106 |
ForallQFilterPUU]) 1); |
107 |
(* main case *) |
|
4098 | 108 |
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,ForallQFilterPnil]) 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4283
diff
changeset
|
109 |
by Auto_tac; |
3275 | 110 |
qed"FilterCut"; |
111 |
||
112 |
||
113 |
goal thy "Cut P (Cut P s) = (Cut P s)"; |
|
114 |
||
3847 | 115 |
by (res_inst_tac [("A1","%x. True") |
3275 | 116 |
,("Q1","%x.~ P x"), ("x1","s")] |
117 |
(take_lemma_less_induct RS mp) 1); |
|
118 |
by (Fast_tac 3); |
|
119 |
by (case_tac "Finite s" 1); |
|
4098 | 120 |
by (asm_full_simp_tac (simpset() addsimps [Cut_nil, |
3275 | 121 |
ForallQFilterPnil]) 1); |
4098 | 122 |
by (asm_full_simp_tac (simpset() addsimps [Cut_UU, |
3275 | 123 |
ForallQFilterPUU]) 1); |
124 |
(* main case *) |
|
4098 | 125 |
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,ForallQFilterPnil]) 1); |
3457 | 126 |
by (rtac take_reduction 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4283
diff
changeset
|
127 |
by Auto_tac; |
3275 | 128 |
qed"Cut_idemp"; |
129 |
||
130 |
||
131 |
goal thy "Map f`(Cut (P o f) s) = Cut P (Map f`s)"; |
|
132 |
||
3847 | 133 |
by (res_inst_tac [("A1","%x. True") |
3275 | 134 |
,("Q1","%x.~ P (f x)"), ("x1","s")] |
135 |
(take_lemma_less_induct RS mp) 1); |
|
136 |
by (Fast_tac 3); |
|
137 |
by (case_tac "Finite s" 1); |
|
4098 | 138 |
by (asm_full_simp_tac (simpset() addsimps [Cut_nil]) 1); |
3457 | 139 |
by (rtac (Cut_nil RS sym) 1); |
4098 | 140 |
by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1); |
141 |
by (asm_full_simp_tac (simpset() addsimps [Map2Finite]) 1); |
|
3275 | 142 |
(* csae ~ Finite s *) |
4098 | 143 |
by (asm_full_simp_tac (simpset() addsimps [Cut_UU]) 1); |
3457 | 144 |
by (rtac (Cut_UU RS sym) 1); |
4098 | 145 |
by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1); |
146 |
by (asm_full_simp_tac (simpset() addsimps [Map2Finite]) 1); |
|
3275 | 147 |
(* main case *) |
4098 | 148 |
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,MapConc, |
3275 | 149 |
ForallMap,FiniteMap1,o_def]) 1); |
3457 | 150 |
by (rtac take_reduction 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4283
diff
changeset
|
151 |
by Auto_tac; |
3275 | 152 |
qed"MapCut"; |
153 |
||
154 |
||
3361 | 155 |
goal thy "~Finite s --> Cut P s << s"; |
156 |
by (strip_tac 1); |
|
3457 | 157 |
by (rtac (take_lemma_less RS iffD1) 1); |
3361 | 158 |
by (strip_tac 1); |
3457 | 159 |
by (rtac mp 1); |
160 |
by (assume_tac 2); |
|
3361 | 161 |
by (thin_tac' 1 1); |
162 |
by (res_inst_tac [("x","s")] spec 1); |
|
3457 | 163 |
by (rtac less_induct 1); |
3361 | 164 |
by (strip_tac 1); |
165 |
ren "na n s" 1; |
|
166 |
by (case_tac "Forall (%x. ~ P x) s" 1); |
|
3457 | 167 |
by (rtac (take_lemma_less RS iffD2 RS spec) 1); |
4098 | 168 |
by (asm_full_simp_tac (simpset() addsimps [Cut_UU]) 1); |
3361 | 169 |
(* main case *) |
3457 | 170 |
by (dtac divide_Seq3 1); |
3361 | 171 |
by (REPEAT (etac exE 1)); |
172 |
by (REPEAT (etac conjE 1)); |
|
173 |
by (hyp_subst_tac 1); |
|
4098 | 174 |
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons]) 1); |
3457 | 175 |
by (rtac take_reduction_less 1); |
3361 | 176 |
(* auto makes also reasoning about Finiteness of parts of s ! *) |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4283
diff
changeset
|
177 |
by Auto_tac; |
3361 | 178 |
qed_spec_mp"Cut_prefixcl_nFinite"; |
179 |
||
180 |
||
181 |
||
182 |
(* |
|
183 |
||
184 |
goal thy "Finite s --> (? y. s = Cut P s @@ y)"; |
|
185 |
by (strip_tac 1); |
|
186 |
by (rtac exI 1); |
|
4042 | 187 |
by (resolve_tac seq.take_lemmas 1); |
3457 | 188 |
by (rtac mp 1); |
189 |
by (assume_tac 2); |
|
3361 | 190 |
by (thin_tac' 1 1); |
191 |
by (res_inst_tac [("x","s")] spec 1); |
|
3457 | 192 |
by (rtac less_induct 1); |
3361 | 193 |
by (strip_tac 1); |
194 |
ren "na n s" 1; |
|
195 |
by (case_tac "Forall (%x. ~ P x) s" 1); |
|
3457 | 196 |
by (rtac (seq_take_lemma RS iffD2 RS spec) 1); |
4098 | 197 |
by (asm_full_simp_tac (simpset() addsimps [Cut_nil]) 1); |
3361 | 198 |
(* main case *) |
3457 | 199 |
by (dtac divide_Seq3 1); |
3361 | 200 |
by (REPEAT (etac exE 1)); |
201 |
by (REPEAT (etac conjE 1)); |
|
202 |
by (hyp_subst_tac 1); |
|
4098 | 203 |
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,Conc_assoc]) 1); |
3457 | 204 |
by (rtac take_reduction 1); |
3361 | 205 |
|
206 |
qed_spec_mp"Cut_prefixcl_Finite"; |
|
207 |
||
208 |
*) |
|
209 |
||
210 |
||
211 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
212 |
goal thy "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)"; |
3361 | 213 |
by (case_tac "Finite ex" 1); |
214 |
by (cut_inst_tac [("s","ex"),("P","P")] Cut_prefixcl_Finite 1); |
|
3457 | 215 |
by (assume_tac 1); |
216 |
by (etac exE 1); |
|
217 |
by (rtac exec_prefix2closed 1); |
|
3361 | 218 |
by (eres_inst_tac [("s","ex"),("t","Cut P ex @@ y")] subst 1); |
3457 | 219 |
by (assume_tac 1); |
220 |
by (etac exec_prefixclosed 1); |
|
221 |
by (etac Cut_prefixcl_nFinite 1); |
|
3361 | 222 |
qed"execThruCut"; |
223 |
||
3275 | 224 |
|
225 |
||
226 |
(* ---------------------------------------------------------------- *) |
|
227 |
section "Main Cut Theorem"; |
|
228 |
(* ---------------------------------------------------------------- *) |
|
229 |
||
230 |
||
231 |
||
232 |
goalw thy [schedules_def,has_schedule_def] |
|
3847 | 233 |
"!! sch. [|sch : schedules A ; tr = Filter (%a. a:ext A)`sch|] \ |
3275 | 234 |
\ ==> ? sch. sch : schedules A & \ |
3847 | 235 |
\ tr = Filter (%a. a:ext A)`sch &\ |
3275 | 236 |
\ LastActExtsch A sch"; |
237 |
||
238 |
by (safe_tac set_cs); |
|
3847 | 239 |
by (res_inst_tac [("x","filter_act`(Cut (%a. fst a:ext A) (snd ex))")] exI 1); |
4098 | 240 |
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); |
3275 | 241 |
by (pair_tac "ex" 1); |
242 |
by (safe_tac set_cs); |
|
3847 | 243 |
by (res_inst_tac [("x","(x,Cut (%a. fst a:ext A) y)")] exI 1); |
3275 | 244 |
by (Asm_simp_tac 1); |
245 |
||
246 |
(* Subgoal 1: Lemma: propagation of execution through Cut *) |
|
247 |
||
4098 | 248 |
by (asm_full_simp_tac (simpset() addsimps [execThruCut]) 1); |
3275 | 249 |
|
250 |
(* Subgoal 2: Lemma: Filter P s = Filter P (Cut P s) *) |
|
251 |
||
4098 | 252 |
by (simp_tac (simpset() addsimps [filter_act_def]) 1); |
3847 | 253 |
by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1); |
4283 | 254 |
|
3457 | 255 |
by (rtac (rewrite_rule [o_def] MapCut) 2); |
4098 | 256 |
by (asm_full_simp_tac (simpset() addsimps [FilterCut RS sym]) 1); |
3275 | 257 |
|
258 |
(* Subgoal 3: Lemma: Cut idempotent *) |
|
259 |
||
4098 | 260 |
by (simp_tac (simpset() addsimps [LastActExtsch_def,filter_act_def]) 1); |
3847 | 261 |
by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1); |
3457 | 262 |
by (rtac (rewrite_rule [o_def] MapCut) 2); |
4098 | 263 |
by (asm_full_simp_tac (simpset() addsimps [Cut_idemp]) 1); |
3275 | 264 |
qed"exists_LastActExtsch"; |
265 |
||
266 |
||
267 |
(* ---------------------------------------------------------------- *) |
|
268 |
section "Further Cut lemmas"; |
|
269 |
(* ---------------------------------------------------------------- *) |
|
270 |
||
271 |
goalw thy [LastActExtsch_def] |
|
3847 | 272 |
"!! A. [| LastActExtsch A sch; Filter (%x. x:ext A)`sch = nil |] \ |
3275 | 273 |
\ ==> sch=nil"; |
3457 | 274 |
by (dtac FilternPnilForallP 1); |
275 |
by (etac conjE 1); |
|
276 |
by (dtac Cut_nil 1); |
|
277 |
by (assume_tac 1); |
|
3275 | 278 |
by (Asm_full_simp_tac 1); |
279 |
qed"LastActExtimplnil"; |
|
280 |
||
281 |
goalw thy [LastActExtsch_def] |
|
3847 | 282 |
"!! A. [| LastActExtsch A sch; Filter (%x. x:ext A)`sch = UU |] \ |
3275 | 283 |
\ ==> sch=UU"; |
3457 | 284 |
by (dtac FilternPUUForallP 1); |
285 |
by (etac conjE 1); |
|
286 |
by (dtac Cut_UU 1); |
|
287 |
by (assume_tac 1); |
|
3275 | 288 |
by (Asm_full_simp_tac 1); |
289 |
qed"LastActExtimplUU"; |