author | wenzelm |
Mon, 11 Jan 2016 00:04:23 +0100 | |
changeset 62116 | bc178c0fe1a1 |
parent 62008 | cbedaddc9351 |
child 62156 | 7355fd313cf8 |
permissions | -rw-r--r-- |
62008 | 1 |
(* Title: HOL/HOLCF/IOA/ShortExecutions.thy |
40945 | 2 |
Author: Olaf Müller |
17256 | 3 |
*) |
3071 | 4 |
|
17256 | 5 |
theory ShortExecutions |
6 |
imports Traces |
|
7 |
begin |
|
3071 | 8 |
|
62002 | 9 |
text \<open> |
10 |
Some properties about \<open>Cut ex\<close>, defined as follows: |
|
3071 | 11 |
|
62002 | 12 |
For every execution ex there is another shorter execution \<open>Cut ex\<close> |
17256 | 13 |
that has the same trace as ex, but its schedule ends with an external action. |
62002 | 14 |
\<close> |
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 |
62000 | 23 |
| Def y => (Takewhile (%x. \<not>P x)$s) |
62001 | 24 |
@@ (y\<leadsto>(h$(TL$(Dropwhile (%x. \<not> 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 |
||
62002 | 50 |
ML \<open> |
60754 | 51 |
fun thin_tac' ctxt j = |
19741 | 52 |
rotate_tac (j - 1) THEN' |
60754 | 53 |
eresolve_tac ctxt [thin_rl] THEN' |
19741 | 54 |
rotate_tac (~ (j - 1)) |
62002 | 55 |
\<close> |
19741 | 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 |
|
62000 | 67 |
| Def y => (Takewhile (%a. \<not> P a)$s) |
62001 | 68 |
@@ (y\<leadsto>(oraclebuild P$(TL$(Dropwhile (%a. \<not> P a)$s))$xs)) |
19741 | 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 |
||
62001 | 88 |
lemma oraclebuild_cons: "oraclebuild P$s$(x\<leadsto>t) = |
62000 | 89 |
(Takewhile (%a. \<not> P a)$s) |
62001 | 90 |
@@ (x\<leadsto>(oraclebuild P$(TL$(Dropwhile (%a. \<not> P a)$s))$t))" |
19741 | 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: |
62000 | 101 |
"[| Forall (%a. \<not> 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: |
62000 | 111 |
"[| Forall (%a. \<not> 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: |
62000 | 121 |
"[| P t; Forall (%x. \<not> P x) ss; Finite ss|] |
62001 | 122 |
==> Cut P (ss @@ (t\<leadsto> rs)) |
123 |
= ss @@ (t \<leadsto> Cut P rs)" |
|
19741 | 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)" |
|
62000 | 132 |
apply (rule_tac A1 = "%x. True" and Q1 = "%x. \<not> P x" and x1 = "s" in take_lemma_induct [THEN mp]) |
19741 | 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)" |
|
62000 | 143 |
apply (rule_tac A1 = "%x. True" and Q1 = "%x. \<not> P x" and x1 = "s" in |
19741 | 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 |
||
62116 | 156 |
lemma MapCut: "Map f$(Cut (P \<circ> f) s) = Cut P (Map f$s)" |
62000 | 157 |
apply (rule_tac A1 = "%x. True" and Q1 = "%x. \<not> P (f x) " and x1 = "s" in |
19741 | 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) |
|
60754 | 183 |
apply (tactic "thin_tac' @{context} 1 1") |
19741 | 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 |
||
62005 | 224 |
apply (unfold schedules_def has_schedule_def [abs_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) |
|
62002 | 228 |
apply (tactic \<open>pair_tac @{context} "ex" 1\<close>) |
26359 | 229 |
apply auto |
61032
b57df8eecad6
standardized some occurences of ancient "split" alias
haftmann
parents:
60754
diff
changeset
|
230 |
apply (rule_tac x = " (x1,Cut (%a. fst a:ext A) x2) " in exI) |
19741 | 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) |
|
61032
b57df8eecad6
standardized some occurences of ancient "split" alias
haftmann
parents:
60754
diff
changeset
|
240 |
apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) x2) = Cut (%a. a:ext A) (Map fst$x2) ") |
19741 | 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) |
|
61032
b57df8eecad6
standardized some occurences of ancient "split" alias
haftmann
parents:
60754
diff
changeset
|
248 |
apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) x2) = Cut (%a. a:ext A) (Map fst$x2) ") |
19741 | 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 |