fun-op-sem/ml/typeSoundScript.sml

51   rw[LIST_EQ_REWRITE,EL_LUPDATE] >> rw[])
59   simp[f_o_f_DEF] >> rw[] >> fs[])
143  rw [check_clock_def, state_component_equality]);
150   rw[dec_clock_def])
154   rw[dec_clock_def])
261  rw[] >> fsrw_tac[ARITH_ss][])
287   rw[Once sem_def] >>
297   `F` suffices_by rw[] >>
304   rw[] >>
306   rw[] >> fs[] >>
454   ho_match_mp_tac sem_ind >> rw[sem_def]
455   >- rw[Once eval_cases]
457     rw[Once eval_cases] >>
460     every_case_tac >> fs[] >> rw[] >> rfs[] >>
461     rw[Once eval_cases] >>
464     every_case_tac >> fs[] >> rw[] >>
465     rw[Once eval_cases] >>
467   >- rw[Once eval_cases]
468   >- rw[Once eval_cases]
470     every_case_tac >> fs[] >> rw[] >>
471     rw[Once eval_cases] >>
474     every_case_tac >> fs[] >> rw[] >>
475     rw[Once eval_cases] >>
478     every_case_tac >> fs[] >> rw[] >> rfs[] >>
479     rw[Once eval_cases] >>
481   >- rw[Once eval_cases]
483     every_case_tac >> fs[] >> rw[] >>
484     rw[Once eval_cases] >>
494     rw[Once eval_cases] >>
500   Cases_on`y`>>rw[])
507   ho_match_mp_tac eval_ind >> rw[sem_def] >>
508   BasicProvers.CASE_TAC >> fs[] >> rw[] >>
509   TRY(BasicProvers.CASE_TAC >> fs[] >> rw[]) >>
510   TRY(BasicProvers.CASE_TAC >> fs[] >> rw[]) >>
511   TRY(BasicProvers.CASE_TAC >> fs[] >> rw[]) >>
512   TRY(BasicProvers.CASE_TAC >> fs[] >> rw[]) >>
573  rw[t_size_def] >> res_tac >>simp[])
589  rw[t_size_def] >> res_tac >>simp[])
612   rw[tenv_vars_def])
722   rw[] >> simp[rich_listTheory.EL_APPEND1] >> metis_tac[])
731   rw[tenv_vars_def,EXISTS_PROD] >> rw[])
741   rw[MAP_MAP_o,MAP_EQ_f])
750   ho_match_mp_tac t_ind >> simp[] >> rw[] >>
752   TRY (fs[FLOOKUP_DEF] >> NO_TAC) >> rw[] >- (
753     rw[Once EXTENSION,PULL_EXISTS] ) >>
763   rw[LIST_EQ_REWRITE,EL_MAP] >>
775   rw[LIST_EQ_REWRITE,EL_MAP] >>
790  rw[] >> res_tac >> simp[])
832     rw[] >>
851     rw[] >> fs[] >>
855     Cases >> simp[] >> rw[] >>
857     rw[] >> first_x_assum (match_mp_tac o MP_CANON) >>
863   Cases >> Cases >> Cases >> rw[tsaconv_def] >> fs[LET_THM] >>
872   ho_match_mp_tac raconv_ind >> reverse(rw[]) >- (
893   rw[] >>
903   Cases >> Cases >> simp[tsaconv_def] >> rw[] >>
906   qexists_tac`FUN_FMAP (Tvar o f) (tvs1 ��� tyvars t1)` >> rw[] >>
919     rw[] >> rfs[FLOOKUP_DEF,FLOOKUP_FUN_FMAP] ) >>
920   rw[] >> fs[] >- (
921     rw[LIST_REL_EL_EQN,EL_MAP] >>
939   rw[tsaconv_def] >>
947   unabbrev_all_tac >> rw[] >- (
959   Cases >> simp[] >> rw[] >>
961   rw[LIST_EQ_REWRITE])
966   rw[tsaconv_def] >> metis_tac[raconv_eq])
970   Cases_on`ts`>> simp[tsaconv_def] >> rw[])
982   Cases_on`h`>>rw[] >> rw[])
996     simp[type_e_clauses] >> rw[] >>
1006     rw[] >> rw[tysubst_tysubst] >>
1025     rw[] >> fs[] >> metis_tac[] ) >>
1027     simp[type_e_clauses] >> rw[] >> fs[] >>
1035       rw[] >> res_tac >>
1042     simp[type_e_clauses] >> rw[] >> fs[] >>
1050     rw[] >> fs[] >>
1053     simp[type_e_clauses] >> rw[] >> fs[] >>
1061       rw[] >> res_tac >>
1067     rw[] >> fs[] >>
1070   rw[] >> fs[] >>
1077   rw[] >>
1079   rfs[] >> rw[] >>
1080   rw[tysubst_tysubst] >>
1089   fs[SUBSET_DEF] >> rw[] >>
1120   simp[Abbr`s`] >> rw[] >>
1136   rw[BIJ_DEF,INJ_DEF,SURJ_DEF,combinTheory.APPLY_UPDATE_THM] >> rw[] >>
1163   match_mp_tac BIJ_UPDATE_NOTIN >> rw[])
1173   rw[RIGHT_EXISTS_IMP_THM] >>
1225   rw[tssubst_def,PULL_EXISTS] >>
1261   rw[] >>
1272   rw[tssubst_def,PULL_EXISTS] >>
1284   rw[EXISTS_PROD] >>
1286   rw[tssubst_def,PULL_EXISTS] >>
1292   rw[Once CONJ_COMM] >>
1307   rw[tenv_subst_def])
1312   rw[tenv_subst_def] >>
1317   simp[LIST_REL_EL_EQN] >> rw[] >>
1328   simp[tssubst_def,PULL_EXISTS] >> rw[] >>
1346   PairCases_on`h`>>simp[] >> rw[] >> fs[] >>
1348   rw[tenv_vars_cons] >>
1361   Cases_on`ts`>>simp[tssubst_def] >> rw[] >>
1362   qexists_tac`r` >> rw[] >- (
1369   rw[])
1377   Cases >> rw[] >> fs[] >>
1395   simp[PULL_EXISTS] >> rw[])
1400   rw[] >>
1416   rw[] >> rw[] >> fs[] >>
1430   rw[] >> rw[] >> fs[] >>
1445     simp[type_e_clauses] >> rw[] >> fs[] >>
1449     simp[type_e_clauses] >> rw[] >>
1452     fs[] >> rw[] >> fs[] >> rw[] >>
1463     simp[type_e_clauses] >> rw[] >> fs[] >>
1483       rw[] >>
1491       simp[FLOOKUP_FUNION] >> rw[] >>
1521         fs[IN_DISJOINT,Abbr`a`,PULL_EXISTS,Abbr`s1`,IN_FRANGE_FLOOKUP,FLOOKUP_DRESTRICT] >> rw[] >>
1567       rw[] >>
1625     rw[sem_def,type_e_clauses] >>
1626     every_case_tac >> fs[] >> rw[] >>
1632     rw[type_e_clauses,sem_def] >> pop_assum mp_tac >>
1633     ntac 6 (BasicProvers.CASE_TAC >> fs[]) >> rw[] >>
1657     rw[type_e_clauses,sem_def] >> pop_assum mp_tac >>
1658     ntac 2 (BasicProvers.CASE_TAC >> fs[]) >> rw[] >>
1666       rw[] >>
1677       rw[]>>fs[type_v_clauses,LENGTH_NIL]>>rw[]>>fs[]>>
1680         fs[] >> rw[] ) >>
1689     rw[LENGTH_NIL] >> metis_tac[APPEND_NIL] ) >>
1693     rw[LENGTH_NIL] >> metis_tac[APPEND_NIL]) >>
1696     rw[type_e_clauses,sem_def] >> pop_assum mp_tac >>
1697     ntac 2 (BasicProvers.CASE_TAC >> fs[]) >> rw[] >>
1715     rw[type_e_clauses,sem_def] >> pop_assum mp_tac >>
1716     ntac 3 (BasicProvers.CASE_TAC >> fs[]) >> rw[] >>
1727     rw[type_e_clauses,sem_def] >> pop_assum mp_tac >>
1728     ntac 5 (BasicProvers.CASE_TAC >> fs[]) >> rw[] >>
1746       fs[LIST_REL_EL_EQN,EL_LUPDATE] >> rw[] >>
1755     simp[LUPDATE_ID] >> rw[] >>
1760     rw[type_e_clauses,sem_def] >>
1777     rw[type_e_clauses,sem_def] >> pop_assum mp_tac >>
1778     ntac 5 (BasicProvers.CASE_TAC >> fs[]) >> rw[] >>
1789   rw[type_e_clauses,sem_def] >> pop_assum mp_tac >>
1790   ntac 8 (BasicProvers.CASE_TAC >> fs[]) >> TRY(BasicProvers.CASE_TAC >> fs[]) >> rw[] >>
1853     rw[] >>
1859     rw[] >>
1862     qexists_tac`[]`>>rw[]) >>
1865     rw[Once type_e_clauses] >>
1867     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
1869     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
1870     Cases_on`v1`>>fs[type_v_clauses]>>rw[]>>
1875        metis_tac[type_v_extend] )) >> rw[] >>
1882     rw[Once type_e_clauses] >>
1885     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
1888     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
1891     rw[Once type_e_clauses] >>
1894     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
1897     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
1902     rw[Once type_e_clauses] >>
1904     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
1909     rw[Once type_e_clauses] >>
1911     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
1916       rw[] >>
1927       Cases_on`e`>>simp[Once eval_cases]>>fs[]>>rw[]>>
1928       fs[type_v_clauses,LENGTH_NIL]>>rw[]>>fs[]>>
1931         fs[] >> rw[] ) >>
1939     rw[Once type_e_clauses] >>
1941     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
1947     rw[LENGTH_NIL] >> metis_tac[APPEND_NIL]) >>
1951     rw[LENGTH_NIL] >> metis_tac[APPEND_NIL]) >>
1954     rw[type_e_clauses] >>
1956     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
1971     rw[type_e_clauses] >>
1973     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
1978     rw[type_e_clauses] >>
1980     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
1985     rw[type_e_clauses] >>
1988     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
1993     rw[type_e_clauses] >>
1996     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
1999     rw[type_e_clauses] >>
2001     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2006     rw[type_e_clauses] >>
2008     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2010     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2011     rw[type_v_clauses] >>
2016       fs[LIST_REL_EL_EQN,EL_LUPDATE] >> rw[] >>
2027     simp[LUPDATE_ID] >> rw[] >>
2031     rw[type_e_clauses] >>
2034     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2037     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2043     rw[type_e_clauses] >>
2045     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2047     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2052     rw[type_e_clauses] >>
2054     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2059     rw[type_e_clauses] >>
2077     rw[type_e_clauses] >>
2079     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2081     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2085     rw[] >> simp[rich_listTheory.EL_APPEND1]) >>
2087     rw[type_e_clauses] >>
2090     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2093     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2096     rw[type_e_clauses] >>
2098     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2100     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2105     rw[type_e_clauses] >>
2107     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2112     rw[type_e_clauses] >>
2114     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2116     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2118     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2119     Cases_on`v2`>>fs[]>>rw[]>>fs[type_v_clauses]>>
2133     rw[type_e_clauses] >>
2135     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2137     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2139     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2143     rw[type_e_clauses] >>
2145     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2147     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2149     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2154     rw[type_e_clauses] >>
2157     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2160     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2163     rw[type_e_clauses] >>
2165     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2167     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2172     rw[type_e_clauses] >>
2175     disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>
2177   rw[type_e_clauses] >>
2179   disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >>