12 |
12 |
13 For every execution ex there is another shorter execution @{text "Cut ex"} |
13 For every execution ex there is another shorter execution @{text "Cut ex"} |
14 that has the same trace as ex, but its schedule ends with an external action. |
14 that has the same trace as ex, but its schedule ends with an external action. |
15 *} |
15 *} |
16 |
16 |
17 consts |
17 definition |
18 |
18 oraclebuild :: "('a => bool) => 'a Seq -> 'a Seq -> 'a Seq" where |
19 (* LastActExtex ::"('a,'s)ioa => ('a,'s) pairs => bool"*) |
19 "oraclebuild P = (fix$(LAM h s t. case t of |
20 LastActExtsch ::"('a,'s)ioa => 'a Seq => bool" |
|
21 |
|
22 Cut ::"('a => bool) => 'a Seq => 'a Seq" |
|
23 |
|
24 oraclebuild ::"('a => bool) => 'a Seq -> 'a Seq -> 'a Seq" |
|
25 |
|
26 defs |
|
27 |
|
28 LastActExtsch_def: |
|
29 "LastActExtsch A sch == (Cut (%x. x: ext A) sch = sch)" |
|
30 |
|
31 (* LastActExtex_def: |
|
32 "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *) |
|
33 |
|
34 Cut_def: |
|
35 "Cut P s == oraclebuild P$s$(Filter P$s)" |
|
36 |
|
37 oraclebuild_def: |
|
38 "oraclebuild P == (fix$(LAM h s t. case t of |
|
39 nil => nil |
20 nil => nil |
40 | x##xs => |
21 | x##xs => |
41 (case x of |
22 (case x of |
42 UU => UU |
23 UU => UU |
43 | Def y => (Takewhile (%x.~P x)$s) |
24 | Def y => (Takewhile (%x.~P x)$s) |
44 @@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs)) |
25 @@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs)) |
45 ) |
26 ) |
46 ))" |
27 ))" |
47 |
28 |
48 |
29 definition |
49 axioms |
30 Cut :: "('a => bool) => 'a Seq => 'a Seq" where |
50 |
31 "Cut P s = oraclebuild P$s$(Filter P$s)" |
51 Cut_prefixcl_Finite: |
32 |
52 "Finite s ==> (? y. s = Cut P s @@ y)" |
33 definition |
53 |
34 LastActExtsch :: "('a,'s)ioa => 'a Seq => bool" where |
54 LastActExtsmall1: |
35 "LastActExtsch A sch = (Cut (%x. x: ext A) sch = sch)" |
55 "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))" |
36 |
56 |
37 (* LastActExtex ::"('a,'s)ioa => ('a,'s) pairs => bool"*) |
57 LastActExtsmall2: |
38 (* LastActExtex_def: |
58 "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2" |
39 "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *) |
59 |
40 |
|
41 axiomatization where |
|
42 Cut_prefixcl_Finite: "Finite s ==> (? y. s = Cut P s @@ y)" |
|
43 |
|
44 axiomatization where |
|
45 LastActExtsmall1: "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))" |
|
46 |
|
47 axiomatization where |
|
48 LastActExtsmall2: "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2" |
60 |
49 |
61 |
50 |
62 ML {* |
51 ML {* |
63 fun thin_tac' j = |
52 fun thin_tac' j = |
64 rotate_tac (j - 1) THEN' |
53 rotate_tac (j - 1) THEN' |
69 |
58 |
70 subsection "oraclebuild rewrite rules" |
59 subsection "oraclebuild rewrite rules" |
71 |
60 |
72 |
61 |
73 lemma oraclebuild_unfold: |
62 lemma oraclebuild_unfold: |
74 "oraclebuild P = (LAM s t. case t of |
63 "oraclebuild P = (LAM s t. case t of |
75 nil => nil |
64 nil => nil |
76 | x##xs => |
65 | x##xs => |
77 (case x of |
66 (case x of |
78 UU => UU |
67 UU => UU |
79 | Def y => (Takewhile (%a.~ P a)$s) |
68 | Def y => (Takewhile (%a.~ P a)$s) |
80 @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs)) |
69 @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs)) |
81 ) |
70 ) |
82 )" |
71 )" |
83 apply (rule trans) |
72 apply (rule trans) |
84 apply (rule fix_eq2) |
73 apply (rule fix_eq2) |
85 apply (rule oraclebuild_def) |
74 apply (simp only: oraclebuild_def) |
86 apply (rule beta_cfun) |
75 apply (rule beta_cfun) |
87 apply simp |
76 apply simp |
88 done |
77 done |
89 |
78 |
90 lemma oraclebuild_UU: "oraclebuild P$sch$UU = UU" |
79 lemma oraclebuild_UU: "oraclebuild P$sch$UU = UU" |
95 lemma oraclebuild_nil: "oraclebuild P$sch$nil = nil" |
84 lemma oraclebuild_nil: "oraclebuild P$sch$nil = nil" |
96 apply (subst oraclebuild_unfold) |
85 apply (subst oraclebuild_unfold) |
97 apply simp |
86 apply simp |
98 done |
87 done |
99 |
88 |
100 lemma oraclebuild_cons: "oraclebuild P$s$(x>>t) = |
89 lemma oraclebuild_cons: "oraclebuild P$s$(x>>t) = |
101 (Takewhile (%a.~ P a)$s) |
90 (Takewhile (%a.~ P a)$s) |
102 @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))" |
91 @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))" |
103 apply (rule trans) |
92 apply (rule trans) |
104 apply (subst oraclebuild_unfold) |
93 apply (subst oraclebuild_unfold) |
105 apply (simp add: Consq_def) |
94 apply (simp add: Consq_def) |
106 apply (simp add: Consq_def) |
95 apply (simp add: Consq_def) |
107 done |
96 done |
108 |
97 |
109 |
98 |
110 subsection "Cut rewrite rules" |
99 subsection "Cut rewrite rules" |
111 |
100 |
112 lemma Cut_nil: |
101 lemma Cut_nil: |
113 "[| Forall (%a.~ P a) s; Finite s|] |
102 "[| Forall (%a.~ P a) s; Finite s|] |
114 ==> Cut P s =nil" |
103 ==> Cut P s =nil" |
115 apply (unfold Cut_def) |
104 apply (unfold Cut_def) |
116 apply (subgoal_tac "Filter P$s = nil") |
105 apply (subgoal_tac "Filter P$s = nil") |
117 apply (simp (no_asm_simp) add: oraclebuild_nil) |
106 apply (simp (no_asm_simp) add: oraclebuild_nil) |
118 apply (rule ForallQFilterPnil) |
107 apply (rule ForallQFilterPnil) |
119 apply assumption+ |
108 apply assumption+ |
120 done |
109 done |
121 |
110 |
122 lemma Cut_UU: |
111 lemma Cut_UU: |
123 "[| Forall (%a.~ P a) s; ~Finite s|] |
112 "[| Forall (%a.~ P a) s; ~Finite s|] |
124 ==> Cut P s =UU" |
113 ==> Cut P s =UU" |
125 apply (unfold Cut_def) |
114 apply (unfold Cut_def) |
126 apply (subgoal_tac "Filter P$s= UU") |
115 apply (subgoal_tac "Filter P$s= UU") |
127 apply (simp (no_asm_simp) add: oraclebuild_UU) |
116 apply (simp (no_asm_simp) add: oraclebuild_UU) |
128 apply (rule ForallQFilterPUU) |
117 apply (rule ForallQFilterPUU) |
129 apply assumption+ |
118 apply assumption+ |
130 done |
119 done |
131 |
120 |
132 lemma Cut_Cons: |
121 lemma Cut_Cons: |
133 "[| P t; Forall (%x.~ P x) ss; Finite ss|] |
122 "[| P t; Forall (%x.~ P x) ss; Finite ss|] |
134 ==> Cut P (ss @@ (t>> rs)) |
123 ==> Cut P (ss @@ (t>> rs)) |
135 = ss @@ (t >> Cut P rs)" |
124 = ss @@ (t >> Cut P rs)" |
136 apply (unfold Cut_def) |
125 apply (unfold Cut_def) |
137 apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc) |
126 apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc) |
138 done |
127 done |
139 |
128 |
225 done |
214 done |
226 |
215 |
227 |
216 |
228 subsection "Main Cut Theorem" |
217 subsection "Main Cut Theorem" |
229 |
218 |
230 lemma exists_LastActExtsch: |
219 lemma exists_LastActExtsch: |
231 "[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|] |
220 "[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|] |
232 ==> ? sch. sch : schedules A & |
221 ==> ? sch. sch : schedules A & |
233 tr = Filter (%a. a:ext A)$sch & |
222 tr = Filter (%a. a:ext A)$sch & |
234 LastActExtsch A sch" |
223 LastActExtsch A sch" |
235 |
224 |
236 apply (unfold schedules_def has_schedule_def) |
225 apply (unfold schedules_def has_schedule_def) |
237 apply (tactic "safe_tac set_cs") |
226 apply (tactic "safe_tac set_cs") |
238 apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI) |
227 apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI) |
263 done |
252 done |
264 |
253 |
265 |
254 |
266 subsection "Further Cut lemmas" |
255 subsection "Further Cut lemmas" |
267 |
256 |
268 lemma LastActExtimplnil: |
257 lemma LastActExtimplnil: |
269 "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |] |
258 "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |] |
270 ==> sch=nil" |
259 ==> sch=nil" |
271 apply (unfold LastActExtsch_def) |
260 apply (unfold LastActExtsch_def) |
272 apply (drule FilternPnilForallP) |
261 apply (drule FilternPnilForallP) |
273 apply (erule conjE) |
262 apply (erule conjE) |
274 apply (drule Cut_nil) |
263 apply (drule Cut_nil) |
275 apply assumption |
264 apply assumption |
276 apply simp |
265 apply simp |
277 done |
266 done |
278 |
267 |
279 lemma LastActExtimplUU: |
268 lemma LastActExtimplUU: |
280 "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |] |
269 "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |] |
281 ==> sch=UU" |
270 ==> sch=UU" |
282 apply (unfold LastActExtsch_def) |
271 apply (unfold LastActExtsch_def) |
283 apply (drule FilternPUUForallP) |
272 apply (drule FilternPUUForallP) |
284 apply (erule conjE) |
273 apply (erule conjE) |
285 apply (drule Cut_UU) |
274 apply (drule Cut_UU) |