src/HOL/Presburger.thy
changeset 36800 59b50c691b75
parent 36799 628fe06cbeff
child 36802 5f9fe7b3295d
     1.1 --- a/src/HOL/Presburger.thy	Mon May 10 14:11:50 2010 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Mon May 10 14:18:41 2010 +0200
     1.3 @@ -15,7 +15,6 @@
     1.4  
     1.5  subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
     1.6  
     1.7 -
     1.8  lemma minf:
     1.9    "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
    1.10       \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<and> Q x) = (P' x \<and> Q' x)"
    1.11 @@ -384,10 +383,11 @@
    1.12  
    1.13  lemma zdiff_int_split: "P (int (x - y)) =
    1.14    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
    1.15 -  by (case_tac "y \<le> x", simp_all add: zdiff_int)
    1.16 +  by (cases "y \<le> x") (simp_all add: zdiff_int)
    1.17  
    1.18  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.19  by simp
    1.20 +
    1.21  lemma number_of2: "(0::int) <= Numeral0" by simp
    1.22  
    1.23  text {*
    1.24 @@ -399,10 +399,6 @@
    1.25  theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')" 
    1.26    by (simp cong: conj_cong)
    1.27  
    1.28 -lemma int_eq_number_of_eq:
    1.29 -  "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
    1.30 -  by (rule eq_number_of_eq)
    1.31 -
    1.32  use "Tools/Qelim/cooper.ML"
    1.33  
    1.34  setup Cooper.setup