author | wenzelm |
Thu, 15 Nov 2001 23:25:46 +0100 | |
changeset 12218 | 6597093b77e7 |
parent 12028 | 52aa183c15bb |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy |
3275 | 2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
3071 | 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. |
3275 | 10 |
*) |
11 |
||
12 |
||
3361 | 13 |
fun thin_tac' j = |
14 |
rotate_tac (j - 1) THEN' |
|
15 |
etac thin_rl THEN' |
|
16 |
rotate_tac (~ (j - 1)); |
|
17 |
||
3275 | 18 |
|
19 |
||
20 |
(* ---------------------------------------------------------------- *) |
|
21 |
section "oraclebuild rewrite rules"; |
|
22 |
(* ---------------------------------------------------------------- *) |
|
23 |
||
24 |
||
25 |
bind_thm ("oraclebuild_unfold", fix_prover2 thy oraclebuild_def |
|
26 |
"oraclebuild P = (LAM s t. case t of \ |
|
27 |
\ nil => nil\ |
|
28 |
\ | x##xs => \ |
|
29 |
\ (case x of\ |
|
12028 | 30 |
\ UU => UU\ |
10835 | 31 |
\ | Def y => (Takewhile (%a.~ P a)$s)\ |
32 |
\ @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs))\ |
|
3275 | 33 |
\ )\ |
34 |
\ )"); |
|
35 |
||
10835 | 36 |
Goal "oraclebuild P$sch$UU = UU"; |
3275 | 37 |
by (stac oraclebuild_unfold 1); |
38 |
by (Simp_tac 1); |
|
39 |
qed"oraclebuild_UU"; |
|
40 |
||
10835 | 41 |
Goal "oraclebuild P$sch$nil = nil"; |
3275 | 42 |
by (stac oraclebuild_unfold 1); |
43 |
by (Simp_tac 1); |
|
44 |
qed"oraclebuild_nil"; |
|
45 |
||
10835 | 46 |
Goal "oraclebuild P$s$(x>>t) = \ |
47 |
\ (Takewhile (%a.~ P a)$s) \ |
|
48 |
\ @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))"; |
|
3457 | 49 |
by (rtac trans 1); |
3275 | 50 |
by (stac oraclebuild_unfold 1); |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
51 |
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
|
52 |
by (simp_tac (simpset() addsimps [Consq_def]) 1); |
3275 | 53 |
qed"oraclebuild_cons"; |
54 |
||
55 |
||
56 |
||
57 |
||
58 |
(* ---------------------------------------------------------------- *) |
|
59 |
section "Cut rewrite rules"; |
|
60 |
(* ---------------------------------------------------------------- *) |
|
61 |
||
5068 | 62 |
Goalw [Cut_def] |
6161 | 63 |
"[| Forall (%a.~ P a) s; Finite s|] \ |
3275 | 64 |
\ ==> Cut P s =nil"; |
10835 | 65 |
by (subgoal_tac "Filter P$s = nil" 1); |
4098 | 66 |
by (asm_simp_tac (simpset() addsimps [oraclebuild_nil]) 1); |
3457 | 67 |
by (rtac ForallQFilterPnil 1); |
3275 | 68 |
by (REPEAT (atac 1)); |
69 |
qed"Cut_nil"; |
|
70 |
||
5068 | 71 |
Goalw [Cut_def] |
6161 | 72 |
"[| Forall (%a.~ P a) s; ~Finite s|] \ |
3275 | 73 |
\ ==> Cut P s =UU"; |
10835 | 74 |
by (subgoal_tac "Filter P$s= UU" 1); |
4098 | 75 |
by (asm_simp_tac (simpset() addsimps [oraclebuild_UU]) 1); |
3457 | 76 |
by (rtac ForallQFilterPUU 1); |
3275 | 77 |
by (REPEAT (atac 1)); |
78 |
qed"Cut_UU"; |
|
79 |
||
5068 | 80 |
Goalw [Cut_def] |
6161 | 81 |
"[| P t; Forall (%x.~ P x) ss; Finite ss|] \ |
3275 | 82 |
\ ==> Cut P (ss @@ (t>> rs)) \ |
83 |
\ = ss @@ (t >> Cut P rs)"; |
|
84 |
||
4098 | 85 |
by (asm_full_simp_tac (simpset() addsimps [ForallQFilterPnil,oraclebuild_cons, |
3275 | 86 |
TakewhileConc,DropwhileConc]) 1); |
87 |
qed"Cut_Cons"; |
|
88 |
||
89 |
||
90 |
(* ---------------------------------------------------------------- *) |
|
91 |
section "Cut lemmas for main theorem"; |
|
92 |
(* ---------------------------------------------------------------- *) |
|
93 |
||
94 |
||
10835 | 95 |
Goal "Filter P$s = Filter P$(Cut P s)"; |
3275 | 96 |
|
3847 | 97 |
by (res_inst_tac [("A1","%x. True") |
3275 | 98 |
,("Q1","%x.~ P x"), ("x1","s")] |
99 |
(take_lemma_induct RS mp) 1); |
|
100 |
by (Fast_tac 3); |
|
101 |
by (case_tac "Finite s" 1); |
|
4098 | 102 |
by (asm_full_simp_tac (simpset() addsimps [Cut_nil, |
3275 | 103 |
ForallQFilterPnil]) 1); |
4098 | 104 |
by (asm_full_simp_tac (simpset() addsimps [Cut_UU, |
3275 | 105 |
ForallQFilterPUU]) 1); |
106 |
(* main case *) |
|
4098 | 107 |
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
|
108 |
by Auto_tac; |
3275 | 109 |
qed"FilterCut"; |
110 |
||
111 |
||
5068 | 112 |
Goal "Cut P (Cut P s) = (Cut P s)"; |
3275 | 113 |
|
3847 | 114 |
by (res_inst_tac [("A1","%x. True") |
3275 | 115 |
,("Q1","%x.~ P x"), ("x1","s")] |
116 |
(take_lemma_less_induct RS mp) 1); |
|
117 |
by (Fast_tac 3); |
|
118 |
by (case_tac "Finite s" 1); |
|
4098 | 119 |
by (asm_full_simp_tac (simpset() addsimps [Cut_nil, |
3275 | 120 |
ForallQFilterPnil]) 1); |
4098 | 121 |
by (asm_full_simp_tac (simpset() addsimps [Cut_UU, |
3275 | 122 |
ForallQFilterPUU]) 1); |
123 |
(* main case *) |
|
4098 | 124 |
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,ForallQFilterPnil]) 1); |
3457 | 125 |
by (rtac take_reduction 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4283
diff
changeset
|
126 |
by Auto_tac; |
3275 | 127 |
qed"Cut_idemp"; |
128 |
||
129 |
||
10835 | 130 |
Goal "Map f$(Cut (P o f) s) = Cut P (Map f$s)"; |
3275 | 131 |
|
3847 | 132 |
by (res_inst_tac [("A1","%x. True") |
3275 | 133 |
,("Q1","%x.~ P (f x)"), ("x1","s")] |
134 |
(take_lemma_less_induct RS mp) 1); |
|
135 |
by (Fast_tac 3); |
|
136 |
by (case_tac "Finite s" 1); |
|
4098 | 137 |
by (asm_full_simp_tac (simpset() addsimps [Cut_nil]) 1); |
3457 | 138 |
by (rtac (Cut_nil RS sym) 1); |
4098 | 139 |
by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1); |
140 |
by (asm_full_simp_tac (simpset() addsimps [Map2Finite]) 1); |
|
3275 | 141 |
(* csae ~ Finite s *) |
4098 | 142 |
by (asm_full_simp_tac (simpset() addsimps [Cut_UU]) 1); |
3457 | 143 |
by (rtac (Cut_UU RS sym) 1); |
4098 | 144 |
by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1); |
145 |
by (asm_full_simp_tac (simpset() addsimps [Map2Finite]) 1); |
|
3275 | 146 |
(* main case *) |
4098 | 147 |
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,MapConc, |
3275 | 148 |
ForallMap,FiniteMap1,o_def]) 1); |
3457 | 149 |
by (rtac take_reduction 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4283
diff
changeset
|
150 |
by Auto_tac; |
3275 | 151 |
qed"MapCut"; |
152 |
||
153 |
||
5068 | 154 |
Goal "~Finite s --> Cut P s << s"; |
3361 | 155 |
by (strip_tac 1); |
3457 | 156 |
by (rtac (take_lemma_less RS iffD1) 1); |
3361 | 157 |
by (strip_tac 1); |
3457 | 158 |
by (rtac mp 1); |
159 |
by (assume_tac 2); |
|
3361 | 160 |
by (thin_tac' 1 1); |
161 |
by (res_inst_tac [("x","s")] spec 1); |
|
9877 | 162 |
by (rtac nat_less_induct 1); |
3361 | 163 |
by (strip_tac 1); |
164 |
ren "na n s" 1; |
|
165 |
by (case_tac "Forall (%x. ~ P x) s" 1); |
|
3457 | 166 |
by (rtac (take_lemma_less RS iffD2 RS spec) 1); |
4098 | 167 |
by (asm_full_simp_tac (simpset() addsimps [Cut_UU]) 1); |
3361 | 168 |
(* main case *) |
3457 | 169 |
by (dtac divide_Seq3 1); |
3361 | 170 |
by (REPEAT (etac exE 1)); |
171 |
by (REPEAT (etac conjE 1)); |
|
172 |
by (hyp_subst_tac 1); |
|
4098 | 173 |
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons]) 1); |
3457 | 174 |
by (rtac take_reduction_less 1); |
3361 | 175 |
(* 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
|
176 |
by Auto_tac; |
3361 | 177 |
qed_spec_mp"Cut_prefixcl_nFinite"; |
178 |
||
179 |
||
180 |
||
5068 | 181 |
Goal "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)"; |
3361 | 182 |
by (case_tac "Finite ex" 1); |
183 |
by (cut_inst_tac [("s","ex"),("P","P")] Cut_prefixcl_Finite 1); |
|
3457 | 184 |
by (assume_tac 1); |
185 |
by (etac exE 1); |
|
186 |
by (rtac exec_prefix2closed 1); |
|
3361 | 187 |
by (eres_inst_tac [("s","ex"),("t","Cut P ex @@ y")] subst 1); |
3457 | 188 |
by (assume_tac 1); |
189 |
by (etac exec_prefixclosed 1); |
|
190 |
by (etac Cut_prefixcl_nFinite 1); |
|
3361 | 191 |
qed"execThruCut"; |
192 |
||
3275 | 193 |
|
194 |
||
195 |
(* ---------------------------------------------------------------- *) |
|
196 |
section "Main Cut Theorem"; |
|
197 |
(* ---------------------------------------------------------------- *) |
|
198 |
||
199 |
||
200 |
||
5068 | 201 |
Goalw [schedules_def,has_schedule_def] |
10835 | 202 |
"[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|] \ |
3275 | 203 |
\ ==> ? sch. sch : schedules A & \ |
10835 | 204 |
\ tr = Filter (%a. a:ext A)$sch &\ |
3275 | 205 |
\ LastActExtsch A sch"; |
206 |
||
207 |
by (safe_tac set_cs); |
|
10835 | 208 |
by (res_inst_tac [("x","filter_act$(Cut (%a. fst a:ext A) (snd ex))")] exI 1); |
4098 | 209 |
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); |
3275 | 210 |
by (pair_tac "ex" 1); |
211 |
by (safe_tac set_cs); |
|
3847 | 212 |
by (res_inst_tac [("x","(x,Cut (%a. fst a:ext A) y)")] exI 1); |
3275 | 213 |
by (Asm_simp_tac 1); |
214 |
||
215 |
(* Subgoal 1: Lemma: propagation of execution through Cut *) |
|
216 |
||
4098 | 217 |
by (asm_full_simp_tac (simpset() addsimps [execThruCut]) 1); |
3275 | 218 |
|
219 |
(* Subgoal 2: Lemma: Filter P s = Filter P (Cut P s) *) |
|
220 |
||
4098 | 221 |
by (simp_tac (simpset() addsimps [filter_act_def]) 1); |
10835 | 222 |
by (subgoal_tac "Map fst$(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst$y)" 1); |
4283 | 223 |
|
3457 | 224 |
by (rtac (rewrite_rule [o_def] MapCut) 2); |
4098 | 225 |
by (asm_full_simp_tac (simpset() addsimps [FilterCut RS sym]) 1); |
3275 | 226 |
|
227 |
(* Subgoal 3: Lemma: Cut idempotent *) |
|
228 |
||
4098 | 229 |
by (simp_tac (simpset() addsimps [LastActExtsch_def,filter_act_def]) 1); |
10835 | 230 |
by (subgoal_tac "Map fst$(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst$y)" 1); |
3457 | 231 |
by (rtac (rewrite_rule [o_def] MapCut) 2); |
4098 | 232 |
by (asm_full_simp_tac (simpset() addsimps [Cut_idemp]) 1); |
3275 | 233 |
qed"exists_LastActExtsch"; |
234 |
||
235 |
||
236 |
(* ---------------------------------------------------------------- *) |
|
237 |
section "Further Cut lemmas"; |
|
238 |
(* ---------------------------------------------------------------- *) |
|
239 |
||
5068 | 240 |
Goalw [LastActExtsch_def] |
10835 | 241 |
"[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |] \ |
3275 | 242 |
\ ==> sch=nil"; |
3457 | 243 |
by (dtac FilternPnilForallP 1); |
244 |
by (etac conjE 1); |
|
245 |
by (dtac Cut_nil 1); |
|
246 |
by (assume_tac 1); |
|
3275 | 247 |
by (Asm_full_simp_tac 1); |
248 |
qed"LastActExtimplnil"; |
|
249 |
||
5068 | 250 |
Goalw [LastActExtsch_def] |
10835 | 251 |
"[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |] \ |
3275 | 252 |
\ ==> sch=UU"; |
3457 | 253 |
by (dtac FilternPUUForallP 1); |
254 |
by (etac conjE 1); |
|
255 |
by (dtac Cut_UU 1); |
|
256 |
by (assume_tac 1); |
|
3275 | 257 |
by (Asm_full_simp_tac 1); |
258 |
qed"LastActExtimplUU"; |