author | nipkow |
Tue, 09 Jan 2001 15:36:30 +0100 | |
changeset 10835 | f4745d77e620 |
parent 9877 | b2a62260f8ac |
child 12028 | 52aa183c15bb |
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\ |
|
10835 | 32 |
\ | Def y => (Takewhile (%a.~ P a)$s)\ |
33 |
\ @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs))\ |
|
3275 | 34 |
\ )\ |
35 |
\ )"); |
|
36 |
||
10835 | 37 |
Goal "oraclebuild P$sch$UU = UU"; |
3275 | 38 |
by (stac oraclebuild_unfold 1); |
39 |
by (Simp_tac 1); |
|
40 |
qed"oraclebuild_UU"; |
|
41 |
||
10835 | 42 |
Goal "oraclebuild P$sch$nil = nil"; |
3275 | 43 |
by (stac oraclebuild_unfold 1); |
44 |
by (Simp_tac 1); |
|
45 |
qed"oraclebuild_nil"; |
|
46 |
||
10835 | 47 |
Goal "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); |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
52 |
by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1); |
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
53 |
by (simp_tac (simpset() addsimps [Consq_def]) 1); |
3275 | 54 |
qed"oraclebuild_cons"; |
55 |
||
56 |
||
57 |
||
58 |
||
59 |
(* ---------------------------------------------------------------- *) |
|
60 |
section "Cut rewrite rules"; |
|
61 |
(* ---------------------------------------------------------------- *) |
|
62 |
||
5068 | 63 |
Goalw [Cut_def] |
6161 | 64 |
"[| Forall (%a.~ P a) s; Finite s|] \ |
3275 | 65 |
\ ==> Cut P s =nil"; |
10835 | 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 |
||
5068 | 72 |
Goalw [Cut_def] |
6161 | 73 |
"[| Forall (%a.~ P a) s; ~Finite s|] \ |
3275 | 74 |
\ ==> Cut P s =UU"; |
10835 | 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 |
||
5068 | 81 |
Goalw [Cut_def] |
6161 | 82 |
"[| P t; Forall (%x.~ P x) ss; Finite ss|] \ |
3275 | 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 |
||
10835 | 96 |
Goal "Filter P$s = Filter P$(Cut P s)"; |
3275 | 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 |
||
5068 | 113 |
Goal "Cut P (Cut P s) = (Cut P s)"; |
3275 | 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 |
||
10835 | 131 |
Goal "Map f$(Cut (P o f) s) = Cut P (Map f$s)"; |
3275 | 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 |
||
5068 | 155 |
Goal "~Finite s --> Cut P s << s"; |
3361 | 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); |
|
9877 | 163 |
by (rtac nat_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 |
||
5068 | 182 |
Goal "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)"; |
3361 | 183 |
by (case_tac "Finite ex" 1); |
184 |
by (cut_inst_tac [("s","ex"),("P","P")] Cut_prefixcl_Finite 1); |
|
3457 | 185 |
by (assume_tac 1); |
186 |
by (etac exE 1); |
|
187 |
by (rtac exec_prefix2closed 1); |
|
3361 | 188 |
by (eres_inst_tac [("s","ex"),("t","Cut P ex @@ y")] subst 1); |
3457 | 189 |
by (assume_tac 1); |
190 |
by (etac exec_prefixclosed 1); |
|
191 |
by (etac Cut_prefixcl_nFinite 1); |
|
3361 | 192 |
qed"execThruCut"; |
193 |
||
3275 | 194 |
|
195 |
||
196 |
(* ---------------------------------------------------------------- *) |
|
197 |
section "Main Cut Theorem"; |
|
198 |
(* ---------------------------------------------------------------- *) |
|
199 |
||
200 |
||
201 |
||
5068 | 202 |
Goalw [schedules_def,has_schedule_def] |
10835 | 203 |
"[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|] \ |
3275 | 204 |
\ ==> ? sch. sch : schedules A & \ |
10835 | 205 |
\ tr = Filter (%a. a:ext A)$sch &\ |
3275 | 206 |
\ LastActExtsch A sch"; |
207 |
||
208 |
by (safe_tac set_cs); |
|
10835 | 209 |
by (res_inst_tac [("x","filter_act$(Cut (%a. fst a:ext A) (snd ex))")] exI 1); |
4098 | 210 |
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); |
3275 | 211 |
by (pair_tac "ex" 1); |
212 |
by (safe_tac set_cs); |
|
3847 | 213 |
by (res_inst_tac [("x","(x,Cut (%a. fst a:ext A) y)")] exI 1); |
3275 | 214 |
by (Asm_simp_tac 1); |
215 |
||
216 |
(* Subgoal 1: Lemma: propagation of execution through Cut *) |
|
217 |
||
4098 | 218 |
by (asm_full_simp_tac (simpset() addsimps [execThruCut]) 1); |
3275 | 219 |
|
220 |
(* Subgoal 2: Lemma: Filter P s = Filter P (Cut P s) *) |
|
221 |
||
4098 | 222 |
by (simp_tac (simpset() addsimps [filter_act_def]) 1); |
10835 | 223 |
by (subgoal_tac "Map fst$(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst$y)" 1); |
4283 | 224 |
|
3457 | 225 |
by (rtac (rewrite_rule [o_def] MapCut) 2); |
4098 | 226 |
by (asm_full_simp_tac (simpset() addsimps [FilterCut RS sym]) 1); |
3275 | 227 |
|
228 |
(* Subgoal 3: Lemma: Cut idempotent *) |
|
229 |
||
4098 | 230 |
by (simp_tac (simpset() addsimps [LastActExtsch_def,filter_act_def]) 1); |
10835 | 231 |
by (subgoal_tac "Map fst$(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst$y)" 1); |
3457 | 232 |
by (rtac (rewrite_rule [o_def] MapCut) 2); |
4098 | 233 |
by (asm_full_simp_tac (simpset() addsimps [Cut_idemp]) 1); |
3275 | 234 |
qed"exists_LastActExtsch"; |
235 |
||
236 |
||
237 |
(* ---------------------------------------------------------------- *) |
|
238 |
section "Further Cut lemmas"; |
|
239 |
(* ---------------------------------------------------------------- *) |
|
240 |
||
5068 | 241 |
Goalw [LastActExtsch_def] |
10835 | 242 |
"[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |] \ |
3275 | 243 |
\ ==> sch=nil"; |
3457 | 244 |
by (dtac FilternPnilForallP 1); |
245 |
by (etac conjE 1); |
|
246 |
by (dtac Cut_nil 1); |
|
247 |
by (assume_tac 1); |
|
3275 | 248 |
by (Asm_full_simp_tac 1); |
249 |
qed"LastActExtimplnil"; |
|
250 |
||
5068 | 251 |
Goalw [LastActExtsch_def] |
10835 | 252 |
"[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |] \ |
3275 | 253 |
\ ==> sch=UU"; |
3457 | 254 |
by (dtac FilternPUUForallP 1); |
255 |
by (etac conjE 1); |
|
256 |
by (dtac Cut_UU 1); |
|
257 |
by (assume_tac 1); |
|
3275 | 258 |
by (Asm_full_simp_tac 1); |
259 |
qed"LastActExtimplUU"; |