55 val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)}; |
55 val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)}; |
56 val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)}; |
56 val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)}; |
57 |
57 |
58 val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps}; |
58 val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps}; |
59 val sumprod_thms_set = |
59 val sumprod_thms_set = |
60 @{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff |
60 @{thms UN_empty UN_insert UN_simps(10) UN_iff Un_empty_left Un_empty_right Un_iff Union_Un_distrib |
61 Union_Un_distrib image_iff o_apply map_prod_simp |
61 image_iff o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; |
62 mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; |
|
63 val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_apply prod.inject id_apply conj_assoc}; |
62 val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_apply prod.inject id_apply conj_assoc}; |
64 |
63 |
65 fun hhf_concl_conv cv ctxt ct = |
64 fun hhf_concl_conv cv ctxt ct = |
66 (case Thm.term_of ct of |
65 (case Thm.term_of ct of |
67 Const (@{const_name Pure.all}, _) $ Abs _ => |
66 Const (@{const_name Pure.all}, _) $ Abs _ => |