# HG changeset patch # User paulson # Date 1070444974 -3600 # Node ID 8ed6989228bb80b195a787a8c7cdc59baae4251b # Parent 342451d763f95d0c28d28ad06a91fbd3169b5475 Simplification of the development of Integers diff -r 342451d763f9 -r 8ed6989228bb src/HOL/Integ/Bin.ML --- 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"; diff -r 342451d763f9 -r 8ed6989228bb src/HOL/Integ/Int.thy --- 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: "(wz) = (~ 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) = (w w+z) = (v \ (w::int))" -by simp - -lemma zadd_left_cancel_zle [simp] : "(z+v \ z+w) = (v \ (w::int))" -by simp - -(*"v\w ==> v+z \ w+z"*) -lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard] - -(*"v\w ==> z+v \ z+w"*) -lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard] - -(*"v\w ==> v+z \ w+z"*) -lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard] - -(*"v\w ==> z+v \ z+w"*) -lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard] - -lemma zadd_zle_mono: "[| w'\w; z'\z |] ==> w' + z' \ w + (z::int)" -by (erule zadd_zle_mono1 [THEN zle_trans], simp) - -lemma zadd_zless_mono: "[| w'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 \ z ==> int (nat z) = z" +by (simp add: neg_eq_less_0 zle_def not_neg_nat) + +lemma nat_le_0 [simp]: "z \ 0 ==> nat z = 0" +by (auto simp add: order_le_less neg_eq_less_0 zle_def neg_nat) + +(*An alternative condition is 0 \ 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 \ w+z) = (v \ (w::int))" +by (simp add: linorder_not_less [symmetric]) + +lemma zadd_left_cancel_zle [simp] : "(z+v \ z+w) = (v \ (w::int))" +by (simp add: linorder_not_less [symmetric]) + +(*"v\w ==> v+z \ w+z"*) +lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard] + +(*"v\w ==> z+v \ z+w"*) +lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard] + +(*"v\w ==> v+z \ w+z"*) +lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard] + +(*"v\w ==> z+v \ z+w"*) +lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard] + +lemma zadd_zle_mono: "[| w'\w; z'\z |] ==> w' + z' \ w + (z::int)" +by (erule zadd_zle_mono1 [THEN zle_trans], simp) + +lemma zadd_zless_mono: "[| w'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 0 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 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 \ (1::int)" by simp + show "i \ j ==> k + i \ k + j" by simp + show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2) + show "\i\ = (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 \ z ==> int (nat z) = z" -by (simp add: neg_eq_less_0 zle_def not_neg_nat) - -lemma nat_le_0 [simp]: "z \ 0 ==> nat z = 0" -by (auto simp add: order_le_less neg_eq_less_0 zle_def neg_nat) +lemma zless_eq_neg: "(w 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 0 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 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\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 \ (1::int)" by simp - show "i \ j ==> k + i \ k + j" by simp - show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2) - show "\i\ = (if i < 0 then -i else i)" by (simp only: zabs_def) -qed subsection{*Monotonicity of Multiplication*} lemma zmult_zle_mono1: "[| i \ j; (0::int) \ k |] ==> i*k \ j*k" - by (rule mult_right_mono) + by (rule Ring_and_Field.mult_right_mono) lemma zmult_zle_mono1_neg: "[| i \ j; k \ (0::int) |] ==> j*k \ i*k" - by (rule mult_right_mono_neg) + by (rule Ring_and_Field.mult_right_mono_neg) lemma zmult_zle_mono2: "[| i \ j; (0::int) \ k |] ==> k*i \ k*j" - by (rule mult_left_mono) + by (rule Ring_and_Field.mult_left_mono) lemma zmult_zle_mono2_neg: "[| i \ j; k \ (0::int) |] ==> k*j \ k*i" - by (rule mult_left_mono_neg) + by (rule Ring_and_Field.mult_left_mono_neg) (* \ monotonicity, BOTH arguments*) lemma zmult_zle_mono: "[| i \ j; k \ l; (0::int) \ j; (0::int) \ k |] ==> i*k \ j*l" - by (rule mult_mono) + by (rule Ring_and_Field.mult_mono) lemma zmult_zless_mono1: "[| i 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\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'<=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) = (wi 1) --> f 0 \ k --> k \ f n --> (\i \ 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 ==> int m - int n = int (m-n)" +by (induct m n rule: diff_induct, simp_all) + lemma nat_add_distrib: "[| (0::int) \ z; 0 \ 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) \ z'; z' \ 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) \ z ==> nat (z*z') = nat z * nat z'" apply (case_tac "0 \ 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 diff -r 342451d763f9 -r 8ed6989228bb src/HOL/Integ/IntDef.thy --- 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. \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. xx y. x bool" @@ -40,12 +37,14 @@ defs (overloaded) + zminus_def: "- Z == Abs_Integ(\(x,y) \ 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(\(x1,y1) \ Rep_Integ(z). \(x2,y2) \ 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(\(x1,y1) \ Rep_Integ(z). \(x2,y2) \ 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)) \ 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) = (\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'<=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 diff -r 342451d763f9 -r 8ed6989228bb src/HOL/Integ/IntDiv.thy --- 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))" diff -r 342451d763f9 -r 8ed6989228bb src/HOL/Integ/Presburger.thy --- 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 \ P (x - i * d)" using step.hyps by blast also have "\ \ 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 \ 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 \ (0::int) <= number_of (n BIT b)" diff -r 342451d763f9 -r 8ed6989228bb src/HOL/Integ/int_arith1.ML --- 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"; diff -r 342451d763f9 -r 8ed6989228bb src/HOL/NumberTheory/Gauss.thy --- 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) diff -r 342451d763f9 -r 8ed6989228bb src/HOL/NumberTheory/IntFact.thy --- 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 \ 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 diff -r 342451d763f9 -r 8ed6989228bb src/HOL/NumberTheory/IntPrimes.thy --- 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)) = (\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) \ y ==> x \ y ==> x < y" diff -r 342451d763f9 -r 8ed6989228bb src/HOL/NumberTheory/ROOT.ML --- 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"; diff -r 342451d763f9 -r 8ed6989228bb src/HOL/NumberTheory/WilsonBij.thy --- 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) diff -r 342451d763f9 -r 8ed6989228bb src/HOL/NumberTheory/WilsonRuss.thy --- 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) diff -r 342451d763f9 -r 8ed6989228bb src/HOL/Presburger.thy --- 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 \ P (x - i * d)" using step.hyps by blast also have "\ \ 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 \ 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 \ (0::int) <= number_of (n BIT b)" diff -r 342451d763f9 -r 8ed6989228bb src/HOL/Real/RealOrd.thy --- 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