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