formal-languages/regular/regexpScript.sml

213   >> rw [rsize_def]
232  rw [regexp_lang_def,Epsilon_def,charset_mem_empty,KSTAR_EMPTYSET,SET_EQ_THM]);
237  rw [regexp_lang_def,Empty_def,charset_mem_empty]);
242  rw [regexp_lang_epsilon,SET_EQ_THM]);
309  recInduct len_cmp_ind >> rw[len_cmp_def]);
315  recInduct len_cmp_ind >> rw[len_cmp_def]);
319  recInduct len_cmp_ind >> rw[len_cmp_def]);
326  recInduct len_cmp_ind >> rw[len_cmp_def]);
330  recInduct len_cmp_ind >> rw[len_cmp_def]);
478    >> rw[]
515    >> rw[]
518          >> rw [])
520         >> full_simp_tac list_ss [] >> rw []
588                   >> rw[LENGTH_APPEND]
596                   >> rw[LENGTH_APPEND]
613    >> `[(r,u)] = ZIP ([r],[u])` by rw[ZIP_def]
618    >> rw[ZIP_def]);
642      >- (every_case_tac >> rw[] >>
671    >> `[(r,u)] = ZIP([r],[u])` by rw[ZIP_def]
676    >> rw[ZIP_def]);
688  rw [total_def, regexp_leq_def] >> every_case_tac >> fs [] >>
694  rw [transitive_def, regexp_leq_def]
736   >> rw [is_regexp_empty_def, regexp_lang_thm, EVERY_EL,charset_mem_empty]
792      >- rw [rsize_def]
793      >- rw [rsize_def]
794      >- (rw [rsize_def] >> decide_tac)
795      >- (rw [rsize_def] >> decide_tac));
816  Induct_on `ss` >> rw [] >> Cases_on `h` >> fs []
817  >| [res_tac >> rw [] >> qexists_tac `""::ss1` >> rw [],
818      qexists_tac `[]` >> rw []]);
822  Induct_on `ss1` >> rw []);
829  rw [regexp_lang_thm, deriv_def, LET_THM, charset_mem_empty,Epsilon_def,Empty_def]
831  >- (rw [EQ_IMP_THM]
832       >- (Q.EXISTS_TAC `[]` >> rw[])
834             >> rw[stringTheory.CHR_ORD]
838  >- (rw [EQ_IMP_THM,charset_mem_def]
840  >- (eq_tac >> rw [regexp_lang_thm, nullable_thm] >|
843         >- (rw[SIMP_RULE std_ss [IN_DEF] IN_dot] >> metis_tac[]),
844       Cases_on `w1` >> fs [] >> rw[] >> metis_tac[],
848  >- (rw [EQ_IMP_THM]
850          >> fs [] >> rw []
853          >> rw []
857      >- (qexists_tac `(c::w1) :: ws` >> rw [])));
866  Induct_on `s` >> rw [deriv_matches_def, nullable_thm] >> metis_tac [deriv_thm]);
883  rw [charset_mem_empty, regexp_lang_thm]
885        rw [EQ_IMP_THM]
887            qexists_tac `[]` >> rw []],
888        rw [EQ_IMP_THM]
890           qexists_tac `[""]` >> rw []]]);
906 rw [regexp_lang_thm] >> metis_tac [SET_EQ_THM]);
1017    >> rw []
1018    >> rw [assoc_cat_def, regexp_lang_eqns, regexp_lang_thm]);
1035  >- (Q.EXISTS_TAC `[]` >> rw[])
1052  rw [flatten_or_def] >>
1054  rw [flatten_or_def] >>
1055  rw [regexp_lang_thm]);
1061  rw [EXISTS_MEM, mergesort_mem]);
1068  rw [merge_charsets_def] >>
1069  rw [charset_mem_union, regexp_lang_thm] >>
1077  rw [remove_dups_def] >>
1079  rw [] >>
1093  rw [build_or_def, LET_THM, regexp_lang_thm,Empty_def,Epsilon_def]
1094  >- (rw [Once build_or_init_correct] >>
1098      rw [] >>
1100  >- (rw [Once build_or_init_correct] >>
1104      rw [] >>
1105      rw [charset_mem_empty, regexp_lang_thm] >>
1115  rw [] >>
1117  rw [build_star_def] >>
1118  rw [regexp_lang_def] >>
1124  rw [build_neg_def, regexp_lang_def]);
1156  >> rw [regexp_lang_eqns, smart_deriv_def, deriv_def, build_cat_correct,Empty_def, Epsilon_def]
1159      rw [build_cat_correct, build_or_correct]
1160      >- (rw [regexp_lang_thm, build_cat_correct])
1163  >- rw [build_or_correct, regexp_lang_thm, EXISTS_MAP]
1207   rw [smart_deriv_matches_def, nullable_thm, deriv_matches_def] >>
1208   rw [regexp_lang_deriv] >>
1209   rw [deriv_matches_def] >>
1210   rw [GSYM regexp_lang_deriv] >>
1240  rw [] >>
1241  rw [normalize_def, build_star_correct, build_cat_correct, build_or_correct,
1245  >- (rw [regexp_lang_thm] >>
1295      >- (rw [rsize_def] >> decide_tac)
1296      >- (rw [rsize_def] >> decide_tac)
1297      >- rw [rsize_def]
1298      >- rw [rsize_def]);
1337  rw [is_normalized_def, regexp_smart_constructors_def]);
1343  rw [is_normalized_def, is_regexp_empty_def] >>
1345  rw [] >>
1347  rw [] >>
1353 recInduct assoc_cat_ind >> rw [assoc_cat_def]);
1366   >> rw [is_normalized_def, regexp_smart_constructors_def]
1373 rw [] >>
1376 rw [] >>
1378 rw [] >-
1382 rw [is_normalized_def]);
1387  rw [is_normalized_def, regexp_smart_constructors_def]);
1393 rw [is_normalized_def, regexp_smart_constructors_def]);
1403 rw [flatten_or_def] >>
1409  rw [EVERY_MEM, mergesort_mem]);
1415  rw [merge_charsets_def] >>
1423  rw [remove_dups_def]);
1434  rw [flatten_or_def, no_sub_or_def] >>
1440  rw [no_sub_or_def, EVERY_MEM, mergesort_mem]);
1446  rw [no_sub_or_def, merge_charsets_def]);
1452  rw [no_sub_or_def, remove_dups_def]);
1461  >> rw [is_charset_def, regexp_leq_def, regexp_compare_def]
1469  rw [] >>
1473  rw [] >>
1475  rw [] >>
1477  rw []
1484          rw [])
1486          rw [] >>
1487          rw [])
1489          rw [])
1491          rw [] >>
1492          rw []))
1495      rw [] >>
1505  rw [merge_charsets_def] >>
1520  rw [merge_charsets_def, is_charset_def] >>
1530  rw [] >>
1532  rw [] >>
1534  rw [] >>
1536  `h::(rs1++rs2) = (h::rs1)++rs2` by rw [] >>
1537  `h::rs1 ��� []` by rw [] >>
1538  `EVERY is_charset (h::rs1)` by rw [] >>
1542  rw [] >>
1546  rw [] >>
1548  rw [] >>
1552  rw [regexp_leq_def] >>
1560  rw [remove_dups_def, regexp_compare_eq] >>
1567  rw [remove_dups_def, SORTED_DEF] >>
1573  rw [] >>
1585  rw [] >>
1587  rw [] >>
1589  rw [] >>
1600  rw [remove_dups_def] >>
1602  rw [] >>
1614  rw [remove_dups_def, regexp_compare_eq] >>
1618  >- (rw [remove_dups_mem] >>
1636  >> rw [is_normalized_def]
1656  >> rw [is_normalized_def]
1661             by (rw [] >> CCONTR_TAC >> fs []
1663                 >> fs [] >> rw []
1666        >- (Cases_on `h` >> rw []
1674        >- (Cases_on `h` >> rw []
1697 rw [normalize_def, norm_char_set, norm_cat, norm_neg, norm_star] >>
1806  >> rw [is_normalized_def, smart_deriv_def, normalize_def,
1809  >> rw []
1825   [rw [build_char_set_def, build_star_def],
1826    rw [build_char_set_def],
1857  >- rw [regexp_lang_thm]
1863              >> rw []
1865  >- (rw [regexp_lang_def] >> metis_tac [DOT_ASSOC])
1866  >- (rw [regexp_lang_def]
1872       >> rw [EQ_IMP_THM,LIST_UNION_def,