--- a/src/HOL/Integ/Bin.ML Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/Integ/Bin.ML Wed Dec 03 10:49:34 2003 +0100
@@ -207,7 +207,7 @@
(** Special-case simplification for small constants **)
Goal "-1 * z = -(z::int)";
-by (simp_tac (simpset() addsimps zcompare_rls@[int_Suc0_eq_1, zmult_zminus]) 1);
+by (simp_tac (simpset() addsimps compare_rls@[int_Suc0_eq_1, zmult_zminus]) 1);
qed "zmult_minus1";
Goal "z * -1 = -(z::int)";
@@ -243,7 +243,7 @@
"((number_of x::int) = number_of y) = \
\ iszero (number_of (bin_add x (bin_minus y)))";
by (simp_tac (simpset()
- addsimps zcompare_rls @ [number_of_add, number_of_minus]) 1);
+ addsimps compare_rls @ [number_of_add, number_of_minus]) 1);
qed "eq_number_of_eq";
Goalw [iszero_def] "iszero ((number_of bin.Pls)::int)";
@@ -261,7 +261,7 @@
by (int_case_tac "number_of w" 1);
by (ALLGOALS
(asm_simp_tac
- (simpset() addsimps zcompare_rls @
+ (simpset() addsimps compare_rls @
[zero_reorient, zminus_zadd_distrib RS sym,
int_Suc0_eq_1 RS sym, zadd_int])));
qed "iszero_number_of_BIT";
@@ -299,7 +299,7 @@
by (int_case_tac "number_of w" 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps [int_Suc0_eq_1 RS sym, zadd_int,
- neg_eq_less_0, symmetric zdiff_def] @ zcompare_rls)));
+ neg_eq_less_0, symmetric zdiff_def] @ compare_rls)));
qed "neg_number_of_BIT";
--- 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
--- a/src/HOL/Integ/IntArith.thy Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/Integ/IntArith.thy Wed Dec 03 10:49:34 2003 +0100
@@ -202,8 +202,7 @@
lemma int_val_lemma:
"(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
-apply (induct_tac "n")
- apply (simp (no_asm_simp))
+apply (induct_tac "n", simp)
apply (intro strip)
apply (erule impE, simp)
apply (erule_tac x = n in allE, simp)
@@ -293,9 +292,9 @@
lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
apply (case_tac "0<m")
-apply (simp (no_asm_simp) add: pos_zmult_eq_1_iff)
+apply (simp add: pos_zmult_eq_1_iff)
apply (case_tac "m=0")
-apply (simp (no_asm_simp) del: number_of_reorient)
+apply (simp del: number_of_reorient)
apply (subgoal_tac "0 < -m")
apply (drule_tac n = "-n" in pos_zmult_eq_1_iff, auto)
done
@@ -303,22 +302,26 @@
subsection{*More about nat*}
+(*Analogous to zadd_int*)
+lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)"
+by (induct m n rule: diff_induct, simp_all)
+
lemma nat_add_distrib:
"[| (0::int) \<le> z; 0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
apply (rule inj_int [THEN injD])
-apply (simp (no_asm_simp) add: zadd_int [symmetric])
+apply (simp add: zadd_int [symmetric])
done
lemma nat_diff_distrib:
"[| (0::int) \<le> z'; z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
apply (rule inj_int [THEN injD])
-apply (simp (no_asm_simp) add: zdiff_int [symmetric] nat_le_eq_zle)
+apply (simp add: zdiff_int [symmetric] nat_le_eq_zle)
done
lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
apply (case_tac "0 \<le> z'")
apply (rule inj_int [THEN injD])
-apply (simp (no_asm_simp) add: zmult_int [symmetric] int_0_le_mult_iff)
+apply (simp add: zmult_int [symmetric] int_0_le_mult_iff)
apply (simp add: zmult_le_0_iff)
done
--- a/src/HOL/Integ/IntDef.thy Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/Integ/IntDef.thy Wed Dec 03 10:49:34 2003 +0100
@@ -3,13 +3,14 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
-The integers as equivalence classes over nat*nat.
*)
+header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
+
theory IntDef = Equiv + NatArith:
constdefs
- intrel :: "((nat * nat) * (nat * nat)) set"
- "intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
+ intrel :: "((nat * nat) * (nat * nat)) set"
+ "intrel == {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
typedef (Integ)
int = "UNIV//intrel"
@@ -22,17 +23,13 @@
instance int :: times ..
instance int :: minus ..
-defs
- zminus_def:
- "- Z == Abs_Integ(UN (x,y):Rep_Integ(Z). intrel``{(y,x)})"
-
constdefs
int :: "nat => int"
"int m == Abs_Integ(intrel `` {(m,0)})"
neg :: "int => bool"
- "neg(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
+ "neg(Z) == \<exists>x y. x<y & (x,y::nat):Rep_Integ(Z)"
(*For simplifying equalities*)
iszero :: "int => bool"
@@ -40,12 +37,14 @@
defs (overloaded)
+ zminus_def: "- Z == Abs_Integ(\<Union>(x,y) \<in> Rep_Integ(Z). intrel``{(y,x)})"
+
Zero_int_def: "0 == int 0"
- One_int_def: "1 == int 1"
+ One_int_def: "1 == int 1"
zadd_def:
"z + w ==
- Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).
+ Abs_Integ(\<Union>(x1,y1) \<in> Rep_Integ(z). \<Union>(x2,y2) \<in> Rep_Integ(w).
intrel``{(x1+x2, y1+y2)})"
zdiff_def: "z - (w::int) == z + (-w)"
@@ -56,10 +55,10 @@
zmult_def:
"z * w ==
- Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).
+ Abs_Integ(\<Union>(x1,y1) \<in> Rep_Integ(z). \<Union>(x2,y2) \<in> Rep_Integ(w).
intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
-lemma intrel_iff [simp]: "(((x1,y1),(x2,y2)): intrel) = (x1+y2 = x2+y1)"
+lemma intrel_iff [simp]: "(((x1,y1),(x2,y2)) \<in> intrel) = (x1+y2 = x2+y1)"
by (unfold intrel_def, blast)
lemma equiv_intrel: "equiv UNIV intrel"
@@ -171,7 +170,7 @@
done
(*For AC rewriting*)
-lemma zadd_left_commute: "x + (y + z) = y + ((x + z)::int)"
+lemma zadd_left_commute: "x + (y + z) = y + ((x + z) ::int)"
apply (rule mk_left_commute [of "op +"])
apply (rule zadd_assoc)
apply (rule zadd_commute)
@@ -180,6 +179,8 @@
(*Integer addition is an AC operator*)
lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
+lemmas zmult_ac = Ring_and_Field.mult_ac
+
lemma zadd_int: "(int m) + (int n) = int (m + n)"
by (simp add: int_def zadd)
@@ -278,16 +279,6 @@
apply (simp (no_asm_simp) add: add_mult_distrib2 zmult add_ac mult_ac)
done
-(*For AC rewriting*)
-lemma zmult_left_commute: "x * (y * z) = y * ((x * z)::int)"
- apply (rule mk_left_commute [of "op *"])
- apply (rule zmult_assoc)
- apply (rule zmult_commute)
- done
-
-(*Integer multiplication is an AC operator*)
-lemmas zmult_ac = zmult_assoc zmult_commute zmult_left_commute
-
lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"
apply (rule_tac z = z1 in eq_Abs_Integ)
apply (rule_tac z = z2 in eq_Abs_Integ)
@@ -340,7 +331,7 @@
(*This lemma allows direct proofs of other <-properties*)
lemma zless_iff_Suc_zadd:
- "(w < z) = (EX n. z = w + int(Suc n))"
+ "(w < z) = (\<exists>n. z = w + int(Suc n))"
apply (unfold zless_def neg_def zdiff_def int_def)
apply (rule_tac z = z in eq_Abs_Integ)
apply (rule_tac z = w in eq_Abs_Integ, clarify)
@@ -465,84 +456,21 @@
apply (blast elim!: zless_asym)
done
-
-(*** Subtraction laws ***)
-
-lemma zadd_zdiff_eq: "x + (y - z) = (x + y) - (z::int)"
-by (simp add: zdiff_def zadd_ac)
-
-lemma zdiff_zadd_eq: "(x - y) + z = (x + z) - (y::int)"
-by (simp add: zdiff_def zadd_ac)
-
-lemma zdiff_zdiff_eq: "(x - y) - z = x - (y + (z::int))"
-by (simp add: zdiff_def zadd_ac)
-
-lemma zdiff_zdiff_eq2: "x - (y - z) = (x + z) - (y::int)"
-by (simp add: zdiff_def zadd_ac)
-
-lemma zdiff_zless_eq: "(x-y < z) = (x < z + (y::int))"
-apply (unfold zless_def zdiff_def)
-apply (simp add: zadd_ac)
-done
-
-lemma zless_zdiff_eq: "(x < z-y) = (x + (y::int) < z)"
-apply (unfold zless_def zdiff_def)
-apply (simp add: zadd_ac)
-done
-
-lemma zdiff_zle_eq: "(x-y <= z) = (x <= z + (y::int))"
-apply (unfold zle_def)
-apply (simp add: zless_zdiff_eq)
-done
-
-lemma zle_zdiff_eq: "(x <= z-y) = (x + (y::int) <= z)"
-apply (unfold zle_def)
-apply (simp add: zdiff_zless_eq)
-done
-
-lemma zdiff_eq_eq: "(x-y = z) = (x = z + (y::int))"
-by (auto simp add: zdiff_def zadd_assoc Zero_int_def [symmetric])
-
-lemma eq_zdiff_eq: "(x = z-y) = (x + (y::int) = z)"
-by (auto simp add: zdiff_def zadd_assoc Zero_int_def [symmetric])
-
-(*This list of rewrites simplifies (in)equalities by bringing subtractions
- to the top and then moving negative terms to the other side.
- Use with zadd_ac*)
-lemmas zcompare_rls =
- zdiff_def [symmetric]
- zadd_zdiff_eq zdiff_zadd_eq zdiff_zdiff_eq zdiff_zdiff_eq2
- zdiff_zless_eq zless_zdiff_eq zdiff_zle_eq zle_zdiff_eq
- zdiff_eq_eq eq_zdiff_eq
-
-
-(** Cancellation laws **)
-
lemma zadd_left_cancel [simp]: "!!w::int. (z + w' = z + w) = (w' = w)"
apply safe
apply (drule_tac f = "%x. x + (-z) " in arg_cong)
apply (simp add: Zero_int_def [symmetric] zadd_ac)
done
-lemma zadd_right_cancel [simp]: "!!z::int. (w' + z = w + z) = (w' = w)"
-by (simp add: zadd_ac)
-
-
-(** For the cancellation simproc.
- 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)
+instance int :: order
+proof qed (assumption | rule zle_refl zle_trans zle_anti_sym int_less_le)+
-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
+instance int :: plus_ac0
+proof qed (rule zadd_commute zadd_assoc zadd_0)+
-lemma zeq_eqI: "(x::int) - y = x' - y' ==> (x=y) = (x'=y')"
-apply safe
-apply (simp_all add: eq_zdiff_eq zdiff_eq_eq)
-done
+instance int :: linorder
+proof qed (rule zle_linear)
+
ML
{*
@@ -578,6 +506,7 @@
val zadd_assoc = thm "zadd_assoc";
val zadd_left_commute = thm "zadd_left_commute";
val zadd_ac = thms "zadd_ac";
+val zmult_ac = thms "zmult_ac";
val zadd_int = thm "zadd_int";
val zadd_int_left = thm "zadd_int_left";
val int_Suc = thm "int_Suc";
@@ -597,8 +526,6 @@
val zmult_zminus = thm "zmult_zminus";
val zmult_commute = thm "zmult_commute";
val zmult_assoc = thm "zmult_assoc";
-val zmult_left_commute = thm "zmult_left_commute";
-val zmult_ac = thms "zmult_ac";
val zadd_zmult_distrib = thm "zadd_zmult_distrib";
val zmult_zminus_right = thm "zmult_zminus_right";
val zadd_zmult_distrib2 = thm "zadd_zmult_distrib2";
@@ -636,22 +563,15 @@
val zle_trans = thm "zle_trans";
val zle_anti_sym = thm "zle_anti_sym";
val int_less_le = thm "int_less_le";
-val zadd_zdiff_eq = thm "zadd_zdiff_eq";
-val zdiff_zadd_eq = thm "zdiff_zadd_eq";
-val zdiff_zdiff_eq = thm "zdiff_zdiff_eq";
-val zdiff_zdiff_eq2 = thm "zdiff_zdiff_eq2";
-val zdiff_zless_eq = thm "zdiff_zless_eq";
-val zless_zdiff_eq = thm "zless_zdiff_eq";
-val zdiff_zle_eq = thm "zdiff_zle_eq";
-val zle_zdiff_eq = thm "zle_zdiff_eq";
-val zdiff_eq_eq = thm "zdiff_eq_eq";
-val eq_zdiff_eq = thm "eq_zdiff_eq";
-val zcompare_rls = thms "zcompare_rls";
val zadd_left_cancel = thm "zadd_left_cancel";
-val zadd_right_cancel = thm "zadd_right_cancel";
-val zless_eqI = thm "zless_eqI";
-val zle_eqI = thm "zle_eqI";
-val zeq_eqI = thm "zeq_eqI";
+
+val diff_less_eq = thm"diff_less_eq";
+val less_diff_eq = thm"less_diff_eq";
+val eq_diff_eq = thm"eq_diff_eq";
+val diff_eq_eq = thm"diff_eq_eq";
+val diff_le_eq = thm"diff_le_eq";
+val le_diff_eq = thm"le_diff_eq";
+val compare_rls = thms "compare_rls";
*}
end
--- a/src/HOL/Integ/IntDiv.thy Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/Integ/IntDiv.thy Wed Dec 03 10:49:34 2003 +0100
@@ -89,7 +89,7 @@
-(*** Uniqueness and monotonicity of quotients and remainders ***)
+subsection{*Uniqueness and Monotonicity of Quotients and Remainders*}
lemma unique_quotient_lemma:
"[| b*q' + r' <= b*q + r; 0 <= r'; 0 < b; r < b |]
@@ -129,7 +129,9 @@
done
-(*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***)
+subsection{*Correctness of posDivAlg, the Algorithm for Non-Negative Dividends*}
+
+text{*And positive divisors*}
lemma adjust_eq [simp]:
"adjust b (q,r) =
@@ -160,7 +162,9 @@
done
-(*** Correctness of negDivAlg, the division algorithm for a<0 and b>0 ***)
+subsection{*Correctness of negDivAlg, the Algorithm for Negative Dividends*}
+
+text{*And positive divisors*}
declare negDivAlg.simps [simp del]
@@ -186,7 +190,7 @@
done
-(*** Existence shown by proving the division algorithm to be correct ***)
+subsection{*Existence Shown by Proving the Division Algorithm to be Correct*}
(*the case a=0*)
lemma quorem_0: "b ~= 0 ==> quorem ((0,b), (0,0))"
@@ -211,8 +215,8 @@
(** Arbitrary definitions for division by zero. Useful to simplify
certain equations **)
-lemma DIVISION_BY_ZERO: "a div (0::int) = 0 & a mod (0::int) = a"
-by (simp add: div_def mod_def divAlg_def posDivAlg.simps) (*NOT for adding to default simpset*)
+lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a"
+by (simp add: div_def mod_def divAlg_def posDivAlg.simps)
(** Basic laws about division and remainder **)
@@ -311,7 +315,7 @@
auto)
done
-(*** div, mod and unary minus ***)
+subsection{*div, mod and unary minus*}
lemma zminus1_lemma:
"quorem((a,b),(q,r))
@@ -349,7 +353,7 @@
by (simp add: zmod_zminus1_eq_if zmod_zminus2)
-(*** division of a number by itself ***)
+subsection{*Division of a Number by Itself*}
lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q"
apply (subgoal_tac "0 < a*q")
@@ -385,7 +389,7 @@
done
-(*** Computation of division and remainder ***)
+subsection{*Computation of Division and Remainder*}
lemma zdiv_zero [simp]: "(0::int) div b = 0"
by (simp add: div_def divAlg_def)
@@ -486,7 +490,7 @@
declare negDivAlg_eqn [of concl: 1 "number_of w", standard, simp]
-(*** Monotonicity in the first argument (divisor) ***)
+subsection{*Monotonicity in the First Argument (Dividend)*}
lemma zdiv_mono1: "[| a <= a'; 0 < (b::int) |] ==> a div b <= a' div b"
apply (cut_tac a = a and b = b in zmod_zdiv_equality)
@@ -507,7 +511,7 @@
done
-(*** Monotonicity in the second argument (dividend) ***)
+subsection{*Monotonicity in the Second Argument (Divisor)*}
lemma q_pos_lemma:
"[| 0 <= b'*q' + r'; r' < b'; 0 < b' |] ==> 0 <= (q'::int)"
@@ -574,7 +578,7 @@
done
-(*** More algebraic laws for div and mod ***)
+subsection{*More Algebraic Laws for div and mod*}
(** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
@@ -686,7 +690,7 @@
done
-(*** proving a div (b*c) = (a div b) div c ***)
+subsection{*Proving @{term "a div (b*c) = (a div b) div c"} *}
(*The condition c>0 seems necessary. Consider that 7 div ~6 = ~2 but
7 div 2 div ~3 = 3 div ~3 = ~1. The subcase (a div b) mod c = 0 seems
@@ -700,7 +704,7 @@
apply (rule order_le_less_trans)
apply (erule_tac [2] zmult_zless_mono1)
apply (rule zmult_zle_mono2_neg)
-apply (auto simp add: zcompare_rls zadd_commute [of 1]
+apply (auto simp add: compare_rls zadd_commute [of 1]
add1_zle_eq pos_mod_bound)
done
@@ -722,13 +726,13 @@
apply (rule order_less_le_trans)
apply (erule zmult_zless_mono1)
apply (rule_tac [2] zmult_zle_mono2)
-apply (auto simp add: zcompare_rls zadd_commute [of 1]
+apply (auto simp add: compare_rls zadd_commute [of 1]
add1_zle_eq pos_mod_bound)
done
lemma zmult2_lemma: "[| quorem ((a,b), (q,r)); b ~= 0; 0 < c |]
==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
-by (auto simp add: zmult_ac quorem_def linorder_neq_iff
+by (auto simp add: mult_ac quorem_def linorder_neq_iff
int_0_less_mult_iff zadd_zmult_distrib2 [symmetric]
zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
@@ -744,7 +748,7 @@
done
-(*** Cancellation of common factors in div ***)
+subsection{*Cancellation of Common Factors in div*}
lemma zdiv_zmult_zmult1_aux1: "[| (0::int) < b; c ~= 0 |] ==> (c*a) div (c*b) = a div b"
by (subst zdiv_zmult2_eq, auto)
@@ -766,7 +770,7 @@
-(*** Distribution of factors over mod ***)
+subsection{*Distribution of Factors over mod*}
lemma zmod_zmult_zmult1_aux1: "[| (0::int) < b; c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
by (subst zmod_zmult2_eq, auto)
@@ -788,7 +792,7 @@
done
-subsection {*splitting rules for div and mod*}
+subsection {*Splitting Rules for div and mod*}
text{*The proofs of the two lemmas below are essentially identical*}
@@ -853,7 +857,7 @@
declare split_zmod [of _ _ "number_of k", simplified, standard, arith_split]
-subsection{*Speeding up the division algorithm with shifting*}
+subsection{*Speeding up the Division Algorithm with Shifting*}
(** computing div by shifting **)
@@ -986,7 +990,7 @@
by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
-subsection {* Divides relation *}
+subsection {* The Divides Relation *}
lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
by(simp add:dvd_def zmod_eq_0_iff)
@@ -1046,7 +1050,7 @@
lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
apply (unfold dvd_def)
- apply (blast intro: zmult_left_commute)
+ apply (blast intro: mult_left_commute)
done
lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
@@ -1077,7 +1081,7 @@
lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
apply (unfold dvd_def, clarify)
apply (rule_tac x = "k * ka" in exI)
- apply (simp add: zmult_ac)
+ apply (simp add: mult_ac)
done
lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
--- a/src/HOL/Integ/Presburger.thy Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/Integ/Presburger.thy Wed Dec 03 10:49:34 2003 +0100
@@ -395,7 +395,7 @@
apply(clarsimp)
apply(rename_tac n m)
apply(rule_tac x = "m - n*k" in exI)
- apply(simp add:int_distrib zmult_ac)
+ apply(simp add:int_distrib mult_ac)
done
lemma not_dvd_modd_pinf: "((d::int) dvd d1) ==>
@@ -405,11 +405,11 @@
apply(clarsimp)
apply(rename_tac n m)
apply(erule_tac x = "m - n*k" in allE)
- apply(simp add:int_distrib zmult_ac)
+ apply(simp add:int_distrib mult_ac)
apply(clarsimp)
apply(rename_tac n m)
apply(erule_tac x = "m + n*k" in allE)
- apply(simp add:int_distrib zmult_ac)
+ apply(simp add:int_distrib mult_ac)
done
(*=============================================================================*)
@@ -462,7 +462,7 @@
apply(clarsimp)
apply(rename_tac n m)
apply(rule_tac x = "m + n*k" in exI)
-apply(simp add:int_distrib zmult_ac)
+apply(simp add:int_distrib mult_ac)
done
@@ -473,11 +473,11 @@
apply(clarsimp)
apply(rename_tac n m)
apply(erule_tac x = "m + n*k" in allE)
-apply(simp add:int_distrib zmult_ac)
+apply(simp add:int_distrib mult_ac)
apply(clarsimp)
apply(rename_tac n m)
apply(erule_tac x = "m - n*k" in allE)
-apply(simp add:int_distrib zmult_ac)
+apply(simp add:int_distrib mult_ac)
done
@@ -626,7 +626,7 @@
assume ?LHS
then obtain x where P: "P x" ..
have "x mod d = x - (x div d)*d"
- by(simp add:zmod_zdiv_equality zmult_ac eq_zdiff_eq)
+ by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
hence Pmod: "P x = P(x mod d)" using modd by simp
show ?RHS
proof (cases)
@@ -661,7 +661,7 @@
assume ?LHS
then obtain x where P: "P x" ..
have "x mod d = x + (-(x div d))*d"
- by(simp add:zmod_zdiv_equality zmult_ac eq_zdiff_eq)
+ by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
hence Pmod: "P x = P(x mod d)" using modd by (simp only:)
show ?RHS
proof (cases)
@@ -702,7 +702,7 @@
have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)"
using minus[THEN spec, of "x - i * d"]
- by (simp add:int_distrib zdiff_zdiff_eq[symmetric])
+ by (simp add:int_distrib Ring_and_Field.diff_diff_eq[symmetric])
ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast
qed
qed
@@ -864,12 +864,12 @@
apply(drule_tac f = "op * k" in arg_cong)
apply(simp only:int_distrib)
apply(rule_tac x = "d" in exI)
- apply(simp only:zmult_ac)
+ apply(simp only:mult_ac)
done
next
assume ?Q
then obtain d where "k * c * n + k * t = (k*m)*d" by(fastsimp simp:dvd_def)
- hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib zmult_ac)
+ hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib mult_ac)
hence "((c * n + t) * k) div k = ((m*d) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
hence "c*n+t = m*d" by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
thus ?P by(simp add:dvd_def)
@@ -879,10 +879,10 @@
shows "((m::int) < (c*n+t)) = (k*m <((k*c)*n+(k*t)))" (is "?P = ?Q")
proof
assume P: ?P
- show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib zmult_ac)
+ show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib mult_ac)
next
assume ?Q
- hence "0 < k*(c*n + t - m)" by(simp add: int_distrib zmult_ac)
+ hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
with gr0 have "0 < (c*n + t - m)" by(simp add:int_0_less_mult_iff)
thus ?P by(simp)
qed
@@ -896,7 +896,7 @@
done
next
assume ?Q
- hence "m * k = (c*n + t) * k" by(simp add:int_distrib zmult_ac)
+ hence "m * k = (c*n + t) * k" by(simp add:int_distrib mult_ac)
hence "((m) * k) div k = ((c*n + t) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
thus ?P by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
qed
@@ -904,9 +904,9 @@
lemma ac_pi_eq: assumes gr0: "0 < (k::int)" shows "(~((0::int) < (c*n + t))) = (0 < ((-k)*c)*n + ((-k)*t + k))"
proof -
have "(~ (0::int) < (c*n + t)) = (0<1-(c*n + t))" by arith
- also have "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib zmult_ac)
+ also have "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib mult_ac)
also have "0<(-1*c)*n + (-t+1) = (0 < (k*(-1*c)*n) + (k*(-t+1)))" by(rule ac_lt_eq[of _ 0,OF gr0,simplified])
- also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib zmult_ac)
+ also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib mult_ac)
finally show ?thesis .
qed
@@ -963,7 +963,7 @@
apply (simp add: linorder_not_le)
apply (drule zmult_zless_mono2_neg [OF iffD2 [OF zero_less_int_conv]])
apply assumption
- apply (simp add: zmult_ac)
+ apply (simp add: mult_ac)
done
theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
--- a/src/HOL/Integ/int_arith1.ML Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/Integ/int_arith1.ML Wed Dec 03 10:49:34 2003 +0100
@@ -5,6 +5,10 @@
Simprocs and decision procedure for linear arithmetic.
*)
+val zadd_ac = thms "Ring_and_Field.add_ac";
+val zmult_ac = thms "Ring_and_Field.mult_ac";
+
+
Addsimps [int_numeral_0_eq_0, int_numeral_1_eq_1];
(*** Simprocs for numeric literals ***)
@@ -12,15 +16,15 @@
(** Combining of literal coefficients in sums of products **)
Goal "(x < y) = (x-y < (0::int))";
-by (simp_tac (simpset() addsimps zcompare_rls) 1);
+by (simp_tac (simpset() addsimps compare_rls) 1);
qed "zless_iff_zdiff_zless_0";
Goal "(x = y) = (x-y = (0::int))";
-by (simp_tac (simpset() addsimps zcompare_rls) 1);
+by (simp_tac (simpset() addsimps compare_rls) 1);
qed "eq_iff_zdiff_eq_0";
Goal "(x <= y) = (x-y <= (0::int))";
-by (simp_tac (simpset() addsimps zcompare_rls) 1);
+by (simp_tac (simpset() addsimps compare_rls) 1);
qed "zle_iff_zdiff_zle_0";
--- a/src/HOL/NumberTheory/Gauss.thy Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/NumberTheory/Gauss.thy Wed Dec 03 10:49:34 2003 +0100
@@ -479,7 +479,7 @@
then have "[gsetprod id A * (-1)^(card E) = gsetprod id A *
(-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)";
apply (rule zcong_trans)
- by (simp add: a zmult_commute zmult_left_commute)
+ by (simp add: a mult_commute mult_left_commute)
then have "[gsetprod id A * (-1)^(card E) = gsetprod id A *
a^(card A)](mod p)";
apply (rule zcong_trans)
--- a/src/HOL/NumberTheory/IntFact.thy Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/NumberTheory/IntFact.thy Wed Dec 03 10:49:34 2003 +0100
@@ -39,7 +39,7 @@
lemma setprod_insert [simp]:
"finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
- by (simp add: setprod_def zmult_left_commute LC.fold_insert [OF LC.intro])
+ by (simp add: setprod_def mult_left_commute LC.fold_insert [OF LC.intro])
text {*
\medskip @{term d22set} --- recursively defined set including all
--- a/src/HOL/NumberTheory/IntPrimes.thy Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy Wed Dec 03 10:49:34 2003 +0100
@@ -305,7 +305,7 @@
apply (rule_tac [!] zrelprime_zdvd_zmult)
apply (simp_all add: zdiff_zmult_distrib)
apply (subgoal_tac "m dvd (-(a * k - b * k))")
- apply (simp add: zminus_zdiff_eq)
+ apply simp
apply (subst zdvd_zminus_iff, assumption)
done
@@ -380,7 +380,7 @@
apply (unfold zcong_def dvd_def)
apply (rule_tac x = "a mod m" in exI, auto)
apply (rule_tac x = "-(a div m)" in exI)
- apply (simp add:zdiff_eq_eq eq_zdiff_eq zadd_commute)
+ apply (simp add: diff_eq_eq eq_diff_eq add_commute)
done
lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)"
@@ -395,7 +395,7 @@
lemma zcong_zmod_aux:
"a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
- by(simp add: zdiff_zmult_distrib2 zadd_zdiff_eq eq_zdiff_eq zadd_ac)
+ by(simp add: zdiff_zmult_distrib2 add_diff_eq eq_diff_eq add_ac)
lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
apply (unfold zcong_def)
@@ -505,7 +505,7 @@
==> (r' mod r) = (s' - (r' div r) * s) * m + (t' - (r' div r) * t) * (n::int)"
apply (rule trans)
apply (rule_tac [2] xzgcda_linear_aux1 [symmetric])
- apply (simp add: eq_zdiff_eq zmult_commute)
+ apply (simp add: eq_diff_eq mult_commute)
done
lemma order_le_neq_implies_less: "(x::'a::order) \<le> y ==> x \<noteq> y ==> x < y"
--- a/src/HOL/NumberTheory/ROOT.ML Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/NumberTheory/ROOT.ML Wed Dec 03 10:49:34 2003 +0100
@@ -19,7 +19,6 @@
use_thy "Fib";
use_thy "Factorization";
use_thy "Chinese";
-use_thy "EulerFermat";
use_thy "WilsonRuss";
use_thy "WilsonBij";
use_thy "Quadratic_Reciprocity";
--- a/src/HOL/NumberTheory/WilsonBij.thy Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/NumberTheory/WilsonBij.thy Wed Dec 03 10:49:34 2003 +0100
@@ -75,9 +75,9 @@
lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
-- {* same as @{text WilsonRuss} *}
apply (unfold zcong_def)
- apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2)
+ apply (simp add: Ring_and_Field.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
- apply (simp add: zmult_commute zminus_zdiff_eq)
+ apply (simp add: mult_commute)
apply (subst zdvd_zminus_iff)
apply (subst zdvd_reduce)
apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
--- a/src/HOL/NumberTheory/WilsonRuss.thy Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Wed Dec 03 10:49:34 2003 +0100
@@ -86,9 +86,9 @@
lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
apply (unfold zcong_def)
- apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2)
+ apply (simp add: Ring_and_Field.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
- apply (simp add: zmult_commute zminus_zdiff_eq)
+ apply (simp add: mult_commute)
apply (subst zdvd_zminus_iff)
apply (subst zdvd_reduce)
apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
--- a/src/HOL/Presburger.thy Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/Presburger.thy Wed Dec 03 10:49:34 2003 +0100
@@ -395,7 +395,7 @@
apply(clarsimp)
apply(rename_tac n m)
apply(rule_tac x = "m - n*k" in exI)
- apply(simp add:int_distrib zmult_ac)
+ apply(simp add:int_distrib mult_ac)
done
lemma not_dvd_modd_pinf: "((d::int) dvd d1) ==>
@@ -405,11 +405,11 @@
apply(clarsimp)
apply(rename_tac n m)
apply(erule_tac x = "m - n*k" in allE)
- apply(simp add:int_distrib zmult_ac)
+ apply(simp add:int_distrib mult_ac)
apply(clarsimp)
apply(rename_tac n m)
apply(erule_tac x = "m + n*k" in allE)
- apply(simp add:int_distrib zmult_ac)
+ apply(simp add:int_distrib mult_ac)
done
(*=============================================================================*)
@@ -462,7 +462,7 @@
apply(clarsimp)
apply(rename_tac n m)
apply(rule_tac x = "m + n*k" in exI)
-apply(simp add:int_distrib zmult_ac)
+apply(simp add:int_distrib mult_ac)
done
@@ -473,11 +473,11 @@
apply(clarsimp)
apply(rename_tac n m)
apply(erule_tac x = "m + n*k" in allE)
-apply(simp add:int_distrib zmult_ac)
+apply(simp add:int_distrib mult_ac)
apply(clarsimp)
apply(rename_tac n m)
apply(erule_tac x = "m - n*k" in allE)
-apply(simp add:int_distrib zmult_ac)
+apply(simp add:int_distrib mult_ac)
done
@@ -626,7 +626,7 @@
assume ?LHS
then obtain x where P: "P x" ..
have "x mod d = x - (x div d)*d"
- by(simp add:zmod_zdiv_equality zmult_ac eq_zdiff_eq)
+ by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
hence Pmod: "P x = P(x mod d)" using modd by simp
show ?RHS
proof (cases)
@@ -661,7 +661,7 @@
assume ?LHS
then obtain x where P: "P x" ..
have "x mod d = x + (-(x div d))*d"
- by(simp add:zmod_zdiv_equality zmult_ac eq_zdiff_eq)
+ by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
hence Pmod: "P x = P(x mod d)" using modd by (simp only:)
show ?RHS
proof (cases)
@@ -702,7 +702,7 @@
have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)"
using minus[THEN spec, of "x - i * d"]
- by (simp add:int_distrib zdiff_zdiff_eq[symmetric])
+ by (simp add:int_distrib Ring_and_Field.diff_diff_eq[symmetric])
ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast
qed
qed
@@ -864,12 +864,12 @@
apply(drule_tac f = "op * k" in arg_cong)
apply(simp only:int_distrib)
apply(rule_tac x = "d" in exI)
- apply(simp only:zmult_ac)
+ apply(simp only:mult_ac)
done
next
assume ?Q
then obtain d where "k * c * n + k * t = (k*m)*d" by(fastsimp simp:dvd_def)
- hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib zmult_ac)
+ hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib mult_ac)
hence "((c * n + t) * k) div k = ((m*d) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
hence "c*n+t = m*d" by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
thus ?P by(simp add:dvd_def)
@@ -879,10 +879,10 @@
shows "((m::int) < (c*n+t)) = (k*m <((k*c)*n+(k*t)))" (is "?P = ?Q")
proof
assume P: ?P
- show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib zmult_ac)
+ show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib mult_ac)
next
assume ?Q
- hence "0 < k*(c*n + t - m)" by(simp add: int_distrib zmult_ac)
+ hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
with gr0 have "0 < (c*n + t - m)" by(simp add:int_0_less_mult_iff)
thus ?P by(simp)
qed
@@ -896,7 +896,7 @@
done
next
assume ?Q
- hence "m * k = (c*n + t) * k" by(simp add:int_distrib zmult_ac)
+ hence "m * k = (c*n + t) * k" by(simp add:int_distrib mult_ac)
hence "((m) * k) div k = ((c*n + t) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"])
thus ?P by(simp add: zdiv_zmult_self1[OF not0[symmetric]])
qed
@@ -904,9 +904,9 @@
lemma ac_pi_eq: assumes gr0: "0 < (k::int)" shows "(~((0::int) < (c*n + t))) = (0 < ((-k)*c)*n + ((-k)*t + k))"
proof -
have "(~ (0::int) < (c*n + t)) = (0<1-(c*n + t))" by arith
- also have "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib zmult_ac)
+ also have "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib mult_ac)
also have "0<(-1*c)*n + (-t+1) = (0 < (k*(-1*c)*n) + (k*(-t+1)))" by(rule ac_lt_eq[of _ 0,OF gr0,simplified])
- also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib zmult_ac)
+ also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib mult_ac)
finally show ?thesis .
qed
@@ -963,7 +963,7 @@
apply (simp add: linorder_not_le)
apply (drule zmult_zless_mono2_neg [OF iffD2 [OF zero_less_int_conv]])
apply assumption
- apply (simp add: zmult_ac)
+ apply (simp add: mult_ac)
done
theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
--- a/src/HOL/Real/RealOrd.thy Tue Dec 02 11:48:15 2003 +0100
+++ b/src/HOL/Real/RealOrd.thy Wed Dec 03 10:49:34 2003 +0100
@@ -1027,13 +1027,6 @@
val real_minus_divide_eq = thm"real_minus_divide_eq";
val real_divide_minus_eq = thm"real_divide_minus_eq";
val real_add_divide_distrib = thm"real_add_divide_distrib";
-
-val diff_less_eq = thm"diff_less_eq";
-val less_diff_eq = thm"less_diff_eq";
-val diff_eq_eq = thm"diff_eq_eq";
-val diff_le_eq = thm"diff_le_eq";
-val le_diff_eq = thm"le_diff_eq";
-val compare_rls = thms "compare_rls";
*}
end