equal
deleted
inserted
replaced
33 open BNF_FP_Util |
33 open BNF_FP_Util |
34 |
34 |
35 val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)}; |
35 val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)}; |
36 val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)}; |
36 val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)}; |
37 |
37 |
38 val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.cases sum.cases sum_map.simps}; |
38 val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.case sum.case sum_map.simps}; |
39 val sum_prod_thms_set0 = |
39 val sum_prod_thms_set0 = |
40 @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff |
40 @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff |
41 Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp |
41 Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp |
42 mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps}; |
42 mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps}; |
43 val sum_prod_thms_set = @{thms UN_compreh_eq_eq} @ sum_prod_thms_set0; |
43 val sum_prod_thms_set = @{thms UN_compreh_eq_eq} @ sum_prod_thms_set0; |