src/HOL/Presburger.thy
 changeset 47108 2a1953f0d20d parent 45425 7fee7d7abf2f child 47142 d64fa2ca54b8
```     1.1 --- a/src/HOL/Presburger.thy	Sat Mar 24 16:27:04 2012 +0100
1.2 +++ b/src/HOL/Presburger.thy	Sun Mar 25 20:15:39 2012 +0200
1.3 @@ -374,18 +374,16 @@
1.4    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
1.5    by (cases "y \<le> x") (simp_all add: zdiff_int)
1.6
1.7 -lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (Int.Bit0 n) \<and> (0::int) <= number_of (Int.Bit1 n)"
1.8 -by simp
1.9 -
1.10 -lemma number_of2: "(0::int) <= Numeral0" by simp
1.11 -
1.12  text {*
1.13    \medskip Specific instances of congruence rules, to prevent
1.14    simplifier from looping. *}
1.15
1.16 -theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')" by simp
1.17 +theorem imp_le_cong:
1.18 +  "\<lbrakk>x = x'; 0 \<le> x' \<Longrightarrow> P = P'\<rbrakk> \<Longrightarrow> (0 \<le> (x::int) \<longrightarrow> P) = (0 \<le> x' \<longrightarrow> P')"
1.19 +  by simp
1.20
1.21 -theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')"
1.22 +theorem conj_le_cong:
1.23 +  "\<lbrakk>x = x'; 0 \<le> x' \<Longrightarrow> P = P'\<rbrakk> \<Longrightarrow> (0 \<le> (x::int) \<and> P) = (0 \<le> x' \<and> P')"
1.24    by (simp cong: conj_cong)
1.25
1.26  use "Tools/Qelim/cooper.ML"
```