further simplifications of the integer development; converting more .ML files
to Isar scripts
--- a/src/HOL/Integ/Int.thy Thu Dec 04 10:29:17 2003 +0100
+++ b/src/HOL/Integ/Int.thy Thu Dec 04 16:16:36 2003 +0100
@@ -54,75 +54,32 @@
by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
-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)
-
-lemma zminus_zle_zminus [simp]: "(- x \<le> - y) = (y \<le> (x::int))"
-by (simp add: zle_def)
-
-text{*The next several equations can make the simplifier loop!*}
-
-lemma zless_zminus: "(x < - y) = (y < - (x::int))"
-by (simp add: zless_def zdiff_def zadd_ac)
-
-lemma zminus_zless: "(- x < y) = (- y < (x::int))"
-by (simp add: zless_def zdiff_def zadd_ac)
-
-lemma zle_zminus: "(x \<le> - y) = (y \<le> - (x::int))"
-by (simp add: zle_def zminus_zless)
-
-lemma zminus_zle: "(- x \<le> y) = (- y \<le> (x::int))"
-by (simp add: zle_def zless_zminus)
-
-lemma equation_zminus: "(x = - y) = (y = - (x::int))"
-by auto
-
-lemma zminus_equation: "(- x = y) = (- (y::int) = x)"
-by auto
-
-
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 neg_nat: "neg z ==> nat z = 0"
+by (unfold nat_def, auto)
+
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 *)
+text{*An alternative condition is @{term "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)
@@ -137,10 +94,11 @@
apply (auto simp add: nat_mono_iff linorder_not_less)
done
-
subsection{*Monotonicity results*}
-(*RING AND FIELD?*)
+text{*Most are available in theory @{text Ring_and_Field}, but they are
+ not yet available: we must prove @{text zadd_zless_mono} before we
+ can prove that the integers are a ring.*}
lemma zadd_right_cancel_zless [simp]: "(v+z < w+z) = (v < (w::int))"
by (simp add: zless_def zdiff_def zadd_ac)
@@ -181,7 +139,7 @@
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)
+apply (simp_all add: zadd_zless_mono int_Suc0_eq_1 order_le_less)
done
lemma zmult_zless_mono2: "[| i<j; (0::int) < k |] ==> k*i < k*j"
@@ -191,6 +149,7 @@
apply (frule conjI [THEN zless_nat_conj [THEN iffD2]], auto)
done
+
text{*The Integers Form an Ordered Ring*}
instance int :: ordered_ring
proof
@@ -210,6 +169,39 @@
show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
qed
+
+subsection{*Comparison laws*}
+
+text{*Legacy bindings: all are in theory @{text Ring_and_Field}.*}
+
+lemma zminus_zless_zminus: "(- x < - y) = (y < (x::int))"
+ by (rule Ring_and_Field.neg_less_iff_less)
+
+lemma zminus_zle_zminus: "(- x \<le> - y) = (y \<le> (x::int))"
+ by (rule Ring_and_Field.neg_le_iff_le)
+
+
+text{*The next several equations can make the simplifier loop!*}
+
+lemma zless_zminus: "(x < - y) = (y < - (x::int))"
+ by (rule Ring_and_Field.less_minus_iff)
+
+lemma zminus_zless: "(- x < y) = (- y < (x::int))"
+ by (rule Ring_and_Field.minus_less_iff)
+
+lemma zle_zminus: "(x \<le> - y) = (y \<le> - (x::int))"
+ by (rule Ring_and_Field.le_minus_iff)
+
+lemma zminus_zle: "(- x \<le> y) = (- y \<le> (x::int))"
+ by (rule Ring_and_Field.minus_le_iff)
+
+lemma equation_zminus: "(x = - y) = (y = - (x::int))"
+ by (rule Ring_and_Field.equation_minus_iff)
+
+lemma zminus_equation: "(- x = y) = (- (y::int) = x)"
+ by (rule Ring_and_Field.minus_equation_iff)
+
+
subsection{*Lemmas about the Function @{term int} and Orderings*}
lemma negative_zless_0: "- (int (Suc n)) < 0"
@@ -254,6 +246,18 @@
subsection{*Misc Results*}
+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 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 zless_eq_neg: "(w<z) = neg(w-z)"
by (simp add: zless_def)
@@ -350,6 +354,22 @@
apply (simp add: eq_diff_eq [symmetric])
done
+
+
+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"
+apply (case_tac "neg z")
+apply (fast dest!: negD)
+apply (drule not_neg_nat [symmetric], auto)
+done
+
+
(*Legacy ML bindings, but no longer the structure Int.*)
ML
{*
@@ -372,61 +392,6 @@
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);
-*}
-
-
-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"
-apply (case_tac "neg z")
-apply (fast dest!: negD)
-apply (drule not_neg_nat [symmetric], auto)
-done
-
-
-ML
-{*
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";
--- a/src/HOL/Integ/NatBin.thy Thu Dec 04 10:29:17 2003 +0100
+++ b/src/HOL/Integ/NatBin.thy Thu Dec 04 16:16:36 2003 +0100
@@ -9,33 +9,31 @@
theory NatBin = IntPower:
text {*
- This case is simply reduced to that for the non-negative integers.
+ Arithmetic for naturals is reduced to that for the non-negative integers.
*}
instance nat :: number ..
defs (overloaded)
- nat_number_of_def: "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
+ nat_number_of_def:
+ "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
(** nat (coercion from int to nat) **)
-lemma nat_number_of: "nat (number_of w) = number_of w"
-apply (simp (no_asm) add: nat_number_of_def)
-done
-declare nat_number_of [simp] nat_0 [simp] nat_1 [simp]
+declare nat_0 [simp] nat_1 [simp]
+
+lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
+by (simp add: nat_number_of_def)
lemma numeral_0_eq_0: "Numeral0 = (0::nat)"
-apply (simp (no_asm) add: nat_number_of_def)
-done
+by (simp add: nat_number_of_def)
lemma numeral_1_eq_1: "Numeral1 = (1::nat)"
-apply (simp (no_asm) add: nat_1 nat_number_of_def)
-done
+by (simp add: nat_1 nat_number_of_def)
lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
-apply (simp (no_asm) add: numeral_1_eq_1)
-done
+by (simp add: numeral_1_eq_1)
lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
apply (unfold nat_number_of_def)
@@ -43,36 +41,36 @@
done
-(** Distributive laws for "nat". The others are in IntArith.ML, but these
- require div and mod to be defined for type "int". They also need
- some of the lemmas proved just above.**)
+text{*Distributive laws for type @{text nat}. The others are in theory
+ @{text IntArith}, but these require div and mod to be defined for type
+ "int". They also need some of the lemmas proved above.*}
lemma nat_div_distrib: "(0::int) <= z ==> nat (z div z') = nat z div nat z'"
apply (case_tac "0 <= z'")
apply (auto simp add: div_nonneg_neg_le0 DIVISION_BY_ZERO_DIV)
-apply (case_tac "z' = 0" , simp (no_asm_simp) add: DIVISION_BY_ZERO)
+apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
apply (auto elim!: nonneg_eq_int)
apply (rename_tac m m')
apply (subgoal_tac "0 <= int m div int m'")
prefer 2 apply (simp add: numeral_0_eq_0 pos_imp_zdiv_nonneg_iff)
-apply (rule inj_int [THEN injD])
-apply (simp (no_asm_simp))
+apply (rule inj_int [THEN injD], simp)
apply (rule_tac r = "int (m mod m') " in quorem_div)
- prefer 2 apply (force)
-apply (simp add: nat_less_iff [symmetric] quorem_def numeral_0_eq_0 zadd_int zmult_int)
+ prefer 2 apply force
+apply (simp add: nat_less_iff [symmetric] quorem_def numeral_0_eq_0 zadd_int
+ zmult_int)
done
(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
-lemma nat_mod_distrib: "[| (0::int) <= z; 0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
-apply (case_tac "z' = 0" , simp (no_asm_simp) add: DIVISION_BY_ZERO)
+lemma nat_mod_distrib:
+ "[| (0::int) <= z; 0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
+apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
apply (auto elim!: nonneg_eq_int)
apply (rename_tac m m')
apply (subgoal_tac "0 <= int m mod int m'")
prefer 2 apply (simp add: nat_less_iff numeral_0_eq_0 pos_mod_sign)
-apply (rule inj_int [THEN injD])
-apply (simp (no_asm_simp))
+apply (rule inj_int [THEN injD], simp)
apply (rule_tac q = "int (m div m') " in quorem_mod)
- prefer 2 apply (force)
+ prefer 2 apply force
apply (simp add: nat_less_iff [symmetric] quorem_def numeral_0_eq_0 zadd_int zmult_int)
done
@@ -80,7 +78,8 @@
(** int (coercion from nat to int) **)
(*"neg" is used in rewrite rules for binary comparisons*)
-lemma int_nat_number_of: "int (number_of v :: nat) =
+lemma int_nat_number_of:
+ "int (number_of v :: nat) =
(if neg (number_of v) then 0
else (number_of v :: int))"
by (simp del: nat_number_of
@@ -92,18 +91,20 @@
lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
apply (rule sym)
-apply (simp (no_asm_simp) add: nat_eq_iff int_Suc)
+apply (simp add: nat_eq_iff int_Suc)
done
-lemma Suc_nat_number_of_add: "Suc (number_of v + n) =
+lemma Suc_nat_number_of_add:
+ "Suc (number_of v + n) =
(if neg (number_of v) then 1+n else number_of (bin_succ v) + n)"
by (simp del: nat_number_of
add: nat_number_of_def neg_nat
Suc_nat_eq_nat_zadd1 number_of_succ)
-lemma Suc_nat_number_of: "Suc (number_of v) =
+lemma Suc_nat_number_of:
+ "Suc (number_of v) =
(if neg (number_of v) then 1 else number_of (bin_succ v))"
-apply (cut_tac n = "0" in Suc_nat_number_of_add)
+apply (cut_tac n = 0 in Suc_nat_number_of_add)
apply (simp cong del: if_weak_cong)
done
declare Suc_nat_number_of [simp]
@@ -112,7 +113,8 @@
(** Addition **)
(*"neg" is used in rewrite rules for binary comparisons*)
-lemma add_nat_number_of: "(number_of v :: nat) + number_of v' =
+lemma add_nat_number_of:
+ "(number_of v :: nat) + number_of v' =
(if neg (number_of v) then number_of v'
else if neg (number_of v') then number_of v
else number_of (bin_add v v'))"
@@ -125,12 +127,13 @@
(** Subtraction **)
-lemma diff_nat_eq_if: "nat z - nat z' =
+lemma diff_nat_eq_if:
+ "nat z - nat z' =
(if neg z' then nat z
else let d = z-z' in
if neg d then 0 else nat d)"
-apply (simp (no_asm) add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
-apply (simp (no_asm) add: diff_is_0_eq nat_le_eq_zle)
+apply (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
+apply (simp add: diff_is_0_eq nat_le_eq_zle)
done
lemma diff_nat_number_of:
@@ -145,7 +148,8 @@
(** Multiplication **)
-lemma mult_nat_number_of: "(number_of v :: nat) * number_of v' =
+lemma mult_nat_number_of:
+ "(number_of v :: nat) * number_of v' =
(if neg (number_of v) then 0 else number_of (bin_mult v v'))"
by (force dest!: neg_nat
simp del: nat_number_of
@@ -156,7 +160,8 @@
(** Quotient **)
-lemma div_nat_number_of: "(number_of v :: nat) div number_of v' =
+lemma div_nat_number_of:
+ "(number_of v :: nat) div number_of v' =
(if neg (number_of v) then 0
else nat (number_of v div number_of v'))"
by (force dest!: neg_nat
@@ -168,7 +173,8 @@
(** Remainder **)
-lemma mod_nat_number_of: "(number_of v :: nat) mod number_of v' =
+lemma mod_nat_number_of:
+ "(number_of v :: nat) mod number_of v' =
(if neg (number_of v) then 0
else if neg (number_of v') then number_of v
else nat (number_of v mod number_of v'))"
@@ -229,18 +235,19 @@
(** Equals (=) **)
-lemma eq_nat_nat_iff: "[| (0::int) <= z; 0 <= z' |] ==> (nat z = nat z') = (z=z')"
-apply (auto elim!: nonneg_eq_int)
-done
+lemma eq_nat_nat_iff:
+ "[| (0::int) <= z; 0 <= z' |] ==> (nat z = nat z') = (z=z')"
+by (auto elim!: nonneg_eq_int)
(*"neg" is used in rewrite rules for binary comparisons*)
-lemma eq_nat_number_of: "((number_of v :: nat) = number_of v') =
+lemma eq_nat_number_of:
+ "((number_of v :: nat) = number_of v') =
(if neg (number_of v) then (iszero (number_of v') | neg (number_of v'))
else if neg (number_of v') then iszero (number_of v)
else iszero (number_of (bin_add v (bin_minus v'))))"
apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def
- split add: split_if cong add: imp_cong);
+ split add: split_if cong add: imp_cong)
apply (simp only: nat_eq_iff nat_eq_iff2)
apply (simp add: not_neg_eq_ge_0 [symmetric])
done
@@ -250,13 +257,13 @@
(** Less-than (<) **)
(*"neg" is used in rewrite rules for binary comparisons*)
-lemma less_nat_number_of: "((number_of v :: nat) < number_of v') =
+lemma less_nat_number_of:
+ "((number_of v :: nat) < number_of v') =
(if neg (number_of v) then neg (number_of (bin_minus v'))
else neg (number_of (bin_add v (bin_minus v'))))"
apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
- cong add: imp_cong);
-apply (simp add: );
+ cong add: imp_cong, simp)
done
declare less_nat_number_of [simp]
@@ -264,7 +271,8 @@
(** Less-than-or-equals (<=) **)
-lemma le_nat_number_of_eq_not_less: "(number_of x <= (number_of y::nat)) =
+lemma le_nat_number_of_eq_not_less:
+ "(number_of x <= (number_of y::nat)) =
(~ number_of y < (number_of x::nat))"
apply (rule linorder_not_less [symmetric])
done
@@ -279,8 +287,7 @@
(** Nat **)
lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
-apply (simp add: numerals)
-done
+by (simp add: numerals)
(*Expresses a natural number constant as the Suc of another one.
NOT suitable for rewriting because n recurs in the condition.*)
@@ -289,8 +296,7 @@
(** Arith **)
lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
-apply (simp add: numerals)
-done
+by (simp add: numerals)
(* These two can be useful when m = number_of... *)
@@ -310,91 +316,96 @@
done
lemma diff_less': "[| 0<n; 0<m |] ==> m - n < (m::nat)"
-apply (simp add: diff_less numerals)
-done
+by (simp add: diff_less numerals)
declare diff_less' [of "number_of v", standard, simp]
(** Power **)
lemma power_two: "(p::nat) ^ 2 = p*p"
-apply (simp add: numerals)
-done
+by (simp add: numerals)
(*** Comparisons involving (0::nat) ***)
-lemma eq_number_of_0: "(number_of v = (0::nat)) =
+lemma eq_number_of_0:
+ "(number_of v = (0::nat)) =
(if neg (number_of v) then True else iszero (number_of v))"
-apply (simp (no_asm) add: numeral_0_eq_0 [symmetric] iszero_0)
+apply (simp add: numeral_0_eq_0 [symmetric] iszero_0)
done
-lemma eq_0_number_of: "((0::nat) = number_of v) =
+lemma eq_0_number_of:
+ "((0::nat) = number_of v) =
(if neg (number_of v) then True else iszero (number_of v))"
apply (rule trans [OF eq_sym_conv eq_number_of_0])
done
-lemma less_0_number_of: "((0::nat) < number_of v) = neg (number_of (bin_minus v))"
-apply (simp (no_asm) add: numeral_0_eq_0 [symmetric])
-done
+lemma less_0_number_of:
+ "((0::nat) < number_of v) = neg (number_of (bin_minus v))"
+by (simp add: numeral_0_eq_0 [symmetric])
(*Simplification already handles n<0, n<=0 and 0<=n.*)
declare eq_number_of_0 [simp] eq_0_number_of [simp] less_0_number_of [simp]
lemma neg_imp_number_of_eq_0: "neg (number_of v) ==> number_of v = (0::nat)"
-apply (simp (no_asm_simp) add: numeral_0_eq_0 [symmetric] iszero_0)
-done
+by (simp add: numeral_0_eq_0 [symmetric] iszero_0)
(*** Comparisons involving Suc ***)
-lemma eq_number_of_Suc [simp]: "(number_of v = Suc n) =
+lemma eq_number_of_Suc [simp]:
+ "(number_of v = Suc n) =
(let pv = number_of (bin_pred v) in
if neg pv then False else nat pv = n)"
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
number_of_pred nat_number_of_def
- split add: split_if);
+ split add: split_if)
apply (rule_tac x = "number_of v" in spec)
apply (auto simp add: nat_eq_iff)
done
-lemma Suc_eq_number_of [simp]: "(Suc n = number_of v) =
+lemma Suc_eq_number_of [simp]:
+ "(Suc n = number_of v) =
(let pv = number_of (bin_pred v) in
if neg pv then False else nat pv = n)"
apply (rule trans [OF eq_sym_conv eq_number_of_Suc])
done
-lemma less_number_of_Suc [simp]: "(number_of v < Suc n) =
+lemma less_number_of_Suc [simp]:
+ "(number_of v < Suc n) =
(let pv = number_of (bin_pred v) in
if neg pv then True else nat pv < n)"
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
number_of_pred nat_number_of_def
- split add: split_if);
+ split add: split_if)
apply (rule_tac x = "number_of v" in spec)
apply (auto simp add: nat_less_iff)
done
-lemma less_Suc_number_of [simp]: "(Suc n < number_of v) =
+lemma less_Suc_number_of [simp]:
+ "(Suc n < number_of v) =
(let pv = number_of (bin_pred v) in
if neg pv then False else n < nat pv)"
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less
number_of_pred nat_number_of_def
- split add: split_if);
+ split add: split_if)
apply (rule_tac x = "number_of v" in spec)
apply (auto simp add: zless_nat_eq_int_zless)
done
-lemma le_number_of_Suc [simp]: "(number_of v <= Suc n) =
+lemma le_number_of_Suc [simp]:
+ "(number_of v <= Suc n) =
(let pv = number_of (bin_pred v) in
if neg pv then True else nat pv <= n)"
-apply (simp (no_asm) add: Let_def less_Suc_number_of linorder_not_less [symmetric])
+apply (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
done
-lemma le_Suc_number_of [simp]: "(Suc n <= number_of v) =
+lemma le_Suc_number_of [simp]:
+ "(Suc n <= number_of v) =
(let pv = number_of (bin_pred v) in
if neg pv then False else n <= nat pv)"
-apply (simp (no_asm) add: Let_def less_number_of_Suc linorder_not_less [symmetric])
+apply (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
done
@@ -402,46 +413,44 @@
declare zadd_int [symmetric, simp]
lemma lemma1: "(m+m = n+n) = (m = (n::int))"
-apply auto
-done
+by auto
lemma lemma2: "m+m ~= (1::int) + (n + n)"
apply auto
apply (drule_tac f = "%x. x mod 2" in arg_cong)
-apply (simp (no_asm_use) add: zmod_zadd1_eq)
+apply (simp add: zmod_zadd1_eq)
done
-lemma eq_number_of_BIT_BIT: "((number_of (v BIT x) ::int) = number_of (w BIT y)) =
+lemma eq_number_of_BIT_BIT:
+ "((number_of (v BIT x) ::int) = number_of (w BIT y)) =
(x=y & (((number_of v) ::int) = number_of w))"
by (simp only: simp_thms number_of_BIT lemma1 lemma2 eq_commute
Ring_and_Field.add_left_cancel add_assoc left_zero
- split add: split_if cong: imp_cong);
+ split add: split_if cong: imp_cong)
-lemma eq_number_of_BIT_Pls: "((number_of (v BIT x) ::int) = number_of bin.Pls) =
+lemma eq_number_of_BIT_Pls:
+ "((number_of (v BIT x) ::int) = number_of bin.Pls) =
(x=False & (((number_of v) ::int) = number_of bin.Pls))"
apply (simp only: simp_thms add: number_of_BIT number_of_Pls eq_commute
split add: split_if cong: imp_cong)
-apply (rule_tac x = "number_of v" in spec)
-apply safe
+apply (rule_tac x = "number_of v" in spec, safe)
apply (simp_all (no_asm_use))
apply (drule_tac f = "%x. x mod 2" in arg_cong)
-apply (simp (no_asm_use) add: zmod_zadd1_eq)
+apply (simp add: zmod_zadd1_eq)
done
-lemma eq_number_of_BIT_Min: "((number_of (v BIT x) ::int) = number_of bin.Min) =
+lemma eq_number_of_BIT_Min:
+ "((number_of (v BIT x) ::int) = number_of bin.Min) =
(x=True & (((number_of v) ::int) = number_of bin.Min))"
apply (simp only: simp_thms add: number_of_BIT number_of_Min eq_commute
split add: split_if cong: imp_cong)
-apply (rule_tac x = "number_of v" in spec)
-apply auto
-apply (drule_tac f = "%x. x mod 2" in arg_cong)
-apply auto
+apply (rule_tac x = "number_of v" in spec, auto)
+apply (drule_tac f = "%x. x mod 2" in arg_cong, auto)
done
lemma eq_number_of_Pls_Min: "(number_of bin.Pls ::int) ~= number_of bin.Min"
-apply auto
-done
+by auto
@@ -452,7 +461,8 @@
apply (simp_all (no_asm_simp) add: nat_mult_distrib)
done
-lemma power_nat_number_of: "(number_of v :: nat) ^ n =
+lemma power_nat_number_of:
+ "(number_of v :: nat) ^ n =
(if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))"
by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
split add: split_if cong: imp_cong)
@@ -465,33 +475,32 @@
(*** Literal arithmetic involving powers, type int ***)
lemma zpower_even: "(z::int) ^ (2*a) = (z^a)^2"
-apply (simp (no_asm) add: zpower_zpower mult_commute)
-done
+by (simp add: zpower_zpower mult_commute)
lemma zpower_two: "(p::int) ^ 2 = p*p"
-apply (simp add: numerals)
-done
+by (simp add: numerals)
lemma zpower_odd: "(z::int) ^ (2*a + 1) = z * (z^a)^2"
-apply (simp (no_asm) add: zpower_even zpower_zadd_distrib)
-done
+by (simp add: zpower_even zpower_zadd_distrib)
-lemma zpower_number_of_even: "(z::int) ^ number_of (w BIT False) =
+lemma zpower_number_of_even:
+ "(z::int) ^ number_of (w BIT False) =
(let w = z ^ (number_of w) in w*w)"
apply (simp del: nat_number_of add: nat_number_of_def number_of_BIT Let_def)
apply (simp only: number_of_add)
-apply (rule_tac x = "number_of w" in spec , clarify)
+apply (rule_tac x = "number_of w" in spec, clarify)
apply (case_tac " (0::int) <= x")
apply (auto simp add: nat_mult_distrib zpower_even zpower_two)
done
-lemma zpower_number_of_odd: "(z::int) ^ number_of (w BIT True) =
+lemma zpower_number_of_odd:
+ "(z::int) ^ number_of (w BIT True) =
(if (0::int) <= number_of w
then (let w = z ^ (number_of w) in z*w*w)
else 1)"
apply (simp del: nat_number_of add: nat_number_of_def number_of_BIT Let_def)
apply (simp only: number_of_add int_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0)
-apply (rule_tac x = "number_of w" in spec , clarify)
+apply (rule_tac x = "number_of w" in spec, clarify)
apply (auto simp add: nat_add_distrib nat_mult_distrib zpower_even zpower_two neg_nat)
done
@@ -606,6 +615,111 @@
val nat_number = thms"nat_number";
*}
+subsection {*Lemmas for the Combination and Cancellation Simprocs*}
+
+lemma nat_number_of_add_left:
+ "number_of v + (number_of v' + (k::nat)) =
+ (if neg (number_of v) then number_of v' + k
+ else if neg (number_of v') then number_of v + k
+ else number_of (bin_add v v') + k)"
+apply simp
+done
+
+
+(** For combine_numerals **)
+
+lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
+by (simp add: add_mult_distrib)
+
+
+(** For cancel_numerals **)
+
+lemma nat_diff_add_eq1:
+ "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
+by (simp split add: nat_diff_split add: add_mult_distrib)
+
+lemma nat_diff_add_eq2:
+ "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
+by (simp split add: nat_diff_split add: add_mult_distrib)
+
+lemma nat_eq_add_iff1:
+ "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_eq_add_iff2:
+ "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_less_add_iff1:
+ "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_less_add_iff2:
+ "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_le_add_iff1:
+ "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_le_add_iff2:
+ "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+
+(** For cancel_numeral_factors **)
+
+lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
+by auto
+
+lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
+by auto
+
+lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
+by auto
+
+lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
+by auto
+
+
+(** For cancel_factor **)
+
+lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
+by auto
+
+lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
+by auto
+
+lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
+by auto
+
+lemma nat_mult_div_cancel_disj:
+ "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
+by (simp add: nat_mult_div_cancel1)
+
+ML
+{*
+val nat_number_of_add_left = thm"nat_number_of_add_left";
+val left_add_mult_distrib = thm"left_add_mult_distrib";
+val nat_diff_add_eq1 = thm"nat_diff_add_eq1";
+val nat_diff_add_eq2 = thm"nat_diff_add_eq2";
+val nat_eq_add_iff1 = thm"nat_eq_add_iff1";
+val nat_eq_add_iff2 = thm"nat_eq_add_iff2";
+val nat_less_add_iff1 = thm"nat_less_add_iff1";
+val nat_less_add_iff2 = thm"nat_less_add_iff2";
+val nat_le_add_iff1 = thm"nat_le_add_iff1";
+val nat_le_add_iff2 = thm"nat_le_add_iff2";
+val nat_mult_le_cancel1 = thm"nat_mult_le_cancel1";
+val nat_mult_less_cancel1 = thm"nat_mult_less_cancel1";
+val nat_mult_eq_cancel1 = thm"nat_mult_eq_cancel1";
+val nat_mult_div_cancel1 = thm"nat_mult_div_cancel1";
+val nat_mult_le_cancel_disj = thm"nat_mult_le_cancel_disj";
+val nat_mult_less_cancel_disj = thm"nat_mult_less_cancel_disj";
+val nat_mult_eq_cancel_disj = thm"nat_mult_eq_cancel_disj";
+val nat_mult_div_cancel_disj = thm"nat_mult_div_cancel_disj";
+*}
+
+
subsection {* Configuration of the code generator *}
ML {*
--- a/src/HOL/Integ/NatSimprocs.ML Thu Dec 04 10:29:17 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,160 +0,0 @@
-(* Title: HOL/NatSimprocs.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 2000 University of Cambridge
-
-Simprocs for nat numerals (see also nat_simprocs.ML).
-*)
-
-val ss_Int = simpset_of Int_thy;
-
-(** For simplifying Suc m - #n **)
-
-Goal "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)";
-by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1]
- addsplits [nat_diff_split]) 1);
-qed "Suc_diff_eq_diff_pred";
-
-(*Now just instantiating n to (number_of v) does the right simplification,
- but with some redundant inequality tests.*)
-Goal "neg (number_of (bin_pred v)) = (number_of v = (0::nat))";
-by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0)" 1);
-by (asm_simp_tac (HOL_ss addsimps [less_Suc_eq_le, le_0_eq]) 1);
-by (stac less_number_of_Suc 1);
-by (Simp_tac 1);
-qed "neg_number_of_bin_pred_iff_0";
-
-Goal "neg (number_of (bin_minus v)) ==> \
-\ Suc m - (number_of v) = m - (number_of (bin_pred v))";
-by (stac Suc_diff_eq_diff_pred 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (asm_full_simp_tac (ss_Int addsimps [diff_nat_number_of,
- less_0_number_of RS sym, neg_number_of_bin_pred_iff_0]) 1);
-qed "Suc_diff_number_of";
-
-(* now redundant because of the inverse_fold simproc
- Addsimps [Suc_diff_number_of]; *)
-
-Goal "nat_case a f (number_of v) = \
-\ (let pv = number_of (bin_pred v) in \
-\ if neg pv then a else f (nat pv))";
-by (simp_tac
- (simpset() addsplits [nat.split]
- addsimps [Let_def, neg_number_of_bin_pred_iff_0]) 1);
-qed "nat_case_number_of";
-
-Goal "nat_case a f ((number_of v) + n) = \
-\ (let pv = number_of (bin_pred v) in \
-\ if neg pv then nat_case a f n else f (nat pv + n))";
-by (stac add_eq_if 1);
-by (asm_simp_tac
- (simpset() addsplits [nat.split]
- addsimps [numeral_1_eq_Suc_0 RS sym, Let_def,
- neg_imp_number_of_eq_0, neg_number_of_bin_pred_iff_0]) 1);
-qed "nat_case_add_eq_if";
-
-Addsimps [nat_case_number_of, nat_case_add_eq_if];
-
-
-Goal "nat_rec a f (number_of v) = \
-\ (let pv = number_of (bin_pred v) in \
-\ if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))";
-by (case_tac "(number_of v)::nat" 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [Let_def, neg_number_of_bin_pred_iff_0])));
-by (asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1);
-qed "nat_rec_number_of";
-
-Goal "nat_rec a f (number_of v + n) = \
-\ (let pv = number_of (bin_pred v) in \
-\ if neg pv then nat_rec a f n \
-\ else f (nat pv + n) (nat_rec a f (nat pv + n)))";
-by (stac add_eq_if 1);
-by (asm_simp_tac
- (simpset() addsplits [nat.split]
- addsimps [numeral_1_eq_Suc_0 RS sym, Let_def,
- neg_imp_number_of_eq_0, neg_number_of_bin_pred_iff_0]) 1);
-qed "nat_rec_add_eq_if";
-
-Addsimps [nat_rec_number_of, nat_rec_add_eq_if];
-
-
-(** For simplifying # m - Suc n **)
-
-Goal "m - Suc n = (m - 1) - n";
-by (simp_tac (numeral_ss addsplits [nat_diff_split]) 1);
-qed "diff_Suc_eq_diff_pred";
-
-(*Obsolete because of natdiff_cancel_numerals
- Addsimps [inst "m" "number_of ?v" diff_Suc_eq_diff_pred];
- It LOOPS if Numeral1 is being replaced by 1.
-*)
-
-
-(** Evens and Odds, for Mutilated Chess Board **)
-
-(*Case analysis on b<2*)
-Goal "(n::nat) < 2 ==> n = 0 | n = Suc 0";
-by (arith_tac 1);
-qed "less_2_cases";
-
-Goal "Suc(Suc(m)) mod 2 = m mod 2";
-by (subgoal_tac "m mod 2 < 2" 1);
-by (Asm_simp_tac 2);
-by (etac (less_2_cases RS disjE) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Let_def, mod_Suc, nat_1])));
-qed "mod2_Suc_Suc";
-Addsimps [mod2_Suc_Suc];
-
-Goal "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)";
-by (subgoal_tac "m mod 2 < 2" 1);
-by (Asm_simp_tac 2);
-by (auto_tac (claset(), simpset() delsimps [mod_less_divisor]));
-qed "mod2_gr_0";
-Addsimps [mod2_gr_0];
-
-(** Removal of small numerals: Numeral0, Numeral1 and (in additive positions) 2 **)
-
-Goal "2 + n = Suc (Suc n)";
-by (Simp_tac 1);
-qed "add_2_eq_Suc";
-
-Goal "n + 2 = Suc (Suc n)";
-by (Simp_tac 1);
-qed "add_2_eq_Suc'";
-
-Addsimps [numeral_0_eq_0, numeral_1_eq_1, add_2_eq_Suc, add_2_eq_Suc'];
-
-(*Can be used to eliminate long strings of Sucs, but not by default*)
-Goal "Suc (Suc (Suc n)) = 3 + n";
-by (Simp_tac 1);
-qed "Suc3_eq_add_3";
-
-
-(** To collapse some needless occurrences of Suc
- At least three Sucs, since two and fewer are rewritten back to Suc again!
-
- We already have some rules to simplify operands smaller than 3.
-**)
-
-Goal "m div (Suc (Suc (Suc n))) = m div (3+n)";
-by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
-qed "div_Suc_eq_div_add3";
-
-Goal "m mod (Suc (Suc (Suc n))) = m mod (3+n)";
-by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
-qed "mod_Suc_eq_mod_add3";
-
-Addsimps [div_Suc_eq_div_add3, mod_Suc_eq_mod_add3];
-
-Goal "(Suc (Suc (Suc m))) div n = (3+m) div n";
-by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
-qed "Suc_div_eq_add3_div";
-
-Goal "(Suc (Suc (Suc m))) mod n = (3+m) mod n";
-by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
-qed "Suc_mod_eq_add3_mod";
-
-Addsimps [inst "n" "number_of ?v" Suc_div_eq_add3_div,
- inst "n" "number_of ?v" Suc_mod_eq_add3_mod];
--- a/src/HOL/Integ/NatSimprocs.thy Thu Dec 04 10:29:17 2003 +0100
+++ b/src/HOL/Integ/NatSimprocs.thy Thu Dec 04 16:16:36 2003 +0100
@@ -10,4 +10,126 @@
setup nat_simprocs_setup
+subsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*}
+
+text{*Where K above is a literal*}
+
+lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
+by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
+
+(*Now just instantiating n to (number_of v) does the right simplification,
+ but with some redundant inequality tests.*)
+lemma neg_number_of_bin_pred_iff_0:
+ "neg (number_of (bin_pred v)) = (number_of v = (0::nat))"
+apply (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0) ")
+apply (simp only: less_Suc_eq_le le_0_eq)
+apply (subst less_number_of_Suc, simp)
+done
+
+text{*No longer required as a simprule because of the @{text inverse_fold}
+ simproc*}
+lemma Suc_diff_number_of:
+ "neg (number_of (bin_minus v)) ==>
+ Suc m - (number_of v) = m - (number_of (bin_pred v))"
+apply (subst Suc_diff_eq_diff_pred, simp, simp)
+apply (force simp only: diff_nat_number_of less_0_number_of [symmetric]
+ neg_number_of_bin_pred_iff_0)
+done
+
+lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
+by (simp add: numerals split add: nat_diff_split)
+
+
+subsection{*For @{term nat_case} and @{term nat_rec}*}
+
+lemma nat_case_number_of [simp]:
+ "nat_case a f (number_of v) =
+ (let pv = number_of (bin_pred v) in
+ if neg pv then a else f (nat pv))"
+by (simp split add: nat.split add: Let_def neg_number_of_bin_pred_iff_0)
+
+lemma nat_case_add_eq_if [simp]:
+ "nat_case a f ((number_of v) + n) =
+ (let pv = number_of (bin_pred v) in
+ if neg pv then nat_case a f n else f (nat pv + n))"
+apply (subst add_eq_if)
+apply (simp split add: nat.split
+ add: numeral_1_eq_Suc_0 [symmetric] Let_def
+ neg_imp_number_of_eq_0 neg_number_of_bin_pred_iff_0)
+done
+
+lemma nat_rec_number_of [simp]:
+ "nat_rec a f (number_of v) =
+ (let pv = number_of (bin_pred v) in
+ if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
+apply (case_tac " (number_of v) ::nat")
+apply (simp_all (no_asm_simp) add: Let_def neg_number_of_bin_pred_iff_0)
+apply (simp split add: split_if_asm)
+done
+
+lemma nat_rec_add_eq_if [simp]:
+ "nat_rec a f (number_of v + n) =
+ (let pv = number_of (bin_pred v) in
+ if neg pv then nat_rec a f n
+ else f (nat pv + n) (nat_rec a f (nat pv + n)))"
+apply (subst add_eq_if)
+apply (simp split add: nat.split
+ add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0
+ neg_number_of_bin_pred_iff_0)
+done
+
+
+subsection{*Various Other Lemmas*}
+
+subsubsection{*Evens and Odds, for Mutilated Chess Board*}
+
+(*Case analysis on b<2*)
+lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
+by arith
+
+lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
+apply (subgoal_tac "m mod 2 < 2")
+apply (erule less_2_cases [THEN disjE])
+apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
+done
+
+lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
+apply (subgoal_tac "m mod 2 < 2")
+apply (force simp del: mod_less_divisor, simp)
+done
+
+subsubsection{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
+
+lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
+by simp
+
+lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
+by simp
+
+declare numeral_0_eq_0 [simp] numeral_1_eq_1 [simp]
+
+text{*Can be used to eliminate long strings of Sucs, but not by default*}
+lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
+by simp
+
+
+text{*These lemmas collapse some needless occurrences of Suc:
+ at least three Sucs, since two and fewer are rewritten back to Suc again!
+ We already have some rules to simplify operands smaller than 3.*}
+
+lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
+by (simp add: Suc3_eq_add_3)
+
+lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
+by (simp add: Suc3_eq_add_3)
+
+lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
+by (simp add: Suc3_eq_add_3)
+
+lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
+by (simp add: Suc3_eq_add_3)
+
+declare Suc_div_eq_add3_div [of _ "number_of v", standard, simp]
+declare Suc_mod_eq_add3_mod [of _ "number_of v", standard, simp]
+
end
--- a/src/HOL/Integ/int_arith1.ML Thu Dec 04 10:29:17 2003 +0100
+++ b/src/HOL/Integ/int_arith1.ML Thu Dec 04 16:16:36 2003 +0100
@@ -420,9 +420,6 @@
Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
-(*The Abel_Cancel simprocs are now obsolete*)
-Delsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
-
(*examples:
print_depth 22;
set timing;
--- a/src/HOL/Integ/nat_simprocs.ML Thu Dec 04 10:29:17 2003 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML Thu Dec 04 16:16:36 2003 +0100
@@ -6,102 +6,6 @@
Simprocs for nat numerals.
*)
-Goal "number_of v + (number_of v' + (k::nat)) = \
-\ (if neg (number_of v) then number_of v' + k \
-\ else if neg (number_of v') then number_of v + k \
-\ else number_of (bin_add v v') + k)";
-by (Simp_tac 1);
-qed "nat_number_of_add_left";
-
-
-(** For combine_numerals **)
-
-Goal "i*u + (j*u + k) = (i+j)*u + (k::nat)";
-by (asm_simp_tac (simpset() addsimps [add_mult_distrib]) 1);
-qed "left_add_mult_distrib";
-
-
-(** For cancel_numerals **)
-
-Goal "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]
- addsimps [add_mult_distrib]) 1);
-qed "nat_diff_add_eq1";
-
-Goal "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]
- addsimps [add_mult_distrib]) 1);
-qed "nat_diff_add_eq2";
-
-Goal "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
- addsimps [add_mult_distrib]));
-qed "nat_eq_add_iff1";
-
-Goal "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
- addsimps [add_mult_distrib]));
-qed "nat_eq_add_iff2";
-
-Goal "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
- addsimps [add_mult_distrib]));
-qed "nat_less_add_iff1";
-
-Goal "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
- addsimps [add_mult_distrib]));
-qed "nat_less_add_iff2";
-
-Goal "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
- addsimps [add_mult_distrib]));
-qed "nat_le_add_iff1";
-
-Goal "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
- addsimps [add_mult_distrib]));
-qed "nat_le_add_iff2";
-
-
-(** For cancel_numeral_factors **)
-
-Goal "(0::nat) < k ==> (k*m <= k*n) = (m<=n)";
-by Auto_tac;
-qed "nat_mult_le_cancel1";
-
-Goal "(0::nat) < k ==> (k*m < k*n) = (m<n)";
-by Auto_tac;
-qed "nat_mult_less_cancel1";
-
-Goal "(0::nat) < k ==> (k*m = k*n) = (m=n)";
-by Auto_tac;
-qed "nat_mult_eq_cancel1";
-
-Goal "(0::nat) < k ==> (k*m) div (k*n) = (m div n)";
-by Auto_tac;
-qed "nat_mult_div_cancel1";
-
-
-(** For cancel_factor **)
-
-Goal "(k*m <= k*n) = ((0::nat) < k --> m<=n)";
-by Auto_tac;
-qed "nat_mult_le_cancel_disj";
-
-Goal "(k*m < k*n) = ((0::nat) < k & m<n)";
-by Auto_tac;
-qed "nat_mult_less_cancel_disj";
-
-Goal "(k*m = k*n) = (k = (0::nat) | m=n)";
-by Auto_tac;
-qed "nat_mult_eq_cancel_disj";
-
-Goal "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)";
-by (simp_tac (simpset() addsimps [nat_mult_div_cancel1]) 1);
-qed "nat_mult_div_cancel_disj";
-
-
structure Nat_Numeral_Simprocs =
struct
--- a/src/HOL/IsaMakefile Thu Dec 04 10:29:17 2003 +0100
+++ b/src/HOL/IsaMakefile Thu Dec 04 16:16:36 2003 +0100
@@ -88,8 +88,7 @@
Integ/cooper_dec.ML Integ/cooper_proof.ML \
Integ/Equiv.thy Integ/Int.thy Integ/IntArith.thy Integ/IntDef.thy \
Integ/IntDiv.thy Integ/IntPower.thy \
- Integ/NatBin.thy Integ/NatSimprocs.ML \
- Integ/NatSimprocs.thy Integ/int_arith1.ML \
+ Integ/NatBin.thy Integ/NatSimprocs.thy Integ/int_arith1.ML \
Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \