1open HolKernel bossLib boolLib countableLib lcsymtacs
2val _ = new_theory "countable"
3
4val [count_bool_aux_inj_rwt] = mk_count_aux_inj_rwt [``:bool``]
5val [count_list_aux_inj_rwt] = mk_count_aux_inj_rwt [``:�� list``]
6
7val count_list_aux_cong = store_thm(
8"count_list_aux_cong",
9``���l1 l2 f f'. (l1 = l2) ��� (���x. MEM x l2 ��� (f x = f' x)) ��� (count_list_aux f l1 = count_list_aux f' l2)``,
10rw[] >> Induct_on `l1` >>
11rw[definition "count_list_aux_def"])
12val _ = DefnBase.export_cong"count_list_aux_cong"
13
14val [count_option_aux_inj_rwt] = mk_count_aux_inj_rwt [``:�� option``]
15val [count_prod_aux_inj_rwt] = mk_count_aux_inj_rwt [``:�� # ��``]
16
17val count_prod_aux_cong = store_thm(
18"count_prod_aux_cong",
19``���p1 p2 ca ca' cb cb'. (p1 = p2) ��� (���x. (x = FST p2) ��� (ca x = ca' x)) ��� (���x. (x = SND p2) ��� (cb x = cb' x))
20    ��� (count_prod_aux ca cb p1 = count_prod_aux ca' cb' p2)``,
21rw[] >> Cases_on `p1` >> fs[])
22val _ = DefnBase.export_cong"count_prod_aux_cong"
23
24val _ = export_theory()
25