1open HolKernel Parse boolLib bossLib;
2open optionTheory pairTheory pred_setTheory finite_mapTheory stringTheory;
3open integerTheory listTheory optionTheory rich_listTheory;
4open lcsymtacs BasicProvers;
5open for_ndTheory for_nd_semTheory oracleSemTheory simple_traceTheory;
6open relationTheory;
7
8val _ = new_theory "for_osmall";
9
10val _ = temp_tight_equality ();
11
12val ect = BasicProvers.EVERY_CASE_TAC;
13val fct = BasicProvers.FULL_CASE_TAC;
14
15val some_no_choice = Q.prove (
16`!f. (some x. f x) = NONE ��� ��?x. f x`,
17 rw [some_def]);
18
19val some_SAT = Q.prove(
20`!P y. (some x. P x) = SOME y ��� P y`,
21rw[some_def,SELECT_THM]>>
22metis_tac[SELECT_AX])
23
24(* A small step semantics for the non-deterministic FOR language with I/O *)
25
26(* Add AddL and AddR to model making the choice one which sub-expression to
27 * evaluate before starting the evaluation. Thus preventing switching in the
28 * middle of evaluating one of them.
29 *)
30val _ = Datatype `
31small_e =
32  | Var string
33  | Num int
34  | Add small_e small_e
35  | AddL small_e small_e
36  | AddR small_e small_e
37  | Assign string small_e
38  | Getchar
39  | Putchar small_e`;
40
41(* Add a Handle statement that will stop breaks from propagating *)
42val _ = Datatype `
43small_t =
44  | Dec string small_t
45  | Exp small_e
46  | Break
47  | Seq small_t small_t
48  | If small_e small_t small_t
49  | For small_e small_e small_t
50  | Handle small_t`;
51
52val _ = Datatype `
53  lab = ND bool | W char | R char`;
54
55val e_to_small_e_def = Define `
56(e_to_small_e ((Num i):e) = ((Num i) : small_e)) ���
57(e_to_small_e (Var x) = Var x) ���
58(e_to_small_e (Add e1 e2) = Add (e_to_small_e e1) (e_to_small_e e2)) ���
59(e_to_small_e (Assign x e) = Assign x (e_to_small_e e)) ���
60(e_to_small_e Getchar = Getchar) ���
61(e_to_small_e (Putchar e) = Putchar (e_to_small_e e))`;
62
63val t_to_small_t_def = Define `
64(t_to_small_t ((Dec string t):t) = ((Dec string (t_to_small_t t)) : small_t)) ���
65(t_to_small_t (Exp e) = Exp (e_to_small_e e)) ���
66(t_to_small_t Break = Break) ���
67(t_to_small_t (Seq t1 t2) = Seq (t_to_small_t t1) (t_to_small_t t2)) ���
68(t_to_small_t (If e t1 t2) = If (e_to_small_e e) (t_to_small_t t1) (t_to_small_t t2)) ���
69(t_to_small_t (For e1 e2 t) = For (e_to_small_e e1) (e_to_small_e e2) (t_to_small_t t))`;
70
71val is_val_e_def = Define `
72(is_val_e (Num n) = T) ���
73(is_val_e _ = F)`;
74
75val (step_e_rules, step_e_ind, step_e_cases) = Hol_reln `
76(!s x n.
77  FLOOKUP s.store x = SOME n
78  ���
79  step_e (s, Var x) NONE (s, Num n)) ���
80(!s e1 e2 o'.
81  oracle_get s.non_det_o = (F, o')
82  ���
83  step_e (s, Add e1 e2)
84         (SOME (INR F))
85         (s with <| non_det_o := o'; io_trace := s.io_trace ++ [INR F] |>, AddL e1 e2)) ���
86(!s e1 e2 o'.
87  oracle_get s.non_det_o = (T, o')
88  ���
89  step_e (s, Add e1 e2) (SOME (INR T)) (s with <| non_det_o := o'; io_trace := s.io_trace ++ [INR T] |>, AddR e1 e2)) ���
90(!s n1 n2.
91  step_e (s, AddL (Num n1) (Num n2)) NONE (s, Num (n1 + n2))) ���
92(!s n1 n2.
93  step_e (s, AddR (Num n1) (Num n2)) NONE (s, Num (n1 + n2))) ���
94(!s s2 e1 e2 e3 l.
95  step_e (s, e1) l (s2, e3)
96  ���
97  step_e (s, AddL e1 e2) l (s2, AddL e3 e2)) ���
98(!s s2 i e1 e2 l.
99  step_e (s, e1) l (s2, e2)
100  ���
101  step_e (s, AddL (Num i) e1) l (s2, AddL (Num i) e2)) ���
102(!s s2 i e1 e2 l.
103  step_e (s, e1) l (s2, e2)
104  ���
105  step_e (s, AddR e1 (Num i)) l (s2, AddR e2 (Num i))) ���
106(!s s2 e1 e2 e3 l.
107  step_e (s, e2) l (s2, e3)
108  ���
109  step_e (s, AddR e1 e2) l (s2, AddR e1 e3)) ���
110(!s x n.
111  step_e (s, Assign x (Num n)) NONE (s with store := s.store |+ (x, n), Num n)) ���
112(!s s2 x e1 e2 l.
113  step_e (s, e1) l (s2, e2)
114  ���
115  step_e (s, Assign x e1) l (s2, Assign x e2)) ���
116(!s i input'.
117  getchar s.input = (i,input')
118  ���
119  step_e (s, Getchar)
120         (SOME (INL (Itag i)))
121         (s with <| input := input'; io_trace := s.io_trace ++ [INL (Itag i)] |>, Num i)) ���
122(!s s2 e1 e2 l.
123  step_e (s, e1) l (s2, e2)
124  ���
125  step_e (s, Putchar e1) l (s2, Putchar e2)) ���
126(!s i.
127  step_e (s, Putchar (Num i))
128         (SOME (INL (Otag i)))
129         (s with io_trace := s.io_trace ++ [INL (Otag i)], Num i))`;
130
131val is_val_t_def = Define `
132(is_val_t (Exp (e : small_e)) = is_val_e e) ���
133(is_val_t Break = T) ���
134(is_val_t _ = F)`;
135
136val (step_t_rules, step_t_ind, step_t_cases) = Hol_reln `
137(!s t x.
138  step_t (s, Dec x t) NONE (s with store := s.store |+ (x, 0), t)) ���
139(!s s2 e e2 l.
140  step_e (s, e) l (s2, e2)
141  ���
142  step_t (s, Exp e) l (s2, Exp e2)) ���
143(!s s2 t1 t2 t1' l.
144  step_t (s, t1) l (s2, t1')
145  ���
146  step_t (s, Seq t1 t2) l (s2, Seq t1' t2)) ���
147(!s t.
148  step_t (s, Seq Break t) NONE (s, Break)) ���
149(!s n t.
150  step_t (s, Seq (Exp (Num n)) t) NONE (s, t)) ���
151(!s s2 e t1 t2 e2 l.
152  step_e (s, e) l (s2,e2)
153  ���
154  step_t (s, If e t1 t2) l (s2, If e2 t1 t2)) ���
155(!s t1 t2.
156  step_t (s, If (Num 0) t1 t2) NONE (s, t2)) ���
157(!s n t1 t2.
158  n ��� 0
159  ���
160  step_t (s, If (Num n) t1 t2) NONE (s, t1)) ���
161(!s.
162  step_t (s, Handle Break) NONE (s, Exp (Num 0))) ���
163(!s t.
164  is_val_t t ���
165  t ��� Break
166  ���
167  step_t (s, Handle t) NONE (s, t)) ���
168(!s1 s2 t1 t2 l.
169  step_t (s1, t1) l (s2, t2)
170  ���
171  step_t (s1, Handle t1) l (s2, Handle t2)) ���
172(!s e1 e2 t.
173  step_t (s, For e1 e2 t) NONE (s, Handle (If e1 (Seq t (Seq (Exp e2) (For e1 e2 t))) (Exp (Num 0)))))`;
174
175val filter_map_def = Define `
176(filter_map f [] = []) ���
177(filter_map f (h::t) =
178  case f h of
179  | NONE => filter_map f t
180  | SOME x => x :: filter_map f t)`;
181
182val path_to_obs_def = Define `
183  path_to_obs p =
184    if ��finite p then
185      Diverge (lfilter_map I (labels p))
186    else if is_val_t (SND (last p)) then
187      Terminate (filter_map I (THE (toList (labels p))))
188    else
189      Crash`;
190
191val semantics_small_def = Define `
192  (semantics_small input prog =
193    { path_to_obs p | p,nd |
194      okpath step_t p ��� complete step_t p ��� first p = (init_st 0 nd input, t_to_small_t prog) })`;
195
196(* ----------- Connect to functional big step -------------- *)
197
198val for_small_sem_def = Define `
199  for_small_sem input =
200    <| step := (\st. some st'. ?l. step_t st l st');
201       is_result := (\st. is_val_t (SND st));
202       load := (\nd t. (init_st 0 nd input , t_to_small_t t));
203       unload := (\st. (FST st).io_trace) |>`;
204
205val for_eval_def = Define `
206  for_eval st env t =
207    case sem_t st t of
208      (Rval v, s) => (s, Val (SOME v))
209    | (Rbreak, s) => (s, Val NONE)
210    | (Rtimeout, s) => (s, Timeout)
211    | (Rfail, s) => (s, Error)`;
212
213val for_big_sem_def = Define `
214  for_big_sem input =
215    <| eval := for_eval;
216       init_st := (\nd. init_st 0 nd input);
217       init_env := ();
218       get_clock := (\x. x.clock);
219       set_clock := (\c st. st with clock := c);
220       get_oracle_events := (\st. st.io_trace) |>`;
221
222val (res_rel_t_rules, res_rel_t_ind, res_rel_t_cases) = Hol_reln `
223(!i s.
224  res_rel_t (Rval i, s) (s with clock := 0, Exp (Num i))) ���
225(!s t.
226  (~?l s' t'. step_t (s with clock := 0, t) l (s', t')) ���
227  ~is_val_t t
228  ���
229  res_rel_t (Rfail, s) (s with clock := 0, t)) ���
230(!s.
231  res_rel_t (Rbreak, s) (s with clock := 0, Break)) ���
232(!s t.
233  (?l s' t'. step_t (s, t) l (s', t')) ���
234  s.clock = 0
235  ���
236  res_rel_t (Rtimeout, s) (s, t))`;
237
238val (res_rel_e_rules, res_rel_e_ind, res_rel_e_cases) = Hol_reln `
239(!i s.
240  res_rel_e (Rval i, s) (s with clock:=0, Num i)) ���
241(!s e.
242  (~?s' e' l. step_e (s, e) l (s', e')) ���
243  ~is_val_e e
244  ���
245  res_rel_e (Rfail, s) (s with clock:=0, e))`
246
247val _ = set_trace "Goalstack.print_goal_at_top" 0;
248
249val step_t_strongind = (fetch "-" "step_t_strongind")
250val step_e_strongind = (fetch "-" "step_e_strongind")
251
252val conjs_def = Define` conjs A B ��� A ��� B`
253
254val etac = (fs[Once step_t_cases]>>fs[Once step_t_cases,Once step_e_cases,conjs_def])
255
256(* Determinism of small-step w.r.t. an oracle *)
257
258val step_e_determ = Q.prove(
259` ���se l1 se1.
260  step_e se l1 se1 ���
261  (���l2 se2.
262  step_e se l2 se2 ��� conjs (se1 = se2) (l1 = l2))`,
263  ho_match_mp_tac step_e_strongind>>rw[]>>fs[FORALL_PROD]
264  >- (rw[conjs_def]>>fs[Once step_e_cases]>>rfs[])
265  >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[]))
266  >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[]))
267  >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[]))
268  >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[]))
269  >>
270  TRY
271    (pop_assum mp_tac>>simp[Once step_e_cases]>>rw[]>>
272    fs[Once step_e_cases])
273  >>
274  fs[conjs_def])|>REWRITE_RULE[conjs_def]
275
276val step_t_determ = Q.prove(
277` ���st l1 st1.
278  step_t st l1 st1 ���
279  (���l2 st2.
280  step_t st l2 st2 ��� conjs (st1 = st2) (l1 = l2))`,
281  ho_match_mp_tac step_t_strongind >>rw[]
282  >- etac
283  >-
284    (fs[Once step_t_cases]>>
285    imp_res_tac step_e_determ>>
286    fs[conjs_def])
287  >-
288    (pop_assum mp_tac>>
289    simp[Once step_t_cases]>>fs[FORALL_PROD]>>rw[]>>
290    fs[Once step_t_cases,Once step_e_cases])
291  >- etac
292  >- etac
293  >-
294    (fs[Once step_t_cases]
295    >-
296      (imp_res_tac step_e_determ>>fs[conjs_def])
297    >> etac)
298  >- etac
299  >- etac
300  >- etac
301  >-
302    (fs[Once step_t_cases]>>rfs[conjs_def]>>
303    Cases_on`t`>>fs[is_val_t_def]>>
304    Cases_on`s'`>>fs[is_val_e_def]>>
305    fs[Once step_t_cases]>>
306    fs[Once step_e_cases])
307  >-
308    (pop_assum mp_tac>>
309    simp[Once step_t_cases]>>rw[]
310    >-
311      etac
312    >-
313      (Cases_on`t1`>>fs[is_val_t_def]>>Cases_on`s`>>fs[is_val_e_def]>>
314      fs[Once step_t_cases,Once step_e_cases])
315    >>
316      fs[FORALL_PROD]>>metis_tac[])
317  >>
318    fs[Once step_t_cases,conjs_def])|>REWRITE_RULE[conjs_def]
319
320val step_t_select_unique = Q.prove(
321`step_t (q,r) l st' ���
322 (@st'. ���l. step_t (q,r) l st') = st'`,
323 rw[]>>
324 metis_tac[step_t_determ])
325
326val some_to_SOME_step_e = Q.prove(
327`step_e A l B ���
328  (some st'. ���l. step_e A l st') = SOME B`,
329 rw[]>>fs[some_def]>>
330 metis_tac[step_e_determ]) |> GEN_ALL
331
332val some_to_SOME_step_t = Q.prove(
333`step_t A l B ���
334 (some st'. ���l. step_t A l st') =
335 SOME B`,
336 rw[]>>fs[some_def]>>metis_tac[step_t_determ]) |>GEN_ALL
337
338(* Contextual transitions of the small step semantics *)
339val check_trace_seq = Q.prove(
340`���tr.
341 check_trace (��st. some st'. ���l. step_t st l st') tr ���
342 check_trace (��st. some st'. ���l. step_t st l st') (MAP (��st,t. (st,Seq t p)) tr)`,
343 Induct>>rw[]>>
344 Cases_on`tr`>>fs[check_trace_def]>>
345 Cases_on`h`>>Cases_on`h'`>>
346 match_mp_tac some_to_SOME_step_t>>
347 fs[some_def]>>
348 simp[Once step_t_cases]>>
349 metis_tac[step_t_select_unique])
350
351val check_trace_assign = Q.prove(
352`���tr.
353 check_trace (��st. some st'. ?l. step_e st l st') tr ���
354 check_trace (��st. some st'. ?l. step_e st l st') (MAP (��st,e. (st,Assign s e)) tr)`,
355 Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>>
356 Cases_on`h`>>Cases_on`h'`>>
357 match_mp_tac some_to_SOME_step_e>>
358 fs[some_def]>>
359 simp[Once step_e_cases]>>
360 metis_tac[step_e_determ])
361
362val check_trace_putchar = Q.prove(
363`���tr.
364 check_trace (��st. some st'. ?l. step_e st l st') tr ���
365 check_trace (��st. some st'. ?l. step_e st l st') (MAP (��st,e. (st,Putchar e)) tr)`,
366 Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>>
367 Cases_on`h`>>Cases_on`h'`>>
368 match_mp_tac some_to_SOME_step_e>>
369 fs[some_def]>>
370 simp[Once step_e_cases]>>
371 metis_tac[step_e_determ])
372
373val check_trace_addl1 = Q.prove(
374`���tr.
375 check_trace (��st. some st'. ?l. step_e st l st') tr ���
376 check_trace (��st. some st'. ?l. step_e st l st') (MAP (��st,e. (st,AddL e e')) tr)`,
377 Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>>
378 Cases_on`h`>>Cases_on`h'`>>
379 match_mp_tac some_to_SOME_step_e>>
380 fs[some_def]>>
381 simp[Once step_e_cases]>>
382 metis_tac[step_e_determ])
383
384val check_trace_addl2 = Q.prove(
385`���tr.
386 check_trace (��st. some st'. ?l. step_e st l st') tr ���
387 check_trace (��st. some st'. ?l. step_e st l st') (MAP (��st,e'. (st,AddL (Num i) e')) tr)`,
388 Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>>
389 Cases_on`h`>>Cases_on`h'`>>
390 match_mp_tac some_to_SOME_step_e>>
391 fs[some_def]>>
392 simp[Once step_e_cases]>>
393 metis_tac[step_e_determ])
394
395val check_trace_addr1 = Q.prove(
396`���tr.
397 check_trace (��st. some st'. ?l. step_e st l st') tr ���
398 check_trace (��st. some st'. ?l. step_e st l st') (MAP (��st,e'. (st,AddR e e')) tr)`,
399 Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>>
400 Cases_on`h`>>Cases_on`h'`>>
401 match_mp_tac some_to_SOME_step_e>>
402 fs[some_def]>>
403 simp[Once step_e_cases]>>
404 metis_tac[step_e_determ,is_val_e_def])
405
406val check_trace_addr2 = Q.prove(
407`���tr.
408 check_trace (��st. some st'. ?l. step_e st l st') tr ���
409 check_trace (��st. some st'. ?l. step_e st l st') (MAP (��st,e'. (st,AddR e' (Num i))) tr)`,
410 Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>>
411 Cases_on`h`>>Cases_on`h'`>>
412 match_mp_tac some_to_SOME_step_e>>
413 fs[some_def]>>
414 simp[Once step_e_cases]>>
415 metis_tac[step_e_determ,is_val_e_def])
416
417val check_trace_exp = Q.prove(
418`���tr.
419 check_trace (��st. some st'. ?l. step_e st l st') tr ���
420 check_trace (��st. some st'. ?l. step_t st l st') (MAP (��st,e'. (st,Exp e')) tr)`,
421 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>>
422 Cases_on`h`>>Cases_on`h'`>>
423 match_mp_tac some_to_SOME_step_t>>
424 fs[some_def]>>
425 simp[Once step_t_cases]>>
426 metis_tac[step_e_determ])
427
428val check_trace_if1 = Q.prove(
429`���tr.
430 check_trace (��st. some st'. ?l. step_e st l st') tr ���
431 check_trace (��st. some st'. ?l. step_t st l st') (MAP (��st,e'. (st,If e' a b)) tr)`,
432 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>>
433 Cases_on`h`>>Cases_on`h'`>>
434 match_mp_tac some_to_SOME_step_t>>
435 fs[some_def]>>
436 simp[Once step_t_cases]>>
437 metis_tac[step_e_determ])
438
439val check_trace_for1 = Q.prove(
440`���tr.
441 check_trace (��st. some st'. ?l. step_e st l st') tr ���
442 check_trace (��st. some st'. ?l. step_t st l st')
443   (MAP (��st,e'. (st,
444   Handle (If e' a b))) tr)`,
445 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>>
446 Cases_on`h`>>Cases_on`h'`>>
447 match_mp_tac some_to_SOME_step_t>>
448 fs[some_def]>>
449 simp[Once step_t_cases]>>
450 simp[Once step_t_cases]>>
451 metis_tac[step_e_determ])
452
453val check_trace_for2 = Q.prove(
454`���tr.
455 check_trace (��st. some st'. ?l. step_t st l st') tr ���
456 check_trace (��st. some st'. ?l. step_t st l st')
457   (MAP (��st,t'. (st,
458   Handle (Seq t' a))) tr)`,
459 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>>
460 Cases_on`h`>>Cases_on`h'`>>
461 match_mp_tac some_to_SOME_step_t>>
462 fs[some_def]>>
463 simp[Once step_t_cases]>>
464 simp[Once step_t_cases]>>
465 metis_tac[step_e_determ])
466
467val check_trace_for3 = Q.prove(
468`���tr.
469 check_trace (��st. some st'. ?l. step_e st l st') tr ���
470 check_trace (��st. some st'. ?l. step_t st l st')
471   (MAP (��st,e'. (st,
472   Handle (Seq (Exp e') a))) tr)`,
473 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>>
474 Cases_on`h`>>Cases_on`h'`>>
475 match_mp_tac some_to_SOME_step_t>>
476 fs[some_def]>>
477 ntac 3 (simp[Once step_t_cases])>>
478 metis_tac[step_e_determ])
479
480val check_trace_handle = Q.prove(
481`���tr.
482 check_trace (��st. some st'. ?l. step_t st l st') tr ���
483 check_trace (��st. some st'. ?l. step_t st l st')
484   (MAP (��st,t'. (st,
485   Handle t')) tr)`,
486 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>>
487 Cases_on`h`>>Cases_on`h'`>>
488 match_mp_tac some_to_SOME_step_t>>
489 fs[some_def]>>
490 simp[Once step_t_cases]>>
491 Cases_on`st'`>>metis_tac[step_t_determ])
492
493(* Non-existence of contextual transitions in small-step *)
494val no_step_e_assign = Q.prove(
495`���e.
496 (���s' e' l. ��step_e (s,e) l (s',e')) ���
497 ��is_val_e e
498 ���
499 ���s' e' l. ��step_e (s,Assign v e) l (s',e')`,
500 Induct>>rw[is_val_e_def]>>
501 simp[Once step_e_cases])
502
503val no_step_e_putchar = Q.prove(
504`���e.
505 (���s' e' l. ��step_e (s,e) l (s',e')) ���
506 ��is_val_e e
507 ���
508 ���s' e' l. ��step_e (s,Putchar e) l (s',e')`,
509 Induct>>rw[is_val_e_def]>>
510 simp[Once step_e_cases])
511
512val no_step_e_addl1 = Q.prove(
513`���e.
514 (���s' e' l. ��step_e (s,e) l (s',e')) ���
515 ��is_val_e e
516 ���
517 ���s' e' l. ��step_e (s,AddL e e'') l (s',e')`,
518 Induct>>rw[is_val_e_def]>>simp[Once step_e_cases,is_val_e_def])
519
520val no_step_e_addl2 = Q.prove(
521`���e.
522 (���s' e' l. ��step_e (s,e) l (s',e')) ���
523 ��is_val_e e
524 ���
525 ���s' e' l. ��step_e (s,AddL (Num i) e) l (s',e')`,
526 Induct>>rw[is_val_e_def]>>rpt (simp[Once step_e_cases,is_val_e_def]))
527
528val no_step_e_addr1 = Q.prove(
529`���e.
530 (���s' e' l. ��step_e (s,e) l (s',e')) ���
531 ��is_val_e e
532 ���
533 ���s' e' l. ��step_e (s,AddR e'' e) l (s',e')`,
534 Induct>>rw[is_val_e_def]>>
535 rpt (simp[Once step_e_cases]))
536
537val no_step_e_addr2 = Q.prove(
538`���e.
539 (���s' e' l. ��step_e (s,e) l (s',e')) ���
540 ��is_val_e e
541 ���
542 ���s' e' l. ��step_e (s,AddR e (Num i)) l (s',e')`,
543 Induct>>rw[is_val_e_def]>>
544 rpt (simp[Once step_e_cases]))
545
546val no_step_t_exp = Q.prove(
547`���e.
548 (���s' e' l. ��step_e (s,e) l (s',e')) ���
549 ��is_val_e e
550 ���
551 ���s' t' l. ��step_t (s,Exp e) l (s',t')`,
552 Induct>>rw[is_val_e_def]>>
553 simp[Once step_t_cases])
554
555val no_step_t_seq = Q.prove(
556`���t.
557 (���s' t' l. ��step_t (s,t) l (s',t')) ���
558 ��is_val_t t
559 ���
560 ���s' t' l. ��step_t (s,Seq t p) l (s',t')`,
561 Induct>>rw[is_val_t_def]>>
562 simp[Once step_t_cases]>>
563 Cases_on`s'`>>fs[is_val_e_def])
564
565val no_step_t_if1 = Q.prove(
566`���e.
567 (���s' e' l. ��step_e (s,e) l (s',e')) ���
568 ��is_val_e e
569 ���
570 ���s' t' l. ��step_t (s,If e a b) l (s',t')`,
571 Induct>>rw[is_val_e_def]>>
572 simp[Once step_t_cases])
573
574val no_step_t_handle = Q.prove(
575`���t.
576 (���s' t' l. ��step_t (s,t) l (s',t')) ���
577 ��is_val_t t
578 ���
579 ���s' t' l. ��step_t (s,Handle t) l (s',t')`,
580 Induct>>rw[is_val_t_def]>>
581 simp[Once step_t_cases,is_val_t_def])
582
583val LAST_MAP = Q.prove(
584`���ls. ls ��� [] ��� LAST (MAP f ls) = f (LAST ls)`,
585 Induct>>fs[LAST_DEF]>>rw[])
586
587val HD_MAP = Q.prove(
588`���ls. ls ��� [] ��� HD(MAP f ls) = f (HD ls)`,
589 Induct>>rw[])
590
591val HD_APPEND = Q.prove(
592`ls ��� [] ��� HD (ls ++ ls') = HD ls`,
593Cases_on`ls`>>fs[])
594
595val LAST_APPEND = Q.prove(
596`ls' ��� [] ��� LAST (ls ++ ls') = LAST ls'`,
597Cases_on`ls'`>>fs[])
598
599val sem_e_not_timeout = Q.prove (
600`!st e r. sem_e st e ��� (Rtimeout, r)`,
601 Induct_on `e` >>
602 rw [sem_e_def, LET_THM, permute_pair_def, oracle_get_def, unpermute_pair_def, getchar_def] >>
603 ect >>
604 fs [] >>
605 metis_tac []);
606
607val sem_e_not_break = Q.prove(
608`!st e r. sem_e st e ��� (Rbreak,r)`,
609 Induct_on`e`>>srw_tac[][sem_e_def]>>
610 ect>>
611 fs[LET_THM,unpermute_pair_def,permute_pair_def,oracle_get_def]>>
612 TRY(qpat_assum`A=(fst_e,snd_e)` mp_tac)>>
613 rw[]>>
614 TRY(metis_tac[]))
615
616val LAST_HD_eq = Q.prove(`
617���ls ls'.
618 ls ��� [] ��� ls' ��� [] ���
619 LAST ls = HD ls' ���
620 BUTLASTN 1 ls ++ ls' =
621 ls ++ TL ls'`,
622 Induct>>fs[LAST_DEF,BUTLASTN_1]>>rw[]>>
623 Cases_on`ls'`>>fs[FRONT_DEF])
624
625val check_trace_append3 = Q.prove(`
626 check_trace f ls ���
627 f h = SOME (HD ls) ���
628 check_trace f (h :: ls)`,
629 rw[]>>imp_res_tac check_trace_append2>>
630 pop_assum(qspec_then`[h]`assume_tac)>>fs[]>>
631 rfs[check_trace_def])
632
633val check_trace_tl = Q.prove(`
634 check_trace f ls ��� ls ��� [] ���
635 check_trace f (TL ls)`,
636 Cases_on`ls`>>fs[check_trace_def]>>
637 Cases_on`t`>>fs[check_trace_def])
638
639(* Start connecting functional big step to small step traces *)
640local val rw = srw_tac[] val fs = fsrw_tac[] in
641val sem_e_big_small_lem = Q.prove(
642`!s e r.
643  sem_e s e = r
644  ���
645  ?tr.
646    tr ��� [] ���
647    check_trace (\st. some st'. ?l. step_e st l st') tr ���
648    HD tr = (s with clock:=0, e_to_small_e e) ���
649    res_rel_e r (LAST tr)`,
650 Induct_on`e`>>rw[]>>fs[sem_e_def,e_to_small_e_def]
651 >-
652   (fct>>fs[res_rel_e_cases]
653   >-
654     (qexists_tac`[(s' with clock:=0,Var s)]`>>fs[check_trace_def,is_val_e_def]>>
655     simp[Once step_e_cases])
656   >-
657     (qexists_tac`[(s' with clock:=0,Var s);(s' with clock:=0,Num x)]`>>
658     fs[check_trace_def,some_def]>>
659     ntac 2 (simp[Once step_e_cases])))
660 >-
661   (fs[res_rel_e_cases]>>
662   qexists_tac`[s with clock:=0,Num i]`>>fs[check_trace_def])
663 >-
664   (fs[LET_THM,permute_pair_def,oracle_get_def]>>IF_CASES_TAC>>fs[]
665   >-
666     (qpat_abbrev_tac`st = s with <|io_trace:=B;non_det_o:=C|>`>>
667     first_x_assum(qspec_then`st`assume_tac)>>
668     Cases_on`sem_e st e'`>>Cases_on`q`>>
669     fs[sem_e_not_break,sem_e_not_timeout,unpermute_pair_def]
670     >-
671       (fct>>Cases_on`q`>>
672       fs[sem_e_not_break,sem_e_not_timeout]>>
673       last_x_assum(qspec_then`r` assume_tac)>>rfs[]>>
674       qpat_abbrev_tac`h =(A,B)`>>
675       qabbrev_tac`ls1 = (MAP (��st,e'. (st,AddR (e_to_small_e e) e')) tr)`>>
676       qabbrev_tac`ls2 = (MAP (��st,e'. (st,AddR e' (Num i))) tr')`>>
677       qabbrev_tac`ls = BUTLASTN 1 ls1 ++ ls2`>>
678       fs[res_rel_e_cases]>>
679       `LAST ls1 = HD ls2` by
680       (unabbrev_all_tac>>fs[LAST_MAP,HD_MAP])>>
681       `ls = ls1 ++ (TL ls2)` by
682       (unabbrev_all_tac>>
683       fs[LAST_HD_eq])>>
684       `check_trace (��st. some st'. ���l. step_e st l st') ls2` by
685         fs[Abbr`ls2`,check_trace_addr2]>>
686       `check_trace (��st. some st'. ���l. step_e st l st') ls` by
687         (fs[Abbr`ls`]>>Cases_on`ls2`>>fs[]>>Cases_on`t`>>fs[]
688         >-
689           fs[check_trace_addr1,Abbr`ls1`]
690         >>
691         match_mp_tac check_trace_append2>>rw[]
692         >-
693           fs[check_trace_addr1,Abbr`ls1`]
694         >-
695           (fs[markerTheory.Abbrev_def]>>
696           `h''::t' = TL (LAST ls1::h''::t')` by fs[]>>
697           pop_assum SUBST_ALL_TAC>>
698           match_mp_tac check_trace_tl>>fs[check_trace_addr2])
699         >>
700           fs[check_trace_def])
701       >-
702         (qexists_tac`[h] ++ ls ++ [(r' with clock:=0,Num(i'+i))]`>>
703         rw[]>>
704         match_mp_tac check_trace_append3>>fs[check_trace_def]>>rw[]
705         >-
706           (match_mp_tac check_trace_append2>>
707           fs[check_trace_def]>>
708           fs[markerTheory.Abbrev_def,LAST_APPEND,LAST_MAP]>>
709           match_mp_tac some_to_SOME_step_e>>
710           simp[Once step_e_cases])
711         >>
712           match_mp_tac some_to_SOME_step_e>>
713           fs[HD_APPEND,Abbr`ls1`,HD_MAP,Abbr`h`,Abbr`st`]>>
714           simp[Once step_e_cases,oracle_get_def])
715       >>
716         qexists_tac`[h]++ls` >>rw[]
717         >-
718           (match_mp_tac check_trace_append3>>
719           fs[HD_APPEND,Abbr`ls1`,HD_MAP]>>
720           match_mp_tac some_to_SOME_step_e>>
721           fs[Abbr`h`,Abbr`st`]>>
722           simp[Once step_e_cases,oracle_get_def])
723         >>
724           fs[markerTheory.Abbrev_def,LAST_DEF,LAST_APPEND,LAST_MAP,is_val_e_def,no_step_e_addr2])
725       >>
726       qpat_abbrev_tac`h =(A,B)`>>
727       qexists_tac`[h]++(MAP (��st,e'. (st,AddR (e_to_small_e e) e')) tr)`>>
728       fs[HD_MAP,res_rel_e_cases,LAST_MAP,is_val_e_def,LAST_APPEND,no_step_e_addr1]>>
729       match_mp_tac check_trace_append3>>fs[check_trace_addr1,HD_MAP]>>
730       match_mp_tac some_to_SOME_step_e>>
731       unabbrev_all_tac>>
732       simp[Once step_e_cases,oracle_get_def])
733     >>
734     (*symmetric*)
735     (qpat_abbrev_tac`st = s with <|io_trace:=B;non_det_o:=C|>`>>
736     last_x_assum(qspec_then`st`assume_tac)>>
737     Cases_on`sem_e st e`>>Cases_on`q`>>
738     fs[sem_e_not_break,sem_e_not_timeout,unpermute_pair_def]
739     >-
740       (fct>>Cases_on`q`>>
741       fs[sem_e_not_break,sem_e_not_timeout]>>
742       last_x_assum(qspec_then`r` assume_tac)>>rfs[]>>
743       qpat_abbrev_tac`h =(A,B)`>>
744       qabbrev_tac`ls1 = (MAP (��st,e. (st,AddL e (e_to_small_e e'))) tr)`>>
745       qabbrev_tac`ls2 = (MAP (��st,e'. (st,AddL (Num i) e')) tr')`>>
746       qabbrev_tac`ls = BUTLASTN 1 ls1 ++ ls2`>>
747       fs[res_rel_e_cases]>>
748       `LAST ls1 = HD ls2` by
749       (unabbrev_all_tac>>fs[LAST_MAP,HD_MAP])>>
750       `ls = ls1 ++ (TL ls2)` by
751       (unabbrev_all_tac>>
752       fs[LAST_HD_eq])>>
753       `check_trace (��st. some st'. ���l. step_e st l st') ls2` by
754         fs[Abbr`ls2`,check_trace_addl2]>>
755       `check_trace (��st. some st'. ���l. step_e st l st') ls` by
756         (fs[Abbr`ls`]>>Cases_on`ls2`>>fs[]>>Cases_on`t`>>fs[]
757         >-
758           fs[check_trace_addl1,Abbr`ls1`]
759         >>
760         match_mp_tac check_trace_append2>>rw[]
761         >-
762           fs[check_trace_addl1,Abbr`ls1`]
763         >-
764           (fs[markerTheory.Abbrev_def]>>
765           `h''::t' = TL (LAST ls1::h''::t')` by fs[]>>
766           pop_assum SUBST_ALL_TAC>>
767           match_mp_tac check_trace_tl>>fs[check_trace_addr2])
768         >>
769           fs[check_trace_def])
770       >-
771         (qexists_tac`[h] ++ ls ++ [(r' with clock:=0,Num(i+i'))]`>>
772         rw[]>>
773         match_mp_tac check_trace_append3>>fs[check_trace_def]>>rw[]
774         >-
775           (match_mp_tac check_trace_append2>>
776           fs[check_trace_def]>>
777           fs[markerTheory.Abbrev_def,LAST_APPEND,LAST_MAP]>>
778           match_mp_tac some_to_SOME_step_e>>
779           simp[Once step_e_cases])
780         >>
781           match_mp_tac some_to_SOME_step_e>>
782           fs[HD_APPEND,Abbr`ls1`,HD_MAP,Abbr`h`,Abbr`st`]>>
783           simp[Once step_e_cases,oracle_get_def])
784       >>
785         qexists_tac`[h]++ls` >>rw[]
786         >-
787           (match_mp_tac check_trace_append3>>
788           fs[HD_APPEND,Abbr`ls1`,HD_MAP]>>
789           match_mp_tac some_to_SOME_step_e>>
790           fs[Abbr`h`,Abbr`st`]>>
791           simp[Once step_e_cases,oracle_get_def])
792         >>
793           fs[markerTheory.Abbrev_def,LAST_DEF,LAST_APPEND,LAST_MAP,is_val_e_def,no_step_e_addl2])
794       >>
795       qpat_abbrev_tac`h =(A,B)`>>
796       qexists_tac`[h]++(MAP (��st,e. (st,AddL e (e_to_small_e e'))) tr)`>>
797       fs[HD_MAP,res_rel_e_cases,LAST_MAP,is_val_e_def,LAST_APPEND,no_step_e_addl1]>>
798       match_mp_tac check_trace_append3>>fs[check_trace_addl1,HD_MAP]>>
799       match_mp_tac some_to_SOME_step_e>>
800       unabbrev_all_tac>>
801       simp[Once step_e_cases,oracle_get_def]))
802 >-
803   (EVERY_CASE_TAC>>fs[res_rel_e_cases,sem_e_not_break,sem_e_not_timeout]>>
804   first_x_assum(qspec_then`s'` assume_tac)>>rfs[]
805   >-
806     (qexists_tac`(MAP (��st,e. (st,Assign s e)) tr)++[r with <|store :=r.store |+ (s,i); clock:=0|>,Num i]`>>fs[HD_MAP,HD_APPEND]>>
807     ho_match_mp_tac check_trace_append2>>
808     fs[check_trace_def,LAST_MAP,check_trace_assign]>>
809     ntac 2 (simp[Once step_e_cases]))
810   >>
811     (qexists_tac`(MAP (��st,e. (st,Assign s e)) tr)`>>
812     fs[HD_MAP,LAST_MAP,is_val_e_def,no_step_e_assign,check_trace_assign]))
813 >-
814   (Cases_on`getchar s.input`>>fs[LET_THM,res_rel_e_cases]>>
815   qpat_abbrev_tac`t = (A,B)`>>
816   qpat_abbrev_tac`t' = (A,B)`>>
817   qexists_tac`[t;t']`>>unabbrev_all_tac>>fs[check_trace_def]>>
818   match_mp_tac some_to_SOME_step_e>>
819   simp[Once step_e_cases])
820 >-
821   (first_x_assum(qspec_then`s` assume_tac)>>fs[]>>
822   Cases_on`sem_e s e`>>Cases_on`q`>>fs[sem_e_not_break,sem_e_not_timeout]>>
823   qpat_abbrev_tac`t = (A,B)`>>
824   qpat_abbrev_tac`t' = (A,B)`
825   >-
826     (qexists_tac`MAP (��st,e. (st,Putchar e)) tr ++ [(r with <|io_trace := r.io_trace ++ [INL(Otag i)];clock:=0|>,Num i)]`>>
827     fs[HD_MAP,HD_APPEND,Abbr`t'`,res_rel_e_cases]>>
828     ho_match_mp_tac check_trace_append2>>
829     fs[check_trace_def,LAST_MAP,check_trace_putchar]>>
830     ntac 2 (simp[Once step_e_cases]))
831   >>
832     qexists_tac`MAP (��st,e. (st,Putchar e)) tr`>>unabbrev_all_tac>>
833     fs[HD_MAP,res_rel_e_cases,LAST_MAP,is_val_e_def,check_trace_putchar,no_step_e_putchar]))
834end
835
836val sem_t_for_no_break = Q.prove(
837 `���s s'. sem_t s (For e1 e2 t) ��� (Rbreak,s')`,
838 completeInduct_on`s.clock`>>fs[sem_t_def_with_stop]>>
839 rw[]>>fct>>Cases_on`q`>>
840 fs[sem_e_not_break,sem_e_not_timeout]>>
841 IF_CASES_TAC>>fs[]>>
842 fct>>Cases_on`q`>>fs[]>>
843 fct>>Cases_on`q`>>fs[sem_e_not_break,sem_e_not_timeout]>>
844 imp_res_tac sem_e_clock>>imp_res_tac sem_t_clock>>fs[]>>
845 IF_CASES_TAC>>fs[dec_clock_def]>>
846 simp[STOP_def]>>
847 simp[sem_t_def_with_stop]>>
848 fs[PULL_FORALL]>>
849 first_x_assum(qspec_then `r'' with clock := r''.clock-1` mp_tac)>>
850 fs[]>>
851 `r''.clock < 1 + r.clock ��� 0 < r.clock` by
852   DECIDE_TAC>>
853 fs[dec_clock_def])
854
855val step_e_clock = Q.prove(`
856  ���se l1 se'.
857  step_e se l1 se' ���
858  ���s e s' e'.
859  se = (s,e) ���
860  se' = (s',e') ���
861  (���c.
862  step_e (s with clock:=c,e) l1 (s' with clock:=c,e'))`,
863  ho_match_mp_tac step_e_strongind>>rw[]>>
864  simp[Once step_e_cases])
865
866val step_e_zero_clock = Q.prove(
867 `(���s e l. ��step_e (r,e') l (s,e))���
868 ���s e l. ��step_e (r with clock:=0,e') l (s,e)`,
869 rw[]>>CCONTR_TAC>>fs[]>>imp_res_tac step_e_clock>>fs[]>>
870 pop_assum(qspec_then`r.clock`assume_tac)>>fs[]>>
871 `r with clock:= r.clock = r` by fs[state_component_equality]>>
872 metis_tac[])
873
874local val rw = srw_tac[] val fs = fsrw_tac[] in
875val big_small_lem = Q.prove (
876`!s t r.
877  sem_t s t = r
878  ���
879  ?tr.
880    tr ��� [] ���
881    s.clock - (SND r).clock ��� LENGTH tr ���
882    check_trace (\st. some st'. ?l. step_t st l st') tr ���
883    HD tr = (s with clock := 0, (t_to_small_t t)) ���
884    res_rel_t r (LAST tr)`,
885 ho_match_mp_tac sem_t_ind >>
886 rw [sem_t_def_with_stop, t_to_small_t_def]
887 >-
888   (qabbrev_tac`r = sem_e s e`>>fs[markerTheory.Abbrev_def]>>
889   pop_assum (assume_tac o SYM)>>
890   imp_res_tac sem_e_big_small_lem>>
891   Cases_on`r`>>
892   qexists_tac`MAP (��st,e. (st,Exp e)) tr`>>
893   imp_res_tac sem_e_clock>>fs[HD_MAP,LAST_MAP]>>
894   CONJ_TAC>-
895     fs[check_trace_exp]
896   >>
897   fs[res_rel_t_cases,res_rel_e_cases,is_val_t_def]>>
898   imp_res_tac step_e_zero_clock>>
899   fs[Once step_t_cases])
900 >-
901   (qpat_abbrev_tac`A = (s with clock:=0,D)`>>
902   qexists_tac`A::tr`>>fs[Abbr`A`,check_trace_def]>>
903   CONJ_TAC >- DECIDE_TAC>>
904   CONJ_TAC >-
905     (Cases_on`tr`>>
906     simp[check_trace_def,optionTheory.some_def]>>
907     ntac 2 (simp[Once step_t_cases])>>
908     fs[])>>
909   fs[LAST_DEF])
910 >-
911   (qexists_tac`[s with clock:=0,Break]`>>
912   fs[res_rel_t_cases,check_trace_def])
913 >-
914   (EVERY_CASE_TAC>>fs[]
915   >-
916     (qpat_abbrev_tac`p = t_to_small_t t'`>>
917     qexists_tac`MAP (��st,t. (st,Seq t p)) tr ++ tr'`>>
918     fs[HD_MAP,HD_APPEND,LAST_APPEND]>>rw[]
919     >-
920       DECIDE_TAC
921     >-
922       (match_mp_tac check_trace_append2>>
923       fs[check_trace_seq,LAST_MAP]>>
924       Cases_on`LAST tr`>>fs[]>>
925       match_mp_tac some_to_SOME_step_t>>
926       simp[Once step_t_cases]>>fs[Abbr`p`,res_rel_t_cases]>>
927       metis_tac[]))
928   >-
929     (qpat_abbrev_tac `p = t_to_small_t t'`>>
930     qexists_tac`(MAP (��st,t. (st,Seq t p)) tr)++[r with clock:=0,Break]`>>
931     fs[HD_APPEND,HD_MAP]>>rw[]
932     >-
933       DECIDE_TAC
934     >-
935       (match_mp_tac check_trace_append2>>
936       fs[check_trace_seq,LAST_MAP,check_trace_def]>>
937       fs[res_rel_t_cases]>>
938       match_mp_tac some_to_SOME_step_t>>
939       simp[Once step_t_cases]>>fs[Abbr`p`,res_rel_t_cases])
940     >-
941       fs[Once res_rel_t_cases])
942   >-
943     (qpat_abbrev_tac `p = t_to_small_t t'`>>
944     qexists_tac`(MAP (��st,t. (st,Seq t p)) tr)`>>
945     fs[HD_APPEND,HD_MAP,check_trace_def,check_trace_seq]>>rw[]>>
946     fs[Once res_rel_t_cases,LAST_MAP]>>
947     `step_t (r,Seq t'' p) l (s',Seq t''' p)` by
948       simp[Once step_t_cases]>>
949     metis_tac[])
950   >-
951     (qpat_abbrev_tac `p = t_to_small_t t'`>>
952     qexists_tac`(MAP (��st,t. (st,Seq t p)) tr)`>>
953     fs[HD_APPEND,HD_MAP,check_trace_def,check_trace_seq]>>rw[]>>
954     fs[Once res_rel_t_cases,LAST_MAP,is_val_t_def]>>
955     metis_tac[no_step_t_seq]))
956 >-
957   (EVERY_CASE_TAC>>fs[sem_e_not_break,sem_e_not_timeout]>>
958   imp_res_tac sem_e_big_small_lem>>
959   imp_res_tac sem_e_clock>>
960   qpat_abbrev_tac`p1 = t_to_small_t t1`>>
961   qpat_abbrev_tac`p2 = t_to_small_t t2`>>
962   TRY
963     (qexists_tac`(MAP (��st,e. (st,(If e p1 p2))) tr') ++ tr`>>
964     fs[HD_MAP,HD_APPEND,LAST_MAP,LAST_APPEND]>>rw[]
965     >-
966       DECIDE_TAC
967     >>
968       match_mp_tac check_trace_append2>>fs[res_rel_e_cases]>>CONJ_TAC
969       >-
970         metis_tac[check_trace_if1]
971       >>
972         match_mp_tac some_to_SOME_step_t>>fs[LAST_MAP]>>
973         simp[Once step_t_cases]>>
974         metis_tac[])
975   >>
976     qexists_tac`(MAP (��st,e. (st,(If e p1 p2))) tr)`>>rw[]>>
977     fs[HD_MAP,res_rel_t_cases,LAST_MAP,res_rel_e_cases,is_val_t_def,check_trace_if1,no_step_t_if1]>>
978     metis_tac[check_trace_if1,no_step_t_if1,step_e_zero_clock])
979 >- (*For*)
980   (Cases_on`sem_e s e1`>>Cases_on`q`>>fs[sem_e_not_break,sem_e_not_timeout]>>
981   qpat_abbrev_tac`e1s = e_to_small_e e1`>>
982   qpat_abbrev_tac`e2s = e_to_small_e e2`>>
983   (*trace for e1*)
984   imp_res_tac sem_e_big_small_lem>>
985   imp_res_tac sem_e_clock>>
986   qpat_abbrev_tac`p = t_to_small_t t`>>
987   qabbrev_tac`e1tr = (MAP (��st,e. (st,Handle (If e (Seq p (Seq (Exp e2s) (For e1s e2s p))) (Exp (Num 0))))) tr)`>>
988   `check_trace (��st. some st'. ���l. step_t st l st') e1tr` by metis_tac[check_trace_for1]>>
989   qabbrev_tac`ls = [s with clock:=0,For e1s e2s p]`>>
990   `check_trace (��st. some st'. ���l. step_t st l st') (ls++e1tr)` by
991     (match_mp_tac check_trace_append2>>unabbrev_all_tac>>
992     fs[check_trace_def,HD_MAP]>>
993     match_mp_tac some_to_SOME_step_t>>
994     simp[Once step_t_cases])
995   >-
996     (IF_CASES_TAC>>fs[]
997     >-
998       (*run out of time*)
999       (fs[res_rel_t_cases,res_rel_e_cases]>>
1000       qexists_tac` (ls ++ e1tr)
1001        ++ [(r with clock:=0,Handle (Exp (Num 0)));(r with clock:=0,Exp (Num 0))]`>>
1002       fs[LAST_APPEND,LAST_MAP]>>fs[]>>rw[]
1003       >-
1004         (match_mp_tac check_trace_append2>>rw[]
1005         >-
1006           (fs[check_trace_def]>>
1007           match_mp_tac some_to_SOME_step_t>>
1008           simp[Once step_t_cases,is_val_e_def,is_val_t_def])
1009         >-
1010           (unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP]>>
1011           match_mp_tac some_to_SOME_step_t>>
1012           ntac 2 (simp[Once step_t_cases])))
1013       >>
1014         unabbrev_all_tac>>fs[HD_APPEND])
1015     >>
1016     Cases_on`sem_t r t`>>Cases_on`q`>>fs[]>>
1017     qabbrev_tac`ttr = (MAP (��st,t. (st,Handle (Seq t (Seq (Exp e2s) (For e1s e2s p))) ))) tr'`>>
1018     `check_trace (��st. some st'. ���l. step_t st l st') ttr` by
1019       metis_tac[check_trace_for2]>>
1020     `check_trace (��st. some st'. ���l. step_t st l st') (ls++e1tr++ttr)` by
1021       (match_mp_tac check_trace_append2>>
1022       fs[]>> unabbrev_all_tac>>
1023       fs[LAST_MAP,res_rel_e_cases,HD_MAP,LAST_DEF]>>
1024       match_mp_tac some_to_SOME_step_t>>
1025       ntac 2 (simp[Once step_t_cases]))
1026     >-
1027       (*continue executing*)
1028       (Cases_on`sem_e r' e2`>>Cases_on`q`>>
1029       fs[sem_e_not_break,sem_e_not_timeout]>>
1030       imp_res_tac sem_e_big_small_lem>>
1031       imp_res_tac sem_e_clock>>
1032       qabbrev_tac`e2tr = (MAP (��st,e. (st,Handle (Seq (Exp e) (For e1s e2s p)) ))) tr''`>>
1033       `check_trace (��st. some st'. ���l. step_t st l st') e2tr` by
1034         metis_tac[check_trace_for3]>>
1035       `check_trace (��st. some st'. ���l. step_t st l st') (ls++e1tr++ttr++e2tr)` by
1036         (match_mp_tac check_trace_append2>>fs[]>>
1037         match_mp_tac some_to_SOME_step_t>>
1038         unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP,HD_MAP,res_rel_t_cases]>>
1039         ntac 2 (simp[Once step_t_cases,res_rel_e_cases]))
1040       >-
1041       (*e2 ok*)
1042         (IF_CASES_TAC>>fs[]
1043         >-
1044           (*clock ok*)
1045           (simp[STOP_def]>>
1046           simp[Once sem_t_def_with_stop]>>
1047           fs[dec_clock_def]>>
1048           (*Need a handle wrapper around rest of trace*)
1049           qabbrev_tac`ftr = MAP (��st,t. (st, Handle t))tr''''` >>
1050           `check_trace (��st. some st'. ���l. step_t st l st') ftr` by
1051             metis_tac[check_trace_handle]>>
1052           `check_trace (��st. some st'. ���l. step_t st l st') (ls++e1tr++ttr++e2tr++ftr)` by
1053             (match_mp_tac check_trace_append2>>fs[]>>
1054             match_mp_tac some_to_SOME_step_t>>
1055             unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP,HD_MAP]>>
1056             fs[res_rel_e_cases]>>
1057             ntac 2 (simp[Once step_t_cases]))>>
1058           fs[res_rel_t_cases]
1059           (*Case split on the rest of loop*)
1060           >-
1061             (qexists_tac`ls ++ e1tr ++ ttr ++ e2tr ++ ftr ++[s' with clock:=0,Exp (Num i''')]`>>fs[]>>rw[]>>
1062             TRY
1063               (unabbrev_all_tac>>fs[]>>
1064               DECIDE_TAC)
1065             >-
1066               (match_mp_tac check_trace_append2>>fs[check_trace_def]>>
1067               match_mp_tac some_to_SOME_step_t>>unabbrev_all_tac>>
1068               fs[LAST_DEF,LAST_APPEND,LAST_MAP,res_rel_e_cases]>>
1069               simp[Once step_t_cases,is_val_t_def,is_val_e_def])
1070             >>
1071               simp[Once sem_t_def_with_stop,LAST_APPEND,dec_clock_def])
1072           >-
1073             (qexists_tac`ls ++ e1tr++ttr++e2tr++ftr`>>fs[]>>rw[]>>
1074             TRY(unabbrev_all_tac>>fs[]>>DECIDE_TAC)>>
1075             ntac 4 (simp[Once sem_t_def_with_stop,LAST_APPEND,dec_clock_def])>>
1076             unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP,is_val_t_def]>>
1077             match_mp_tac no_step_t_handle>>
1078             metis_tac[])
1079           >-
1080             (*break never occurs*)
1081             (qpat_assum `A = (RBreak,s')` mp_tac>>
1082             fct>>Cases_on`q`>>
1083             fs[sem_e_not_timeout,sem_e_not_break]>>
1084             IF_CASES_TAC>>fs[]>>
1085             fct>>Cases_on`q`>>
1086             fs[]>>
1087             fct>>Cases_on`q`>>
1088             fs[sem_e_not_timeout,sem_e_not_break]>>
1089             IF_CASES_TAC>>fs[]>>
1090             simp[STOP_def]>>
1091             metis_tac[sem_t_for_no_break])
1092           >>
1093             (qexists_tac`ls ++ e1tr ++ ttr ++ e2tr ++ ftr`>>fs[]>>rw[]>>
1094             TRY
1095               (unabbrev_all_tac>>fs[]>>
1096               DECIDE_TAC)
1097             >>
1098             unabbrev_all_tac>>
1099             ntac 3 (simp[Once sem_t_def_with_stop,LAST_APPEND,dec_clock_def,LAST_MAP])>>
1100             simp[Once step_t_cases]>>metis_tac[]))
1101         >>
1102           (*clock ended*)
1103           fs[res_rel_t_cases]>>
1104           qexists_tac`ls++e1tr++ttr++e2tr`>>fs[]>>rw[]>>
1105           TRY (unabbrev_all_tac>>fs[]>>DECIDE_TAC)>>
1106           unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP,res_rel_e_cases]>>
1107           `r'' with clock:=0 = r''` by fs[state_component_equality]>>
1108           ntac 2 (simp[Once step_t_cases,is_val_t_def])>>
1109           metis_tac[])
1110       >>
1111       (*e2 fails*)
1112       (qexists_tac`ls++e1tr++ttr++e2tr`>>fs[res_rel_e_cases]>>
1113       unabbrev_all_tac>>
1114       fs[LAST_APPEND,LAST_MAP,res_rel_t_cases,is_val_t_def]>>rw[]
1115       >-
1116         DECIDE_TAC
1117       >>
1118         imp_res_tac step_e_zero_clock>>
1119         metis_tac[no_step_t_exp,no_step_t_handle
1120         ,no_step_t_seq,is_val_t_def]))
1121     >-
1122       (qexists_tac`ls++e1tr++ttr++[(r' with clock:= 0,Handle Break);(r' with clock:=0,Exp (Num 0))]`>>
1123       fs[LAST_APPEND,LAST_MAP,res_rel_t_cases]>>rw[]>>
1124       TRY(unabbrev_all_tac>>fs[]>>DECIDE_TAC)>>
1125       match_mp_tac check_trace_append2>>fs[check_trace_def]>>CONJ_TAC>>
1126       match_mp_tac some_to_SOME_step_t>>
1127       unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP,res_rel_t_cases]>>
1128       ntac 2 (simp[Once step_t_cases]))
1129     >-
1130       (qexists_tac`ls++e1tr++ttr`>>unabbrev_all_tac>>
1131       fs[LAST_APPEND,LAST_MAP,res_rel_t_cases]>>CONJ_TAC
1132       >-
1133         DECIDE_TAC
1134       >>
1135         ntac 2 (simp[Once step_t_cases,is_val_t_def])>>
1136         metis_tac[])
1137     >>
1138       (qexists_tac`ls++e1tr++ttr`>>unabbrev_all_tac>>
1139       fs[LAST_APPEND,LAST_MAP,res_rel_t_cases]>>CONJ_TAC
1140       >-
1141         DECIDE_TAC
1142       >>
1143         fs[is_val_t_def]>>match_mp_tac no_step_t_handle>>
1144         fs[is_val_t_def]>>match_mp_tac no_step_t_seq>>
1145         metis_tac[]))
1146   >>
1147     (*e1 fails, expand it 1 step*)
1148     qexists_tac` ls ++ e1tr`>>
1149     unabbrev_all_tac>>fs[res_rel_t_cases,LAST_DEF,LAST_MAP,HD_APPEND]>>
1150     fs[LAST_APPEND,LAST_MAP,res_rel_e_cases,is_val_t_def]>>
1151     match_mp_tac no_step_t_handle>>fs[is_val_t_def]>>
1152     imp_res_tac step_e_zero_clock>>
1153     metis_tac[no_step_t_if1]))
1154end
1155
1156val big_timeout_0 = Q.prove (
1157`!st p r.
1158  sem_t st p = (Rtimeout,r)
1159  ���
1160  r.clock = 0`,
1161 ho_match_mp_tac sem_t_ind >>
1162 conj_tac >- (
1163   rw [sem_t_def_with_stop, sem_e_not_timeout]) >>
1164 conj_tac >- (
1165   rw [sem_t_def_with_stop, sem_e_not_timeout]) >>
1166 conj_tac >- (
1167   rw [sem_t_def_with_stop, sem_e_not_timeout] >>
1168   ect >> fs []) >>
1169 conj_tac >- (
1170   rw [sem_t_def_with_stop, sem_e_not_timeout] >>
1171   ect >> fs []) >>
1172 conj_tac >- (
1173   rw [sem_t_def_with_stop, sem_e_not_timeout] >>
1174   ect >> fs [sem_e_not_timeout])
1175 >- (
1176   rw [] >>
1177   pop_assum mp_tac >>
1178   simp [sem_t_def_with_stop] >>
1179   ect >>
1180   fs [sem_e_not_timeout, STOP_def] >>
1181   rw [] >>
1182   fs []));
1183
1184(* check traces are unique up to prefixing *)
1185val check_trace_determ = Q.prove(
1186`���tr h f.
1187 check_trace f (h::tr) ���
1188 ���tr'.
1189 LENGTH tr' ��� LENGTH tr ���
1190 check_trace f (h::tr') ���
1191 isPREFIX tr' tr`,
1192 Induct>>rw[]>>fs[check_clock_def,isPREFIX,LENGTH_NIL]>>
1193 Cases_on`tr'`>>fs[check_trace_def]>>
1194 metis_tac[])
1195
1196val check_trace_prefixes = Q.prove(
1197`���tr f.
1198 tr ��� [] ���
1199 check_trace f tr ���
1200 ���tr'.
1201 tr' ��� [] ��� HD tr' = HD tr ���
1202 check_trace f tr' ���
1203 isPREFIX tr tr' ��� isPREFIX tr' tr`,
1204 rw[]>>
1205 Cases_on`tr`>>Cases_on`tr'`>>fs[]>>
1206 Cases_on`LENGTH t' ��� LENGTH t`>>
1207 TRY(`LENGTH t ��� LENGTH t'` by DECIDE_TAC)>>
1208 metis_tac[check_trace_determ])
1209
1210val check_trace_TL = Q.prove(
1211`���tr tr'.
1212 (tr ��� [] ���
1213 check_trace (��st. some st'. ?l. step_t st l st') tr ���
1214 (���l t'. ��step_t (LAST tr) l t') ���
1215 check_trace (��st. some st'. ?l. step_t st l st') tr' ���
1216 isPREFIX tr tr') ���
1217 tr = tr'`,
1218 Induct>>fs[check_trace_def,LAST_DEF]>>rw[]>>Cases_on`tr'`>>fs[]
1219 >-
1220   (Cases_on`t`>>fs[check_trace_def,some_def]>>
1221   metis_tac[])
1222 >>
1223   Cases_on`tr`>>Cases_on`t`>>fs[check_trace_def]>>
1224   res_tac>>fs[])
1225
1226val prefix_append = Q.prove(
1227`���ls ls'.
1228  ls ��� ls' ���
1229  ���ls''. ls++ls'' = ls'`,
1230  metis_tac[rich_listTheory.IS_PREFIX_APPEND])
1231
1232val res_rel_t_io_trace = Q.prove(
1233 `res_rel_t (q,r) s ���
1234  r.io_trace = (FST s).io_trace`,
1235  simp[res_rel_t_cases]>>rw[]>>fs[])
1236
1237(*slow*)
1238val res_rel_t_clock = Q.prove(
1239 `res_rel_t (q,r) s ���
1240  step_t s l t ���
1241  q = Rtimeout ��� (FST s).clock = 0`,
1242  simp[res_rel_t_cases]>>rw[]
1243  >>
1244    fs[Once step_t_cases,Once step_e_cases]
1245  >>
1246   metis_tac[PAIR,FST])
1247
1248val step_e_io_mono = Q.prove(
1249`���s l s'.
1250  step_e s l s' ���
1251  (FST s).io_trace ��� (FST s').io_trace`,
1252  ho_match_mp_tac step_e_strongind>>fs[])
1253
1254val step_t_io_mono = Q.prove(
1255`���s l s'.
1256  step_t s l s' ���
1257  (FST s).io_trace ��� (FST s').io_trace`,
1258  ho_match_mp_tac step_t_strongind>>
1259  fs[]>>metis_tac[step_e_io_mono,FORALL_PROD,FST])
1260
1261val RTC_step_t_io_mono = Q.prove(
1262  `���x y. (��s1 s2. (some st'. ���l. step_t s1 l st') = SOME s2)^* x y ���
1263      (FST x).io_trace ��� (FST y).io_trace`,
1264  ho_match_mp_tac RTC_INDUCT >> rw[] >>
1265  last_x_assum mp_tac >>
1266  DEEP_INTRO_TAC some_intro >> rw[] >>
1267  metis_tac[step_t_io_mono,IS_PREFIX_TRANS])
1268
1269val check_trace_io_trace = Q.prove(
1270 `���tr ls.
1271  tr ��� [] ��� check_trace (��st. some st'. ���l. step_t st l st') (tr ++ ls) ���
1272  (FST(LAST tr)).io_trace ���
1273  (FST(LAST (tr++ls))).io_trace`,
1274  rw[] >>
1275  match_mp_tac RTC_step_t_io_mono >>
1276  simp[check_trace_thm] >>
1277  qexists_tac`LAST tr::ls` >>
1278  simp[] >>
1279  conj_tac >- ( Cases_on`ls`>>simp[] ) >>
1280  `LAST tr::ls = DROP (LENGTH tr - 1) (tr++ls)` suffices_by (
1281    disch_then SUBST1_TAC >>
1282    match_mp_tac check_trace_drop >> simp[] ) >>
1283  simp[DROP_APPEND1] >>
1284  Q.ISPECL_THEN[`1n`,`tr`]mp_tac (GSYM LASTN_DROP) >>
1285  `1 ��� LENGTH tr` by (
1286    Cases_on`tr`>>fs[] >> simp[] ) >>
1287  simp[] >>
1288  Q.ISPEC_THEN`tr`FULL_STRUCT_CASES_TAC SNOC_CASES >- fs[] >>
1289  REWRITE_TAC[arithmeticTheory.ONE,LASTN,LAST,SNOC])
1290
1291val sem_e_ignores_clock = Q.prove(
1292 `���s e c r s'.
1293  sem_e s e = (r,s') ���
1294  sem_e (s with clock:=c) e = (r,s' with clock:=c)`,
1295  ho_match_mp_tac sem_e_ind>>srw_tac[][sem_e_def]>>fs[LET_THM]
1296  >-
1297    (ect>>fs[])
1298  >-
1299    (fs[permute_pair_def,LET_THM,oracle_get_def,unpermute_pair_def]>>
1300    Cases_on`switch`>>fs[]>>
1301    qpat_assum`A=(r,s')` mp_tac>>
1302    fct>>Cases_on`q`>>res_tac>>
1303    fs[sem_e_not_break,sem_e_not_timeout]>>
1304    fct>>Cases_on`q`>>res_tac>>
1305    rw[]>>
1306    fs[sem_e_not_break,sem_e_not_timeout])
1307  >>
1308    Cases_on`sem_e s e`>>res_tac>>fs[]>>
1309    Cases_on`q`>>fs[state_component_equality])
1310
1311val sem_e_io_mono = Q.prove(
1312  `���s e c.
1313  (SND (sem_e s e)).io_trace ���
1314  (SND (sem_e (s with clock:= c) e)).io_trace`,
1315  rw[]>>Cases_on`sem_e s e`>>imp_res_tac sem_e_ignores_clock>>
1316  fs[])
1317
1318val sem_e_clock_inc = Q.prove(
1319  `���s e r.
1320  sem_e s e = r ���
1321  ���k. sem_e (s with clock:= s.clock+k) e =(FST r,(SND r)with clock:= (SND r).clock+k)`,
1322  metis_tac[sem_e_ignores_clock,sem_e_clock,FST,SND,PAIR])
1323
1324val sem_t_clock_inc = Q.prove(
1325  `���s t r.
1326  sem_t s t = r ��� FST r ��� Rtimeout ���
1327  ���k. sem_t (s with clock:= s.clock+k) t =(FST r,(SND r)with clock:= (SND r).clock+k)`,
1328  ho_match_mp_tac sem_t_ind>>rw[]>>fs[sem_e_clock]>>
1329  TRY(fs[sem_t_def_with_stop]>>NO_TAC)
1330  >-
1331    (fs[sem_t_def_with_stop]>>
1332    Cases_on`sem_e s e`>>
1333    imp_res_tac sem_e_ignores_clock>>
1334    fs[]>>metis_tac[sem_e_clock])
1335  >-
1336    (fs[sem_t_def_with_stop]>>Cases_on`sem_t s t`>>Cases_on`q`>>fs[])
1337  >-
1338    (fs[sem_t_def_with_stop]>>Cases_on`sem_e s e`>>Cases_on`q`>>fs[sem_e_res]>>
1339    imp_res_tac sem_e_clock_inc>>
1340    pop_assum(qspec_then`k` assume_tac)>>fs[]>>
1341    IF_CASES_TAC>>fs[])
1342  >>
1343    pop_assum mp_tac>>
1344    simp[sem_t_def_with_stop]>>
1345    Cases_on`sem_e s e1`>>Cases_on`q`>>fs[]>>
1346    imp_res_tac sem_e_clock_inc>>fs[]>>
1347    TRY(pop_assum(qspec_then`k` assume_tac))>>
1348    fs[DECIDE ``(A:num)+B = B+A``]>>
1349    IF_CASES_TAC>>fs[]>>
1350    Cases_on`sem_t r t`>>Cases_on`q`>>fs[]>>
1351    Cases_on`sem_e r' e2`>>Cases_on`q`>>fs[]>>
1352    TRY(metis_tac[sem_e_res])>>
1353    imp_res_tac sem_e_clock_inc>>fs[]>>
1354    TRY(pop_assum(qspec_then`k` assume_tac))>>
1355    fs[DECIDE ``(A:num)+B = B+A``]>>
1356    IF_CASES_TAC>>fs[]>>rw[]>>
1357    fs[dec_clock_def,STOP_def]>>
1358    `1 ��� r''.clock` by DECIDE_TAC>>
1359    metis_tac[arithmeticTheory.LESS_EQ_ADD_SUB])
1360
1361val check_trace_io_trace_simp = Q.prove(
1362  `tr ��� [] ���
1363  check_trace (��st.some st'. ���l. step_t st l st') tr ���
1364  (FST(HD tr)).io_trace ��� (FST (LAST tr)).io_trace`,
1365  Cases_on`tr`>>rw[]>>
1366  `FST h = FST(LAST [h])` by fs[]>>
1367  pop_assum SUBST1_TAC>>
1368  `h::t = [h]++t` by fs[]>>
1369  pop_assum SUBST1_TAC>>
1370  ho_match_mp_tac check_trace_io_trace>>
1371  rw[])
1372
1373val sem_t_sing_io_mono = Q.prove(
1374  `���s t res s'.
1375  sem_t s t = (res,s') ���
1376  s.io_trace ��� s'.io_trace`,
1377  rw[]>>imp_res_tac big_small_lem>>
1378  imp_res_tac check_trace_io_trace_simp>>
1379  fs[res_rel_t_cases]>>
1380  rfs[])
1381
1382val sem_e_sing_io_mono = Q.prove(
1383`���s e res s'.
1384  sem_e s e = (res,s') ���
1385  s.io_trace ��� s'.io_trace`,
1386  CCONTR_TAC>>fs[]>>
1387  `sem_t s (Exp e) = (res,s')` by
1388    fs[sem_t_def_with_stop]>>
1389  metis_tac[sem_t_sing_io_mono])
1390
1391(* Monotonicity of io_trace w.r.t. to clock *)
1392val sem_t_io_mono_lem = Q.prove(
1393 `���s t k.
1394  (SND (sem_t s t)).io_trace ���
1395  (SND (sem_t (s with clock:=s.clock+k) t)).io_trace`,
1396  ho_match_mp_tac sem_t_ind>>rw[]>>
1397  TRY(fs[sem_t_def_with_stop,sem_e_io_mono]>>NO_TAC)
1398  >-
1399    (fs[sem_t_def_with_stop]>>
1400    fct>>Cases_on`q`>>fs[]>>
1401    imp_res_tac sem_t_clock_inc>>fs[]>>
1402    fct>>Cases_on`q`>>fs[]>>
1403    first_x_assum(qspec_then`k` assume_tac)>>rfs[]>>
1404    Cases_on`sem_t r' t'`>>
1405    imp_res_tac sem_t_sing_io_mono>>
1406    fs[]>>
1407    metis_tac[IS_PREFIX_TRANS])
1408  >-
1409    (fs[sem_t_def_with_stop]>>
1410    fct>>Cases_on`q`>>fs[]>>TRY(metis_tac[sem_e_res])>>
1411    imp_res_tac sem_e_clock_inc>>fs[]>>
1412    IF_CASES_TAC>>fs[])
1413  >>
1414    simp[Once sem_t_def_with_stop]>>
1415    simp[Once sem_t_def_with_stop]>>
1416    fct>>Cases_on`q`>>fs[]>>TRY(metis_tac[sem_e_res])>>
1417    imp_res_tac sem_e_clock_inc>>
1418    pop_assum(qspec_then`k` assume_tac)>>
1419    fs[DECIDE ``(A:num)+B = B+A``]>>
1420    IF_CASES_TAC>>fs[]>>
1421    fct>>Cases_on`q`>>fs[]>>
1422    TRY(imp_res_tac sem_t_clock_inc>>fs[]>>
1423    pop_assum(qspec_then`k` assume_tac))>>rfs[]>>
1424    fs[DECIDE ``(A:num)+B = B+A``]
1425    >-
1426      (fct>>Cases_on`q`>>fs[]>>TRY(metis_tac[sem_e_res])>>
1427      imp_res_tac sem_e_clock_inc>>
1428      pop_assum(qspec_then`k` assume_tac)>>
1429      fs[DECIDE ``(A:num)+B = B+A``]>>
1430      IF_CASES_TAC>>fs[]
1431      >-
1432        (fs[dec_clock_def,STOP_def]>>
1433        `1 ��� r''.clock` by DECIDE_TAC>>
1434        metis_tac[arithmeticTheory.LESS_EQ_ADD_SUB])
1435      >>
1436      IF_CASES_TAC>>fs[]>>
1437      qpat_abbrev_tac`A = sem_t B C`>>
1438      Cases_on`A`>>fs[markerTheory.Abbrev_def]>>
1439      pop_assum (assume_tac o SYM)>>imp_res_tac sem_t_sing_io_mono>>
1440      fs[dec_clock_def])
1441    >>
1442      first_x_assum(qspec_then`k` assume_tac)>>
1443      fct>>Cases_on`q`>>fs[]>>
1444      fct>>Cases_on`q`>>fs[]>>TRY(metis_tac[sem_e_res])>>
1445      imp_res_tac sem_e_sing_io_mono
1446      >-
1447        (IF_CASES_TAC>>fs[dec_clock_def]>>
1448        TRY(qpat_abbrev_tac`A = sem_t B C`>>
1449        Cases_on`A`>>fs[markerTheory.Abbrev_def]>>
1450        pop_assum (assume_tac o SYM)>>imp_res_tac sem_t_sing_io_mono)>>
1451        fs[]>>metis_tac[IS_PREFIX_TRANS])
1452      >>
1453      metis_tac[IS_PREFIX_TRANS])
1454
1455val sem_t_io_mono = Q.prove (
1456`k1 ��� k2 ���
1457 (SND (sem_t (init_st 0 nd input with clock := k1) p)).io_trace ���
1458 (SND (sem_t (init_st 0 nd input with clock := k2) p)).io_trace`,
1459 qpat_abbrev_tac `st = init_st A B C`>>
1460 rw[]>>imp_res_tac arithmeticTheory.LESS_EQUAL_ADD >>
1461 Q.ISPECL_THEN [`st with clock:=k1`,`p`,`p'`] assume_tac sem_t_io_mono_lem>>
1462 fs[])
1463
1464val sem_equiv_lem = Q.store_thm ("sem_equiv_lem",
1465`���input prog r. ofbs_sem (for_big_sem input) prog r ��� osmall_sem (for_small_sem input) prog r`,
1466 gen_tac >>
1467 match_mp_tac osmall_fbs_equiv2 >>
1468 conj_tac >- (
1469   rw [for_small_sem_def] >>
1470   match_mp_tac step_t_io_mono>>
1471   Q.ISPEC_THEN `��st. ���l. step_t s1 l st` assume_tac some_SAT>>
1472   fs[ETA_AX])>>
1473 conj_tac >- (
1474   rw [for_big_sem_def] >>
1475   rw [eval_with_clock_def, for_eval_def] >>
1476   every_case_tac >>
1477   fs [] >>
1478   metis_tac [sem_t_io_mono, SND]) >>
1479 conj_tac >- (
1480   rw [for_big_sem_def, eval_with_clock_def, for_eval_def] >>
1481   ect >>
1482   fs [] >>
1483   metis_tac [big_timeout_0]) >>
1484 qexists_tac `I` >>
1485 conj_tac
1486 >- (
1487   rw [unbounded_def] >>
1488   qexists_tac `SUC x` >>
1489   simp []) >>
1490 rpt gen_tac >>
1491 simp [for_big_sem_def, for_eval_def, eval_with_clock_def] >>
1492 DISCH_TAC >>
1493 ect >>
1494 imp_res_tac big_small_lem >>
1495 fs [] >>
1496 qexists_tac `tr` >>
1497 fs [for_small_sem_def] >>
1498 rw [same_result_def] >>
1499 fs [res_rel_t_cases, is_val_t_def, is_val_e_def, some_no_choice, init_st_def] >>
1500 simp [] >>
1501 rw []
1502 >- (rw [Once step_t_cases] >>
1503     rw [Once step_e_cases])
1504 >- rw [Once step_t_cases]
1505 >- (rw [some_def] >>
1506     metis_tac [])
1507 >- metis_tac [PAIR]);
1508
1509val FST_SPLIT = Q.prove(
1510`FST x = y ��� ���z. x = (y,z)`,
1511Cases_on`x`>>fs[])
1512
1513val big_val_no_errors = Q.prove(
1514`!st p v s.
1515  sem_t st p = (Rval v,s)
1516  ���
1517  (���c.
1518    (FST (sem_t (st with clock:= c) p) ��� Rbreak)
1519  ��� (FST (sem_t (st with clock:=c) p) ��� Rfail))`,
1520  rw[]>>CCONTR_TAC>>fs[]>>imp_res_tac FST_SPLIT>>
1521  imp_res_tac big_small_lem>>
1522  `HD tr = HD tr'` by fs[]>>
1523  fs[res_rel_t_cases]>>
1524  `���l t'. ��step_t (LAST tr) l t'` by
1525    fs[Once step_t_cases,FORALL_PROD]>>
1526  `���l t'. ��step_t (LAST tr') l t'` by
1527    fs[Once step_t_cases,FORALL_PROD,Once step_e_cases]>>
1528  `isPREFIX tr tr' ��� isPREFIX tr' tr` by
1529    metis_tac[check_trace_prefixes]>>
1530  `tr = tr'` by metis_tac[check_trace_TL]>>
1531  fs[]>>
1532  qpat_assum`A=t` (SUBST_ALL_TAC o SYM)>>fs[is_val_t_def,is_val_e_def])
1533
1534(* we can prove an alternative characterisation of the semantics, now that we
1535   know sem_t's io_trace is a chain *)
1536
1537val over_all_def = Define`over_all f = GSPEC (��c. f c,T)`;
1538
1539val init_st_with_clock = Q.prove(
1540  `init_st a b c with clock := d = init_st d b c`,
1541  EVAL_TAC)
1542
1543val prefix_chain_sem_t_io_trace_over_all_c = Q.store_thm("lprefix_chain_sem_t_io_trace_over_all_c",
1544  `prefix_chain (over_all (��c. (SND (sem_t (init_st c nd input) t)).io_trace))`,
1545  rw[lprefix_lubTheory.prefix_chain_def,over_all_def] >>
1546  qspecl_then[`c`,`c'`]strip_assume_tac arithmeticTheory.LESS_EQ_CASES >|[disj1_tac,disj2_tac] >>
1547  imp_res_tac sem_t_io_mono >> fs[init_st_with_clock])
1548
1549val image_intro = Q.prove(
1550  `{fromList (FILTER P (Q c)) | c | T} = IMAGE fromList (IMAGE (FILTER P) (over_all Q))`,
1551  rw[EXTENSION,over_all_def,PULL_EXISTS])
1552
1553val IMAGE_over_all = Q.store_thm("IMAGE_over_all",
1554  `IMAGE P (over_all f) = over_all (P o f)`,
1555  rw[EXTENSION,over_all_def,PULL_EXISTS])
1556
1557(* Pretty Printing *)
1558val BIGSUP_def = Define`BIGSUP f = build_lprefix_lub (over_all f)`
1559
1560val _ = Parse.add_rule{term_name="BIGSUP",fixity=Parse.Binder,pp_elements=[TOK"BIGSUP"],
1561                       block_style=(NoPhrasing,(PP.CONSISTENT,0)),paren_style=OnlyIfNecessary}
1562
1563val semantics_alt = save_thm("semantics_alt",
1564  semantics_def
1565    |> SIMP_RULE bool_ss [image_intro]
1566    |> SIMP_RULE bool_ss [prefix_chain_sem_t_io_trace_over_all_c,lprefix_lubTheory.prefix_chain_FILTER,lprefix_lubTheory.prefix_chain_lprefix_chain,lprefix_lubTheory.build_prefix_lub_intro]
1567    |> SIMP_RULE bool_ss [IMAGE_over_all]
1568    |> SIMP_RULE bool_ss [prove(``f o g = ��c. f (g c)``,rw[FUN_EQ_THM])]
1569    |> SIMP_RULE bool_ss [GSYM BIGSUP_def])
1570
1571val oracle_upd_def = Define`
1572  oracle_upd s (b,a) =
1573  s with <|non_det_o := a; io_trace:=s.io_trace ++[INR b]|>`
1574
1575val _ = save_thm ("step_e_rules_oracle_upd",step_e_rules|>REWRITE_RULE[GSYM oracle_upd_def])
1576
1577val _ = export_theory ();
1578