1.1 --- a/NEWS Wed Apr 18 20:38:15 2012 +0200
1.2 +++ b/NEWS Wed Apr 18 20:40:52 2012 +0200
1.3 @@ -185,34 +185,6 @@
1.4
1.5 * New type synonym 'a rel = ('a * 'a) set
1.6
1.7 -* Theory Divides: Discontinued redundant theorems about div and mod.
1.8 -INCOMPATIBILITY, use the corresponding generic theorems instead.
1.9 -
1.10 - DIVISION_BY_ZERO ~> div_by_0, mod_by_0
1.11 - zdiv_self ~> div_self
1.12 - zmod_self ~> mod_self
1.13 - zdiv_zero ~> div_0
1.14 - zmod_zero ~> mod_0
1.15 - zdiv_zmod_equality ~> div_mod_equality2
1.16 - zdiv_zmod_equality2 ~> div_mod_equality
1.17 - zmod_zdiv_trivial ~> mod_div_trivial
1.18 - zdiv_zminus_zminus ~> div_minus_minus
1.19 - zmod_zminus_zminus ~> mod_minus_minus
1.20 - zdiv_zminus2 ~> div_minus_right
1.21 - zmod_zminus2 ~> mod_minus_right
1.22 - zdiv_minus1_right ~> div_minus1_right
1.23 - zmod_minus1_right ~> mod_minus1_right
1.24 - zdvd_mult_div_cancel ~> dvd_mult_div_cancel
1.25 - zmod_zmult1_eq ~> mod_mult_right_eq
1.26 - zpower_zmod ~> power_mod
1.27 - zdvd_zmod ~> dvd_mod
1.28 - zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd
1.29 - mod_mult_distrib ~> mult_mod_left
1.30 - mod_mult_distrib2 ~> mult_mod_right
1.31 -
1.32 -* Removed redundant theorems nat_mult_2 and nat_mult_2_right; use
1.33 -generic mult_2 and mult_2_right instead. INCOMPATIBILITY.
1.34 -
1.35 * More default pred/set conversions on a couple of relation operations
1.36 and predicates. Added powers of predicate relations. Consolidation
1.37 of some relation theorems:
1.38 @@ -231,75 +203,6 @@
1.39
1.40 INCOMPATIBILITY.
1.41
1.42 -* Consolidated various theorem names relating to Finite_Set.fold
1.43 -combinator:
1.44 -
1.45 - inf_INFI_fold_inf ~> inf_INF_fold_inf
1.46 - sup_SUPR_fold_sup ~> sup_SUP_fold_sup
1.47 - INFI_fold_inf ~> INF_fold_inf
1.48 - SUPR_fold_sup ~> SUP_fold_sup
1.49 - union_set ~> union_set_fold
1.50 - minus_set ~> minus_set_fold
1.51 -
1.52 -INCOMPATIBILITY.
1.53 -
1.54 -* Consolidated theorem names concerning fold combinators:
1.55 -
1.56 - INFI_set_fold ~> INF_set_fold
1.57 - SUPR_set_fold ~> SUP_set_fold
1.58 - INF_code ~> INF_set_foldr
1.59 - SUP_code ~> SUP_set_foldr
1.60 - foldr.simps ~> foldr.simps (in point-free formulation)
1.61 - foldr_fold_rev ~> foldr_conv_fold
1.62 - foldl_fold ~> foldl_conv_fold
1.63 - foldr_foldr ~> foldr_conv_foldl
1.64 - foldl_foldr ~> foldl_conv_foldr
1.65 -
1.66 -INCOMPATIBILITY.
1.67 -
1.68 -* Dropped rarely useful theorems concerning fold combinators:
1.69 -foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant,
1.70 -rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,
1.71 -concat_conv_foldl, foldl_weak_invariant, foldl_invariant,
1.72 -foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,
1.73 -listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc,
1.74 -foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv.
1.75 -INCOMPATIBILITY. For the common phrases "%xs. List.foldr plus xs 0"
1.76 -and "List.foldl plus 0", prefer "List.listsum". Otherwise it can be
1.77 -useful to boil down "List.foldr" and "List.foldl" to "List.fold" by
1.78 -unfolding "foldr_conv_fold" and "foldl_conv_fold".
1.79 -
1.80 -* Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr,
1.81 -inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr,
1.82 -Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr,
1.83 -INF_set_foldr, SUP_set_foldr. INCOMPATIBILITY. Prefer corresponding
1.84 -lemmas over fold rather than foldr, or make use of lemmas
1.85 -fold_conv_foldr and fold_rev.
1.86 -
1.87 -* Congruence rules Option.map_cong and Option.bind_cong for recursion
1.88 -through option types.
1.89 -
1.90 -* Concrete syntax for case expressions includes constraints for source
1.91 -positions, and thus produces Prover IDE markup for its bindings.
1.92 -INCOMPATIBILITY for old-style syntax translations that augment the
1.93 -pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
1.94 -one_case.
1.95 -
1.96 -* Discontinued configuration option "syntax_positions": atomic terms
1.97 -in parse trees are always annotated by position constraints.
1.98 -
1.99 -* Finite_Set.fold now qualified. INCOMPATIBILITY.
1.100 -
1.101 -* Renamed some facts on canonical fold on lists, in order to avoid
1.102 -problems with interpretation involving corresponding facts on foldl
1.103 -with the same base names:
1.104 -
1.105 - fold_set_remdups ~> fold_set_fold_remdups
1.106 - fold_set ~> fold_set_fold
1.107 - fold1_set ~> fold1_set_fold
1.108 -
1.109 -INCOMPATIBILITY.
1.110 -
1.111 * Renamed facts about the power operation on relations, i.e., relpow
1.112 to match the constant's name:
1.113
1.114 @@ -369,6 +272,103 @@
1.115
1.116 INCOMPATIBILITY.
1.117
1.118 +* Theory Divides: Discontinued redundant theorems about div and mod.
1.119 +INCOMPATIBILITY, use the corresponding generic theorems instead.
1.120 +
1.121 + DIVISION_BY_ZERO ~> div_by_0, mod_by_0
1.122 + zdiv_self ~> div_self
1.123 + zmod_self ~> mod_self
1.124 + zdiv_zero ~> div_0
1.125 + zmod_zero ~> mod_0
1.126 + zdiv_zmod_equality ~> div_mod_equality2
1.127 + zdiv_zmod_equality2 ~> div_mod_equality
1.128 + zmod_zdiv_trivial ~> mod_div_trivial
1.129 + zdiv_zminus_zminus ~> div_minus_minus
1.130 + zmod_zminus_zminus ~> mod_minus_minus
1.131 + zdiv_zminus2 ~> div_minus_right
1.132 + zmod_zminus2 ~> mod_minus_right
1.133 + zdiv_minus1_right ~> div_minus1_right
1.134 + zmod_minus1_right ~> mod_minus1_right
1.135 + zdvd_mult_div_cancel ~> dvd_mult_div_cancel
1.136 + zmod_zmult1_eq ~> mod_mult_right_eq
1.137 + zpower_zmod ~> power_mod
1.138 + zdvd_zmod ~> dvd_mod
1.139 + zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd
1.140 + mod_mult_distrib ~> mult_mod_left
1.141 + mod_mult_distrib2 ~> mult_mod_right
1.142 +
1.143 +* Removed redundant theorems nat_mult_2 and nat_mult_2_right; use
1.144 +generic mult_2 and mult_2_right instead. INCOMPATIBILITY.
1.145 +
1.146 +* Consolidated various theorem names relating to Finite_Set.fold
1.147 +combinator:
1.148 +
1.149 + inf_INFI_fold_inf ~> inf_INF_fold_inf
1.150 + sup_SUPR_fold_sup ~> sup_SUP_fold_sup
1.151 + INFI_fold_inf ~> INF_fold_inf
1.152 + SUPR_fold_sup ~> SUP_fold_sup
1.153 + union_set ~> union_set_fold
1.154 + minus_set ~> minus_set_fold
1.155 +
1.156 +INCOMPATIBILITY.
1.157 +
1.158 +* Consolidated theorem names concerning fold combinators:
1.159 +
1.160 + INFI_set_fold ~> INF_set_fold
1.161 + SUPR_set_fold ~> SUP_set_fold
1.162 + INF_code ~> INF_set_foldr
1.163 + SUP_code ~> SUP_set_foldr
1.164 + foldr.simps ~> foldr.simps (in point-free formulation)
1.165 + foldr_fold_rev ~> foldr_conv_fold
1.166 + foldl_fold ~> foldl_conv_fold
1.167 + foldr_foldr ~> foldr_conv_foldl
1.168 + foldl_foldr ~> foldl_conv_foldr
1.169 +
1.170 +INCOMPATIBILITY.
1.171 +
1.172 +* Dropped rarely useful theorems concerning fold combinators:
1.173 +foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant,
1.174 +rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,
1.175 +concat_conv_foldl, foldl_weak_invariant, foldl_invariant,
1.176 +foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,
1.177 +listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc,
1.178 +foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv.
1.179 +INCOMPATIBILITY. For the common phrases "%xs. List.foldr plus xs 0"
1.180 +and "List.foldl plus 0", prefer "List.listsum". Otherwise it can be
1.181 +useful to boil down "List.foldr" and "List.foldl" to "List.fold" by
1.182 +unfolding "foldr_conv_fold" and "foldl_conv_fold".
1.183 +
1.184 +* Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr,
1.185 +inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr,
1.186 +Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr,
1.187 +INF_set_foldr, SUP_set_foldr. INCOMPATIBILITY. Prefer corresponding
1.188 +lemmas over fold rather than foldr, or make use of lemmas
1.189 +fold_conv_foldr and fold_rev.
1.190 +
1.191 +* Congruence rules Option.map_cong and Option.bind_cong for recursion
1.192 +through option types.
1.193 +
1.194 +* Concrete syntax for case expressions includes constraints for source
1.195 +positions, and thus produces Prover IDE markup for its bindings.
1.196 +INCOMPATIBILITY for old-style syntax translations that augment the
1.197 +pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
1.198 +one_case.
1.199 +
1.200 +* Discontinued configuration option "syntax_positions": atomic terms
1.201 +in parse trees are always annotated by position constraints.
1.202 +
1.203 +* Finite_Set.fold now qualified. INCOMPATIBILITY.
1.204 +
1.205 +* Renamed some facts on canonical fold on lists, in order to avoid
1.206 +problems with interpretation involving corresponding facts on foldl
1.207 +with the same base names:
1.208 +
1.209 + fold_set_remdups ~> fold_set_fold_remdups
1.210 + fold_set ~> fold_set_fold
1.211 + fold1_set ~> fold1_set_fold
1.212 +
1.213 +INCOMPATIBILITY.
1.214 +
1.215 * New theory HOL/Library/DAList provides an abstract type for
1.216 association lists with distinct keys.
1.217