formal-languages/regular/regexp_compilerScript.sml

196  Cases >> rw[Once Brz_def])
212     >- (rw[] >> rw[Once Brz_def,LET_THM]
215             >- rw [Brz_def]
216             >- (rw [Once Brz_def] >> metis_tac [])
218                  >> rw[LET_THM]
287    >> rw [Once Brz_def]);
299    >> rw [Once Brz_def,LET_THM]);
333    >- rw [Once Brz_def]
337            >- rw []
344  rw [dom_Brz_def, dom_Brz_alt_def] >> metis_tac [acc_irrelevant]);
430  Cases_on `worklist` >> rpt gen_tac >> CASE_TAC >> rw[LET_THM]
453         >> CASE_TAC >> rw[LET_THM]
476         >> CASE_TAC >> rw[LET_THM]
531   >> rw[]
564     >- rw [Brzozo_eqns,dom_Brz_eqns]
565     >- rw [Brzozo_eqns,dom_Brz_eqns,LET_THM]);
605      >- rw [Brzozo_eqns]
606      >- (rw [Brzozo_eqns,LET_THM]
788       >> RES_THEN MP_TAC >> BETA_TAC >> rw[]
849   >> rw [extend_states_def]
853   >> rw []
860        >> rw [regexp_compare_eq,fdom_insert]
862   >- (rw [lookup_insert_thm,regexp_compare_eq,EQ_IMP_THM]
879  rw [submap_def]);
883  rw [submap_def]);
891   rw [submap_def,fdom_insert]
894   >> rw [lookup_insert_thm]
896   >> rw []
909        >> `fdom cmp (insert cmp x v bmap) x'` by rw [fdom_insert,IN_DEF]
938   >> rw [extend_states_def]
945   >- (`r' IN fdom regexp_compare state_map` by rw [fdom_def]
948       >> rw [fdom_def]
951   >- (pat_elim `$! M` >> rw[]
955       >> rw [fdom_insert]
958       >> rw [lookup_insert_thm,regexp_compare_eq]
960   >- (pat_elim `$! M` >> rw[]
964       >> rw [fdom_def]
1009  rw [Brz_invariant_def]);
1014  rw[fdom_def,ounion_def,SET_EQ_THM]
1036  Induct >> rw []
1037   >- rw [oempty_def,empty_def,fdom_def,lookup_def]
1040        >> rw [oset_def]
1041        >> rw [GSYM oset_def]
1042        >> rw [oinsert_def]
1048  rw[dom_def,set_def,EXTENSION] >>
1050  rw [in_dom_oset]);
1057  rw [member_iff_lookup,GSYM (SIMP_RULE set_ss [SET_EQ_THM] fdom_def)] >>
1058  rw [fdom_insert] >> metis_tac [IN_DEF]);
1060 val triv_lem = Q.prove(`!s1 s2. (s1 = s2) ==> ((s1 UNION s) = (s2 UNION s))`,rw[]);
1064  rw [EXTENSION,in_dom_oset,eq_cmp_regexp_compare]);
1072  >> Induct >> rw [foldrWithKey_def,invariant_def] >> fs []
1073  >- rw [lookup_def]
1075       >> rw [lookup_bin,EQ_IMP_THM]
1093      >- rw []
1094      >- (Cases_on `h` >> rw []
1098                      >> Induct >> rw [invariant_def]
1099                      >> Cases_on `h` >> rw [] >> metis_tac [insert_thm])
1100           >> rw [lookup_insert_thm]
1108   Induct >> rw [invariant_def]
1109          >> Cases_on `h` >> rw [] >> metis_tac [insert_thm]);
1128      >- rw []
1129      >- (Cases_on `h` >> rw [] >> fs []
1133                      >> Induct >> rw [invariant_def]
1134                      >> Cases_on `h` >> rw [] >> metis_tac [insert_thm])
1135           >> rw [lookup_insert_thm]
1151  rw [fdom_def, oin_def, member_iff_lookup]);
1159  Induct >> rw [oin_fdom]
1163   >> rw[fdom_insert]
1182  >> rw [EQ_IMP_THM]
1183     >- (mp_tac left_to_right_lem >> rw[invariant_def]
1184         >- (qexists_tac `a` >> rw[]
1189              >> rw[oin_def,member_iff_lookup,fdom_def])
1193          >> mp_tac mem_oin_inst >> rw [invariant_def]
1214  >> rw [oin_def, member_iff_lookup, oinsert_def]
1238    by (qpat_x_assum `dom (union a b) = dom state_map` (mp_tac o SYM) >> rw [] >>
1241        >> rw [dom_union]
1244        >> rw [dom_def,in_dom_oset])
1248  pop_assum (strip_assume_tac o SIMP_RULE set_ss [dom_def, fdom_def]) >> rw [] >>
1249   rw [Brz_invariant_def, good_table_def,invar_def]
1251   >- (rw [EVERY_MAP] >> Q.SPEC_TAC (`ALPHABET`,`alphabet`)
1252        >> Induct >> rw [smart_deriv_normalized])
1260        >> rw [GSYM set_def]
1268        >> rw [dom_union]
1272             by (rw [dom_def,fdom_insert,eq_cmp_regexp_compare,Once INSERT_SING_UNION]
1275                >> rw [in_dom_oset,eq_cmp_regexp_compare])
1276        >> rw []
1277        >> rw [AC UNION_COMM UNION_ASSOC]
1280                by (rw [extend_states_inv_def] >> metis_tac [range_def])
1286       >> rw [GSYM oinsert_def,fdom_oimage_insert]
1287       >> `apply state_map' todo1 = x` by rw [apply_def,fapply_def]
1293       >> rw[fdom_oimage_inst,SET_EQ_THM,EQ_IMP_THM,oin_fdom]
1294       >> Q.EXISTS_TAC `x''` >> rw[]
1299       >> rw [apply_def,fapply_def])
1301                by (rw [extend_states_inv_def] >> metis_tac [range_def])
1304        >> rw [extend_states_inv_def])
1310                  by (rw [extend_states_inv_def] >> metis_tac [range_def])
1313                >> rw [extend_states_inv_def])
1322        >> Q.EXISTS_TAC `x'` >> rw[]
1332         >> rw[MAP_MAP_o,combinTheory.o_DEF]
1336         >> rw[MAP_MAP_o,combinTheory.o_DEF]
1341         >> rw[MAP_MAP_o,combinTheory.o_DEF]
1342            >- (qexists_tac `todo1` >> rw[]
1347                       by (rw [MAP_MAP_o,combinTheory.o_DEF,MEM_MAP]
1349                            >> qexists_tac `c` >> rw[]
1362  >> rw[Brz_invariant_def,EQ_IMP_THM]
1365          >> rw [EVERY_MEM]
1373           >> rw [dom_union,EXTENSION]
1375           >> rw [in_dom_oset,dom_def,set_def])));
1387    >> rw []
1389    >> rw [Brzozowski_eqns]
1392    >> rw[]
1398           >> rw [Brz_invariant_def]
1404           >> rw [dom_union,EXTENSION]
1406           >> rw [in_dom_oset,dom_def,set_def]
1408           >> rw [fdom_def]
1411           >> rw[]
1417                     by rw [EXTENSION,remove_dups_mem]
1431     >- (rw []
1433          >> rw [Brzozowski_eqns,submap_id])
1434     >- (rw []
1436          >> rw [Brzozowski_eqns]
1441                 >> rw [Brz_invariant_def]
1447                 >> rw [dom_union,EXTENSION]
1449                 >> rw [in_dom_oset,dom_def,set_def]
1451                 >> rw [fdom_def]
1453             >- (rw[]
1459                         by rw [EXTENSION,remove_dups_mem]
1465                 >> rw[build_table_def,LET_THM]
1472                 >> rw []
1476                 >> rw[eq_cmp_regexp_compare]
1478                 >> rw [submap_def]
1514  rw [table_lang_def, smart_deriv_matches_def] >>
1517  rw []
1533      >> rw []
1539  rw [EQ_IMP_THM]
1540   >- rw [alistTheory.ALOOKUP_TABULATE]
1562  rw [] >>
1564  rw [] >>
1608                 rw [] >>
1615             by rw [MAP_MAP_o, combinTheory.o_DEF]
1619             by rw [MAP_MAP_o, combinTheory.o_DEF]
1631               >- (NTAC 2 (POP_ASSUM MP_TAC) >> rw [vec_lang_lem1]
1632                   >> DISCH_TAC >> fs[] >> rw[] >> metis_tac [alist_to_vec_thm])))
1635  >- (rw [] >> eq_tac >> rw []
1644          rw [])) >>
1651  >- (rw [] >>
1653      rw [] >>
1663   rw [] >>  eq_tac >>  strip_tac >>
1667  rw [] >>
1678      rw [] >>
1681                 rw [EL_MAP]) >>
1682      rw [] >>
1687      rw [] >>
1696                     rw [EL_MAP]) >>
1708         rw [] >>
1732                 >> rw [fdom_oimage_inst,apply_def,oin_fdom]
1740            rw [fdom_oimage_inst,apply_def, oin_fdom,fapply_def, dom_def] >>
1742      >> rw [])
1745           >> rw [all_distinct_count_list, MEM_COUNT_LIST]
1750                         rw [fdom_oimage_inst,apply_def, oin_fdom,fapply_def, dom_def] >>
1752                     >> rw[]))
1754    >- (rw [mem_get_accepts]
1758    >- (rw [] >> fs [good_table_def] >> metis_tac [])
1799         >> rw [sorted_get_accepts]
1801   >> rw []
1802  >- (fs [MEM_EL] >> rw []
1806       >> rw [fdom_oimage_inst,apply_def, oin_fdom,fapply_def,SYM dom_def]
1807       >> rw [dom_def,fdom_def, member_iff_lookup]
1811        >> rw [fdom_oimage_inst,apply_def, oin_fdom,fapply_def,SYM dom_def]
1837         >> rw [lookup_def]
1840                 >> rw []
1842            >- (rw [union_def,set_def,GSYM empty_def, GSYM oempty_def] >>
1843                rw [EXTENSION,fdom_def, osingleton_def, singleton_def, lookup_def] >>
1845            >- (rw [range_def,frange_def, EXTENSION, singleton_def,lookup_def,EQ_IMP_THM]
1846                 >- (BasicProvers.EVERY_CASE_TAC >> rw [])
1847                 >- (Q.EXISTS_TAC `normalize r` >> rw [regexp_compare_id] >> decide_tac))
1848            >- (rw [GSYM empty_def, GSYM oempty_def]
1849                >> rw [fdom_def, lookup_def, empty_def, oempty_def])
1853                 >> rw[]
1859  >> rw []
1862          by rw [submap_def,fdom_def,singleton_def,lookup_def,regexp_compare_id]
1900              >> rw []
1903   >> rw [table_lang_def, exec_dfa_thm,fromList_Vector,sub_def]
1905   >> rw [ORD_CHR_lem]
1918           >> rw []
1922           >> rw [PULL_EXISTS]
1923           >> rw [alistTheory.alist_range_def, EXTENSION]
1939  Induct >> rw []
1943   >> rw []
1955  rw [GSYM regexp_lang_smart_deriv, Brz_lang_def]
1963   >> rw []
1971                 >> rw []
1973            >- (rw [union_def,set_def,GSYM empty_def, GSYM oempty_def] >>
1974                rw [EXTENSION,fdom_def, osingleton_def, singleton_def, lookup_def] >>
1976            >- (rw [range_def,frange_def, EXTENSION, singleton_def,lookup_def,EQ_IMP_THM]
1977                 >- (BasicProvers.EVERY_CASE_TAC >> rw [])
1978                 >- (Q.EXISTS_TAC `normalize r` >> rw [regexp_compare_id] >> decide_tac))
1979            >- (rw [GSYM empty_def, GSYM oempty_def]
1980                >> rw [fdom_def, lookup_def, empty_def, oempty_def])
1984                 >> rw[]
2000                         rw [fdom_oimage_inst,apply_def, oin_fdom,fapply_def, dom_def] >>
2010                by (rw [mem_get_accepts,EQ_IMP_THM]
2011                     >- (`r' IN fdom regexp_compare state_map` by rw [fdom_def]
2014           >> rw []
2019           >> rw[]
2021                 by (rw [fdom_def, singleton_def,lookup_def,EQ_IMP_THM]
2032           >> rw [MAP_MAP_o,combinTheory.o_DEF,apply_def, fapply_def]
2034           >> rw []
2036               by (irule MAP_CONG >> rw [] >> metis_tac [mem_alphabet,ORD_CHR_lem])
2037          >> rw[])
2038  >> rw []
2040  >> rw [MAP_MAP_o,combinTheory.o_DEF,apply_def, fapply_def]
2042               by (irule MAP_CONG >> rw [] >> metis_tac [mem_alphabet,ORD_CHR_lem])
2043  >> rw []
2045  >> rw []
2046     >- rw [sorted_get_accepts]
2056           by (rw [fdom_def, singleton_def,lookup_def,EQ_IMP_THM]
2063         >> rw [singleton_def,lookup_def,regexp_compare_id]
2067                     >> rw [singleton_def,lookup_def,EQ_IMP_THM]
2082  rw []
2086   >> rw [Brz_lang_def, regexp_matcher_def, LET_THM,apply_def,fapply_def]);
2100  rw [EVERY_MEM]
2104   >> rw [regexp_matcher_def, LET_THM]);