author | avigad |

Tue Jul 19 17:24:09 2005 +0200 (2005-07-19) | |

changeset 16888 | 7cb4bcfa058e |

parent 16887 | b24c067b32d6 |

child 16889 | b50947fa958d |

added list of theorem changes to NEWS

added real_of_int_abs to RealDef.thy

added real_of_int_abs to RealDef.thy

1.1 --- a/NEWS Tue Jul 19 17:21:59 2005 +0200 1.2 +++ b/NEWS Tue Jul 19 17:24:09 2005 +0200 1.3 @@ -351,6 +351,41 @@ 1.4 1.5 * Classical reasoning: the meson method now accepts theorems as arguments. 1.6 1.7 +* Introduced various additions and improvements in OrderedGroup.thy and 1.8 +Ring_and_Field.thy, to faciliate calculations involving equalities 1.9 +and inequalities. 1.10 + 1.11 +* Added rules for simplifying exponents to Parity.thy 1.12 + 1.13 +Below are some theorems that have been eliminated or modified in this release: 1.14 + 1.15 + abs_eq now named abs_of_nonneg 1.16 + abs_of_ge_0 now named abs_of_nonneg 1.17 + abs_minus_eq now named abs_of_nonpos 1.18 + imp_abs_id now named abs_of_nonneg 1.19 + imp_abs_neg_id now named abs_of_nonpos 1.20 + mult_pos now named mult_pos_pos 1.21 + mult_pos_le now named mult_nonneg_nonneg 1.22 + mult_pos_neg_le now named mult_nonneg_nonpos 1.23 + mult_pos_neg2_le now named mult_nonneg_nonpos2 1.24 + mult_neg now named mult_neg_neg 1.25 + mult_neg_le now named mult_nonpos_nonpos 1.26 + 1.27 + 1.28 +*** HOL-Complex *** 1.29 + 1.30 +* Introduced better support for embedding natural numbers and integers 1.31 +in the reals, in RealDef.thy. 1.32 + 1.33 +* Expanded support for floor and ceiling functions, in RComplete.thy. 1.34 + 1.35 +Below are some theorems that have been eliminated or modified in this release: 1.36 + 1.37 + real_of_int_add reversed direction of equality (use "THEN sym") 1.38 + real_of_int_minus reversed direction of equality (use "THEN sym") 1.39 + real_of_int_diff reversed direction of equality (use "THEN sym") 1.40 + real_of_int_mult reversed direction of equality (use "THEN sym") 1.41 + 1.42 1.43 *** HOLCF *** 1.44

2.1 --- a/src/HOL/Real/RealDef.thy Tue Jul 19 17:21:59 2005 +0200 2.2 +++ b/src/HOL/Real/RealDef.thy Tue Jul 19 17:24:09 2005 +0200 2.3 @@ -701,6 +701,9 @@ 2.4 lemma real_of_int_le_zero_cancel_iff [simp]: "(real (n::int) <= 0) = (n <= 0)" 2.5 by (simp add: real_of_int_def) 2.6 2.7 +lemma real_of_int_abs [simp]: "real (abs x) = abs(real (x::int))" 2.8 +by (auto simp add: abs_if) 2.9 + 2.10 lemma int_less_real_le: "((n::int) < m) = (real n + 1 <= real m)" 2.11 apply (subgoal_tac "real n + 1 = real (n + 1)") 2.12 apply (simp del: real_of_int_add)