fun-op-sem/small-step/forSmallScript.sml

19  rw [some_def]);
197   ho_match_mp_tac step_e_strongind>>rw[]>>fs[FORALL_PROD]
203     (pop_assum mp_tac>>simp[Once step_e_cases]>>rw[]
211     (pop_assum mp_tac>>simp[Once step_e_cases]>>rw[]
221     (pop_assum mp_tac >> simp[Once step_e_cases]>>rw[]
232   ho_match_mp_tac step_t_strongind >>rw[]
240     simp[Once step_t_cases]>>fs[FORALL_PROD]>>rw[]
265     simp[Once step_t_cases]>>rw[]
279  rw[]>>
286  rw[]>>fs[some_def]>>
293  rw[]>>fs[some_def]>>metis_tac[step_t_determ]) |>GEN_ALL
300  Induct>>rw[]>>
312  Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>>
323  Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>>
334  Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>>
345  Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>>
356  Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>>
369  Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>>
383  Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>>
397  Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>>
410  Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>>
424  Induct>>rw[is_val_e_def]>>
433  Induct>>rw[is_val_e_def]>>simp[Once step_e_cases,is_val_e_def])
441  Induct>>rw[is_val_e_def]>>
450  Induct>>rw[is_val_e_def]>>
459  Induct>>rw[is_val_t_def]>>
469  Induct>>rw[is_val_e_def]>>
478  Induct>>rw[is_val_t_def]>>
483  Induct>>fs[LAST_DEF]>>rw[])
487  Induct>>rw[])
500  rw [sem_e_def] >>
507  Induct_on`e`>>rw[sem_e_def]>>
517  Induct>>fs[LAST_DEF,BUTLASTN_1]>>rw[]>>
530  Induct_on`e`>>rw[]>>fs[sem_e_def]
559        (qexists_tac`ls ++ [(r'.store,Num(i+i'))]`>>reverse (rw[])
563        match_mp_tac check_trace_append2>>fs[check_trace_def]>>rw[]
571          match_mp_tac check_trace_append2>>fs[check_trace_def]>>rw[]>>
576          (fs[Abbr`ls2`,LAST_APPEND,LAST_MAP]>>rw[]>>
584        qexists_tac`ls`>>rw[]
594          match_mp_tac check_trace_append2>>fs[check_trace_def]>>rw[]>>
621  rw[]>>FULL_CASE_TAC>>Cases_on`q`>>
637 local val rw = srw_tac[] val fs = fsrw_tac[] in
649  rw [sem_t_def_with_stop, t_to_small_t_def]
679      fs[HD_MAP,HD_APPEND,LAST_APPEND]>>rw[]
696      fs[HD_APPEND,HD_MAP]>>rw[]
710      fs[HD_APPEND,HD_MAP,check_trace_def,check_trace_seq]>>rw[]>>
718      fs[HD_APPEND,HD_MAP,check_trace_def,check_trace_seq]>>rw[]>>
729      fs[HD_MAP,HD_APPEND,LAST_MAP,LAST_APPEND]>>rw[]
740      qexists_tac`(MAP (��st,e. (st,(If e p1 p2))) tr)`>>rw[]>>
764        fs[LAST_APPEND,LAST_MAP]>>fs[]>>rw[]
766          (match_mp_tac check_trace_append2>>rw[]
823              (qexists_tac`ls ++ e1tr ++ ttr ++ e2tr ++ ftr ++[s'.store,Exp (Num i''')]`>>fs[]>>rw[]>>
835              (qexists_tac`ls ++ e1tr++ttr++e2tr++ftr`>>fs[]>>rw[]>>
855              (qexists_tac`ls ++ e1tr ++ ttr ++ e2tr ++ ftr`>>fs[]>>rw[]>>
866            qexists_tac`ls++e1tr++ttr++e2tr`>>fs[]>>rw[]>>
875        fs[LAST_APPEND,LAST_MAP,res_rel_t_cases,is_val_t_def]>>rw[]
883        fs[LAST_APPEND,LAST_MAP,res_rel_t_cases]>>rw[]>>
922    rw [sem_t_def_with_stop, sem_e_not_timeout]) >>
924    rw [sem_t_def_with_stop, sem_e_not_timeout]) >>
926    rw [sem_t_def_with_stop, sem_e_not_timeout] >>
929    rw [sem_t_def_with_stop, sem_e_not_timeout] >>
932    rw [sem_t_def_with_stop, sem_e_not_timeout] >>
935    rw [] >>
940    rw [] >>
947    rw [for_big_sem_def, eval_with_clock_def, for_eval_def] >>
954    rw [unbounded_def] >>
964  rw [same_result_def, for_unload_def] >>
967  rw []
968  >- (rw [Once step_t_cases] >>
969      rw [Once step_e_cases])
970  >- rw [Once step_t_cases]
971  >- (rw [some_def] >>
983  Induct>>rw[]>>fs[check_clock_def,isPREFIX,LENGTH_NIL]>>
995  rw[]>>
1009  Induct>>fs[check_trace_def,LAST_DEF]>>rw[]>>Cases_on`tr'`>>fs[]
1028   rw[]>>CCONTR_TAC>>fs[]>>imp_res_tac FST_SPLIT>>
1053 rw[some_def,SELECT_THM]>>
1060  rw [semantics_def, to_obs_def, fbs_sem_def, for_big_sem_def] >>
1073 rw[]>>eq_tac>>qspec_tac (`s2`,`s2`) >>qspec_tac (`s1`,`s1`) >>
1074 ho_match_mp_tac RTC_INDUCT>>rw[]>>simp[Once RTC_CASES1]>>
1083 rw[some_def,FORALL_PROD])
1098  rw [semantics_small_def, small_sem_def, for_small_sem_def] >>
1100  rw [] >>
1107  rw [small_equiv, fbs_equiv] >>