src/HOL/Presburger.thy
 changeset 22026 cc60e54aa7cb parent 21454 a1937c51ed88 child 22394 54ea68b5a92f
```     1.1 --- a/src/HOL/Presburger.thy	Fri Jan 05 17:38:05 2007 +0100
1.2 +++ b/src/HOL/Presburger.thy	Sat Jan 06 20:47:09 2007 +0100
1.3 @@ -926,18 +926,6 @@
1.4  theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
1.5    by (simp split add: split_nat)
1.6
1.7 -theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
1.8 -  apply (simp split add: split_nat)
1.9 -  apply (rule iffI)
1.10 -  apply (erule exE)
1.11 -  apply (rule_tac x = "int x" in exI)
1.12 -  apply simp
1.13 -  apply (erule exE)
1.14 -  apply (rule_tac x = "nat x" in exI)
1.15 -  apply (erule conjE)
1.16 -  apply (erule_tac x = "nat x" in allE)
1.17 -  apply simp
1.18 -  done
1.19
1.20  theorem zdiff_int_split: "P (int (x - y)) =
1.21    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
1.22 @@ -945,22 +933,6 @@
1.24    done
1.25
1.26 -theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
1.27 -  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
1.28 -    nat_0_le cong add: conj_cong)
1.29 -  apply (rule iffI)
1.30 -  apply iprover
1.31 -  apply (erule exE)
1.32 -  apply (case_tac "x=0")
1.33 -  apply (rule_tac x=0 in exI)
1.34 -  apply simp
1.35 -  apply (case_tac "0 \<le> k")
1.36 -  apply iprover
1.37 -  apply (simp add: linorder_not_le)
1.38 -  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
1.39 -  apply assumption
1.40 -  apply (simp add: mult_ac)
1.41 -  done
1.42
1.43  theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
1.44    by simp
```