src/HOL/Presburger.thy
changeset 23365 f31794033ae1
parent 23333 ec5b4ab52026
child 23389 aaca6a8e5414
     1.1 --- a/src/HOL/Presburger.thy	Wed Jun 13 03:28:21 2007 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Wed Jun 13 03:31:11 2007 +0200
     1.3 @@ -383,29 +383,14 @@
     1.4    by (simp split add: split_nat)
     1.5  
     1.6  lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
     1.7 -  by (auto split add: split_nat) 
     1.8 -(rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
     1.9 +  apply (auto split add: split_nat)
    1.10 +  apply (rule_tac x="int x" in exI, simp)
    1.11 +  apply (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
    1.12 +  done
    1.13  
    1.14  lemma zdiff_int_split: "P (int (x - y)) =
    1.15    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
    1.16 -  by (case_tac "y \<le> x",simp_all add: zdiff_int)
    1.17 -
    1.18 -lemma zdvd_int: "(x dvd y) = (int x dvd int y)"
    1.19 -  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
    1.20 -    nat_0_le cong add: conj_cong)
    1.21 -  apply (rule iffI)
    1.22 -  apply iprover
    1.23 -  apply (erule exE)
    1.24 -  apply (case_tac "x=0")
    1.25 -  apply (rule_tac x=0 in exI)
    1.26 -  apply simp
    1.27 -  apply (case_tac "0 \<le> k")
    1.28 -  apply iprover
    1.29 -  apply (simp add: linorder_not_le)
    1.30 -  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
    1.31 -  apply assumption
    1.32 -  apply (simp add: mult_ac)
    1.33 -  done
    1.34 +  by (case_tac "y \<le> x", simp_all)
    1.35  
    1.36  lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp
    1.37  lemma number_of2: "(0::int) <= Numeral0" by simp
    1.38 @@ -670,4 +655,4 @@
    1.39    less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
    1.40    less_number_of
    1.41  
    1.42 -end
    1.43 \ No newline at end of file
    1.44 +end