# HG changeset patch # User wenzelm # Date 1163069929 -3600 # Node ID de65ce2bfb32bf14d26f17159297068ddeb37a0f # Parent a2bd14226f9a1898c779df5883c1c6a35ce031f5 tuned; diff -r a2bd14226f9a -r de65ce2bfb32 src/HOL/Library/Binomial.thy --- a/src/HOL/Library/Binomial.thy Thu Nov 09 11:58:47 2006 +0100 +++ b/src/HOL/Library/Binomial.thy Thu Nov 09 11:58:49 2006 +0100 @@ -4,87 +4,82 @@ Copyright 1997 University of Cambridge *) -header{*Binomial Coefficients*} +header {* Binomial Coefficients *} theory Binomial imports Main begin -text{*This development is based on the work of Andy Gordon and -Florian Kammueller*} +text {* This development is based on the work of Andy Gordon and + Florian Kammueller. *} consts binomial :: "nat \ nat \ nat" (infixl "choose" 65) - primrec - binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)" - + binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)" binomial_Suc: "(Suc n choose k) = (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" lemma binomial_n_0 [simp]: "(n choose 0) = 1" -by (cases n) simp_all + by (cases n) simp_all lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0" -by simp + by simp lemma binomial_Suc_Suc [simp]: - "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)" -by simp + "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)" + by simp -lemma binomial_eq_0 [rule_format]: "\k. n < k --> (n choose k) = 0" -apply (induct "n") -apply auto -done +lemma binomial_eq_0: "!!k. n < k ==> (n choose k) = 0" + by (induct n) auto declare binomial_0 [simp del] binomial_Suc [simp del] lemma binomial_n_n [simp]: "(n choose n) = 1" -apply (induct "n") -apply (simp_all add: binomial_eq_0) -done + by (induct n) (simp_all add: binomial_eq_0) lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n" -by (induct "n", simp_all) + by (induct n) simp_all lemma binomial_1 [simp]: "(n choose Suc 0) = n" -by (induct "n", simp_all) + by (induct n) simp_all -lemma zero_less_binomial [rule_format]: "k \ n --> 0 < (n choose k)" -by (rule_tac m = n and n = k in diff_induct, simp_all) +lemma zero_less_binomial: "k \ n ==> 0 < (n choose k)" + by (induct n k rule: diff_induct) simp_all lemma binomial_eq_0_iff: "(n choose k = 0) = (nn)" -by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric]) + by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric]) (*Might be more useful if re-oriented*) -lemma Suc_times_binomial_eq [rule_format]: - "\k. k \ n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" -apply (induct "n") -apply (simp add: binomial_0, clarify) -apply (case_tac "k") -apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq - binomial_eq_0) -done +lemma Suc_times_binomial_eq: + "!!k. k \ n ==> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" + apply (induct n) + apply (simp add: binomial_0) + apply (case_tac k) + apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq + binomial_eq_0) + done text{*This is the well-known version, but it's harder to use because of the need to reason about division.*} lemma binomial_Suc_Suc_eq_times: - "k \ n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k" -by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc - del: mult_Suc mult_Suc_right) + "k \ n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k" + by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc + del: mult_Suc mult_Suc_right) text{*Another version, with -1 instead of Suc.*} lemma times_binomial_minus1_eq: - "[|k \ n; 0 (n choose k) * k = n * ((n - 1) choose (k - 1))" -apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq) -apply (simp split add: nat_diff_split, auto) -done + "[|k \ n; 0 (n choose k) * k = n * ((n - 1) choose (k - 1))" + apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq) + apply (simp split add: nat_diff_split, auto) + done + subsubsection {* Theorems about @{text "choose"} *} @@ -132,7 +127,7 @@ *} lemma n_sub_lemma: - "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)" + "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)" apply (induct k) apply (simp add: card_s_0_eq_empty, atomize) apply (rotate_tac -1, erule finite_induct) @@ -166,10 +161,10 @@ using Suc by simp also have "\ = a*(\k=0..n. (n choose k) * a^k * b^(n-k)) + b*(\k=0..n. (n choose k) * a^k * b^(n-k))" - by(rule nat_distrib) + by (rule nat_distrib) also have "\ = (\k=0..n. (n choose k) * a^(k+1) * b^(n-k)) + (\k=0..n. (n choose k) * a^k * b^(n-k+1))" - by(simp add: setsum_right_distrib mult_ac) + by (simp add: setsum_right_distrib mult_ac) also have "\ = (\k=0..n. (n choose k) * a^k * b^(n+1-k)) + (\k=1..n+1. (n choose (k - 1)) * a^k * b^(n+1-k))" by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le @@ -177,10 +172,10 @@ also have "\ = a^(n+1) + b^(n+1) + (\k=1..n. (n choose (k - 1)) * a^k * b^(n+1-k)) + (\k=1..n. (n choose k) * a^k * b^(n+1-k))" - by(simp add: decomp2) + by (simp add: decomp2) also have - "\ = a^(n+1) + b^(n+1) + (\k=1..n. (n+1 choose k) * a^k * b^(n+1-k))" - by(simp add: nat_distrib setsum_addf binomial.simps) + "\ = a^(n+1) + b^(n+1) + (\k=1..n. (n+1 choose k) * a^k * b^(n+1-k))" + by (simp add: nat_distrib setsum_addf binomial.simps) also have "\ = (\k=0..n+1. (n+1 choose k) * a^k * b^(n+1-k))" using decomp by simp finally show ?case by simp diff -r a2bd14226f9a -r de65ce2bfb32 src/HOL/Library/GCD.thy --- a/src/HOL/Library/GCD.thy Thu Nov 09 11:58:47 2006 +0100 +++ b/src/HOL/Library/GCD.thy Thu Nov 09 11:58:49 2006 +0100 @@ -21,10 +21,10 @@ recdef gcd "measure ((\(m, n). n) :: nat \ nat => nat)" "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))" -constdefs +definition is_gcd :: "nat => nat => nat => bool" -- {* @{term gcd} as a relation *} - "is_gcd p m n == p dvd m \ p dvd n \ - (\d. d dvd m \ d dvd n --> d dvd p)" + "is_gcd p m n = (p dvd m \ p dvd n \ + (\d. d dvd m \ d dvd n --> d dvd p))" lemma gcd_induct: @@ -38,18 +38,15 @@ lemma gcd_0 [simp]: "gcd (m, 0) = m" - apply simp - done + by simp lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)" - apply simp - done + by simp declare gcd.simps [simp del] lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1" - apply (simp add: gcd_non_0) - done + by (simp add: gcd_non_0) text {* \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}. The @@ -59,7 +56,7 @@ lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m" and gcd_dvd2 [iff]: "gcd (m, n) dvd n" apply (induct m n rule: gcd_induct) - apply (simp_all add: gcd_non_0) + apply (simp_all add: gcd_non_0) apply (blast dest: dvd_mod_imp_dvd) done @@ -70,16 +67,13 @@ *} lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)" - apply (induct m n rule: gcd_induct) - apply (simp_all add: gcd_non_0 dvd_mod) - done + by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod) lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \ k dvd n)" - apply (blast intro!: gcd_greatest intro: dvd_trans) - done + by (blast intro!: gcd_greatest intro: dvd_trans) lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \ n = 0)" - by (simp only: dvd_0_left_iff [THEN sym] gcd_greatest_iff) + by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff) text {* @@ -199,8 +193,6 @@ done lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)" - apply (induct k) - apply (simp_all add: add_assoc) - done + by (induct k) (simp_all add: add_assoc) end diff -r a2bd14226f9a -r de65ce2bfb32 src/HOL/Library/Parity.thy --- a/src/HOL/Library/Parity.thy Thu Nov 09 11:58:47 2006 +0100 +++ b/src/HOL/Library/Parity.thy Thu Nov 09 11:58:49 2006 +0100 @@ -1,4 +1,4 @@ -(* Title: Parity.thy +(* Title: HOL/Library/Parity.thy ID: $Id$ Author: Jeremy Avigad *) @@ -28,14 +28,17 @@ subsection {* Even and odd are mutually exclusive *} -lemma int_pos_lt_two_imp_zero_or_one: +lemma int_pos_lt_two_imp_zero_or_one: "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1" by auto lemma neq_one_mod_two [simp]: "((x::int) mod 2 ~= 0) = (x mod 2 = 1)" - apply (subgoal_tac "x mod 2 = 0 | x mod 2 = 1", force) - apply (rule int_pos_lt_two_imp_zero_or_one, auto) - done +proof - + have "x mod 2 = 0 | x mod 2 = 1" + by (rule int_pos_lt_two_imp_zero_or_one) auto + then show ?thesis by force +qed + subsection {* Behavior under integer arithmetic operations *} @@ -49,7 +52,7 @@ by (simp add: even_def zmod_zmult1_eq) lemma even_product: "even((x::int) * y) = (even x | even y)" - apply (auto simp add: even_times_anything anything_times_even) + apply (auto simp add: even_times_anything anything_times_even) apply (rule ccontr) apply (auto simp add: odd_times_odd) done @@ -75,24 +78,22 @@ lemma even_neg: "even (-(x::int)) = even x" by (auto simp add: even_def zmod_zminus1_eq_if) -lemma even_difference: - "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))" +lemma even_difference: + "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))" by (simp only: diff_minus even_sum even_neg) -lemma even_pow_gt_zero [rule_format]: - "even (x::int) ==> 0 < n --> even (x^n)" - apply (induct n) - apply (auto simp add: even_product) - done +lemma even_pow_gt_zero: + "even (x::int) ==> 0 < n ==> even (x^n)" + by (induct n) (auto simp add: even_product) lemma odd_pow: "odd x ==> odd((x::int)^n)" apply (induct n) - apply (simp add: even_def) + apply (simp add: even_def) apply (simp add: even_product) done lemma even_power: "even ((x::int)^n) = (even x & 0 < n)" - apply (auto simp add: even_pow_gt_zero) + apply (auto simp add: even_pow_gt_zero) apply (erule contrapos_pp, erule odd_pow) apply (erule contrapos_pp, simp add: even_def) done @@ -103,29 +104,32 @@ lemma odd_one: "odd (1::int)" by (simp add: even_def) -lemmas even_odd_simps [simp] = even_def[of "number_of v",standard] even_zero +lemmas even_odd_simps [simp] = even_def[of "number_of v",standard] even_zero odd_one even_product even_sum even_neg even_difference even_power subsection {* Equivalent definitions *} -lemma two_times_even_div_two: "even (x::int) ==> 2 * (x div 2) = x" +lemma two_times_even_div_two: "even (x::int) ==> 2 * (x div 2) = x" by (auto simp add: even_def) -lemma two_times_odd_div_two_plus_one: "odd (x::int) ==> +lemma two_times_odd_div_two_plus_one: "odd (x::int) ==> 2 * (x div 2) + 1 = x" - apply (insert zmod_zdiv_equality [of x 2, THEN sym]) - by (simp add: even_def) + apply (insert zmod_zdiv_equality [of x 2, symmetric]) + apply (simp add: even_def) + done lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)" apply auto apply (rule exI) - by (erule two_times_even_div_two [THEN sym]) + apply (erule two_times_even_div_two [symmetric]) + done lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)" apply auto apply (rule exI) - by (erule two_times_odd_div_two_plus_one [THEN sym]) + apply (erule two_times_odd_div_two_plus_one [symmetric]) + done subsection {* even and odd for nats *} @@ -136,15 +140,15 @@ lemma even_nat_product: "even((x::nat) * y) = (even x | even y)" by (simp add: even_nat_def int_mult) -lemma even_nat_sum: "even ((x::nat) + y) = +lemma even_nat_sum: "even ((x::nat) + y) = ((even x & even y) | (odd x & odd y))" by (unfold even_nat_def, simp) -lemma even_nat_difference: +lemma even_nat_difference: "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))" - apply (auto simp add: even_nat_def zdiff_int [THEN sym]) - apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym]) - apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym]) + apply (auto simp add: even_nat_def zdiff_int [symmetric]) + apply (case_tac "x < y", auto simp add: zdiff_int [symmetric]) + apply (case_tac "x < y", auto simp add: zdiff_int [symmetric]) done lemma even_nat_Suc: "even (Suc x) = odd x" @@ -156,18 +160,18 @@ lemma even_nat_zero: "even (0::nat)" by (simp add: even_nat_def) -lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard] +lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard] even_nat_zero even_nat_Suc even_nat_product even_nat_sum even_nat_power subsection {* Equivalent definitions *} -lemma nat_lt_two_imp_zero_or_one: "(x::nat) < Suc (Suc 0) ==> +lemma nat_lt_two_imp_zero_or_one: "(x::nat) < Suc (Suc 0) ==> x = 0 | x = Suc 0" by auto lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0" - apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) + apply (insert mod_div_equality [of x "Suc (Suc 0)", symmetric]) apply (drule subst, assumption) apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0") apply force @@ -177,16 +181,16 @@ done lemma odd_nat_mod_two_eq_one: "odd (x::nat) ==> x mod (Suc (Suc 0)) = Suc 0" - apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) + apply (insert mod_div_equality [of x "Suc (Suc 0)", symmetric]) apply (drule subst, assumption) apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0") - apply force + apply force apply (subgoal_tac "0 < Suc (Suc 0)") apply (frule mod_less_divisor [of "Suc (Suc 0)" x]) apply (erule nat_lt_two_imp_zero_or_one, auto) done -lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)" +lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)" apply (rule iffI) apply (erule even_nat_mod_two_eq_zero) apply (insert odd_nat_mod_two_eq_one [of x], auto) @@ -198,69 +202,71 @@ apply (frule nat_lt_two_imp_zero_or_one, auto) done -lemma even_nat_div_two_times_two: "even (x::nat) ==> +lemma even_nat_div_two_times_two: "even (x::nat) ==> Suc (Suc 0) * (x div Suc (Suc 0)) = x" - apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) + apply (insert mod_div_equality [of x "Suc (Suc 0)", symmetric]) apply (drule even_nat_mod_two_eq_zero, simp) done -lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==> - Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x" - apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) +lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==> + Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x" + apply (insert mod_div_equality [of x "Suc (Suc 0)", symmetric]) apply (drule odd_nat_mod_two_eq_one, simp) done lemma even_nat_equiv_def2: "even (x::nat) = (EX y. x = Suc (Suc 0) * y)" apply (rule iffI, rule exI) - apply (erule even_nat_div_two_times_two [THEN sym], auto) + apply (erule even_nat_div_two_times_two [symmetric], auto) done lemma odd_nat_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))" apply (rule iffI, rule exI) - apply (erule odd_nat_div_two_times_two_plus_one [THEN sym], auto) + apply (erule odd_nat_div_two_times_two_plus_one [symmetric], auto) done subsection {* Parity and powers *} -lemma minus_one_even_odd_power: - "(even x --> (- 1::'a::{comm_ring_1,recpower})^x = 1) & +lemma minus_one_even_odd_power: + "(even x --> (- 1::'a::{comm_ring_1,recpower})^x = 1) & (odd x --> (- 1::'a)^x = - 1)" apply (induct x) apply (rule conjI) apply simp apply (insert even_nat_zero, blast) apply (simp add: power_Suc) -done + done lemma minus_one_even_power [simp]: - "even x ==> (- 1::'a::{comm_ring_1,recpower})^x = 1" - by (rule minus_one_even_odd_power [THEN conjunct1, THEN mp], assumption) + "even x ==> (- 1::'a::{comm_ring_1,recpower})^x = 1" + using minus_one_even_odd_power by blast lemma minus_one_odd_power [simp]: - "odd x ==> (- 1::'a::{comm_ring_1,recpower})^x = - 1" - by (rule minus_one_even_odd_power [THEN conjunct2, THEN mp], assumption) + "odd x ==> (- 1::'a::{comm_ring_1,recpower})^x = - 1" + using minus_one_even_odd_power by blast lemma neg_one_even_odd_power: - "(even x --> (-1::'a::{number_ring,recpower})^x = 1) & + "(even x --> (-1::'a::{number_ring,recpower})^x = 1) & (odd x --> (-1::'a)^x = -1)" apply (induct x) apply (simp, simp add: power_Suc) done lemma neg_one_even_power [simp]: - "even x ==> (-1::'a::{number_ring,recpower})^x = 1" - by (rule neg_one_even_odd_power [THEN conjunct1, THEN mp], assumption) + "even x ==> (-1::'a::{number_ring,recpower})^x = 1" + using neg_one_even_odd_power by blast lemma neg_one_odd_power [simp]: - "odd x ==> (-1::'a::{number_ring,recpower})^x = -1" - by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption) + "odd x ==> (-1::'a::{number_ring,recpower})^x = -1" + using neg_one_even_odd_power by blast lemma neg_power_if: - "(-x::'a::{comm_ring_1,recpower}) ^ n = + "(-x::'a::{comm_ring_1,recpower}) ^ n = (if even n then (x ^ n) else -(x ^ n))" - by (induct n, simp_all split: split_if_asm add: power_Suc) + apply (induct n) + apply (simp_all split: split_if_asm add: power_Suc) + done -lemma zero_le_even_power: "even n ==> +lemma zero_le_even_power: "even n ==> 0 <= (x::'a::{recpower,ordered_ring_strict}) ^ n" apply (simp add: even_nat_equiv_def2) apply (erule exE) @@ -269,7 +275,7 @@ apply (rule zero_le_square) done -lemma zero_le_odd_power: "odd n ==> +lemma zero_le_odd_power: "odd n ==> (0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)" apply (simp add: odd_nat_equiv_def2) apply (erule exE) @@ -280,23 +286,23 @@ apply auto apply (subgoal_tac "x = 0 & 0 < y") apply (erule conjE, assumption) - apply (subst power_eq_0_iff [THEN sym]) + apply (subst power_eq_0_iff [symmetric]) apply (subgoal_tac "0 <= x^y * x^y") apply simp apply (rule zero_le_square)+ -done + done -lemma zero_le_power_eq: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) = +lemma zero_le_power_eq: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (even n | (odd n & 0 <= x))" apply auto - apply (subst zero_le_odd_power [THEN sym]) + apply (subst zero_le_odd_power [symmetric]) apply assumption+ apply (erule zero_le_even_power) - apply (subst zero_le_odd_power) + apply (subst zero_le_odd_power) apply assumption+ -done + done -lemma zero_less_power_eq: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) = +lemma zero_less_power_eq: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) = (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))" apply (rule iffI) apply clarsimp @@ -306,7 +312,7 @@ apply (subgoal_tac "~ (0 <= x^n)") apply simp apply (subst zero_le_odd_power) - apply assumption + apply assumption apply simp apply (rule notI) apply (simp add: power_0_left) @@ -323,99 +329,91 @@ apply (subst zero_le_odd_power) apply assumption apply (erule order_less_imp_le) -done + done lemma power_less_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n < 0) = - (odd n & x < 0)" - apply (subst linorder_not_le [THEN sym])+ + (odd n & x < 0)" + apply (subst linorder_not_le [symmetric])+ apply (subst zero_le_power_eq) apply auto -done + done lemma power_le_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n <= 0) = (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))" - apply (subst linorder_not_less [THEN sym])+ + apply (subst linorder_not_less [symmetric])+ apply (subst zero_less_power_eq) apply auto -done + done -lemma power_even_abs: "even n ==> +lemma power_even_abs: "even n ==> (abs (x::'a::{recpower,ordered_idom}))^n = x^n" - apply (subst power_abs [THEN sym]) + apply (subst power_abs [symmetric]) apply (simp add: zero_le_even_power) -done + done lemma zero_less_power_nat_eq: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)" - by (induct n, auto) + by (induct n) auto -lemma power_minus_even [simp]: "even n ==> +lemma power_minus_even [simp]: "even n ==> (- x)^n = (x^n::'a::{recpower,comm_ring_1})" apply (subst power_minus) apply simp -done + done -lemma power_minus_odd [simp]: "odd n ==> +lemma power_minus_odd [simp]: "odd n ==> (- x)^n = - (x^n::'a::{recpower,comm_ring_1})" apply (subst power_minus) apply simp -done + done -(* Simplify, when the exponent is a numeral *) + +text {* Simplify, when the exponent is a numeral *} lemmas power_0_left_number_of = power_0_left [of "number_of w", standard] declare power_0_left_number_of [simp] -lemmas zero_le_power_eq_number_of = +lemmas zero_le_power_eq_number_of [simp] = zero_le_power_eq [of _ "number_of w", standard] -declare zero_le_power_eq_number_of [simp] -lemmas zero_less_power_eq_number_of = +lemmas zero_less_power_eq_number_of [simp] = zero_less_power_eq [of _ "number_of w", standard] -declare zero_less_power_eq_number_of [simp] -lemmas power_le_zero_eq_number_of = +lemmas power_le_zero_eq_number_of [simp] = power_le_zero_eq [of _ "number_of w", standard] -declare power_le_zero_eq_number_of [simp] -lemmas power_less_zero_eq_number_of = +lemmas power_less_zero_eq_number_of [simp] = power_less_zero_eq [of _ "number_of w", standard] -declare power_less_zero_eq_number_of [simp] -lemmas zero_less_power_nat_eq_number_of = +lemmas zero_less_power_nat_eq_number_of [simp] = zero_less_power_nat_eq [of _ "number_of w", standard] -declare zero_less_power_nat_eq_number_of [simp] -lemmas power_eq_0_iff_number_of = power_eq_0_iff [of _ "number_of w", standard] -declare power_eq_0_iff_number_of [simp] +lemmas power_eq_0_iff_number_of [simp] = power_eq_0_iff [of _ "number_of w", standard] -lemmas power_even_abs_number_of = power_even_abs [of "number_of w" _, standard] -declare power_even_abs_number_of [simp] +lemmas power_even_abs_number_of [simp] = power_even_abs [of "number_of w" _, standard] subsection {* An Equivalence for @{term [source] "0 \ a^n"} *} lemma even_power_le_0_imp_0: - "a ^ (2*k) \ (0::'a::{ordered_idom,recpower}) ==> a=0" -apply (induct k) -apply (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) -done + "a ^ (2*k) \ (0::'a::{ordered_idom,recpower}) ==> a=0" + by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) lemma zero_le_power_iff: - "(0 \ a^n) = (0 \ (a::'a::{ordered_idom,recpower}) | even n)" - (is "?P n") + "(0 \ a^n) = (0 \ (a::'a::{ordered_idom,recpower}) | even n)" proof cases assume even: "even n" then obtain k where "n = 2*k" by (auto simp add: even_nat_equiv_def2 numeral_2_eq_2) - thus ?thesis by (simp add: zero_le_even_power even) + thus ?thesis by (simp add: zero_le_even_power even) next assume odd: "odd n" then obtain k where "n = Suc(2*k)" by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2) thus ?thesis - by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power - dest!: even_power_le_0_imp_0) -qed + by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power + dest!: even_power_le_0_imp_0) +qed + subsection {* Miscellaneous *} @@ -429,20 +427,20 @@ apply (simp add: even_def) done -lemma div_Suc: "Suc a div c = a div c + Suc 0 div c + +lemma div_Suc: "Suc a div c = a div c + Suc 0 div c + (a mod c + Suc 0 mod c) div c" apply (subgoal_tac "Suc a = a + Suc 0") apply (erule ssubst) apply (rule div_add1_eq, simp) done -lemma even_nat_plus_one_div_two: "even (x::nat) ==> - (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" +lemma even_nat_plus_one_div_two: "even (x::nat) ==> + (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" apply (subst div_Suc) apply (simp add: even_nat_equiv_def) done -lemma odd_nat_plus_one_div_two: "odd (x::nat) ==> +lemma odd_nat_plus_one_div_two: "odd (x::nat) ==> (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" apply (subst div_Suc) apply (simp add: odd_nat_equiv_def)