# HG changeset patch # User wenzelm # Date 1470859438 -7200 # Node ID 804b80a80016578e1f3a3a09e1ac5b70f1862de3 # Parent f8e79d14d61fff02993951d1388bd92124710955 misc tuning and modernization; diff -r f8e79d14d61f -r 804b80a80016 src/HOL/Int.thy --- a/src/HOL/Int.thy Wed Aug 10 16:55:49 2016 +0200 +++ b/src/HOL/Int.thy Wed Aug 10 22:03:58 2016 +0200 @@ -6,13 +6,13 @@ section \The Integers as Equivalence Classes over Pairs of Natural Numbers\ theory Int -imports Equiv_Relations Power Quotient Fun_Def + imports Equiv_Relations Power Quotient Fun_Def begin subsection \Definition of integers as a quotient type\ -definition intrel :: "(nat \ nat) \ (nat \ nat) \ bool" where - "intrel = (\(x, y) (u, v). x + v = u + y)" +definition intrel :: "(nat \ nat) \ (nat \ nat) \ bool" + where "intrel = (\(x, y) (u, v). x + v = u + y)" lemma intrel_iff [simp]: "intrel (x, y) (u, v) \ x + v = u + y" by (simp add: intrel_def) @@ -20,17 +20,15 @@ quotient_type int = "nat \ nat" / "intrel" morphisms Rep_Integ Abs_Integ proof (rule equivpI) - show "reflp intrel" - unfolding reflp_def by auto - show "symp intrel" - unfolding symp_def by auto - show "transp intrel" - unfolding transp_def by auto + show "reflp intrel" by (auto simp: reflp_def) + show "symp intrel" by (auto simp: symp_def) + show "transp intrel" by (auto simp: transp_def) qed lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]: - "(!!x y. z = Abs_Integ (x, y) ==> P) ==> P" -by (induct z) auto + "(\x y. z = Abs_Integ (x, y) \ P) \ P" + by (induct z) auto + subsection \Integers form a commutative ring\ @@ -58,33 +56,31 @@ proof (clarsimp) fix s t u v w x y z :: nat assume "s + v = u + t" and "w + z = y + x" - hence "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x) - = (u + t) * w + (s + v) * x + u * (y + x) + v * (w + z)" + then have "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x) = + (u + t) * w + (s + v) * x + u * (y + x) + v * (w + z)" by simp - thus "(s * w + t * x) + (u * z + v * y) = (u * y + v * z) + (s * x + t * w)" + then show "(s * w + t * x) + (u * z + v * y) = (u * y + v * z) + (s * x + t * w)" by (simp add: algebra_simps) qed instance - by standard (transfer, clarsimp simp: algebra_simps)+ + by standard (transfer; clarsimp simp: algebra_simps)+ end -abbreviation int :: "nat \ int" where - "int \ of_nat" +abbreviation int :: "nat \ int" + where "int \ of_nat" lemma int_def: "int n = Abs_Integ (n, 0)" - by (induct n, simp add: zero_int.abs_eq, - simp add: one_int.abs_eq plus_int.abs_eq) + by (induct n) (simp add: zero_int.abs_eq, simp add: one_int.abs_eq plus_int.abs_eq) -lemma int_transfer [transfer_rule]: - "(rel_fun (op =) pcr_int) (\n. (n, 0)) int" - unfolding rel_fun_def int.pcr_cr_eq cr_int_def int_def by simp +lemma int_transfer [transfer_rule]: "(rel_fun (op =) pcr_int) (\n. (n, 0)) int" + by (simp add: rel_fun_def int.pcr_cr_eq cr_int_def int_def) -lemma int_diff_cases: - obtains (diff) m n where "z = int m - int n" +lemma int_diff_cases: obtains (diff) m n where "z = int m - int n" by transfer clarsimp + subsection \Integers are totally ordered\ instantiation int :: linorder @@ -106,18 +102,16 @@ instantiation int :: distrib_lattice begin -definition - "(inf :: int \ int \ int) = min" +definition "(inf :: int \ int \ int) = min" -definition - "(sup :: int \ int \ int) = max" +definition "(sup :: int \ int \ int) = max" instance - by intro_classes - (auto simp add: inf_int_def sup_int_def max_min_distrib2) + by standard (auto simp add: inf_int_def sup_int_def max_min_distrib2) end + subsection \Ordering properties of arithmetic operations\ instance int :: ordered_cancel_ab_semigroup_add @@ -127,46 +121,52 @@ by transfer clarsimp qed -text\Strict Monotonicity of Multiplication\ +text \Strict Monotonicity of Multiplication.\ -text\strict, in 1st argument; proof is by induction on k>0\ -lemma zmult_zless_mono2_lemma: - "(i::int) 0 int k * i < int k * j" -apply (induct k) -apply simp -apply (simp add: distrib_right) -apply (case_tac "k=0") -apply (simp_all add: add_strict_mono) -done +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" + for i j :: int +proof (induct k) + case 0 + then show ?case by simp +next + case (Suc k) + then show ?case + by (cases "k = 0") (simp_all add: distrib_right add_strict_mono) +qed -lemma zero_le_imp_eq_int: "(0::int) \ k ==> \n. k = int n" -apply transfer -apply clarsimp -apply (rule_tac x="a - b" in exI, simp) -done +lemma zero_le_imp_eq_int: "0 \ k \ \n. k = int n" + for k :: int + apply transfer + apply clarsimp + apply (rule_tac x="a - b" in exI) + apply simp + done -lemma zero_less_imp_eq_int: "(0::int) < k ==> \n>0. k = int n" -apply transfer -apply clarsimp -apply (rule_tac x="a - b" in exI, simp) -done +lemma zero_less_imp_eq_int: "0 < k \ \n>0. k = int n" + for k :: int + apply transfer + apply clarsimp + apply (rule_tac x="a - b" in exI) + apply simp + done -lemma zmult_zless_mono2: "[| i k*i < k*j" -apply (drule zero_less_imp_eq_int) -apply (auto simp add: zmult_zless_mono2_lemma) -done +lemma zmult_zless_mono2: "i < j \ 0 < k \ k * i < k * j" + for i j k :: int + by (drule zero_less_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma) -text\The integers form an ordered integral domain\ + +text \The integers form an ordered integral domain.\ + instantiation int :: linordered_idom begin -definition - zabs_def: "\i::int\ = (if i < 0 then - i else i)" +definition zabs_def: "\i::int\ = (if i < 0 then - i else i)" -definition - zsgn_def: "sgn (i::int) = (if i=0 then 0 else if 0 0 < k \ k * i < k * j" by (rule zmult_zless_mono2) @@ -178,31 +178,29 @@ end -lemma zless_imp_add1_zle: "w < z \ w + (1::int) \ z" +lemma zless_imp_add1_zle: "w < z \ w + 1 \ z" + for w z :: int by transfer clarsimp -lemma zless_iff_Suc_zadd: - "(w :: int) < z \ (\n. z = w + int (Suc n))" -apply transfer -apply auto -apply (rename_tac a b c d) -apply (rule_tac x="c+b - Suc(a+d)" in exI) -apply arith -done +lemma zless_iff_Suc_zadd: "w < z \ (\n. z = w + int (Suc n))" + for w z :: int + apply transfer + apply auto + apply (rename_tac a b c d) + apply (rule_tac x="c+b - Suc(a+d)" in exI) + apply arith + done -lemma zabs_less_one_iff [simp]: - fixes z :: int - shows "\z\ < 1 \ z = 0" (is "?P \ ?Q") +lemma zabs_less_one_iff [simp]: "\z\ < 1 \ z = 0" (is "?lhs \ ?rhs") + for z :: int proof - assume ?Q then show ?P by simp + assume ?rhs + then show ?lhs by simp next - assume ?P - with zless_imp_add1_zle [of "\z\" 1] have "\z\ + 1 \ 1" - by simp - then have "\z\ \ 0" - by simp - then show ?Q - by simp + assume ?lhs + with zless_imp_add1_zle [of "\z\" 1] have "\z\ + 1 \ 1" by simp + then have "\z\ \ 0" by simp + then show ?rhs by simp qed lemmas int_distrib = @@ -218,9 +216,10 @@ context ring_1 begin -lift_definition of_int :: "int \ 'a" is "\(i, j). of_nat i - of_nat j" +lift_definition of_int :: "int \ 'a" + is "\(i, j). of_nat i - of_nat j" by (clarsimp simp add: diff_eq_eq eq_diff_eq diff_add_eq - of_nat_add [symmetric] simp del: of_nat_add) + of_nat_add [symmetric] simp del: of_nat_add) lemma of_int_0 [simp]: "of_int 0 = 0" by transfer simp @@ -228,24 +227,24 @@ lemma of_int_1 [simp]: "of_int 1 = 1" by transfer simp -lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z" +lemma of_int_add [simp]: "of_int (w + z) = of_int w + of_int z" by transfer (clarsimp simp add: algebra_simps) -lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)" +lemma of_int_minus [simp]: "of_int (- z) = - (of_int z)" by (transfer fixing: uminus) clarsimp lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z" using of_int_add [of w "- z"] by simp lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z" - by (transfer fixing: times) (clarsimp simp add: algebra_simps of_nat_mult) + by (transfer fixing: times) (clarsimp simp add: algebra_simps) lemma mult_of_int_commute: "of_int x * y = y * of_int x" by (transfer fixing: times) (auto simp: algebra_simps mult_of_nat_commute) -text\Collapse nested embeddings\ +text \Collapse nested embeddings.\ lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n" -by (induct n) auto + by (induct n) auto lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k" by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric]) @@ -253,8 +252,7 @@ lemma of_int_neg_numeral [code_post]: "of_int (- numeral k) = - numeral k" by simp -lemma of_int_power [simp]: - "of_int (z ^ n) = of_int z ^ n" +lemma of_int_power [simp]: "of_int (z ^ n) = of_int z ^ n" by (induct n) simp_all end @@ -262,22 +260,17 @@ context ring_char_0 begin -lemma of_int_eq_iff [simp]: - "of_int w = of_int z \ w = z" - by transfer (clarsimp simp add: algebra_simps - of_nat_add [symmetric] simp del: of_nat_add) +lemma of_int_eq_iff [simp]: "of_int w = of_int z \ w = z" + by transfer (clarsimp simp add: algebra_simps of_nat_add [symmetric] simp del: of_nat_add) -text\Special cases where either operand is zero\ -lemma of_int_eq_0_iff [simp]: - "of_int z = 0 \ z = 0" +text \Special cases where either operand is zero.\ +lemma of_int_eq_0_iff [simp]: "of_int z = 0 \ z = 0" using of_int_eq_iff [of z 0] by simp -lemma of_int_0_eq_iff [simp]: - "0 = of_int z \ z = 0" +lemma of_int_0_eq_iff [simp]: "0 = of_int z \ z = 0" using of_int_eq_iff [of 0 z] by simp -lemma of_int_eq_1_iff [iff]: - "of_int z = 1 \ z = 1" +lemma of_int_eq_1_iff [iff]: "of_int z = 1 \ z = 1" using of_int_eq_iff [of z 1] by simp end @@ -285,48 +278,38 @@ context linordered_idom begin -text\Every \linordered_idom\ has characteristic zero.\ +text \Every \linordered_idom\ has characteristic zero.\ subclass ring_char_0 .. -lemma of_int_le_iff [simp]: - "of_int w \ of_int z \ w \ z" - by (transfer fixing: less_eq) (clarsimp simp add: algebra_simps - of_nat_add [symmetric] simp del: of_nat_add) +lemma of_int_le_iff [simp]: "of_int w \ of_int z \ w \ z" + by (transfer fixing: less_eq) + (clarsimp simp add: algebra_simps of_nat_add [symmetric] simp del: of_nat_add) -lemma of_int_less_iff [simp]: - "of_int w < of_int z \ w < z" +lemma of_int_less_iff [simp]: "of_int w < of_int z \ w < z" by (simp add: less_le order_less_le) -lemma of_int_0_le_iff [simp]: - "0 \ of_int z \ 0 \ z" +lemma of_int_0_le_iff [simp]: "0 \ of_int z \ 0 \ z" using of_int_le_iff [of 0 z] by simp -lemma of_int_le_0_iff [simp]: - "of_int z \ 0 \ z \ 0" +lemma of_int_le_0_iff [simp]: "of_int z \ 0 \ z \ 0" using of_int_le_iff [of z 0] by simp -lemma of_int_0_less_iff [simp]: - "0 < of_int z \ 0 < z" +lemma of_int_0_less_iff [simp]: "0 < of_int z \ 0 < z" using of_int_less_iff [of 0 z] by simp -lemma of_int_less_0_iff [simp]: - "of_int z < 0 \ z < 0" +lemma of_int_less_0_iff [simp]: "of_int z < 0 \ z < 0" using of_int_less_iff [of z 0] by simp -lemma of_int_1_le_iff [simp]: - "1 \ of_int z \ 1 \ z" +lemma of_int_1_le_iff [simp]: "1 \ of_int z \ 1 \ z" using of_int_le_iff [of 1 z] by simp -lemma of_int_le_1_iff [simp]: - "of_int z \ 1 \ z \ 1" +lemma of_int_le_1_iff [simp]: "of_int z \ 1 \ z \ 1" using of_int_le_iff [of z 1] by simp -lemma of_int_1_less_iff [simp]: - "1 < of_int z \ 1 < z" +lemma of_int_1_less_iff [simp]: "1 < of_int z \ 1 < z" using of_int_less_iff [of 1 z] by simp -lemma of_int_less_1_iff [simp]: - "of_int z < 1 \ z < 1" +lemma of_int_less_1_iff [simp]: "of_int z < 1 \ z < 1" using of_int_less_iff [of z 1] by simp lemma of_int_pos: "z > 0 \ of_int z > 0" @@ -335,15 +318,15 @@ lemma of_int_nonneg: "z \ 0 \ of_int z \ 0" by simp -lemma of_int_abs [simp]: - "of_int \x\ = \of_int x\" +lemma of_int_abs [simp]: "of_int \x\ = \of_int x\" by (auto simp add: abs_if) lemma of_int_lessD: assumes "\of_int n\ < x" shows "n = 0 \ x > 1" proof (cases "n = 0") - case True then show ?thesis by simp + case True + then show ?thesis by simp next case False then have "\n\ \ 0" by simp @@ -360,7 +343,8 @@ assumes "\of_int n\ \ x" shows "n = 0 \ 1 \ x" proof (cases "n = 0") - case True then show ?thesis by simp + case True + then show ?thesis by simp next case False then have "\n\ \ 0" by simp @@ -378,40 +362,34 @@ text \Comparisons involving @{term of_int}.\ -lemma of_int_eq_numeral_iff [iff]: - "of_int z = (numeral n :: 'a::ring_char_0) - \ z = numeral n" +lemma of_int_eq_numeral_iff [iff]: "of_int z = (numeral n :: 'a::ring_char_0) \ z = numeral n" using of_int_eq_iff by fastforce lemma of_int_le_numeral_iff [simp]: - "of_int z \ (numeral n :: 'a::linordered_idom) - \ z \ numeral n" + "of_int z \ (numeral n :: 'a::linordered_idom) \ z \ numeral n" using of_int_le_iff [of z "numeral n"] by simp lemma of_int_numeral_le_iff [simp]: - "(numeral n :: 'a::linordered_idom) \ of_int z \ numeral n \ z" + "(numeral n :: 'a::linordered_idom) \ of_int z \ numeral n \ z" using of_int_le_iff [of "numeral n"] by simp lemma of_int_less_numeral_iff [simp]: - "of_int z < (numeral n :: 'a::linordered_idom) - \ z < numeral n" + "of_int z < (numeral n :: 'a::linordered_idom) \ z < numeral n" using of_int_less_iff [of z "numeral n"] by simp lemma of_int_numeral_less_iff [simp]: - "(numeral n :: 'a::linordered_idom) < of_int z \ numeral n < z" + "(numeral n :: 'a::linordered_idom) < of_int z \ numeral n < z" using of_int_less_iff [of "numeral n" z] by simp -lemma of_nat_less_of_int_iff: - "(of_nat n::'a::linordered_idom) < of_int x \ int n < x" +lemma of_nat_less_of_int_iff: "(of_nat n::'a::linordered_idom) < of_int x \ int n < x" by (metis of_int_of_nat_eq of_int_less_iff) lemma of_int_eq_id [simp]: "of_int = id" proof - fix z show "of_int z = id z" - by (cases z rule: int_diff_cases, simp) + show "of_int z = id z" for z + by (cases z rule: int_diff_cases) simp qed - instance int :: no_top apply standard apply (rule_tac x="x + 1" in exI) @@ -424,6 +402,7 @@ apply simp done + subsection \Magnitude of an Integer, as a Natural Number: \nat\\ lift_definition nat :: "int \ nat" is "\(x, y). x - y" @@ -435,23 +414,23 @@ lemma int_nat_eq [simp]: "int (nat z) = (if 0 \ z then z else 0)" by transfer clarsimp -corollary nat_0_le: "0 \ z ==> int (nat z) = z" -by simp +lemma nat_0_le: "0 \ z \ int (nat z) = z" + by simp -lemma nat_le_0 [simp]: "z \ 0 ==> nat z = 0" +lemma nat_le_0 [simp]: "z \ 0 \ nat z = 0" by transfer clarsimp -lemma nat_le_eq_zle: "0 < w | 0 \ z ==> (nat w \ nat z) = (w\z)" +lemma nat_le_eq_zle: "0 < w \ 0 \ z \ nat w \ nat z \ w \ z" by transfer (clarsimp, arith) -text\An alternative condition is @{term "0 \ w"}\ -corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)" -by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) +text \An alternative condition is @{term "0 \ w"}.\ +lemma nat_mono_iff: "0 < z \ nat w < nat z \ w < z" + by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) -corollary nat_less_eq_zless: "0 \ w ==> (nat w < nat z) = (w w \ nat w < nat z \ w < z" + by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) -lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)" +lemma zless_nat_conj [simp]: "nat w < nat z \ 0 < z \ w < z" by transfer (clarsimp, arith) lemma nonneg_eq_int: @@ -460,34 +439,28 @@ shows P using assms by (blast dest: nat_0_le sym) -lemma nat_eq_iff: - "nat w = m \ (if 0 \ w then w = int m else m = 0)" +lemma nat_eq_iff: "nat w = m \ (if 0 \ w then w = int m else m = 0)" by transfer (clarsimp simp add: le_imp_diff_is_add) -corollary nat_eq_iff2: - "m = nat w \ (if 0 \ w then w = int m else m = 0)" +lemma nat_eq_iff2: "m = nat w \ (if 0 \ w then w = int m else m = 0)" using nat_eq_iff [of w m] by auto -lemma nat_0 [simp]: - "nat 0 = 0" +lemma nat_0 [simp]: "nat 0 = 0" by (simp add: nat_eq_iff) -lemma nat_1 [simp]: - "nat 1 = Suc 0" +lemma nat_1 [simp]: "nat 1 = Suc 0" by (simp add: nat_eq_iff) -lemma nat_numeral [simp]: - "nat (numeral k) = numeral k" +lemma nat_numeral [simp]: "nat (numeral k) = numeral k" by (simp add: nat_eq_iff) -lemma nat_neg_numeral [simp]: - "nat (- numeral k) = 0" +lemma nat_neg_numeral [simp]: "nat (- numeral k) = 0" by simp lemma nat_2: "nat 2 = Suc (Suc 0)" by simp -lemma nat_less_iff: "0 \ w ==> (nat w < m) = (w < of_nat m)" +lemma nat_less_iff: "0 \ w \ nat w < m \ w < of_nat m" by transfer (clarsimp, arith) lemma nat_le_iff: "nat x \ n \ x \ int n" @@ -496,133 +469,127 @@ lemma nat_mono: "x \ y \ nat x \ nat y" by transfer auto -lemma nat_0_iff[simp]: "nat(i::int) = 0 \ i\0" +lemma nat_0_iff[simp]: "nat i = 0 \ i \ 0" + for i :: int by transfer clarsimp -lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \ z)" -by (auto simp add: nat_eq_iff2) +lemma int_eq_iff: "of_nat m = z \ m = nat z \ 0 \ z" + by (auto simp add: nat_eq_iff2) -lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)" -by (insert zless_nat_conj [of 0], auto) +lemma zero_less_nat_eq [simp]: "0 < nat z \ 0 < z" + using zless_nat_conj [of 0] by auto -lemma nat_add_distrib: - "0 \ z \ 0 \ z' \ nat (z + z') = nat z + nat z'" +lemma nat_add_distrib: "0 \ z \ 0 \ z' \ nat (z + z') = nat z + nat z'" by transfer clarsimp -lemma nat_diff_distrib': - "0 \ x \ 0 \ y \ nat (x - y) = nat x - nat y" +lemma nat_diff_distrib': "0 \ x \ 0 \ y \ nat (x - y) = nat x - nat y" by transfer clarsimp -lemma nat_diff_distrib: - "0 \ z' \ z' \ z \ nat (z - z') = nat z - nat z'" +lemma nat_diff_distrib: "0 \ z' \ z' \ z \ nat (z - z') = nat z - nat z'" by (rule nat_diff_distrib') auto lemma nat_zminus_int [simp]: "nat (- int n) = 0" by transfer simp -lemma le_nat_iff: - "k \ 0 \ n \ nat k \ int n \ k" +lemma le_nat_iff: "k \ 0 \ n \ nat k \ int n \ k" by transfer auto -lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)" +lemma zless_nat_eq_int_zless: "m < nat z \ int m < z" by transfer (clarsimp simp add: less_diff_conv) -context ring_1 -begin - -lemma of_nat_nat [simp]: "0 \ z \ of_nat (nat z) = of_int z" +lemma (in ring_1) of_nat_nat [simp]: "0 \ z \ of_nat (nat z) = of_int z" by transfer (clarsimp simp add: of_nat_diff) -end - -lemma diff_nat_numeral [simp]: - "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')" +lemma diff_nat_numeral [simp]: "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')" by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral) text \For termination proofs:\ -lemma measure_function_int[measure_function]: "is_measure (nat o abs)" .. +lemma measure_function_int[measure_function]: "is_measure (nat \ abs)" .. -subsection\Lemmas about the Function @{term of_nat} and Orderings\ +subsection \Lemmas about the Function @{term of_nat} and Orderings\ lemma negative_zless_0: "- (int (Suc n)) < (0 :: int)" -by (simp add: order_less_le del: of_nat_Suc) + by (simp add: order_less_le del: of_nat_Suc) lemma negative_zless [iff]: "- (int (Suc n)) < int m" -by (rule negative_zless_0 [THEN order_less_le_trans], simp) + by (rule negative_zless_0 [THEN order_less_le_trans], simp) lemma negative_zle_0: "- int n \ 0" -by (simp add: minus_le_iff) + by (simp add: minus_le_iff) lemma negative_zle [iff]: "- int n \ int m" -by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff]) + by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff]) -lemma not_zle_0_negative [simp]: "~ (0 \ - (int (Suc n)))" -by (subst le_minus_iff, simp del: of_nat_Suc) +lemma not_zle_0_negative [simp]: "\ 0 \ - int (Suc n)" + by (subst le_minus_iff) (simp del: of_nat_Suc) -lemma int_zle_neg: "(int n \ - int m) = (n = 0 & m = 0)" +lemma int_zle_neg: "int n \ - int m \ n = 0 \ m = 0" by transfer simp -lemma not_int_zless_negative [simp]: "~ (int n < - int m)" -by (simp add: linorder_not_less) +lemma not_int_zless_negative [simp]: "\ int n < - int m" + by (simp add: linorder_not_less) -lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)" -by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg) +lemma negative_eq_positive [simp]: "- int n = of_nat m \ n = 0 \ m = 0" + by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg) -lemma zle_iff_zadd: - "w \ z \ (\n. z = w + int n)" (is "?P \ ?Q") +lemma zle_iff_zadd: "w \ z \ (\n. z = w + int n)" + (is "?lhs \ ?rhs") proof - assume ?Q - then show ?P by auto + assume ?rhs + then show ?lhs by auto next - assume ?P + assume ?lhs then have "0 \ z - w" by simp then obtain n where "z - w = int n" using zero_le_imp_eq_int [of "z - w"] by blast - then have "z = w + int n" - by simp - then show ?Q .. + then have "z = w + int n" by simp + then show ?rhs .. qed lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z" -by simp + by simp -text\This version is proved for all ordered rings, not just integers! - It is proved here because attribute \arith_split\ is not available - in theory \Rings\. - But is it really better than just rewriting with \abs_if\?\ -lemma abs_split [arith_split, no_atp]: - "P \a::'a::linordered_idom\ = ((0 \ a --> P a) & (a < 0 --> P(-a)))" -by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) +text \ + This version is proved for all ordered rings, not just integers! + It is proved here because attribute \arith_split\ is not available + in theory \Rings\. + But is it really better than just rewriting with \abs_if\? +\ +lemma abs_split [arith_split, no_atp]: "P \a\ \ (0 \ a \ P a) \ (a < 0 \ P (- a))" + for a :: "'a::linordered_idom" + by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) lemma negD: "x < 0 \ \n. x = - (int (Suc n))" -apply transfer -apply clarsimp -apply (rule_tac x="b - Suc a" in exI, arith) -done + apply transfer + apply clarsimp + apply (rule_tac x="b - Suc a" in exI) + apply arith + done + subsection \Cases and induction\ -text\Now we replace the case analysis rule by a more conventional one: -whether an integer is negative or not.\ +text \ + Now we replace the case analysis rule by a more conventional one: + whether an integer is negative or not. +\ -text\This version is symmetric in the two subgoals.\ -theorem int_cases2 [case_names nonneg nonpos, cases type: int]: - "\!! n. z = int n \ P; !! n. z = - (int n) \ P\ \ P" -apply (cases "z < 0") -apply (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym]) -done +text \This version is symmetric in the two subgoals.\ +lemma int_cases2 [case_names nonneg nonpos, cases type: int]: + "(\n. z = int n \ P) \ (\n. z = - (int n) \ P) \ P" + by (cases "z < 0") (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym]) -text\This is the default, with a negative case.\ -theorem int_cases [case_names nonneg neg, cases type: int]: - "[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P" -apply (cases "z < 0") -apply (blast dest!: negD) -apply (simp add: linorder_not_less del: of_nat_Suc) -apply auto -apply (blast dest: nat_0_le [THEN sym]) -done +text \This is the default, with a negative case.\ +lemma int_cases [case_names nonneg neg, cases type: int]: + "(\n. z = int n \ P) \ (\n. z = - (int (Suc n)) \ P) \ P" + apply (cases "z < 0") + apply (blast dest!: negD) + apply (simp add: linorder_not_less del: of_nat_Suc) + apply auto + apply (blast dest: nat_0_le [THEN sym]) + done lemma int_cases3 [case_names zero pos neg]: fixes k :: int @@ -630,7 +597,8 @@ and "\n. k = - int n \ n > 0 \ P" shows "P" proof (cases k "0::int" rule: linorder_cases) - case equal with assms(1) show P by simp + case equal + with assms(1) show P by simp next case greater then have *: "nat k > 0" by simp @@ -643,12 +611,13 @@ ultimately show P using assms(3) by blast qed -theorem int_of_nat_induct [case_names nonneg neg, induct type: int]: - "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z" +lemma int_of_nat_induct [case_names nonneg neg, induct type: int]: + "(\n. P (int n)) \ (\n. P (- (int (Suc n)))) \ P z" by (cases z) auto lemma nonneg_int_cases: - assumes "0 \ k" obtains n where "k = int n" + assumes "0 \ k" + obtains n where "k = int n" using assms by (rule nonneg_eq_int) lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)" @@ -679,50 +648,54 @@ text \Preliminaries\ lemma le_imp_0_less: + fixes z :: int assumes le: "0 \ z" - shows "(0::int) < 1 + z" + shows "0 < 1 + z" proof - have "0 \ z" by fact - also have "... < z + 1" by (rule less_add_one) - also have "... = 1 + z" by (simp add: ac_simps) + also have "\ < z + 1" by (rule less_add_one) + also have "\ = 1 + z" by (simp add: ac_simps) finally show "0 < 1 + z" . qed -lemma odd_less_0_iff: - "(1 + z + z < 0) = (z < (0::int))" +lemma odd_less_0_iff: "1 + z + z < 0 \ z < 0" + for z :: int proof (cases z) case (nonneg n) - thus ?thesis by (simp add: linorder_not_less add.assoc add_increasing - le_imp_0_less [THEN order_less_imp_le]) + then show ?thesis + by (simp add: linorder_not_less add.assoc add_increasing le_imp_0_less [THEN order_less_imp_le]) next case (neg n) - thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1 - add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) + then show ?thesis + by (simp del: of_nat_Suc of_nat_add of_nat_1 + add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) qed + subsubsection \Comparisons, for Ordered Rings\ lemmas double_eq_0_iff = double_zero -lemma odd_nonzero: - "1 + z + z \ (0::int)" +lemma odd_nonzero: "1 + z + z \ 0" + for z :: int proof (cases z) case (nonneg n) - have le: "0 \ z+z" by (simp add: nonneg add_increasing) - thus ?thesis using le_imp_0_less [OF le] - by (auto simp add: add.assoc) + have le: "0 \ z + z" + by (simp add: nonneg add_increasing) + then show ?thesis + using le_imp_0_less [OF le] by (auto simp: add.assoc) next case (neg n) show ?thesis proof assume eq: "1 + z + z = 0" - have "(0::int) < 1 + (int n + int n)" + have "0 < 1 + (int n + int n)" by (simp add: le_imp_0_less add_increasing) - also have "... = - (1 + z + z)" + also have "\ = - (1 + z + z)" by (simp add: neg add.assoc [symmetric]) - also have "... = 0" by (simp add: eq) + also have "\ = 0" by (simp add: eq) finally have "0<0" .. - thus False by blast + then show False by blast qed qed @@ -751,31 +724,31 @@ by (subst of_nat_numeral [symmetric], rule Ints_of_nat) lemma Ints_add [simp]: "a \ \ \ b \ \ \ a + b \ \" -apply (auto simp add: Ints_def) -apply (rule range_eqI) -apply (rule of_int_add [symmetric]) -done + apply (auto simp add: Ints_def) + apply (rule range_eqI) + apply (rule of_int_add [symmetric]) + done lemma Ints_minus [simp]: "a \ \ \ -a \ \" -apply (auto simp add: Ints_def) -apply (rule range_eqI) -apply (rule of_int_minus [symmetric]) -done + apply (auto simp add: Ints_def) + apply (rule range_eqI) + apply (rule of_int_minus [symmetric]) + done lemma Ints_diff [simp]: "a \ \ \ b \ \ \ a - b \ \" -apply (auto simp add: Ints_def) -apply (rule range_eqI) -apply (rule of_int_diff [symmetric]) -done + apply (auto simp add: Ints_def) + apply (rule range_eqI) + apply (rule of_int_diff [symmetric]) + done lemma Ints_mult [simp]: "a \ \ \ b \ \ \ a * b \ \" -apply (auto simp add: Ints_def) -apply (rule range_eqI) -apply (rule of_int_mult [symmetric]) -done + apply (auto simp add: Ints_def) + apply (rule range_eqI) + apply (rule of_int_mult [symmetric]) + done lemma Ints_power [simp]: "a \ \ \ a ^ n \ \" -by (induct n) simp_all + by (induct n) simp_all lemma Ints_cases [cases set: Ints]: assumes "q \ \" @@ -797,16 +770,22 @@ lemma Nats_altdef1: "\ = {of_int n |n. n \ 0}" proof (intro subsetI equalityI) - fix x :: 'a assume "x \ {of_int n |n. n \ 0}" - then obtain n where "x = of_int n" "n \ 0" by (auto elim!: Ints_cases) - hence "x = of_nat (nat n)" by (subst of_nat_nat) simp_all - thus "x \ \" by simp + fix x :: 'a + assume "x \ {of_int n |n. n \ 0}" + then obtain n where "x = of_int n" "n \ 0" + by (auto elim!: Ints_cases) + then have "x = of_nat (nat n)" + by (subst of_nat_nat) simp_all + then show "x \ \" + by simp next - fix x :: 'a assume "x \ \" - then obtain n where "x = of_nat n" by (auto elim!: Nats_cases) - hence "x = of_int (int n)" by simp + fix x :: 'a + assume "x \ \" + then obtain n where "x = of_nat n" + by (auto elim!: Nats_cases) + then have "x = of_int (int n)" by simp also have "int n \ 0" by simp - hence "of_int (int n) \ {of_int n |n. n \ 0}" by blast + then have "of_int (int n) \ {of_int n |n. n \ 0}" by blast finally show "x \ {of_int n |n. n \ 0}" . qed @@ -814,45 +793,54 @@ lemma (in linordered_idom) Nats_altdef2: "\ = {n \ \. n \ 0}" proof (intro subsetI equalityI) - fix x :: 'a assume "x \ {n \ \. n \ 0}" - then obtain n where "x = of_int n" "n \ 0" by (auto elim!: Ints_cases) - hence "x = of_nat (nat n)" by (subst of_nat_nat) simp_all - thus "x \ \" by simp + fix x :: 'a + assume "x \ {n \ \. n \ 0}" + then obtain n where "x = of_int n" "n \ 0" + by (auto elim!: Ints_cases) + then have "x = of_nat (nat n)" + by (subst of_nat_nat) simp_all + then show "x \ \" + by simp qed (auto elim!: Nats_cases) text \The premise involving @{term Ints} prevents @{term "a = 1/2"}.\ lemma Ints_double_eq_0_iff: + fixes a :: "'a::ring_char_0" assumes in_Ints: "a \ \" - shows "(a + a = 0) = (a = (0::'a::ring_char_0))" + shows "a + a = 0 \ a = 0" + (is "?lhs \ ?rhs") proof - - from in_Ints have "a \ range of_int" unfolding Ints_def [symmetric] . + from in_Ints have "a \ range of_int" + unfolding Ints_def [symmetric] . then obtain z where a: "a = of_int z" .. show ?thesis proof - assume "a = 0" - thus "a + a = 0" by simp + assume ?rhs + then show ?lhs by simp next - assume eq: "a + a = 0" - hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a) - hence "z + z = 0" by (simp only: of_int_eq_iff) - hence "z = 0" by (simp only: double_eq_0_iff) - thus "a = 0" by (simp add: a) + assume ?lhs + with a have "of_int (z + z) = (of_int 0 :: 'a)" by simp + then have "z + z = 0" by (simp only: of_int_eq_iff) + then have "z = 0" by (simp only: double_eq_0_iff) + with a show ?rhs by simp qed qed lemma Ints_odd_nonzero: + fixes a :: "'a::ring_char_0" assumes in_Ints: "a \ \" - shows "1 + a + a \ (0::'a::ring_char_0)" + shows "1 + a + a \ 0" proof - - from in_Ints have "a \ range of_int" unfolding Ints_def [symmetric] . + from in_Ints have "a \ range of_int" + unfolding Ints_def [symmetric] . then obtain z where a: "a = of_int z" .. show ?thesis proof - assume eq: "1 + a + a = 0" - hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a) - hence "1 + z + z = 0" by (simp only: of_int_eq_iff) + assume "1 + a + a = 0" + with a have "of_int (1 + z + z) = (of_int 0 :: 'a)" by simp + then have "1 + z + z = 0" by (simp only: of_int_eq_iff) with odd_nonzero show False by blast qed qed @@ -861,15 +849,19 @@ using of_nat_in_Nats [of "numeral w"] by simp lemma Ints_odd_less_0: + fixes a :: "'a::linordered_idom" assumes in_Ints: "a \ \" - shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))" + shows "1 + a + a < 0 \ a < 0" proof - - from in_Ints have "a \ range of_int" unfolding Ints_def [symmetric] . + from in_Ints have "a \ range of_int" + unfolding Ints_def [symmetric] . then obtain z where a: "a = of_int z" .. - hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))" + with a have "1 + a + a < 0 \ of_int (1 + z + z) < (of_int 0 :: 'a)" + by simp + also have "\ \ z < 0" + by (simp only: of_int_less_iff odd_less_0_iff) + also have "\ \ a < 0" by (simp add: a) - also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0_iff) - also have "... = (a < 0)" by (simp add: a) finally show ?thesis . qed @@ -877,24 +869,16 @@ subsection \@{term setsum} and @{term setprod}\ lemma of_nat_setsum [simp]: "of_nat (setsum f A) = (\x\A. of_nat(f x))" - apply (cases "finite A") - apply (erule finite_induct, auto) - done + by (induct A rule: infinite_finite_induct) auto lemma of_int_setsum [simp]: "of_int (setsum f A) = (\x\A. of_int(f x))" - apply (cases "finite A") - apply (erule finite_induct, auto) - done + by (induct A rule: infinite_finite_induct) auto lemma of_nat_setprod [simp]: "of_nat (setprod f A) = (\x\A. of_nat(f x))" - apply (cases "finite A") - apply (erule finite_induct, auto simp add: of_nat_mult) - done + by (induct A rule: infinite_finite_induct) auto lemma of_int_setprod [simp]: "of_int (setprod f A) = (\x\A. of_int(f x))" - apply (cases "finite A") - apply (erule finite_induct, auto) - done + by (induct A rule: infinite_finite_induct) auto lemmas int_setsum = of_nat_setsum [where 'a=int] lemmas int_setprod = of_nat_setprod [where 'a=int] @@ -905,6 +889,7 @@ lemmas zle_int = of_nat_le_iff [where 'a=int] lemmas int_int_eq = of_nat_eq_iff [where 'a=int] + subsection \Setting up simplification procedures\ lemmas of_int_simps = @@ -913,53 +898,64 @@ ML_file "Tools/int_arith.ML" declaration \K Int_Arith.setup\ -simproc_setup fast_arith ("(m::'a::linordered_idom) < n" | - "(m::'a::linordered_idom) \ n" | - "(m::'a::linordered_idom) = n") = +simproc_setup fast_arith + ("(m::'a::linordered_idom) < n" | + "(m::'a::linordered_idom) \ n" | + "(m::'a::linordered_idom) = n") = \K Lin_Arith.simproc\ subsection\More Inequality Reasoning\ -lemma zless_add1_eq: "(w < z + (1::int)) = (w w < z \ w = z" + for w z :: int + by arith -lemma add1_zle_eq: "(w + (1::int) \ z) = (w z \ w < z" + for w z :: int + by arith -lemma zle_diff1_eq [simp]: "(w \ z - (1::int)) = (w z - 1 \ w < z" + for w z :: int + by arith -lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\z)" -by arith +lemma zle_add1_eq_le [simp]: "w < z + 1 \ w \ z" + for w z :: int + by arith -lemma int_one_le_iff_zero_less: "((1::int) \ z) = (0 < z)" -by arith +lemma int_one_le_iff_zero_less: "1 \ z \ 0 < z" + for z :: int + by arith -subsection\The functions @{term nat} and @{term int}\ +subsection \The functions @{term nat} and @{term int}\ -text\Simplify the term @{term "w + - z"}\ +text \Simplify the term @{term "w + - z"}.\ -lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)" +lemma one_less_nat_eq [simp]: "Suc 0 < nat z \ 1 < z" using zless_nat_conj [of 1 z] by auto -text\This simplifies expressions of the form @{term "int n = z"} where - z is an integer literal.\ +text \ + This simplifies expressions of the form @{term "int n = z"} where + \z\ is an integer literal. +\ lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v -lemma split_nat [arith_split]: - "P(nat(i::int)) = ((\n. i = int n \ P n) & (i < 0 \ P 0))" - (is "?P = (?L & ?R)") +lemma split_nat [arith_split]: "P (nat i) = ((\n. i = int n \ P n) \ (i < 0 \ P 0))" + (is "?P = (?L \ ?R)") + for i :: int proof (cases "i < 0") - case True thus ?thesis by auto + case True + then show ?thesis by auto next case False have "?P = ?L" proof - assume ?P thus ?L using False by clarsimp + assume ?P + then show ?L using False by auto next - assume ?L thus ?P using False by simp + assume ?L + then show ?P using False by simp qed with False show ?thesis by simp qed @@ -976,11 +972,13 @@ lemma of_int_of_nat [nitpick_simp]: "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))" proof (cases "k < 0") - case True then have "0 \ - k" by simp + case True + then have "0 \ - k" by simp then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat) with True show ?thesis by simp next - case False then show ?thesis by (simp add: not_less of_nat_nat) + case False + then show ?thesis by (simp add: not_less) qed end @@ -990,39 +988,39 @@ assumes "0 \ z" shows "nat (z * z') = nat z * nat z'" proof (cases "0 \ z'") - case False with assms have "z * z' \ 0" + case False + with assms have "z * z' \ 0" by (simp add: not_le mult_le_0_iff) then have "nat (z * z') = 0" by simp moreover from False have "nat z' = 0" by simp ultimately show ?thesis by simp next - case True with assms have ge_0: "z * z' \ 0" by (simp add: zero_le_mult_iff) + case True + with assms have ge_0: "z * z' \ 0" by (simp add: zero_le_mult_iff) show ?thesis by (rule injD [of "of_nat :: nat \ int", OF inj_of_nat]) (simp only: of_nat_mult of_nat_nat [OF True] of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp) qed -lemma nat_mult_distrib_neg: "z \ (0::int) ==> nat(z*z') = nat(-z) * nat(-z')" -apply (rule trans) -apply (rule_tac [2] nat_mult_distrib, auto) -done +lemma nat_mult_distrib_neg: "z \ 0 \ nat (z * z') = nat (- z) * nat (- z')" + for z z' :: int + apply (rule trans) + apply (rule_tac [2] nat_mult_distrib) + apply auto + done lemma nat_abs_mult_distrib: "nat \w * z\ = nat \w\ * nat \z\" -apply (cases "z=0 | w=0") -apply (auto simp add: abs_if nat_mult_distrib [symmetric] - nat_mult_distrib_neg [symmetric] mult_less_0_iff) -done + by (cases "z = 0 \ w = 0") + (auto simp add: abs_if nat_mult_distrib [symmetric] + nat_mult_distrib_neg [symmetric] mult_less_0_iff) -lemma int_in_range_abs [simp]: - "int n \ range abs" +lemma int_in_range_abs [simp]: "int n \ range abs" proof (rule range_eqI) - show "int n = \int n\" - by simp + show "int n = \int n\" by simp qed -lemma range_abs_Nats [simp]: - "range abs = (\ :: int set)" +lemma range_abs_Nats [simp]: "range abs = (\ :: int set)" proof - have "\k\ \ \" for k :: int by (cases k) simp_all @@ -1031,130 +1029,123 @@ ultimately show ?thesis by blast qed -lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)" -apply (rule sym) -apply (simp add: nat_eq_iff) -done +lemma Suc_nat_eq_nat_zadd1: "0 \ z \ Suc (nat z) = nat (1 + z)" + for z :: int + by (rule sym) (simp add: nat_eq_iff) lemma diff_nat_eq_if: - "nat z - nat z' = - (if z' < 0 then nat z - else let d = z-z' in - if d < 0 then 0 else nat d)" -by (simp add: Let_def nat_diff_distrib [symmetric]) + "nat z - nat z' = + (if z' < 0 then nat z + else + let d = z - z' + in if d < 0 then 0 else nat d)" + by (simp add: Let_def nat_diff_distrib [symmetric]) -lemma nat_numeral_diff_1 [simp]: - "numeral v - (1::nat) = nat (numeral v - 1)" +lemma nat_numeral_diff_1 [simp]: "numeral v - (1::nat) = nat (numeral v - 1)" using diff_nat_numeral [of v Num.One] by simp -subsection "Induction principles for int" +subsection \Induction principles for int\ -text\Well-founded segments of the integers\ +text \Well-founded segments of the integers.\ -definition - int_ge_less_than :: "int => (int * int) set" -where - "int_ge_less_than d = {(z',z). d \ z' & z' < z}" +definition int_ge_less_than :: "int \ (int \ int) set" + where "int_ge_less_than d = {(z', z). d \ z' \ z' < z}" -theorem wf_int_ge_less_than: "wf (int_ge_less_than d)" +lemma wf_int_ge_less_than: "wf (int_ge_less_than d)" proof - - have "int_ge_less_than d \ measure (%z. nat (z-d))" + have "int_ge_less_than d \ measure (\z. nat (z - d))" by (auto simp add: int_ge_less_than_def) - thus ?thesis + then show ?thesis by (rule wf_subset [OF wf_measure]) qed -text\This variant looks odd, but is typical of the relations suggested -by RankFinder.\ +text \ + This variant looks odd, but is typical of the relations suggested + by RankFinder.\ -definition - int_ge_less_than2 :: "int => (int * int) set" -where - "int_ge_less_than2 d = {(z',z). d \ z & z' < z}" +definition int_ge_less_than2 :: "int \ (int \ int) set" + where "int_ge_less_than2 d = {(z',z). d \ z \ z' < z}" -theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)" +lemma wf_int_ge_less_than2: "wf (int_ge_less_than2 d)" proof - - have "int_ge_less_than2 d \ measure (%z. nat (1+z-d))" + have "int_ge_less_than2 d \ measure (\z. nat (1 + z - d))" by (auto simp add: int_ge_less_than2_def) - thus ?thesis + then show ?thesis by (rule wf_subset [OF wf_measure]) qed (* `set:int': dummy construction *) theorem int_ge_induct [case_names base step, induct set: int]: fixes i :: int - assumes ge: "k \ i" and - base: "P k" and - step: "\i. k \ i \ P i \ P (i + 1)" + assumes ge: "k \ i" + and base: "P k" + and step: "\i. k \ i \ P i \ P (i + 1)" shows "P i" proof - - { fix n - have "\i::int. n = nat (i - k) \ k \ i \ P i" - proof (induct n) - case 0 - hence "i = k" by arith - thus "P i" using base by simp - next - case (Suc n) - then have "n = nat((i - 1) - k)" by arith - moreover - have ki1: "k \ i - 1" using Suc.prems by arith - ultimately - have "P (i - 1)" by (rule Suc.hyps) - from step [OF ki1 this] show ?case by simp - qed - } + have "\i::int. n = nat (i - k) \ k \ i \ P i" for n + proof (induct n) + case 0 + then have "i = k" by arith + with base show "P i" by simp + next + case (Suc n) + then have "n = nat ((i - 1) - k)" by arith + moreover have k: "k \ i - 1" using Suc.prems by arith + ultimately have "P (i - 1)" by (rule Suc.hyps) + from step [OF k this] show ?case by simp + qed with ge show ?thesis by fast qed (* `set:int': dummy construction *) theorem int_gr_induct [case_names base step, induct set: int]: - assumes gr: "k < (i::int)" and - base: "P(k+1)" and - step: "\i. \k < i; P i\ \ P(i+1)" + fixes i k :: int + assumes gr: "k < i" + and base: "P (k + 1)" + and step: "\i. k < i \ P i \ P (i + 1)" shows "P i" -apply(rule int_ge_induct[of "k + 1"]) + apply (rule int_ge_induct[of "k + 1"]) using gr apply arith - apply(rule base) -apply (rule step, simp+) -done + apply (rule base) + apply (rule step) + apply simp_all + done theorem int_le_induct [consumes 1, case_names base step]: - assumes le: "i \ (k::int)" and - base: "P(k)" and - step: "\i. \i \ k; P i\ \ P(i - 1)" + fixes i k :: int + assumes le: "i \ k" + and base: "P k" + and step: "\i. i \ k \ P i \ P (i - 1)" shows "P i" proof - - { fix n - have "\i::int. n = nat(k-i) \ i \ k \ P i" - proof (induct n) - case 0 - hence "i = k" by arith - thus "P i" using base by simp - next - case (Suc n) - hence "n = nat (k - (i + 1))" by arith - moreover - have ki1: "i + 1 \ k" using Suc.prems by arith - ultimately - have "P (i + 1)" by(rule Suc.hyps) - from step[OF ki1 this] show ?case by simp - qed - } + have "\i::int. n = nat(k-i) \ i \ k \ P i" for n + proof (induct n) + case 0 + then have "i = k" by arith + with base show "P i" by simp + next + case (Suc n) + then have "n = nat (k - (i + 1))" by arith + moreover have k: "i + 1 \ k" using Suc.prems by arith + ultimately have "P (i + 1)" by (rule Suc.hyps) + from step[OF k this] show ?case by simp + qed with le show ?thesis by fast qed theorem int_less_induct [consumes 1, case_names base step]: - assumes less: "(i::int) < k" and - base: "P(k - 1)" and - step: "\i. \i < k; P i\ \ P(i - 1)" + fixes i k :: int + assumes less: "i < k" + and base: "P (k - 1)" + and step: "\i. i < k \ P i \ P (i - 1)" shows "P i" -apply(rule int_le_induct[of _ "k - 1"]) + apply (rule int_le_induct[of _ "k - 1"]) using less apply arith - apply(rule base) -apply (rule step, simp+) -done + apply (rule base) + apply (rule step) + apply simp_all + done theorem int_induct [case_names base step1 step2]: fixes k :: int @@ -1167,88 +1158,93 @@ then show ?thesis proof assume "i \ k" - then show ?thesis using base - by (rule int_ge_induct) (fact step1) + then show ?thesis + using base by (rule int_ge_induct) (fact step1) next assume "i \ k" - then show ?thesis using base - by (rule int_le_induct) (fact step2) + then show ?thesis + using base by (rule int_le_induct) (fact step2) qed qed -subsection\Intermediate value theorems\ + +subsection \Intermediate value theorems\ -lemma int_val_lemma: - "(\if(i+1) - f i\ \ 1) --> - f 0 \ k --> k \ f n --> (\i \ n. f i = (k::int))" -unfolding One_nat_def -apply (induct n) -apply simp -apply (intro strip) -apply (erule impE, simp) -apply (erule_tac x = n in allE, simp) -apply (case_tac "k = f (Suc n)") -apply force -apply (erule impE) - apply (simp add: abs_if split: if_split_asm) -apply (blast intro: le_SucI) -done +lemma int_val_lemma: "(\if (i + 1) - f i\ \ 1) \ f 0 \ k \ k \ f n \ (\i \ n. f i = k)" + for n :: nat and k :: int + unfolding One_nat_def + apply (induct n) + apply simp + apply (intro strip) + apply (erule impE) + apply simp + apply (erule_tac x = n in allE) + apply simp + apply (case_tac "k = f (Suc n)") + apply force + apply (erule impE) + apply (simp add: abs_if split: if_split_asm) + apply (blast intro: le_SucI) + done lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)] lemma nat_intermed_int_val: - "[| \i. m \ i & i < n --> \f(i + 1::nat) - f i\ \ 1; m < n; - f m \ k; k \ f n |] ==> ? i. m \ i & i \ n & f i = (k::int)" -apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k - in int_val_lemma) -unfolding One_nat_def -apply simp -apply (erule exE) -apply (rule_tac x = "i+m" in exI, arith) -done + "\i. m \ i \ i < n \ \f (i + 1) - f i\ \ 1 \ m < n \ + f m \ k \ k \ f n \ \i. m \ i \ i \ n \ f i = k" + for f :: "nat \ int" and k :: int + apply (cut_tac n = "n-m" and f = "\i. f (i + m)" and k = k in int_val_lemma) + unfolding One_nat_def + apply simp + apply (erule exE) + apply (rule_tac x = "i+m" in exI) + apply arith + done -subsection\Products and 1, by T. M. Rasmussen\ +subsection \Products and 1, by T. M. Rasmussen\ lemma abs_zmult_eq_1: + fixes m n :: int assumes mn: "\m * n\ = 1" - shows "\m\ = (1::int)" + shows "\m\ = 1" proof - - have 0: "m \ 0 & n \ 0" using mn - by auto - have "~ (2 \ \m\)" + from mn have 0: "m \ 0" "n \ 0" by auto + have "\ 2 \ \m\" proof assume "2 \ \m\" - hence "2*\n\ \ \m\*\n\" - by (simp add: mult_mono 0) - also have "... = \m*n\" - by (simp add: abs_mult) - also have "... = 1" - by (simp add: mn) - finally have "2*\n\ \ 1" . - thus "False" using 0 - by arith + then have "2 * \n\ \ \m\ * \n\" by (simp add: mult_mono 0) + also have "\ = \m * n\" by (simp add: abs_mult) + also from mn have "\ = 1" by simp + finally have "2 * \n\ \ 1" . + with 0 show "False" by arith qed - thus ?thesis using 0 - by auto + with 0 show ?thesis by auto qed -lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1" -by (insert abs_zmult_eq_1 [of m n], arith) +lemma pos_zmult_eq_1_iff_lemma: "m * n = 1 \ m = 1 \ m = - 1" + for m n :: int + using abs_zmult_eq_1 [of m n] by arith lemma pos_zmult_eq_1_iff: - assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)" + fixes m n :: int + assumes "0 < m" + shows "m * n = 1 \ m = 1 \ n = 1" proof - - from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma) - thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma) + from assms have "m * n = 1 \ m = 1" + by (auto dest: pos_zmult_eq_1_iff_lemma) + then show ?thesis + by (auto dest: pos_zmult_eq_1_iff_lemma) qed -lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))" -apply (rule iffI) - apply (frule pos_zmult_eq_1_iff_lemma) - apply (simp add: mult.commute [of m]) - apply (frule pos_zmult_eq_1_iff_lemma, auto) -done +lemma zmult_eq_1_iff: "m * n = 1 \ (m = 1 \ n = 1) \ (m = - 1 \ n = - 1)" + for m n :: int + apply (rule iffI) + apply (frule pos_zmult_eq_1_iff_lemma) + apply (simp add: mult.commute [of m]) + apply (frule pos_zmult_eq_1_iff_lemma) + apply auto + done lemma infinite_UNIV_int: "\ finite (UNIV::int set)" proof @@ -1264,16 +1260,16 @@ subsection \Further theorems on numerals\ -subsubsection\Special Simplification for Constants\ +subsubsection \Special Simplification for Constants\ -text\These distributive laws move literals inside sums and differences.\ +text \These distributive laws move literals inside sums and differences.\ lemmas distrib_right_numeral [simp] = distrib_right [of _ _ "numeral v"] for v lemmas distrib_left_numeral [simp] = distrib_left [of "numeral v"] for v lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v -text\These are actually for fields, like real: but where else to put them?\ +text \These are actually for fields, like real: but where else to put them?\ lemmas zero_less_divide_iff_numeral [simp, no_atp] = zero_less_divide_iff [of "numeral w"] for w lemmas divide_less_0_iff_numeral [simp, no_atp] = divide_less_0_iff [of "numeral w"] for w @@ -1291,7 +1287,7 @@ inverse_eq_divide [of "- numeral w"] for w text \These laws simplify inequalities, moving unary minus from a term -into the literal.\ + into the literal.\ lemmas equation_minus_iff_numeral [no_atp] = equation_minus_iff [of "numeral v"] for v @@ -1311,7 +1307,7 @@ lemmas minus_less_iff_numeral [no_atp] = minus_less_iff [of _ "numeral v"] for v -\ \FIXME maybe simproc\ +(* FIXME maybe simproc *) text \Cancellation of constant factors in comparisons (\<\ and \\\)\ @@ -1351,9 +1347,9 @@ divide_eq_eq [of _ "- numeral w"] for w -subsubsection\Optional Simplification Rules Involving Constants\ +subsubsection \Optional Simplification Rules Involving Constants\ -text\Simplify quotients that are compared with a literal constant.\ +text \Simplify quotients that are compared with a literal constant.\ lemmas le_divide_eq_numeral [divide_const_simps] = le_divide_eq [of "numeral w"] @@ -1380,37 +1376,44 @@ divide_eq_eq [of _ _ "- numeral w"] for w -text\Not good as automatic simprules because they cause case splits.\ -lemmas [divide_const_simps] = le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 +text \Not good as automatic simprules because they cause case splits.\ +lemmas [divide_const_simps] = + le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 subsection \The divides relation\ -lemma zdvd_antisym_nonneg: - "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)" - apply (simp add: dvd_def, auto) - apply (auto simp add: mult.assoc zero_le_mult_iff zmult_eq_1_iff) - done +lemma zdvd_antisym_nonneg: "0 \ m \ 0 \ n \ m dvd n \ n dvd m \ m = n" + for m n :: int + by (auto simp add: dvd_def mult.assoc zero_le_mult_iff zmult_eq_1_iff) -lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a" +lemma zdvd_antisym_abs: + fixes a b :: int + assumes "a dvd b" and "b dvd a" shows "\a\ = \b\" -proof cases - assume "a = 0" with assms show ?thesis by simp +proof (cases "a = 0") + case True + with assms show ?thesis by simp next - assume "a \ 0" - from \a dvd b\ obtain k where k:"b = a*k" unfolding dvd_def by blast - from \b dvd a\ obtain k' where k':"a = b*k'" unfolding dvd_def by blast - from k k' have "a = a*k*k'" by simp - with mult_cancel_left1[where c="a" and b="k*k'"] - have kk':"k*k' = 1" using \a\0\ by (simp add: mult.assoc) - hence "k = 1 \ k' = 1 \ k = -1 \ k' = -1" by (simp add: zmult_eq_1_iff) - thus ?thesis using k k' by auto + case False + from \a dvd b\ obtain k where k: "b = a * k" + unfolding dvd_def by blast + from \b dvd a\ obtain k' where k': "a = b * k'" + unfolding dvd_def by blast + from k k' have "a = a * k * k'" by simp + with mult_cancel_left1[where c="a" and b="k*k'"] have kk': "k * k' = 1" + using \a \ 0\ by (simp add: mult.assoc) + then have "k = 1 \ k' = 1 \ k = -1 \ k' = -1" + by (simp add: zmult_eq_1_iff) + with k k' show ?thesis by auto qed -lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)" +lemma zdvd_zdiffD: "k dvd m - n \ k dvd n \ k dvd m" + for k m n :: int using dvd_add_right_iff [of k "- n" m] by simp -lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" +lemma zdvd_reduce: "k dvd n + k * m \ k dvd n" + for k m n :: int using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps) lemma dvd_imp_le_int: @@ -1438,167 +1441,184 @@ with \0 < n\ \0 < k\ show False unfolding mult_less_cancel_left by auto qed -lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \ (0::int)" +lemma zdvd_mult_cancel: + fixes k m n :: int + assumes d: "k * m dvd k * n" + and "k \ 0" shows "m dvd n" -proof- - from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast - {assume "n \ m*h" hence "k* n \ k* (m*h)" using kz by simp - with h have False by (simp add: mult.assoc)} - hence "n = m * h" by blast - thus ?thesis by simp +proof - + from d obtain h where h: "k * n = k * m * h" + unfolding dvd_def by blast + have "n = m * h" + proof (rule ccontr) + assume "\ ?thesis" + with \k \ 0\ have "k * n \ k * (m * h)" by simp + with h show False + by (simp add: mult.assoc) + qed + then show ?thesis by simp qed -theorem zdvd_int: "(x dvd y) = (int x dvd int y)" +theorem zdvd_int: "x dvd y \ int x dvd int y" proof - - have "\k. int y = int x * k \ x dvd y" - proof - - fix k - assume A: "int y = int x * k" - then show "x dvd y" - proof (cases k) - case (nonneg n) - with A have "y = x * n" by (simp del: of_nat_mult add: of_nat_mult [symmetric]) - then show ?thesis .. - next - case (neg n) - with A have "int y = int x * (- int (Suc n))" by simp - also have "\ = - (int x * int (Suc n))" by (simp only: mult_minus_right) - also have "\ = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric]) - finally have "- int (x * Suc n) = int y" .. - then show ?thesis by (simp only: negative_eq_positive) auto - qed + have "x dvd y" if "int y = int x * k" for k + proof (cases k) + case (nonneg n) + with that have "y = x * n" + by (simp del: of_nat_mult add: of_nat_mult [symmetric]) + then show ?thesis .. + next + case (neg n) + with that have "int y = int x * (- int (Suc n))" + by simp + also have "\ = - (int x * int (Suc n))" + by (simp only: mult_minus_right) + also have "\ = - int (x * Suc n)" + by (simp only: of_nat_mult [symmetric]) + finally have "- int (x * Suc n) = int y" .. + then show ?thesis + by (simp only: negative_eq_positive) auto qed - then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult) + then show ?thesis + by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult) qed -lemma zdvd1_eq[simp]: "(x::int) dvd 1 = (\x\ = 1)" +lemma zdvd1_eq[simp]: "x dvd 1 \ \x\ = 1" + (is "?lhs \ ?rhs") + for x :: int proof - assume d: "x dvd 1" hence "int (nat \x\) dvd int (nat 1)" by simp - hence "nat \x\ dvd 1" by (simp add: zdvd_int) - hence "nat \x\ = 1" by simp - thus "\x\ = 1" by (cases "x < 0") auto + assume ?lhs + then have "int (nat \x\) dvd int (nat 1)" by simp + then have "nat \x\ dvd 1" by (simp add: zdvd_int) + then have "nat \x\ = 1" by simp + then show ?rhs by (cases "x < 0") auto next - assume "\x\=1" - then have "x = 1 \ x = -1" by auto - then show "x dvd 1" by (auto intro: dvdI) + assume ?rhs + then have "x = 1 \ x = - 1" by auto + then show ?lhs by (auto intro: dvdI) qed lemma zdvd_mult_cancel1: - assumes mp:"m \(0::int)" shows "(m * n dvd m) = (\n\ = 1)" + fixes m :: int + assumes mp: "m \ 0" + shows "m * n dvd m \ \n\ = 1" + (is "?lhs \ ?rhs") proof - assume n1: "\n\ = 1" thus "m * n dvd m" - by (cases "n >0") (auto simp add: minus_equation_iff) + assume ?rhs + then show ?lhs + by (cases "n > 0") (auto simp add: minus_equation_iff) next - assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp - from zdvd_mult_cancel[OF H2 mp] show "\n\ = 1" by (simp only: zdvd1_eq) + assume ?lhs + then have "m * n dvd m * 1" by simp + from zdvd_mult_cancel[OF this mp] show ?rhs + by (simp only: zdvd1_eq) qed -lemma int_dvd_iff: "(int m dvd z) = (m dvd nat \z\)" - unfolding zdvd_int by (cases "z \ 0") simp_all - -lemma dvd_int_iff: "(z dvd int m) = (nat \z\ dvd m)" - unfolding zdvd_int by (cases "z \ 0") simp_all +lemma int_dvd_iff: "int m dvd z \ m dvd nat \z\" + by (cases "z \ 0") (simp_all add: zdvd_int) -lemma dvd_int_unfold_dvd_nat: - "k dvd l \ nat \k\ dvd nat \l\" - unfolding dvd_int_iff [symmetric] by simp +lemma dvd_int_iff: "z dvd int m \ nat \z\ dvd m" + by (cases "z \ 0") (simp_all add: zdvd_int) -lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \ z then (z dvd int m) else m = 0)" +lemma dvd_int_unfold_dvd_nat: "k dvd l \ nat \k\ dvd nat \l\" + by (simp add: dvd_int_iff [symmetric]) + +lemma nat_dvd_iff: "nat z dvd m \ (if 0 \ z then z dvd int m else m = 0)" by (auto simp add: dvd_int_iff) -lemma eq_nat_nat_iff: - "0 \ z \ 0 \ z' \ nat z = nat z' \ z = z'" +lemma eq_nat_nat_iff: "0 \ z \ 0 \ z' \ nat z = nat z' \ z = z'" by (auto elim!: nonneg_eq_int) -lemma nat_power_eq: - "0 \ z \ nat (z ^ n) = nat z ^ n" +lemma nat_power_eq: "0 \ z \ nat (z ^ n) = nat z ^ n" by (induct n) (simp_all add: nat_mult_distrib) -lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \ (n::int)" +lemma zdvd_imp_le: "z dvd n \ 0 < n \ z \ n" + for n z :: int apply (cases n) - apply (auto simp add: dvd_int_iff) + apply (auto simp add: dvd_int_iff) apply (cases z) - apply (auto simp add: dvd_imp_le) + apply (auto simp add: dvd_imp_le) done lemma zdvd_period: fixes a d :: int assumes "a dvd d" shows "a dvd (x + t) \ a dvd ((x + c * d) + t)" + (is "?lhs \ ?rhs") proof - from assms obtain k where "d = a * k" by (rule dvdE) show ?thesis proof - assume "a dvd (x + t)" + assume ?lhs then obtain l where "x + t = a * l" by (rule dvdE) then have "x = a * l - t" by simp - with \d = a * k\ show "a dvd x + c * d + t" by simp + with \d = a * k\ show ?rhs by simp next - assume "a dvd x + c * d + t" + assume ?rhs then obtain l where "x + c * d + t = a * l" by (rule dvdE) then have "x = a * l - c * d - t" by simp - with \d = a * k\ show "a dvd (x + t)" by simp + with \d = a * k\ show ?lhs by simp qed qed subsection \Finiteness of intervals\ -lemma finite_interval_int1 [iff]: "finite {i :: int. a <= i & i <= b}" -proof (cases "a <= b") +lemma finite_interval_int1 [iff]: "finite {i :: int. a \ i \ i \ b}" +proof (cases "a \ b") case True - from this show ?thesis + then show ?thesis proof (induct b rule: int_ge_induct) case base - have "{i. a <= i & i <= a} = {a}" by auto - from this show ?case by simp + have "{i. a \ i \ i \ a} = {a}" by auto + then show ?case by simp next case (step b) - from this have "{i. a <= i & i <= b + 1} = {i. a <= i & i <= b} \ {b + 1}" by auto - from this step show ?case by simp + then have "{i. a \ i \ i \ b + 1} = {i. a \ i \ i \ b} \ {b + 1}" by auto + with step show ?case by simp qed next - case False from this show ?thesis + case False + then show ?thesis by (metis (lifting, no_types) Collect_empty_eq finite.emptyI order_trans) qed -lemma finite_interval_int2 [iff]: "finite {i :: int. a <= i & i < b}" -by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto +lemma finite_interval_int2 [iff]: "finite {i :: int. a \ i \ i < b}" + by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto -lemma finite_interval_int3 [iff]: "finite {i :: int. a < i & i <= b}" -by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto +lemma finite_interval_int3 [iff]: "finite {i :: int. a < i \ i \ b}" + by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto -lemma finite_interval_int4 [iff]: "finite {i :: int. a < i & i < b}" -by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto +lemma finite_interval_int4 [iff]: "finite {i :: int. a < i \ i < b}" + by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto subsection \Configuration of the code generator\ text \Constructors\ -definition Pos :: "num \ int" where - [simp, code_abbrev]: "Pos = numeral" +definition Pos :: "num \ int" + where [simp, code_abbrev]: "Pos = numeral" -definition Neg :: "num \ int" where - [simp, code_abbrev]: "Neg n = - (Pos n)" +definition Neg :: "num \ int" + where [simp, code_abbrev]: "Neg n = - (Pos n)" code_datatype "0::int" Pos Neg -text \Auxiliary operations\ +text \Auxiliary operations.\ -definition dup :: "int \ int" where - [simp]: "dup k = k + k" +definition dup :: "int \ int" + where [simp]: "dup k = k + k" lemma dup_code [code]: "dup 0 = 0" "dup (Pos n) = Pos (Num.Bit0 n)" "dup (Neg n) = Neg (Num.Bit0 n)" - unfolding Pos_def Neg_def by (simp_all add: numeral_Bit0) -definition sub :: "num \ num \ int" where - [simp]: "sub m n = numeral m - numeral n" +definition sub :: "num \ num \ int" + where [simp]: "sub m n = numeral m - numeral n" lemma sub_code [code]: "sub Num.One Num.One = 0" @@ -1610,25 +1630,25 @@ "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1" - apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM) - apply (simp_all only: algebra_simps minus_diff_eq) + apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM) + apply (simp_all only: algebra_simps minus_diff_eq) apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"]) apply (simp_all only: minus_add add.assoc left_minus) done -text \Implementations\ +text \Implementations.\ -lemma one_int_code [code, code_unfold]: - "1 = Pos Num.One" +lemma one_int_code [code, code_unfold]: "1 = Pos Num.One" by simp lemma plus_int_code [code]: - "k + 0 = (k::int)" - "0 + l = (l::int)" + "k + 0 = k" + "0 + l = l" "Pos m + Pos n = Pos (m + n)" "Pos m + Neg n = sub m n" "Neg m + Pos n = sub n m" "Neg m + Neg n = Neg (m + n)" + for k l :: int by simp_all lemma uminus_int_code [code]: @@ -1638,28 +1658,29 @@ by simp_all lemma minus_int_code [code]: - "k - 0 = (k::int)" - "0 - l = uminus (l::int)" + "k - 0 = k" + "0 - l = uminus l" "Pos m - Pos n = sub m n" "Pos m - Neg n = Pos (m + n)" "Neg m - Pos n = Neg (m + n)" "Neg m - Neg n = sub n m" + for k l :: int by simp_all lemma times_int_code [code]: - "k * 0 = (0::int)" - "0 * l = (0::int)" + "k * 0 = 0" + "0 * l = 0" "Pos m * Pos n = Pos (m * n)" "Pos m * Neg n = Neg (m * n)" "Neg m * Pos n = Neg (m * n)" "Neg m * Neg n = Pos (m * n)" + for k l :: int by simp_all instantiation int :: equal begin -definition - "HOL.equal k l \ k = (l::int)" +definition "HOL.equal k l \ k = (l::int)" instance by standard (rule equal_int_def) @@ -1678,8 +1699,8 @@ "HOL.equal (Neg k) (Neg l) \ HOL.equal k l" by (auto simp add: equal) -lemma equal_int_refl [code nbe]: - "HOL.equal (k::int) k \ True" +lemma equal_int_refl [code nbe]: "HOL.equal k k \ True" + for k :: int by (fact equal_refl) lemma less_eq_int_code [code]: @@ -1719,7 +1740,7 @@ by simp_all -text \Serializer setup\ +text \Serializer setup.\ code_identifier code_module Int \ (SML) Arith and (OCaml) Arith and (Haskell) Arith