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