1open HolKernel Parse boolLib bossLib;
2
3open finite_mapTheory sortingTheory
4
5val _ = new_theory "countchars";
6
7val _ = ParseExtras.tight_equality()
8
9val countchars_def = Define���
10  countchars fm [] = fm ���
11  countchars fm (c::cs) =
12    let fm' =
13      case FLOOKUP fm c of
14        NONE => fm |+ (c,1)
15      | SOME n => fm |+ (c, n + 1)
16    in
17      countchars fm' cs
18���
19
20val countchars_aux_def = Define���
21  countchars_aux fm s i =
22    if i = 0 then fm
23    else
24      let c = EL (i - 1) s in
25      let fm' =
26        case FLOOKUP fm c of
27          NONE => fm |+ (c,1)
28        | SOME n => fm |+ (c, n + 1)
29      in
30        countchars_aux fm' s (i - 1)
31���
32
33val countchars_PERM = Q.store_thm(
34  "countchars_PERM",
35  ������s1 s2. PERM s1 s2 ��� ���fm. countchars fm s1 = countchars fm s2���,
36  Induct_on `PERM` >> simp[countchars_def] >> rpt strip_tac >>
37  BasicProvers.EVERY_CASE_TAC >> fs[FLOOKUP_UPDATE] >> rfs[] >> fs[] >>
38  BasicProvers.EVERY_CASE_TAC >> fs[] >> metis_tac[FUPDATE_COMMUTES]);
39
40val aux_correctness = Q.store_thm(
41  "aux_correctness",
42  ������i fm s. i ��� LENGTH s ��� countchars_aux fm s i = countchars fm (TAKE i s)���,
43  Induct_on `i` >> simp[Once countchars_aux_def]
44  >- simp[countchars_def] >>
45  rw[] >>
46  qmatch_abbrev_tac ���LHS = _��� >>
47  ���LHS = countchars fm (EL i s :: TAKE i s)���
48    by simp[Abbr`LHS`, countchars_def] >>
49  simp[Abbr`LHS`] >> irule countchars_PERM >>
50  simp[PERM_CONS_EQ_APPEND] >> map_every qexists_tac [���TAKE i s���, ���[]���] >>
51  simp[GSYM rich_listTheory.SNOC_EL_TAKE]);
52
53val countchars_EQN = Q.store_thm(
54  "countchars_EQN",
55  ���countchars fm s = countchars_aux fm s (LENGTH s)���,
56  simp[aux_correctness]);
57
58val correctness = Q.store_thm(
59  "correctness",
60  ������fm0 s fm.
61     countchars fm0 s =
62       FUN_FMAP (��c. LENGTH (FILTER ((=) c) s) +
63                     (case FLOOKUP fm0 c of NONE => 0 | SOME i => i))
64                (FDOM fm0 ��� set s)���,
65  Induct_on ���s��� >> simp[countchars_def, fmap_EXT, FUN_FMAP_DEF]
66  >- simp[FLOOKUP_DEF] >>
67  rpt gen_tac >> Cases_on `FLOOKUP fm0 h` >> fs[flookup_thm] >>
68  simp[FLOOKUP_DEF] >>
69  dsimp[FUN_FMAP_DEF, FAPPLY_FUPDATE_THM] >> rw[] >> fs[] >>
70  simp[pred_setTheory.EXTENSION] >> metis_tac[]);
71
72val _ = export_theory();
73