# HG changeset patch # User wenzelm # Date 1413665435 -7200 # Node ID ad09a4635e26eb1f3d208371d27bcdf9e0bf6d8d # Parent 68f8d22a68676bd98010b374a1fc87f375eb2c44# Parent 92f935f34b283ab38897feefb2b7ec4e21348864 merged diff -r 92f935f34b28 -r ad09a4635e26 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Sat Oct 18 22:49:59 2014 +0200 +++ b/src/HOL/Parity.thy Sat Oct 18 22:50:35 2014 +0200 @@ -19,6 +19,20 @@ "2 dvd Suc n \ \ 2 dvd n" by (induct n) auto +lemma two_dvd_diff_nat_iff: + fixes m n :: nat + shows "2 dvd m - n \ m < n \ 2 dvd m + n" +proof (cases "n \ m") + case True + then have "m - n + n * 2 = m + n" by simp + moreover have "2 dvd m - n \ 2 dvd m - n + n * 2" by simp + ultimately have "2 dvd m - n \ 2 dvd m + n" by (simp only:) + then show ?thesis by auto +next + case False + then show ?thesis by simp +qed + lemma two_dvd_diff_iff: fixes k l :: int shows "2 dvd k - l \ 2 dvd k + l" @@ -183,6 +197,14 @@ where "odd a \ \ even a" +lemma evenE [elim?]: + assumes "even a" + obtains b where "a = 2 * b" +proof - + from assms have "2 dvd a" by (simp add: even_def) + then show thesis using that .. +qed + lemma oddE [elim?]: assumes "odd a" obtains b where "a = 2 * b + 1" @@ -267,239 +289,95 @@ end -subsubsection {* Particularities for @{typ nat}/@{typ int} *} +subsubsection {* Particularities for @{typ nat} and @{typ int} *} + +lemma even_Suc [simp, presburger, algebra]: + "even (Suc n) = odd n" + by (simp add: even_def two_dvd_Suc_iff) + +lemma odd_pos: + "odd (n :: nat) \ 0 < n" + by (auto elim: oddE) + +lemma even_diff_nat [simp]: + fixes m n :: nat + shows "even (m - n) \ m < n \ even (m + n)" + by (simp add: even_def two_dvd_diff_nat_iff) lemma even_int_iff: "even (int n) \ even n" by (simp add: even_def dvd_int_iff) -declare transfer_morphism_int_nat [transfer add return: - even_int_iff -] - - -subsubsection {* Tools setup *} - -lemma [presburger]: - "even n \ even (int n)" - using even_int_iff [of n] by simp - -lemma [presburger]: - "even (a + b) \ even a \ even b \ odd a \ odd b" - by auto - - -subsubsection {* Legacy cruft *} - - -subsubsection {* Equivalent definitions *} - -lemma two_times_even_div_two: - "even (x::int) ==> 2 * (x div 2) = x" - by presburger - -lemma two_times_odd_div_two_plus_one: - "odd (x::int) ==> 2 * (x div 2) + 1 = x" - by presburger - - -subsubsection {* even and odd for nats *} - -lemma pos_int_even_equiv_nat_even: "0 \ x ==> even x = even (nat x)" -by (simp add: even_int_iff [symmetric]) - -lemma even_difference_nat [simp,presburger,algebra]: - "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))" - by presburger - -lemma even_Suc [simp ,presburger, algebra]: - "even (Suc x) = odd x" - by presburger - -lemma even_power_nat[simp,presburger,algebra]: - "even ((x::nat)^y) = (even x & 0 < y)" - by simp - - -subsubsection {* Equivalent definitions *} - -lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0" -by presburger - -lemma odd_nat_mod_two_eq_one: "odd (x::nat) ==> x mod (Suc (Suc 0)) = Suc 0" -by presburger - -lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)" -by presburger - -lemma odd_nat_equiv_def: "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)" -by presburger - -lemma even_nat_div_two_times_two: "even (x::nat) ==> - Suc (Suc 0) * (x div Suc (Suc 0)) = x" by presburger - -lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==> - Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x" by presburger +lemma even_nat_iff: + "0 \ k \ even (nat k) \ even k" + by (simp add: even_int_iff [symmetric]) subsubsection {* Parity and powers *} -lemma (in comm_ring_1) neg_power_if: - "(- a) ^ n = (if even n then (a ^ n) else - (a ^ n))" - by (induct n) simp_all +context comm_ring_1 +begin -lemma (in comm_ring_1) - shows neg_one_even_power [simp]: "even n \ (- 1) ^ n = 1" - and neg_one_odd_power [simp]: "odd n \ (- 1) ^ n = - 1" - by (simp_all add: neg_power_if) +lemma power_minus_even [simp]: + "even n \ (- a) ^ n = a ^ n" + by (auto elim: evenE) + +lemma power_minus_odd [simp]: + "odd n \ (- a) ^ n = - (a ^ n)" + by (auto elim: oddE) -lemma zero_le_even_power: "even n ==> - 0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n" - apply (simp add: even_def) - apply (erule dvdE) - apply (erule ssubst) - unfolding mult.commute [of 2] - unfolding power_mult power2_eq_square - apply (rule zero_le_square) - done +lemma neg_power_if: + "(- a) ^ n = (if even n then a ^ n else - (a ^ n))" + by simp -lemma zero_le_odd_power: - "odd n \ 0 \ (x::'a::{linordered_idom}) ^ n \ 0 \ x" - by (erule oddE) (auto simp: power_add zero_le_mult_iff mult_2 order_antisym_conv) +lemma neg_one_even_power [simp]: + "even n \ (- 1) ^ n = 1" + by simp -lemma zero_le_power_eq [presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) = - (even n | (odd n & 0 <= x))" - apply auto - apply (subst zero_le_odd_power [symmetric]) - apply assumption+ - apply (erule zero_le_even_power) - done - -lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{linordered_idom}) ^ n) = - (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))" - unfolding order_less_le zero_le_power_eq by auto +lemma neg_one_odd_power [simp]: + "odd n \ (- 1) ^ n = - 1" + by simp -lemma power_less_zero_eq[presburger]: "((x::'a::{linordered_idom}) ^ n < 0) = - (odd n & x < 0)" - apply (subst linorder_not_le [symmetric])+ - apply (subst zero_le_power_eq) - apply auto - done +end -lemma power_le_zero_eq[presburger]: "((x::'a::{linordered_idom}) ^ n <= 0) = - (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))" - apply (subst linorder_not_less [symmetric])+ - apply (subst zero_less_power_eq) - apply auto - done +lemma zero_less_power_nat_eq_numeral [simp]: -- \FIXME move\ + "0 < (n :: nat) ^ numeral w \ 0 < n \ numeral w = (0 :: nat)" + by (fact nat_zero_less_power_iff) -lemma power_even_abs: "even n ==> - (abs (x::'a::{linordered_idom}))^n = x^n" - apply (subst power_abs [symmetric]) - apply (simp add: zero_le_even_power) - done +context linordered_idom +begin -lemma power_minus_even [simp]: "even n ==> - (- x)^n = (x^n::'a::{comm_ring_1})" - apply (subst power_minus) - apply simp - done +lemma power_eq_0_iff' [simp]: -- \FIXME move\ + "a ^ n = 0 \ a = 0 \ n > 0" + by (induct n) auto -lemma power_minus_odd [simp]: "odd n ==> - (- x)^n = - (x^n::'a::{comm_ring_1})" - apply (subst power_minus) - apply simp - done - -lemma power_mono_even: fixes x y :: "'a :: {linordered_idom}" - assumes "even n" and "\x\ \ \y\" - shows "x^n \ y^n" -proof - - have "0 \ \x\" by auto - with `\x\ \ \y\` - have "\x\^n \ \y\^n" by (rule power_mono) - thus ?thesis unfolding power_even_abs[OF `even n`] . +lemma power2_less_eq_zero_iff [simp]: -- \FIXME move\ + "a\<^sup>2 \ 0 \ a = 0" +proof (cases "a = 0") + case True then show ?thesis by simp +next + case False then have "a < 0 \ a > 0" by auto + then have "a\<^sup>2 > 0" by auto + then have "\ a\<^sup>2 \ 0" by (simp add: not_le) + with False show ?thesis by simp qed -lemma odd_pos: "odd (n::nat) \ 0 < n" by presburger +lemma zero_le_even_power: + "even n \ 0 \ a ^ n" + by (auto elim: evenE) -lemma power_mono_odd: fixes x y :: "'a :: {linordered_idom}" - assumes "odd n" and "x \ y" - shows "x^n \ y^n" -proof (cases "y < 0") - case True with `x \ y` have "-y \ -x" and "0 \ -y" by auto - hence "(-y)^n \ (-x)^n" by (rule power_mono) - thus ?thesis unfolding power_minus_odd[OF `odd n`] by auto +lemma zero_le_odd_power: + "odd n \ 0 \ a ^ n \ 0 \ a" + by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE) + +lemma zero_le_power_iff [presburger]: + "0 \ a ^ n \ 0 \ a \ even n" +proof (cases "even n") + case True + then obtain k where "n = 2 * k" .. + then show ?thesis by simp next case False - show ?thesis - proof (cases "x < 0") - case True hence "n \ 0" and "x \ 0" using `odd n`[THEN odd_pos] by auto - hence "x^n \ 0" unfolding power_le_zero_eq using `odd n` by auto - moreover - from `\ y < 0` have "0 \ y" by auto - hence "0 \ y^n" by auto - ultimately show ?thesis by auto - next - case False hence "0 \ x" by auto - with `x \ y` show ?thesis using power_mono by auto - qed -qed - - -subsubsection {* More Even/Odd Results *} - -lemma even_mult_two_ex: "even(n) = (\m::nat. n = 2*m)" by presburger -lemma odd_Suc_mult_two_ex: "odd(n) = (\m. n = Suc (2*m))" by presburger - -lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" by presburger - -lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)" -by presburger - -lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))" by presburger -lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)" by presburger - -lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)" by presburger - -lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)" - by presburger - -text {* Simplify, when the exponent is a numeral *} - -lemmas zero_le_power_eq_numeral [simp] = - zero_le_power_eq [of _ "numeral w"] for w - -lemmas zero_less_power_eq_numeral [simp] = - zero_less_power_eq [of _ "numeral w"] for w - -lemmas power_le_zero_eq_numeral [simp] = - power_le_zero_eq [of _ "numeral w"] for w - -lemmas power_less_zero_eq_numeral [simp] = - power_less_zero_eq [of _ "numeral w"] for w - -lemmas zero_less_power_nat_eq_numeral [simp] = - nat_zero_less_power_iff [of _ "numeral w"] for w - -lemmas power_eq_0_iff_numeral [simp] = - power_eq_0_iff [of _ "numeral w"] for w - -lemmas power_even_abs_numeral [simp] = - power_even_abs [of "numeral w" _] for w - - -subsubsection {* An Equivalence for @{term [source] "0 \ a^n"} *} - -lemma zero_le_power_iff[presburger]: - "(0 \ a^n) = (0 \ (a::'a::{linordered_idom}) | even n)" -proof cases - assume even: "even n" - then have "2 dvd n" by (simp add: even_def) - then obtain k where "n = 2 * k" .. - thus ?thesis by (simp add: zero_le_even_power even) -next - assume odd: "odd n" then obtain k where "n = 2 * k + 1" .. moreover have "a ^ (2 * k) \ 0 \ a = 0" by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff) @@ -507,20 +385,198 @@ by (auto simp add: zero_le_mult_iff zero_le_even_power) qed +lemma zero_le_power_eq [presburger]: -- \FIXME weaker version of @{text zero_le_power_iff}\ + "0 \ a ^ n \ even n \ odd n \ 0 \ a" + using zero_le_power_iff [of a n] by auto + +lemma zero_less_power_eq [presburger]: + "0 < a ^ n \ n = 0 \ even n \ a \ 0 \ odd n \ 0 < a" +proof - + have [simp]: "0 = a ^ n \ a = 0 \ n > 0" + unfolding power_eq_0_iff' [of a n, symmetric] by blast + show ?thesis + unfolding less_le zero_le_power_iff by auto +qed + +lemma power_less_zero_eq [presburger]: + "a ^ n < 0 \ odd n \ a < 0" + unfolding not_le [symmetric] zero_le_power_eq by auto + +lemma power_le_zero_eq [presburger]: + "a ^ n \ 0 \ n > 0 \ (odd n \ a \ 0 \ even n \ a = 0)" + unfolding not_less [symmetric] zero_less_power_eq by auto + +lemma power_even_abs: + "even n \ \a\ ^ n = a ^ n" + using power_abs [of a n] by (simp add: zero_le_even_power) + +lemma power_mono_even: + assumes "even n" and "\a\ \ \b\" + shows "a ^ n \ b ^ n" +proof - + have "0 \ \a\" by auto + with `\a\ \ \b\` + have "\a\ ^ n \ \b\ ^ n" by (rule power_mono) + with `even n` show ?thesis by (simp add: power_even_abs) +qed + +lemma power_mono_odd: + assumes "odd n" and "a \ b" + shows "a ^ n \ b ^ n" +proof (cases "b < 0") + case True with `a \ b` have "- b \ - a" and "0 \ - b" by auto + hence "(- b) ^ n \ (- a) ^ n" by (rule power_mono) + with `odd n` show ?thesis by simp +next + case False then have "0 \ b" by auto + show ?thesis + proof (cases "a < 0") + case True then have "n \ 0" and "a \ 0" using `odd n` [THEN odd_pos] by auto + then have "a ^ n \ 0" unfolding power_le_zero_eq using `odd n` by auto + moreover + from `0 \ b` have "0 \ b ^ n" by auto + ultimately show ?thesis by auto + next + case False then have "0 \ a" by auto + with `a \ b` show ?thesis using power_mono by auto + qed +qed + +text {* Simplify, when the exponent is a numeral *} + +lemma zero_le_power_eq_numeral [simp]: + "0 \ a ^ numeral w \ even (numeral w :: nat) \ odd (numeral w :: nat) \ 0 \ a" + by (fact zero_le_power_eq) + +lemma zero_less_power_eq_numeral [simp]: + "0 < a ^ numeral w \ numeral w = (0 :: nat) + \ even (numeral w :: nat) \ a \ 0 \ odd (numeral w :: nat) \ 0 < a" + by (fact zero_less_power_eq) + +lemma power_le_zero_eq_numeral [simp]: + "a ^ numeral w \ 0 \ (0 :: nat) < numeral w + \ (odd (numeral w :: nat) \ a \ 0 \ even (numeral w :: nat) \ a = 0)" + by (fact power_le_zero_eq) + +lemma power_less_zero_eq_numeral [simp]: + "a ^ numeral w < 0 \ odd (numeral w :: nat) \ a < 0" + by (fact power_less_zero_eq) + +lemma power_eq_0_iff_numeral [simp]: + "a ^ numeral w = (0 :: nat) \ a = 0 \ numeral w \ (0 :: nat)" + by (fact power_eq_0_iff) + +lemma power_even_abs_numeral [simp]: + "even (numeral w :: nat) \ \a\ ^ numeral w = a ^ numeral w" + by (fact power_even_abs) + +end + + +subsubsection {* Tools setup *} + +declare transfer_morphism_int_nat [transfer add return: + even_int_iff +] + +lemma [presburger]: + "even n \ even (int n)" + using even_int_iff [of n] by simp + +lemma (in semiring_parity) [presburger]: + "even (a + b) \ even a \ even b \ odd a \ odd b" + by auto + +lemma [presburger, algebra]: + fixes m n :: nat + shows "even (m - n) \ m < n \ even m \ even n \ odd m \ odd n" + by auto + +lemma [presburger, algebra]: + fixes m n :: nat + shows "even (m ^ n) \ even m \ 0 < n" + by simp + +lemma [presburger]: + fixes k :: int + shows "(k + 1) div 2 = k div 2 \ even k" + by presburger + +lemma [presburger]: + fixes k :: int + shows "(k + 1) div 2 = k div 2 + 1 \ odd k" + by presburger + +lemma [presburger]: + "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \ even n" + by presburger + subsubsection {* Miscellaneous *} -lemma [presburger]:"(x + 1) div 2 = x div 2 \ even (x::int)" by presburger -lemma [presburger]: "(x + 1) div 2 = x div 2 + 1 \ odd (x::int)" by presburger -lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2" by presburger -lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1" by presburger +lemma even_mult_two_ex: + "even(n) = (\m::nat. n = 2*m)" + by presburger + +lemma odd_Suc_mult_two_ex: + "odd(n) = (\m. n = Suc (2*m))" + by presburger + +lemma even_nat_plus_one_div_two: + "even (x::nat) ==> (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" + by presburger + +lemma odd_nat_plus_one_div_two: + "odd (x::nat) ==> (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" + by presburger + +lemma even_nat_mod_two_eq_zero: + "even (x::nat) ==> x mod Suc (Suc 0) = 0" + by presburger + +lemma odd_nat_mod_two_eq_one: + "odd (x::nat) ==> x mod Suc (Suc 0) = Suc 0" + by presburger + +lemma even_nat_equiv_def: + "even (x::nat) = (x mod Suc (Suc 0) = 0)" + by presburger + +lemma odd_nat_equiv_def: + "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)" + by presburger -lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \ even x" by presburger -lemma even_nat_plus_one_div_two: "even (x::nat) ==> - (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" by presburger +lemma even_nat_div_two_times_two: + "even (x::nat) ==> Suc (Suc 0) * (x div Suc (Suc 0)) = x" + by presburger + +lemma odd_nat_div_two_times_two_plus_one: + "odd (x::nat) ==> Suc (Suc (Suc 0) * (x div Suc (Suc 0))) = x" + by presburger + +lemma lemma_even_div2 [simp]: + "even (n::nat) ==> (n + 1) div 2 = n div 2" + by presburger + +lemma lemma_odd_div2 [simp]: + "odd n ==> (n + 1) div 2 = Suc (n div 2)" + by presburger -lemma odd_nat_plus_one_div_two: "odd (x::nat) ==> - (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" by presburger +lemma even_num_iff: + "0 < n ==> even n = (odd (n - 1 :: nat))" + by presburger + +lemma even_even_mod_4_iff: + "even (n::nat) = even (n mod 4)" + by presburger + +lemma lemma_odd_mod_4_div_2: + "n mod 4 = (3::nat) ==> odd((n - 1) div 2)" + by presburger + +lemma lemma_even_mod_4_div_2: + "n mod 4 = (1::nat) ==> even ((n - 1) div 2)" + by presburger end diff -r 92f935f34b28 -r ad09a4635e26 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sat Oct 18 22:49:59 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sat Oct 18 22:50:35 2014 +0200 @@ -415,16 +415,16 @@ fun zipper_map f = let fun zed _ [] = [] - | zed xs (y :: ys) = f (xs, y, ys) :: zed (xs @ [y]) ys + | zed xs (y :: ys) = f (xs, y, ys) :: zed (xs @ [y]) ys; in zed [] end; -val unfla = fold_map (fn _ => fn y :: ys => (y, ys)) -val unflat = fold_map unfla -val unflatt = fold_map unflat -val unflattt = fold_map unflatt +fun unfla _ = rpair []; +fun unflat xss = fold_map unfla xss; +fun unflatt xsss = fold_map unflat xsss; +fun unflattt xssss = fold_map unflatt xssss; fun ctr_sugar_kind_of_fp_kind Least_FP = Datatype - | ctr_sugar_kind_of_fp_kind Greatest_FP = Codatatype + | ctr_sugar_kind_of_fp_kind Greatest_FP = Codatatype; fun uncurry_thm 0 thm = thm | uncurry_thm 1 thm = thm