--- a/src/HOL/Integ/Int.thy Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/Integ/Int.thy Wed Dec 03 10:49:34 2003 +0100
@@ -4,19 +4,10 @@
Copyright 1998 University of Cambridge
*)
-header {*Type "int" is a Linear Order and Other Lemmas*}
+header {*Type "int" is an Ordered Ring and Other Lemmas*}
theory Int = IntDef:
-instance int :: order
-proof qed (assumption | rule zle_refl zle_trans zle_anti_sym int_less_le)+
-
-instance int :: plus_ac0
-proof qed (rule zadd_commute zadd_assoc zadd_0)+
-
-instance int :: linorder
-proof qed (rule zle_linear)
-
constdefs
nat :: "int => nat"
"nat(Z) == if neg Z then 0 else (THE m. Z = int m)"
@@ -63,152 +54,9 @@
by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
-
-subsection{*@{text Abel_Cancel} simproc on the integers*}
-
-(* Lemmas needed for the simprocs *)
-
-(*Deletion of other terms in the formula, seeking the -x at the front of z*)
-lemma zadd_cancel_21: "((x::int) + (y + z) = y + u) = ((x + z) = u)"
-apply (subst zadd_left_commute)
-apply (rule zadd_left_cancel)
-done
-
-(*A further rule to deal with the case that
- everything gets cancelled on the right.*)
-lemma zadd_cancel_end: "((x::int) + (y + z) = y) = (x = -z)"
-apply (subst zadd_left_commute)
-apply (rule_tac t = y in zadd_0_right [THEN subst], subst zadd_left_cancel)
-apply (simp add: eq_zdiff_eq [symmetric])
-done
-
-(*Legacy ML bindings, but no longer the structure Int.*)
-ML
-{*
-val Int_thy = the_context ()
-val zabs_def = thm "zabs_def"
-val nat_def = thm "nat_def"
-
-val int_0 = thm "int_0";
-val int_1 = thm "int_1";
-val int_Suc0_eq_1 = thm "int_Suc0_eq_1";
-val neg_eq_less_0 = thm "neg_eq_less_0";
-val not_neg_eq_ge_0 = thm "not_neg_eq_ge_0";
-val not_neg_0 = thm "not_neg_0";
-val not_neg_1 = thm "not_neg_1";
-val iszero_0 = thm "iszero_0";
-val not_iszero_1 = thm "not_iszero_1";
-val int_0_less_1 = thm "int_0_less_1";
-val int_0_neq_1 = thm "int_0_neq_1";
-val zadd_cancel_21 = thm "zadd_cancel_21";
-val zadd_cancel_end = thm "zadd_cancel_end";
-
-structure Int_Cancel_Data =
-struct
- val ss = HOL_ss
- val eq_reflection = eq_reflection
-
- val sg_ref = Sign.self_ref (Theory.sign_of (the_context()))
- val T = HOLogic.intT
- val zero = Const ("0", HOLogic.intT)
- val restrict_to_left = restrict_to_left
- val add_cancel_21 = zadd_cancel_21
- val add_cancel_end = zadd_cancel_end
- val add_left_cancel = zadd_left_cancel
- val add_assoc = zadd_assoc
- val add_commute = zadd_commute
- val add_left_commute = zadd_left_commute
- val add_0 = zadd_0
- val add_0_right = zadd_0_right
-
- val eq_diff_eq = eq_zdiff_eq
- val eqI_rules = [zless_eqI, zeq_eqI, zle_eqI]
- fun dest_eqI th =
- #1 (HOLogic.dest_bin "op =" HOLogic.boolT
- (HOLogic.dest_Trueprop (concl_of th)))
-
- val diff_def = zdiff_def
- val minus_add_distrib = zminus_zadd_distrib
- val minus_minus = zminus_zminus
- val minus_0 = zminus_0
- val add_inverses = [zadd_zminus_inverse, zadd_zminus_inverse2]
- val cancel_simps = [zadd_zminus_cancel, zminus_zadd_cancel]
-end;
+subsection{*Comparison laws*}
-structure Int_Cancel = Abel_Cancel (Int_Cancel_Data);
-
-Addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
-*}
-
-
-subsection{*Misc Results*}
-
-lemma zminus_zdiff_eq [simp]: "- (z - y) = y - (z::int)"
-by simp
-
-lemma zless_eq_neg: "(w<z) = neg(w-z)"
-by (simp add: zless_def)
-
-lemma eq_eq_iszero: "(w=z) = iszero(w-z)"
-by (simp add: iszero_def zdiff_eq_eq)
-
-lemma zle_eq_not_neg: "(w\<le>z) = (~ neg(z-w))"
-by (simp add: zle_def zless_def)
-
-subsection{*Inequality reasoning*}
-
-lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
-apply (auto simp add: zless_iff_Suc_zadd int_Suc gr0_conv_Suc zero_reorient)
-apply (rule_tac x = "Suc n" in exI)
-apply (simp add: int_Suc)
-done
-
-lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
-apply (simp add: zle_def zless_add1_eq)
-apply (auto intro: zless_asym zle_anti_sym
- simp add: order_less_imp_le symmetric zle_def)
-done
-
-lemma add1_left_zle_eq: "((1::int) + w \<le> z) = (w<z)"
-apply (subst zadd_commute)
-apply (rule add1_zle_eq)
-done
-
-
-subsection{*Monotonicity results*}
-
-lemma zadd_right_cancel_zless [simp]: "(v+z < w+z) = (v < (w::int))"
-by simp
-
-lemma zadd_left_cancel_zless [simp]: "(z+v < z+w) = (v < (w::int))"
-by simp
-
-lemma zadd_right_cancel_zle [simp] : "(v+z \<le> w+z) = (v \<le> (w::int))"
-by simp
-
-lemma zadd_left_cancel_zle [simp] : "(z+v \<le> z+w) = (v \<le> (w::int))"
-by simp
-
-(*"v\<le>w ==> v+z \<le> w+z"*)
-lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard]
-
-(*"v\<le>w ==> z+v \<le> z+w"*)
-lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard]
-
-(*"v\<le>w ==> v+z \<le> w+z"*)
-lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard]
-
-(*"v\<le>w ==> z+v \<le> z+w"*)
-lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard]
-
-lemma zadd_zle_mono: "[| w'\<le>w; z'\<le>z |] ==> w' + z' \<le> w + (z::int)"
-by (erule zadd_zle_mono1 [THEN zle_trans], simp)
-
-lemma zadd_zless_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::int)"
-by (erule zadd_zless_mono1 [THEN order_less_le_trans], simp)
-
-
-subsection{*Comparison laws*}
+(*ring and field?*)
lemma zminus_zless_zminus [simp]: "(- x < - y) = (y < (x::int))"
by (simp add: zless_def zdiff_def zadd_ac)
@@ -237,7 +85,132 @@
by auto
-subsection{*Instances of the equations above, for zero*}
+subsection{*nat: magnitide of an integer, as a natural number*}
+
+lemma nat_int [simp]: "nat(int n) = n"
+by (unfold nat_def, auto)
+
+lemma nat_zminus_int [simp]: "nat(- (int n)) = 0"
+apply (unfold nat_def)
+apply (auto simp add: neg_eq_less_0 zero_reorient zminus_zless)
+done
+
+lemma nat_zero [simp]: "nat 0 = 0"
+apply (unfold Zero_int_def)
+apply (rule nat_int)
+done
+
+lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
+apply (drule not_neg_eq_ge_0 [THEN iffD1])
+apply (drule zle_imp_zless_or_eq)
+apply (auto simp add: zless_iff_Suc_zadd)
+done
+
+lemma neg_nat: "neg z ==> nat z = 0"
+by (unfold nat_def, auto)
+
+lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
+apply (case_tac "neg z")
+apply (erule_tac [2] not_neg_nat [THEN subst])
+apply (auto simp add: neg_nat)
+apply (auto dest: order_less_trans simp add: neg_eq_less_0)
+done
+
+lemma nat_0_le [simp]: "0 \<le> z ==> int (nat z) = z"
+by (simp add: neg_eq_less_0 zle_def not_neg_nat)
+
+lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
+by (auto simp add: order_le_less neg_eq_less_0 zle_def neg_nat)
+
+(*An alternative condition is 0 \<le> w *)
+lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
+apply (subst zless_int [symmetric])
+apply (simp (no_asm_simp) add: not_neg_nat not_neg_eq_ge_0 order_le_less)
+apply (case_tac "neg w")
+ apply (simp add: neg_eq_less_0 neg_nat)
+ apply (blast intro: order_less_trans)
+apply (simp add: not_neg_nat)
+done
+
+lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)"
+apply (case_tac "0 < z")
+apply (auto simp add: nat_mono_iff linorder_not_less)
+done
+
+
+subsection{*Monotonicity results*}
+
+(*RING AND FIELD?*)
+
+lemma zadd_right_cancel_zless [simp]: "(v+z < w+z) = (v < (w::int))"
+by (simp add: zless_def zdiff_def zadd_ac)
+
+lemma zadd_left_cancel_zless [simp]: "(z+v < z+w) = (v < (w::int))"
+by (simp add: zless_def zdiff_def zadd_ac)
+
+lemma zadd_right_cancel_zle [simp] : "(v+z \<le> w+z) = (v \<le> (w::int))"
+by (simp add: linorder_not_less [symmetric])
+
+lemma zadd_left_cancel_zle [simp] : "(z+v \<le> z+w) = (v \<le> (w::int))"
+by (simp add: linorder_not_less [symmetric])
+
+(*"v\<le>w ==> v+z \<le> w+z"*)
+lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard]
+
+(*"v\<le>w ==> z+v \<le> z+w"*)
+lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard]
+
+(*"v\<le>w ==> v+z \<le> w+z"*)
+lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard]
+
+(*"v\<le>w ==> z+v \<le> z+w"*)
+lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard]
+
+lemma zadd_zle_mono: "[| w'\<le>w; z'\<le>z |] ==> w' + z' \<le> w + (z::int)"
+by (erule zadd_zle_mono1 [THEN zle_trans], simp)
+
+lemma zadd_zless_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::int)"
+by (erule zadd_zless_mono1 [THEN order_less_le_trans], simp)
+
+
+subsection{*Strict Monotonicity of Multiplication*}
+
+text{*strict, in 1st argument; proof is by induction on k>0*}
+lemma zmult_zless_mono2_lemma: "i<j ==> 0<k --> int k * i < int k * j"
+apply (induct_tac "k", simp)
+apply (simp add: int_Suc)
+apply (case_tac "n=0")
+apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less)
+apply (simp_all add: zadd_zmult_distrib zadd_zless_mono int_Suc0_eq_1 order_le_less)
+done
+
+lemma zmult_zless_mono2: "[| i<j; (0::int) < k |] ==> k*i < k*j"
+apply (rule_tac t = k in not_neg_nat [THEN subst])
+apply (erule_tac [2] zmult_zless_mono2_lemma [THEN mp])
+apply (simp add: not_neg_eq_ge_0 order_le_less)
+apply (frule conjI [THEN zless_nat_conj [THEN iffD2]], auto)
+done
+
+text{*The Integers Form an Ordered Ring*}
+instance int :: ordered_ring
+proof
+ fix i j k :: int
+ show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
+ show "i + j = j + i" by (simp add: zadd_commute)
+ show "0 + i = i" by simp
+ show "- i + i = 0" by simp
+ show "i - j = i + (-j)" by (simp add: zdiff_def)
+ show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
+ show "i * j = j * i" by (rule zmult_commute)
+ show "1 * i = i" by simp
+ show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
+ show "0 \<noteq> (1::int)" by simp
+ show "i \<le> j ==> k + i \<le> k + j" by simp
+ show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
+ show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
+qed
+
+subsection{*Lemmas about the Function @{term int} and Orderings*}
lemma negative_zless_0: "- (int (Suc n)) < 0"
by (simp add: zless_def)
@@ -279,116 +252,36 @@
by (simp add: zabs_def)
-subsection{*nat: magnitide of an integer, as a natural number*}
-
-lemma nat_int [simp]: "nat(int n) = n"
-by (unfold nat_def, auto)
-
-lemma nat_zminus_int [simp]: "nat(- (int n)) = 0"
-apply (unfold nat_def)
-apply (auto simp add: neg_eq_less_0 zero_reorient zminus_zless)
-done
-
-lemma nat_zero [simp]: "nat 0 = 0"
-apply (unfold Zero_int_def)
-apply (rule nat_int)
-done
+subsection{*Misc Results*}
-lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
-apply (drule not_neg_eq_ge_0 [THEN iffD1])
-apply (drule zle_imp_zless_or_eq)
-apply (auto simp add: zless_iff_Suc_zadd)
-done
-
-lemma negD: "neg x ==> EX n. x = - (int (Suc n))"
-by (auto simp add: neg_eq_less_0 zless_iff_Suc_zadd zdiff_eq_eq [symmetric] zdiff_def)
-
-lemma neg_nat: "neg z ==> nat z = 0"
-by (unfold nat_def, auto)
-
-lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
-apply (case_tac "neg z")
-apply (erule_tac [2] not_neg_nat [THEN subst])
-apply (auto simp add: neg_nat)
-apply (auto dest: order_less_trans simp add: neg_eq_less_0)
-done
-
-lemma nat_0_le [simp]: "0 \<le> z ==> int (nat z) = z"
-by (simp add: neg_eq_less_0 zle_def not_neg_nat)
-
-lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
-by (auto simp add: order_le_less neg_eq_less_0 zle_def neg_nat)
+lemma zless_eq_neg: "(w<z) = neg(w-z)"
+by (simp add: zless_def)
-(*An alternative condition is 0 \<le> w *)
-lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
-apply (subst zless_int [symmetric])
-apply (simp (no_asm_simp) add: not_neg_nat not_neg_eq_ge_0 order_le_less)
-apply (case_tac "neg w")
- apply (simp add: neg_eq_less_0 neg_nat)
- apply (blast intro: order_less_trans)
-apply (simp add: not_neg_nat)
-done
-
-lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)"
-apply (case_tac "0 < z")
-apply (auto simp add: nat_mono_iff linorder_not_less)
-done
-
-
-subsection{*Strict Monotonicity of Multiplication*}
-
-text{*strict, in 1st argument; proof is by induction on k>0*}
-lemma zmult_zless_mono2_lemma: "i<j ==> 0<k --> int k * i < int k * j"
-apply (induct_tac "k", simp)
-apply (simp add: int_Suc)
-apply (case_tac "n=0")
-apply (simp_all add: zadd_zmult_distrib zadd_zless_mono int_Suc0_eq_1 order_le_less)
-done
+lemma eq_eq_iszero: "(w=z) = iszero(w-z)"
+by (simp add: iszero_def diff_eq_eq)
-lemma zmult_zless_mono2: "[| i<j; (0::int) < k |] ==> k*i < k*j"
-apply (rule_tac t = k in not_neg_nat [THEN subst])
-apply (erule_tac [2] zmult_zless_mono2_lemma [THEN mp])
-apply (simp add: not_neg_eq_ge_0 order_le_less)
-apply (frule conjI [THEN zless_nat_conj [THEN iffD2]], auto)
-done
+lemma zle_eq_not_neg: "(w\<le>z) = (~ neg(z-w))"
+by (simp add: zle_def zless_def)
-text{*The Integers Form an Ordered Ring*}
-instance int :: ordered_ring
-proof
- fix i j k :: int
- show "(i + j) + k = i + (j + k)" by simp
- show "i + j = j + i" by simp
- show "0 + i = i" by simp
- show "- i + i = 0" by simp
- show "i - j = i + (-j)" by simp
- show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
- show "i * j = j * i" by (rule zmult_commute)
- show "1 * i = i" by simp
- show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
- show "0 \<noteq> (1::int)" by simp
- show "i \<le> j ==> k + i \<le> k + j" by simp
- show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
- show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
-qed
subsection{*Monotonicity of Multiplication*}
lemma zmult_zle_mono1: "[| i \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*k"
- by (rule mult_right_mono)
+ by (rule Ring_and_Field.mult_right_mono)
lemma zmult_zle_mono1_neg: "[| i \<le> j; k \<le> (0::int) |] ==> j*k \<le> i*k"
- by (rule mult_right_mono_neg)
+ by (rule Ring_and_Field.mult_right_mono_neg)
lemma zmult_zle_mono2: "[| i \<le> j; (0::int) \<le> k |] ==> k*i \<le> k*j"
- by (rule mult_left_mono)
+ by (rule Ring_and_Field.mult_left_mono)
lemma zmult_zle_mono2_neg: "[| i \<le> j; k \<le> (0::int) |] ==> k*j \<le> k*i"
- by (rule mult_left_mono_neg)
+ by (rule Ring_and_Field.mult_left_mono_neg)
(* \<le> monotonicity, BOTH arguments*)
lemma zmult_zle_mono:
"[| i \<le> j; k \<le> l; (0::int) \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*l"
- by (rule mult_mono)
+ by (rule Ring_and_Field.mult_mono)
lemma zmult_zless_mono1: "[| i<j; (0::int) < k |] ==> i*k < j*k"
by (rule Ring_and_Field.mult_strict_right_mono)
@@ -423,13 +316,108 @@
lemma zmult_cancel1 [simp]: "(k*m = k*n) = (k = (0::int) | m=n)"
by (rule Ring_and_Field.mult_cancel_left)
-(*Analogous to zadd_int*)
-lemma zdiff_int [rule_format]: "n\<le>m --> int m - int n = int (m-n)"
-apply (induct_tac m n rule: diff_induct)
-apply (auto simp add: int_Suc symmetric zdiff_def)
+
+subsection{*For the @{text abel_cancel} Simproc (DELETE)*}
+
+(* Lemmas needed for the simprocs *)
+
+(** The idea is to cancel like terms on opposite sides by subtraction **)
+
+lemma zless_eqI: "(x::int) - y = x' - y' ==> (x<y) = (x'<y')"
+by (simp add: zless_def)
+
+lemma zle_eqI: "(x::int) - y = x' - y' ==> (y<=x) = (y'<=x')"
+apply (drule zless_eqI)
+apply (simp (no_asm_simp) add: zle_def)
+done
+
+lemma zeq_eqI: "(x::int) - y = x' - y' ==> (x=y) = (x'=y')"
+apply safe
+apply (simp_all add: eq_diff_eq diff_eq_eq)
+done
+
+(*Deletion of other terms in the formula, seeking the -x at the front of z*)
+lemma zadd_cancel_21: "((x::int) + (y + z) = y + u) = ((x + z) = u)"
+apply (subst zadd_left_commute)
+apply (rule zadd_left_cancel)
+done
+
+(*A further rule to deal with the case that
+ everything gets cancelled on the right.*)
+lemma zadd_cancel_end: "((x::int) + (y + z) = y) = (x = -z)"
+apply (subst zadd_left_commute)
+apply (rule_tac t = y in zadd_0_right [THEN subst], subst zadd_left_cancel)
+apply (simp add: eq_diff_eq [symmetric])
done
-(* a case theorem distinguishing non-negative and negative int *)
+(*Legacy ML bindings, but no longer the structure Int.*)
+ML
+{*
+val Int_thy = the_context ()
+val zabs_def = thm "zabs_def"
+val nat_def = thm "nat_def"
+
+val zless_eqI = thm "zless_eqI";
+val zle_eqI = thm "zle_eqI";
+val zeq_eqI = thm "zeq_eqI";
+
+val int_0 = thm "int_0";
+val int_1 = thm "int_1";
+val int_Suc0_eq_1 = thm "int_Suc0_eq_1";
+val neg_eq_less_0 = thm "neg_eq_less_0";
+val not_neg_eq_ge_0 = thm "not_neg_eq_ge_0";
+val not_neg_0 = thm "not_neg_0";
+val not_neg_1 = thm "not_neg_1";
+val iszero_0 = thm "iszero_0";
+val not_iszero_1 = thm "not_iszero_1";
+val int_0_less_1 = thm "int_0_less_1";
+val int_0_neq_1 = thm "int_0_neq_1";
+val zadd_cancel_21 = thm "zadd_cancel_21";
+val zadd_cancel_end = thm "zadd_cancel_end";
+
+structure Int_Cancel_Data =
+struct
+ val ss = HOL_ss
+ val eq_reflection = eq_reflection
+
+ val sg_ref = Sign.self_ref (Theory.sign_of (the_context()))
+ val T = HOLogic.intT
+ val zero = Const ("0", HOLogic.intT)
+ val restrict_to_left = restrict_to_left
+ val add_cancel_21 = zadd_cancel_21
+ val add_cancel_end = zadd_cancel_end
+ val add_left_cancel = zadd_left_cancel
+ val add_assoc = zadd_assoc
+ val add_commute = zadd_commute
+ val add_left_commute = zadd_left_commute
+ val add_0 = zadd_0
+ val add_0_right = zadd_0_right
+
+ val eq_diff_eq = eq_diff_eq
+ val eqI_rules = [zless_eqI, zeq_eqI, zle_eqI]
+ fun dest_eqI th =
+ #1 (HOLogic.dest_bin "op =" HOLogic.boolT
+ (HOLogic.dest_Trueprop (concl_of th)))
+
+ val diff_def = zdiff_def
+ val minus_add_distrib = zminus_zadd_distrib
+ val minus_minus = zminus_zminus
+ val minus_0 = zminus_0
+ val add_inverses = [zadd_zminus_inverse, zadd_zminus_inverse2]
+ val cancel_simps = [zadd_zminus_cancel, zminus_zadd_cancel]
+end;
+
+structure Int_Cancel = Abel_Cancel (Int_Cancel_Data);
+
+Addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
+*}
+
+
+text{*A case theorem distinguishing non-negative and negative int*}
+
+lemma negD: "neg x ==> EX n. x = - (int (Suc n))"
+by (auto simp add: neg_eq_less_0 zless_iff_Suc_zadd
+ diff_eq_eq [symmetric] zdiff_def)
lemma int_cases:
"[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P"
@@ -439,11 +427,31 @@
done
+subsection{*Inequality reasoning*}
+
+text{*Are they needed????*}
+lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
+apply (auto simp add: zless_iff_Suc_zadd int_Suc gr0_conv_Suc zero_reorient)
+apply (rule_tac x = "Suc n" in exI)
+apply (simp add: int_Suc)
+done
+
+lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
+apply (simp add: zle_def zless_add1_eq)
+apply (auto intro: zless_asym zle_anti_sym
+ simp add: order_less_imp_le symmetric zle_def)
+done
+
+lemma add1_left_zle_eq: "((1::int) + w \<le> z) = (w<z)"
+apply (subst zadd_commute)
+apply (rule add1_zle_eq)
+done
+
+
ML
{*
-val zminus_zdiff_eq = thm "zminus_zdiff_eq";
val zless_eq_neg = thm "zless_eq_neg";
val eq_eq_iszero = thm "eq_eq_iszero";
val zle_eq_not_neg = thm "zle_eq_not_neg";
@@ -468,12 +476,9 @@
val zminus_zle = thm "zminus_zle";
val equation_zminus = thm "equation_zminus";
val zminus_equation = thm "zminus_equation";
-val negative_zless_0 = thm "negative_zless_0";
val negative_zless = thm "negative_zless";
-val negative_zle_0 = thm "negative_zle_0";
val negative_zle = thm "negative_zle";
val not_zle_0_negative = thm "not_zle_0_negative";
-val int_zle_neg = thm "int_zle_neg";
val not_int_zless_negative = thm "not_int_zless_negative";
val negative_eq_positive = thm "negative_eq_positive";
val zle_iff_zadd = thm "zle_iff_zadd";
@@ -482,7 +487,6 @@
val nat_zminus_int = thm "nat_zminus_int";
val nat_zero = thm "nat_zero";
val not_neg_nat = thm "not_neg_nat";
-val negD = thm "negD";
val neg_nat = thm "neg_nat";
val zless_nat_eq_int_zless = thm "zless_nat_eq_int_zless";
val nat_0_le = thm "nat_0_le";
@@ -505,7 +509,6 @@
val zmult_zle_cancel1 = thm "zmult_zle_cancel1";
val zmult_cancel2 = thm "zmult_cancel2";
val zmult_cancel1 = thm "zmult_cancel1";
-val zdiff_int = thm "zdiff_int";
*}
end