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"