src/HOL/Library/Nonpos_Ints.thy
 author hoelzl Tue Jan 05 13:35:06 2016 +0100 (2016-01-05) changeset 62055 755fda743c49 parent 62049 b0f941e207cf child 62072 bf3d9f113474 permissions -rw-r--r--
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
 hoelzl@62055 ` 1` ```(* Title: HOL/Library/Nonpos_Ints.thy ``` hoelzl@62055 ` 2` ``` Author: Manuel Eberl, TU München ``` eberlm@62049 ` 3` ```*) ``` hoelzl@62055 ` 4` hoelzl@62055 ` 5` ```section \Non-positive integers\ ``` hoelzl@62055 ` 6` eberlm@62049 ` 7` ```theory Nonpos_Ints ``` eberlm@62049 ` 8` ```imports Complex_Main ``` eberlm@62049 ` 9` ```begin ``` eberlm@62049 ` 10` hoelzl@62055 ` 11` ```text \ ``` hoelzl@62055 ` 12` ``` The set of non-positive integers on a ring. (in analogy to the set of non-negative ``` hoelzl@62055 ` 13` ``` integers @{term "\"}) This is useful e.g. for the Gamma function. ``` hoelzl@62055 ` 14` ```\ ``` eberlm@62049 ` 15` eberlm@62049 ` 16` ```definition nonpos_Ints ("\\<^sub>\\<^sub>0") where "\\<^sub>\\<^sub>0 = {of_int n |n. n \ 0}" ``` eberlm@62049 ` 17` eberlm@62049 ` 18` ```lemma zero_in_nonpos_Ints [simp,intro]: "0 \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 19` ``` unfolding nonpos_Ints_def by (auto intro!: exI[of _ "0::int"]) ``` eberlm@62049 ` 20` eberlm@62049 ` 21` ```lemma neg_one_in_nonpos_Ints [simp,intro]: "-1 \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 22` ``` unfolding nonpos_Ints_def by (auto intro!: exI[of _ "-1::int"]) ``` eberlm@62049 ` 23` eberlm@62049 ` 24` ```lemma neg_numeral_in_nonpos_Ints [simp,intro]: "-numeral n \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 25` ``` unfolding nonpos_Ints_def by (auto intro!: exI[of _ "-numeral n::int"]) ``` eberlm@62049 ` 26` eberlm@62049 ` 27` ```lemma one_notin_nonpos_Ints [simp]: "(1 :: 'a :: ring_char_0) \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 28` ``` by (auto simp: nonpos_Ints_def) ``` eberlm@62049 ` 29` eberlm@62049 ` 30` ```lemma numeral_notin_nonpos_Ints [simp]: "(numeral n :: 'a :: ring_char_0) \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 31` ``` by (auto simp: nonpos_Ints_def) ``` eberlm@62049 ` 32` eberlm@62049 ` 33` eberlm@62049 ` 34` ```lemma minus_of_nat_in_nonpos_Ints [simp, intro]: "- of_nat n \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 35` ```proof - ``` eberlm@62049 ` 36` ``` have "- of_nat n = of_int (-int n)" by simp ``` eberlm@62049 ` 37` ``` also have "-int n \ 0" by simp ``` eberlm@62049 ` 38` ``` hence "of_int (-int n) \ \\<^sub>\\<^sub>0" unfolding nonpos_Ints_def by blast ``` eberlm@62049 ` 39` ``` finally show ?thesis . ``` eberlm@62049 ` 40` ```qed ``` eberlm@62049 ` 41` eberlm@62049 ` 42` ```lemma of_nat_in_nonpos_Ints_iff: "(of_nat n :: 'a :: {ring_1,ring_char_0}) \ \\<^sub>\\<^sub>0 \ n = 0" ``` eberlm@62049 ` 43` ```proof ``` eberlm@62049 ` 44` ``` assume "(of_nat n :: 'a) \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 45` ``` then obtain m where "of_nat n = (of_int m :: 'a)" "m \ 0" by (auto simp: nonpos_Ints_def) ``` eberlm@62049 ` 46` ``` hence "(of_int m :: 'a) = of_nat n" by simp ``` eberlm@62049 ` 47` ``` also have "... = of_int (int n)" by simp ``` eberlm@62049 ` 48` ``` finally have "m = int n" by (subst (asm) of_int_eq_iff) ``` eberlm@62049 ` 49` ``` with `m \ 0` show "n = 0" by auto ``` eberlm@62049 ` 50` ```qed simp ``` eberlm@62049 ` 51` eberlm@62049 ` 52` ```lemma nonpos_Ints_of_int: "n \ 0 \ of_int n \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 53` ``` unfolding nonpos_Ints_def by blast ``` eberlm@62049 ` 54` eberlm@62049 ` 55` ```lemma nonpos_IntsI: ``` eberlm@62049 ` 56` ``` "x \ \ \ x \ 0 \ (x :: 'a :: linordered_idom) \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 57` ``` using assms unfolding nonpos_Ints_def Ints_def by auto ``` eberlm@62049 ` 58` eberlm@62049 ` 59` ```lemma nonpos_Ints_subset_Ints: "\\<^sub>\\<^sub>0 \ \" ``` eberlm@62049 ` 60` ``` unfolding nonpos_Ints_def Ints_def by blast ``` eberlm@62049 ` 61` eberlm@62049 ` 62` ```lemma nonpos_Ints_nonpos [dest]: "x \ \\<^sub>\\<^sub>0 \ x \ (0 :: 'a :: linordered_idom)" ``` eberlm@62049 ` 63` ``` unfolding nonpos_Ints_def by auto ``` eberlm@62049 ` 64` eberlm@62049 ` 65` ```lemma nonpos_Ints_Int [dest]: "x \ \\<^sub>\\<^sub>0 \ x \ \" ``` eberlm@62049 ` 66` ``` unfolding nonpos_Ints_def Ints_def by blast ``` eberlm@62049 ` 67` eberlm@62049 ` 68` ```lemma nonpos_Ints_cases: ``` eberlm@62049 ` 69` ``` assumes "x \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 70` ``` obtains n where "x = of_int n" "n \ 0" ``` eberlm@62049 ` 71` ``` using assms unfolding nonpos_Ints_def by (auto elim!: Ints_cases) ``` eberlm@62049 ` 72` eberlm@62049 ` 73` ```lemma nonpos_Ints_cases': ``` eberlm@62049 ` 74` ``` assumes "x \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 75` ``` obtains n where "x = -of_nat n" ``` eberlm@62049 ` 76` ```proof - ``` eberlm@62049 ` 77` ``` from assms obtain m where "x = of_int m" and m: "m \ 0" by (auto elim!: nonpos_Ints_cases) ``` eberlm@62049 ` 78` ``` hence "x = - of_int (-m)" by auto ``` eberlm@62049 ` 79` ``` also from m have "(of_int (-m) :: 'a) = of_nat (nat (-m))" by simp_all ``` eberlm@62049 ` 80` ``` finally show ?thesis by (rule that) ``` eberlm@62049 ` 81` ```qed ``` eberlm@62049 ` 82` eberlm@62049 ` 83` ```lemma of_real_in_nonpos_Ints_iff: "(of_real x :: 'a :: real_algebra_1) \ \\<^sub>\\<^sub>0 \ x \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 84` ```proof ``` eberlm@62049 ` 85` ``` assume "of_real x \ (\\<^sub>\\<^sub>0 :: 'a set)" ``` eberlm@62049 ` 86` ``` then obtain n where "(of_real x :: 'a) = of_int n" "n \ 0" by (erule nonpos_Ints_cases) ``` eberlm@62049 ` 87` ``` note `of_real x = of_int n` ``` eberlm@62049 ` 88` ``` also have "of_int n = of_real (of_int n)" by (rule of_real_of_int_eq [symmetric]) ``` eberlm@62049 ` 89` ``` finally have "x = of_int n" by (subst (asm) of_real_eq_iff) ``` eberlm@62049 ` 90` ``` with `n \ 0` show "x \ \\<^sub>\\<^sub>0" by (simp add: nonpos_Ints_of_int) ``` eberlm@62049 ` 91` ```qed (auto elim!: nonpos_Ints_cases intro!: nonpos_Ints_of_int) ``` eberlm@62049 ` 92` eberlm@62049 ` 93` ```lemma nonpos_Ints_altdef: "\\<^sub>\\<^sub>0 = {n \ \. (n :: 'a :: linordered_idom) \ 0}" ``` eberlm@62049 ` 94` ``` by (auto intro!: nonpos_IntsI elim!: nonpos_Ints_cases) ``` eberlm@62049 ` 95` eberlm@62049 ` 96` ```lemma uminus_in_Nats_iff: "-x \ \ \ x \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 97` ```proof ``` eberlm@62049 ` 98` ``` assume "-x \ \" ``` eberlm@62049 ` 99` ``` then obtain n where "n \ 0" "-x = of_int n" by (auto simp: Nats_altdef1) ``` eberlm@62049 ` 100` ``` hence "-n \ 0" "x = of_int (-n)" by (simp_all add: eq_commute minus_equation_iff[of x]) ``` eberlm@62049 ` 101` ``` thus "x \ \\<^sub>\\<^sub>0" unfolding nonpos_Ints_def by blast ``` eberlm@62049 ` 102` ```next ``` eberlm@62049 ` 103` ``` assume "x \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 104` ``` then obtain n where "n \ 0" "x = of_int n" by (auto simp: nonpos_Ints_def) ``` eberlm@62049 ` 105` ``` hence "-n \ 0" "-x = of_int (-n)" by (simp_all add: eq_commute minus_equation_iff[of x]) ``` eberlm@62049 ` 106` ``` thus "-x \ \" unfolding Nats_altdef1 by blast ``` eberlm@62049 ` 107` ```qed ``` eberlm@62049 ` 108` eberlm@62049 ` 109` ```lemma uminus_in_nonpos_Ints_iff: "-x \ \\<^sub>\\<^sub>0 \ x \ \" ``` eberlm@62049 ` 110` ``` using uminus_in_Nats_iff[of "-x"] by simp ``` eberlm@62049 ` 111` eberlm@62049 ` 112` ```lemma nonpos_Ints_mult: "x \ \\<^sub>\\<^sub>0 \ y \ \\<^sub>\\<^sub>0 \ x * y \ \" ``` eberlm@62049 ` 113` ``` using Nats_mult[of "-x" "-y"] by (simp add: uminus_in_Nats_iff) ``` eberlm@62049 ` 114` eberlm@62049 ` 115` ```lemma Nats_mult_nonpos_Ints: "x \ \ \ y \ \\<^sub>\\<^sub>0 \ x * y \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 116` ``` using Nats_mult[of x "-y"] by (simp add: uminus_in_Nats_iff) ``` eberlm@62049 ` 117` eberlm@62049 ` 118` ```lemma nonpos_Ints_mult_Nats: ``` eberlm@62049 ` 119` ``` "x \ \\<^sub>\\<^sub>0 \ y \ \ \ x * y \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 120` ``` using Nats_mult[of "-x" y] by (simp add: uminus_in_Nats_iff) ``` eberlm@62049 ` 121` eberlm@62049 ` 122` ```lemma nonpos_Ints_add: ``` eberlm@62049 ` 123` ``` "x \ \\<^sub>\\<^sub>0 \ y \ \\<^sub>\\<^sub>0 \ x + y \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 124` ``` using Nats_add[of "-x" "-y"] uminus_in_Nats_iff[of "y+x", simplified minus_add] ``` eberlm@62049 ` 125` ``` by (simp add: uminus_in_Nats_iff add.commute) ``` eberlm@62049 ` 126` eberlm@62049 ` 127` ```lemma nonpos_Ints_diff_Nats: ``` eberlm@62049 ` 128` ``` "x \ \\<^sub>\\<^sub>0 \ y \ \ \ x - y \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 129` ``` using Nats_add[of "-x" "y"] uminus_in_Nats_iff[of "x-y", simplified minus_add] ``` eberlm@62049 ` 130` ``` by (simp add: uminus_in_Nats_iff add.commute) ``` eberlm@62049 ` 131` eberlm@62049 ` 132` ```lemma Nats_diff_nonpos_Ints: ``` eberlm@62049 ` 133` ``` "x \ \ \ y \ \\<^sub>\\<^sub>0 \ x - y \ \" ``` eberlm@62049 ` 134` ``` using Nats_add[of "x" "-y"] by (simp add: uminus_in_Nats_iff add.commute) ``` eberlm@62049 ` 135` eberlm@62049 ` 136` ```lemma plus_of_nat_eq_0_imp: "z + of_nat n = 0 \ z \ \\<^sub>\\<^sub>0" ``` eberlm@62049 ` 137` ```proof - ``` eberlm@62049 ` 138` ``` assume "z + of_nat n = 0" ``` eberlm@62049 ` 139` ``` hence A: "z = - of_nat n" by (simp add: eq_neg_iff_add_eq_0) ``` eberlm@62049 ` 140` ``` show "z \ \\<^sub>\\<^sub>0" by (subst A) simp ``` eberlm@62049 ` 141` ```qed ``` eberlm@62049 ` 142` eberlm@62049 ` 143` `end`