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