|
1 (* |
|
2 Title: HOL/Computational_Algebra/Formal_Laurent_Series.thy |
|
3 Author: Jeremy Sylvestre, University of Alberta (Augustana Campus) |
|
4 *) |
|
5 |
|
6 |
|
7 section \<open>A formalization of formal Laurent series\<close> |
|
8 |
|
9 theory Formal_Laurent_Series |
|
10 imports |
|
11 Polynomial_FPS |
|
12 begin |
|
13 |
|
14 |
|
15 subsection \<open>The type of formal Laurent series\<close> |
|
16 |
|
17 subsubsection \<open>Type definition\<close> |
|
18 |
|
19 typedef (overloaded) 'a fls = "{f::int \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n::nat. f (- int n) = 0}" |
|
20 morphisms fls_nth Abs_fls |
|
21 proof |
|
22 show "(\<lambda>x. 0) \<in> {f::int \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n::nat. f (- int n) = 0}" |
|
23 by simp |
|
24 qed |
|
25 |
|
26 setup_lifting type_definition_fls |
|
27 |
|
28 unbundle fps_notation |
|
29 notation fls_nth (infixl "$$" 75) |
|
30 |
|
31 lemmas fls_eqI = iffD1[OF fls_nth_inject, OF iffD2, OF fun_eq_iff, OF allI] |
|
32 |
|
33 lemma expand_fls_eq: "f = g \<longleftrightarrow> (\<forall>n. f $$ n = g $$ n)" |
|
34 by (simp add: fls_nth_inject[symmetric] fun_eq_iff) |
|
35 |
|
36 lemma nth_Abs_fls [simp]: "\<forall>\<^sub>\<infinity>n. f (- int n) = 0 \<Longrightarrow> Abs_fls f $$ n = f n" |
|
37 by (simp add: Abs_fls_inverse[OF CollectI]) |
|
38 |
|
39 lemmas nth_Abs_fls_finite_nonzero_neg_nth = nth_Abs_fls[OF iffD2, OF eventually_cofinite] |
|
40 lemmas nth_Abs_fls_ex_nat_lower_bound = nth_Abs_fls[OF iffD2, OF MOST_nat] |
|
41 lemmas nth_Abs_fls_nat_lower_bound = nth_Abs_fls_ex_nat_lower_bound[OF exI] |
|
42 |
|
43 lemma nth_Abs_fls_ex_lower_bound: |
|
44 assumes "\<exists>N. \<forall>n<N. f n = 0" |
|
45 shows "Abs_fls f $$ n = f n" |
|
46 proof (intro nth_Abs_fls_ex_nat_lower_bound) |
|
47 from assms obtain N::int where "\<forall>n<N. f n = 0" by fast |
|
48 hence "\<forall>n > (if N < 0 then nat (-N) else 0). f (-int n) = 0" by auto |
|
49 thus "\<exists>M. \<forall>n>M. f (- int n) = 0" by fast |
|
50 qed |
|
51 |
|
52 lemmas nth_Abs_fls_lower_bound = nth_Abs_fls_ex_lower_bound[OF exI] |
|
53 |
|
54 lemmas MOST_fls_neg_nth_eq_0 [simp] = CollectD[OF fls_nth] |
|
55 lemmas fls_finite_nonzero_neg_nth = iffD1[OF eventually_cofinite MOST_fls_neg_nth_eq_0] |
|
56 |
|
57 lemma fls_nth_vanishes_below_natE: |
|
58 fixes f :: "'a::zero fls" |
|
59 obtains N :: nat |
|
60 where "\<forall>n>N. f$$(-int n) = 0" |
|
61 using iffD1[OF MOST_nat MOST_fls_neg_nth_eq_0] |
|
62 by blast |
|
63 |
|
64 lemma fls_nth_vanishes_belowE: |
|
65 fixes f :: "'a::zero fls" |
|
66 obtains N :: int |
|
67 where "\<forall>n<N. f$$n = 0" |
|
68 proof- |
|
69 obtain K :: nat where K: "\<forall>n>K. f$$(-int n) = 0" by (elim fls_nth_vanishes_below_natE) |
|
70 have "\<forall>n < -int K. f$$n = 0" |
|
71 proof clarify |
|
72 fix n assume n: "n < -int K" |
|
73 define m where "m \<equiv> nat (-n)" |
|
74 with n have "m > K" by simp |
|
75 moreover from n m_def have "f$$n = f $$ (-int m)" by simp |
|
76 ultimately show "f $$ n = 0" using K by simp |
|
77 qed |
|
78 thus "(\<And>N. \<forall>n<N. f $$ n = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis" by fast |
|
79 qed |
|
80 |
|
81 |
|
82 subsubsection \<open>Definition of basic zero, one, constant, X, and inverse X elements\<close> |
|
83 |
|
84 instantiation fls :: (zero) zero |
|
85 begin |
|
86 lift_definition zero_fls :: "'a fls" is "\<lambda>_. 0" by simp |
|
87 instance .. |
|
88 end |
|
89 |
|
90 lemma fls_zero_nth [simp]: "0 $$ n = 0" |
|
91 by (simp add: zero_fls_def) |
|
92 |
|
93 lemma fls_zero_eqI: "(\<And>n. f$$n = 0) \<Longrightarrow> f = 0" |
|
94 by (fastforce intro: fls_eqI) |
|
95 |
|
96 lemma fls_nonzeroI: "f$$n \<noteq> 0 \<Longrightarrow> f \<noteq> 0" |
|
97 by auto |
|
98 |
|
99 lemma fls_nonzero_nth: "f \<noteq> 0 \<longleftrightarrow> (\<exists> n. f $$ n \<noteq> 0)" |
|
100 using fls_zero_eqI by fastforce |
|
101 |
|
102 lemma fls_trivial_delta_eq_zero [simp]: "b = 0 \<Longrightarrow> Abs_fls (\<lambda>n. if n=a then b else 0) = 0" |
|
103 by (intro fls_zero_eqI) simp |
|
104 |
|
105 lemma fls_delta_nth [simp]: |
|
106 "Abs_fls (\<lambda>n. if n=a then b else 0) $$ n = (if n=a then b else 0)" |
|
107 using nth_Abs_fls_lower_bound[of a "\<lambda>n. if n=a then b else 0"] by simp |
|
108 |
|
109 instantiation fls :: ("{zero,one}") one |
|
110 begin |
|
111 lift_definition one_fls :: "'a fls" is "\<lambda>k. if k = 0 then 1 else 0" |
|
112 by (simp add: eventually_cofinite) |
|
113 instance .. |
|
114 end |
|
115 |
|
116 lemma fls_one_nth [simp]: |
|
117 "1 $$ n = (if n = 0 then 1 else 0)" |
|
118 by (simp add: one_fls_def eventually_cofinite) |
|
119 |
|
120 instance fls :: (zero_neq_one) zero_neq_one |
|
121 proof (standard, standard) |
|
122 assume "(0::'a fls) = (1::'a fls)" |
|
123 hence "(0::'a fls) $$ 0 = (1::'a fls) $$ 0" by simp |
|
124 thus False by simp |
|
125 qed |
|
126 |
|
127 definition fls_const :: "'a::zero \<Rightarrow> 'a fls" |
|
128 where "fls_const c \<equiv> Abs_fls (\<lambda>n. if n = 0 then c else 0)" |
|
129 |
|
130 lemma fls_const_nth [simp]: "fls_const c $$ n = (if n = 0 then c else 0)" |
|
131 by (simp add: fls_const_def eventually_cofinite) |
|
132 |
|
133 lemma fls_const_0 [simp]: "fls_const 0 = 0" |
|
134 unfolding fls_const_def using fls_trivial_delta_eq_zero by fast |
|
135 |
|
136 lemma fls_const_nonzero: "c \<noteq> 0 \<Longrightarrow> fls_const c \<noteq> 0" |
|
137 using fls_nonzeroI[of "fls_const c" 0] by simp |
|
138 |
|
139 lemma fls_const_1 [simp]: "fls_const 1 = 1" |
|
140 unfolding fls_const_def one_fls_def .. |
|
141 |
|
142 lift_definition fls_X :: "'a::{zero,one} fls" |
|
143 is "\<lambda>n. if n = 1 then 1 else 0" |
|
144 by simp |
|
145 |
|
146 lemma fls_X_nth [simp]: |
|
147 "fls_X $$ n = (if n = 1 then 1 else 0)" |
|
148 by (simp add: fls_X_def) |
|
149 |
|
150 lemma fls_X_nonzero [simp]: "(fls_X :: 'a :: zero_neq_one fls) \<noteq> 0" |
|
151 by (intro fls_nonzeroI) simp |
|
152 |
|
153 lift_definition fls_X_inv :: "'a::{zero,one} fls" |
|
154 is "\<lambda>n. if n = -1 then 1 else 0" |
|
155 by (simp add: eventually_cofinite) |
|
156 |
|
157 lemma fls_X_inv_nth [simp]: |
|
158 "fls_X_inv $$ n = (if n = -1 then 1 else 0)" |
|
159 by (simp add: fls_X_inv_def eventually_cofinite) |
|
160 |
|
161 lemma fls_X_inv_nonzero [simp]: "(fls_X_inv :: 'a :: zero_neq_one fls) \<noteq> 0" |
|
162 by (intro fls_nonzeroI) simp |
|
163 |
|
164 |
|
165 subsection \<open>Subdegrees\<close> |
|
166 |
|
167 lemma unique_fls_subdegree: |
|
168 assumes "f \<noteq> 0" |
|
169 shows "\<exists>!n. f$$n \<noteq> 0 \<and> (\<forall>m. f$$m \<noteq> 0 \<longrightarrow> n \<le> m)" |
|
170 proof- |
|
171 obtain N::nat where N: "\<forall>n>N. f$$(-int n) = 0" by (elim fls_nth_vanishes_below_natE) |
|
172 define M where "M \<equiv> -int N" |
|
173 have M: "\<And>m. f$$m \<noteq> 0 \<Longrightarrow> M \<le> m" |
|
174 proof- |
|
175 fix m assume m: "f$$m \<noteq> 0" |
|
176 show "M \<le> m" |
|
177 proof (cases "m<0") |
|
178 case True with m N M_def show ?thesis |
|
179 using allE[OF N, of "nat (-m)" False] by force |
|
180 qed (simp add: M_def) |
|
181 qed |
|
182 have "\<not> (\<forall>k::nat. f$$(M + int k) = 0)" |
|
183 proof |
|
184 assume above0: "\<forall>k::nat. f$$(M + int k) = 0" |
|
185 have "f=0" |
|
186 proof (rule fls_zero_eqI) |
|
187 fix n show "f$$n = 0" |
|
188 proof (cases "M \<le> n") |
|
189 case True |
|
190 define k where "k = nat (n - M)" |
|
191 from True have "n = M + int k" by (simp add: k_def) |
|
192 with above0 show ?thesis by simp |
|
193 next |
|
194 case False with M show ?thesis by auto |
|
195 qed |
|
196 qed |
|
197 with assms show False by fast |
|
198 qed |
|
199 hence ex_k: "\<exists>k::nat. f$$(M + int k) \<noteq> 0" by fast |
|
200 define k where "k \<equiv> (LEAST k::nat. f$$(M + int k) \<noteq> 0)" |
|
201 define n where "n \<equiv> M + int k" |
|
202 from k_def n_def have fn: "f$$n \<noteq> 0" using LeastI_ex[OF ex_k] by simp |
|
203 moreover have "\<forall>m. f$$m \<noteq> 0 \<longrightarrow> n \<le> m" |
|
204 proof (clarify) |
|
205 fix m assume m: "f$$m \<noteq> 0" |
|
206 with M have "M \<le> m" by fast |
|
207 define l where "l = nat (m - M)" |
|
208 from \<open>M \<le> m\<close> have l: "m = M + int l" by (simp add: l_def) |
|
209 with n_def m k_def l show "n \<le> m" |
|
210 using Least_le[of "\<lambda>k. f$$(M + int k) \<noteq> 0" l] by auto |
|
211 qed |
|
212 moreover have "\<And>n'. f$$n' \<noteq> 0 \<Longrightarrow> (\<forall>m. f$$m \<noteq> 0 \<longrightarrow> n' \<le> m) \<Longrightarrow> n' = n" |
|
213 proof- |
|
214 fix n' :: int |
|
215 assume n': "f$$n' \<noteq> 0" "\<forall>m. f$$m \<noteq> 0 \<longrightarrow> n' \<le> m" |
|
216 from n'(1) M have "M \<le> n'" by fast |
|
217 define l where "l = nat (n' - M)" |
|
218 from \<open>M \<le> n'\<close> have l: "n' = M + int l" by (simp add: l_def) |
|
219 with n_def k_def n' fn show "n' = n" |
|
220 using Least_le[of "\<lambda>k. f$$(M + int k) \<noteq> 0" l] by force |
|
221 qed |
|
222 ultimately show ?thesis |
|
223 using ex1I[of "\<lambda>n. f$$n \<noteq> 0 \<and> (\<forall>m. f$$m \<noteq> 0 \<longrightarrow> n \<le> m)" n] by blast |
|
224 qed |
|
225 |
|
226 definition fls_subdegree :: "('a::zero) fls \<Rightarrow> int" |
|
227 where "fls_subdegree f \<equiv> (if f = 0 then 0 else LEAST n::int. f$$n \<noteq> 0)" |
|
228 |
|
229 lemma fls_zero_subdegree [simp]: "fls_subdegree 0 = 0" |
|
230 by (simp add: fls_subdegree_def) |
|
231 |
|
232 lemma nth_fls_subdegree_nonzero [simp]: "f \<noteq> 0 \<Longrightarrow> f $$ fls_subdegree f \<noteq> 0" |
|
233 using Least1I[OF unique_fls_subdegree] by (simp add: fls_subdegree_def) |
|
234 |
|
235 lemma nth_fls_subdegree_zero_iff: "(f $$ fls_subdegree f = 0) \<longleftrightarrow> (f = 0)" |
|
236 using nth_fls_subdegree_nonzero by auto |
|
237 |
|
238 lemma fls_subdegree_leI: "f $$ n \<noteq> 0 \<Longrightarrow> fls_subdegree f \<le> n" |
|
239 using Least1_le[OF unique_fls_subdegree] |
|
240 by (auto simp: fls_subdegree_def) |
|
241 |
|
242 lemma fls_subdegree_leI': "f $$ n \<noteq> 0 \<Longrightarrow> n \<le> m \<Longrightarrow> fls_subdegree f \<le> m" |
|
243 using fls_subdegree_leI by fastforce |
|
244 |
|
245 lemma fls_eq0_below_subdegree [simp]: "n < fls_subdegree f \<Longrightarrow> f $$ n = 0" |
|
246 using fls_subdegree_leI by fastforce |
|
247 |
|
248 lemma fls_subdegree_geI: "f \<noteq> 0 \<Longrightarrow> (\<And>k. k < n \<Longrightarrow> f $$ k = 0) \<Longrightarrow> n \<le> fls_subdegree f" |
|
249 using nth_fls_subdegree_nonzero by force |
|
250 |
|
251 lemma fls_subdegree_ge0I: "(\<And>k. k < 0 \<Longrightarrow> f $$ k = 0) \<Longrightarrow> 0 \<le> fls_subdegree f" |
|
252 using fls_subdegree_geI[of f 0] by (cases "f=0") auto |
|
253 |
|
254 lemma fls_subdegree_greaterI: |
|
255 assumes "f \<noteq> 0" "\<And>k. k \<le> n \<Longrightarrow> f $$ k = 0" |
|
256 shows "n < fls_subdegree f" |
|
257 using assms(1) assms(2)[of "fls_subdegree f"] nth_fls_subdegree_nonzero[of f] |
|
258 by force |
|
259 |
|
260 lemma fls_subdegree_eqI: "f $$ n \<noteq> 0 \<Longrightarrow> (\<And>k. k < n \<Longrightarrow> f $$ k = 0) \<Longrightarrow> fls_subdegree f = n" |
|
261 using fls_subdegree_leI fls_subdegree_geI[of f] |
|
262 by fastforce |
|
263 |
|
264 lemma fls_delta_subdegree [simp]: |
|
265 "b \<noteq> 0 \<Longrightarrow> fls_subdegree (Abs_fls (\<lambda>n. if n=a then b else 0)) = a" |
|
266 by (intro fls_subdegree_eqI) simp_all |
|
267 |
|
268 lemma fls_delta0_subdegree: "fls_subdegree (Abs_fls (\<lambda>n. if n=0 then a else 0)) = 0" |
|
269 by (cases "a=0") simp_all |
|
270 |
|
271 lemma fls_one_subdegree [simp]: "fls_subdegree 1 = 0" |
|
272 by (auto intro: fls_delta0_subdegree simp: one_fls_def) |
|
273 |
|
274 lemma fls_const_subdegree [simp]: "fls_subdegree (fls_const c) = 0" |
|
275 by (cases "c=0") (auto intro: fls_subdegree_eqI) |
|
276 |
|
277 lemma fls_X_subdegree [simp]: "fls_subdegree (fls_X::'a::{zero_neq_one} fls) = 1" |
|
278 by (intro fls_subdegree_eqI) simp_all |
|
279 |
|
280 lemma fls_X_inv_subdegree [simp]: "fls_subdegree (fls_X_inv::'a::{zero_neq_one} fls) = -1" |
|
281 by (intro fls_subdegree_eqI) simp_all |
|
282 |
|
283 lemma fls_eq_above_subdegreeI: |
|
284 assumes "N \<le> fls_subdegree f" "N \<le> fls_subdegree g" "\<forall>k\<ge>N. f $$ k = g $$ k" |
|
285 shows "f = g" |
|
286 proof (rule fls_eqI) |
|
287 fix n from assms show "f $$ n = g $$ n" by (cases "n < N") auto |
|
288 qed |
|
289 |
|
290 |
|
291 subsection \<open>Shifting\<close> |
|
292 |
|
293 subsubsection \<open>Shift definition\<close> |
|
294 |
|
295 definition fls_shift :: "int \<Rightarrow> ('a::zero) fls \<Rightarrow> 'a fls" |
|
296 where "fls_shift n f \<equiv> Abs_fls (\<lambda>k. f $$ (k+n))" |
|
297 \<comment> \<open>Since the index set is unbounded in both directions, we can shift in either direction.\<close> |
|
298 |
|
299 lemma fls_shift_nth [simp]: "fls_shift m f $$ n = f $$ (n+m)" |
|
300 unfolding fls_shift_def |
|
301 proof (rule nth_Abs_fls_ex_lower_bound) |
|
302 obtain K::int where K: "\<forall>n<K. f$$n = 0" by (elim fls_nth_vanishes_belowE) |
|
303 hence "\<forall>n<K-m. f$$(n+m) = 0" by auto |
|
304 thus "\<exists>N. \<forall>n<N. f $$ (n + m) = 0" by fast |
|
305 qed |
|
306 |
|
307 lemma fls_shift_eq_iff: "(fls_shift m f = fls_shift m g) \<longleftrightarrow> (f = g)" |
|
308 proof (rule iffI, rule fls_eqI) |
|
309 fix k |
|
310 assume 1: "fls_shift m f = fls_shift m g" |
|
311 have "f $$ k = fls_shift m g $$ (k - m)" by (simp add: 1[symmetric]) |
|
312 thus "f $$ k = g $$ k" by simp |
|
313 qed (intro fls_eqI, simp) |
|
314 |
|
315 lemma fls_shift_0 [simp]: "fls_shift 0 f = f" |
|
316 by (intro fls_eqI) simp |
|
317 |
|
318 lemma fls_shift_subdegree [simp]: |
|
319 "f \<noteq> 0 \<Longrightarrow> fls_subdegree (fls_shift n f) = fls_subdegree f - n" |
|
320 by (intro fls_subdegree_eqI) simp_all |
|
321 |
|
322 lemma fls_shift_fls_shift [simp]: "fls_shift m (fls_shift k f) = fls_shift (k+m) f" |
|
323 by (intro fls_eqI) (simp add: algebra_simps) |
|
324 |
|
325 lemma fls_shift_fls_shift_reorder: |
|
326 "fls_shift m (fls_shift k f) = fls_shift k (fls_shift m f)" |
|
327 using fls_shift_fls_shift[of m k f] fls_shift_fls_shift[of k m f] by (simp add: add.commute) |
|
328 |
|
329 lemma fls_shift_zero [simp]: "fls_shift m 0 = 0" |
|
330 by (intro fls_zero_eqI) simp |
|
331 |
|
332 lemma fls_shift_eq0_iff: "fls_shift m f = 0 \<longleftrightarrow> f = 0" |
|
333 using fls_shift_eq_iff[of m f 0] by simp |
|
334 |
|
335 lemma fls_shift_nonneg_subdegree: "m \<le> fls_subdegree f \<Longrightarrow> fls_subdegree (fls_shift m f) \<ge> 0" |
|
336 by (cases "f=0") (auto intro: fls_subdegree_geI) |
|
337 |
|
338 lemma fls_shift_delta: |
|
339 "fls_shift m (Abs_fls (\<lambda>n. if n=a then b else 0)) = Abs_fls (\<lambda>n. if n=a-m then b else 0)" |
|
340 by (intro fls_eqI) simp |
|
341 |
|
342 lemma fls_shift_const: |
|
343 "fls_shift m (fls_const c) = Abs_fls (\<lambda>n. if n=-m then c else 0)" |
|
344 by (intro fls_eqI) simp |
|
345 |
|
346 lemma fls_shift_const_nth: |
|
347 "fls_shift m (fls_const c) $$ n = (if n=-m then c else 0)" |
|
348 by (simp add: fls_shift_const) |
|
349 |
|
350 lemma fls_X_conv_shift_1: "fls_X = fls_shift (-1) 1" |
|
351 by (intro fls_eqI) simp |
|
352 |
|
353 lemma fls_X_shift_to_one [simp]: "fls_shift 1 fls_X = 1" |
|
354 using fls_shift_fls_shift[of "-1" 1 1] by (simp add: fls_X_conv_shift_1) |
|
355 |
|
356 lemma fls_X_inv_conv_shift_1: "fls_X_inv = fls_shift 1 1" |
|
357 by (intro fls_eqI) simp |
|
358 |
|
359 lemma fls_X_inv_shift_to_one [simp]: "fls_shift (-1) fls_X_inv = 1" |
|
360 using fls_shift_fls_shift[of 1 "-1" 1] by (simp add: fls_X_inv_conv_shift_1) |
|
361 |
|
362 lemma fls_X_fls_X_inv_conv: |
|
363 "fls_X = fls_shift (-2) fls_X_inv" "fls_X_inv = fls_shift 2 fls_X" |
|
364 by (simp_all add: fls_X_conv_shift_1 fls_X_inv_conv_shift_1) |
|
365 |
|
366 |
|
367 subsubsection \<open>Base factor\<close> |
|
368 |
|
369 text \<open> |
|
370 Similarly to the @{const unit_factor} for formal power series, we can decompose a formal Laurent |
|
371 series as a power of the implied variable times a series of subdegree 0. |
|
372 (See lemma @{text "fls_base_factor_X_power_decompose"}.) |
|
373 But we will call this something other @{const unit_factor} |
|
374 because it will not satisfy assumption @{text "is_unit_unit_factor"} of |
|
375 @{class semidom_divide_unit_factor}. |
|
376 \<close> |
|
377 |
|
378 definition fls_base_factor :: "('a::zero) fls \<Rightarrow> 'a fls" |
|
379 where fls_base_factor_def[simp]: "fls_base_factor f = fls_shift (fls_subdegree f) f" |
|
380 |
|
381 lemma fls_base_factor_nth: "fls_base_factor f $$ n = f $$ (n + fls_subdegree f)" |
|
382 by simp |
|
383 |
|
384 lemma fls_base_factor_nonzero [simp]: "f \<noteq> 0 \<Longrightarrow> fls_base_factor f \<noteq> 0" |
|
385 using fls_nonzeroI[of "fls_base_factor f" 0] by simp |
|
386 |
|
387 lemma fls_base_factor_subdegree [simp]: "fls_subdegree (fls_base_factor f) = 0" |
|
388 by (cases "f=0") auto |
|
389 |
|
390 lemma fls_base_factor_base [simp]: |
|
391 "fls_base_factor f $$ fls_subdegree (fls_base_factor f) = f $$ fls_subdegree f" |
|
392 using fls_base_factor_subdegree[of f] by simp |
|
393 |
|
394 lemma fls_conv_base_factor_shift_subdegree: |
|
395 "f = fls_shift (-fls_subdegree f) (fls_base_factor f)" |
|
396 by simp |
|
397 |
|
398 lemma fls_base_factor_idem: |
|
399 "fls_base_factor (fls_base_factor (f::'a::zero fls)) = fls_base_factor f" |
|
400 using fls_base_factor_subdegree[of f] by simp |
|
401 |
|
402 lemma fls_base_factor_zero: "fls_base_factor (0::'a::zero fls) = 0" |
|
403 by simp |
|
404 |
|
405 lemma fls_base_factor_zero_iff: "fls_base_factor (f::'a::zero fls) = 0 \<longleftrightarrow> f = 0" |
|
406 proof |
|
407 have "fls_shift (-fls_subdegree f) (fls_shift (fls_subdegree f) f) = f" by simp |
|
408 thus "fls_base_factor f = 0 \<Longrightarrow> f=0" by simp |
|
409 qed simp |
|
410 |
|
411 lemma fls_base_factor_nth_0: "f \<noteq> 0 \<Longrightarrow> fls_base_factor f $$ 0 \<noteq> 0" |
|
412 by simp |
|
413 |
|
414 lemma fls_base_factor_one: "fls_base_factor (1::'a::{zero,one} fls) = 1" |
|
415 by simp |
|
416 |
|
417 lemma fls_base_factor_const: "fls_base_factor (fls_const c) = fls_const c" |
|
418 by simp |
|
419 |
|
420 lemma fls_base_factor_delta: |
|
421 "fls_base_factor (Abs_fls (\<lambda>n. if n=a then c else 0)) = fls_const c" |
|
422 by (cases "c=0") (auto intro: fls_eqI) |
|
423 |
|
424 lemma fls_base_factor_X: "fls_base_factor (fls_X::'a::{zero_neq_one} fls) = 1" |
|
425 by simp |
|
426 |
|
427 lemma fls_base_factor_X_inv: "fls_base_factor (fls_X_inv::'a::{zero_neq_one} fls) = 1" |
|
428 by simp |
|
429 |
|
430 lemma fls_base_factor_shift [simp]: "fls_base_factor (fls_shift n f) = fls_base_factor f" |
|
431 by (cases "f=0") simp_all |
|
432 |
|
433 |
|
434 subsection \<open>Conversion between formal power and Laurent series\<close> |
|
435 |
|
436 subsubsection \<open>Converting Laurent to power series\<close> |
|
437 |
|
438 text \<open> |
|
439 We can truncate a Laurent series at index 0 to create a power series, called the regular part. |
|
440 \<close> |
|
441 |
|
442 lift_definition fls_regpart :: "('a::zero) fls \<Rightarrow> 'a fps" |
|
443 is "\<lambda>f. Abs_fps (\<lambda>n. f (int n))" |
|
444 . |
|
445 |
|
446 lemma fls_regpart_nth [simp]: "fls_regpart f $ n = f $$ (int n)" |
|
447 by (simp add: fls_regpart_def) |
|
448 |
|
449 lemma fls_regpart_zero [simp]: "fls_regpart 0 = 0" |
|
450 by (intro fps_ext) simp |
|
451 |
|
452 lemma fls_regpart_one [simp]: "fls_regpart 1 = 1" |
|
453 by (intro fps_ext) simp |
|
454 |
|
455 lemma fls_regpart_Abs_fls: |
|
456 "\<forall>\<^sub>\<infinity>n. F (- int n) = 0 \<Longrightarrow> fls_regpart (Abs_fls F) = Abs_fps (\<lambda>n. F (int n))" |
|
457 by (intro fps_ext) auto |
|
458 |
|
459 lemma fls_regpart_delta: |
|
460 "fls_regpart (Abs_fls (\<lambda>n. if n=a then b else 0)) = |
|
461 (if a < 0 then 0 else Abs_fps (\<lambda>n. if n=nat a then b else 0))" |
|
462 by (rule fps_ext, auto) |
|
463 |
|
464 lemma fls_regpart_const [simp]: "fls_regpart (fls_const c) = fps_const c" |
|
465 by (intro fps_ext) simp |
|
466 |
|
467 lemma fls_regpart_fls_X [simp]: "fls_regpart fls_X = fps_X" |
|
468 by (intro fps_ext) simp |
|
469 |
|
470 lemma fls_regpart_fls_X_inv [simp]: "fls_regpart fls_X_inv = 0" |
|
471 by (intro fps_ext) simp |
|
472 |
|
473 lemma fls_regpart_eq0_imp_nonpos_subdegree: |
|
474 assumes "fls_regpart f = 0" |
|
475 shows "fls_subdegree f \<le> 0" |
|
476 proof (cases "f=0") |
|
477 case False |
|
478 have "fls_subdegree f \<ge> 0 \<Longrightarrow> f $$ fls_subdegree f = 0" |
|
479 proof- |
|
480 assume "fls_subdegree f \<ge> 0" |
|
481 hence "f $$ (fls_subdegree f) = (fls_regpart f) $ (nat (fls_subdegree f))" by simp |
|
482 with assms show "f $$ (fls_subdegree f) = 0" by simp |
|
483 qed |
|
484 with False show ?thesis by fastforce |
|
485 qed simp |
|
486 |
|
487 lemma fls_subdegree_lt_fls_regpart_subdegree: |
|
488 "fls_subdegree f \<le> int (subdegree (fls_regpart f))" |
|
489 using fls_subdegree_leI nth_subdegree_nonzero[of "fls_regpart f"] |
|
490 by (cases "(fls_regpart f) = 0") |
|
491 (simp_all add: fls_regpart_eq0_imp_nonpos_subdegree) |
|
492 |
|
493 lemma fls_regpart_subdegree_conv: |
|
494 assumes "fls_subdegree f \<ge> 0" |
|
495 shows "subdegree (fls_regpart f) = nat (fls_subdegree f)" |
|
496 \<comment>\<open> |
|
497 This is the best we can do since if the subdegree is negative, we might still have the bad luck |
|
498 that the term at index 0 is equal to 0. |
|
499 \<close> |
|
500 proof (cases "f=0") |
|
501 case False with assms show ?thesis by (intro subdegreeI) simp_all |
|
502 qed simp |
|
503 |
|
504 lemma fls_eq_conv_fps_eqI: |
|
505 assumes "0 \<le> fls_subdegree f" "0 \<le> fls_subdegree g" "fls_regpart f = fls_regpart g" |
|
506 shows "f = g" |
|
507 proof (rule fls_eq_above_subdegreeI, rule assms(1), rule assms(2), clarify) |
|
508 fix k::int assume "0 \<le> k" |
|
509 with assms(3) show "f $$ k = g $$ k" |
|
510 using fls_regpart_nth[of f "nat k"] fls_regpart_nth[of g] by simp |
|
511 qed |
|
512 |
|
513 lemma fls_regpart_shift_conv_fps_shift: |
|
514 "m \<ge> 0 \<Longrightarrow> fls_regpart (fls_shift m f) = fps_shift (nat m) (fls_regpart f)" |
|
515 by (intro fps_ext) simp_all |
|
516 |
|
517 lemma fps_shift_fls_regpart_conv_fls_shift: |
|
518 "fps_shift m (fls_regpart f) = fls_regpart (fls_shift m f)" |
|
519 by (intro fps_ext) simp_all |
|
520 |
|
521 lemma fps_unit_factor_fls_regpart: |
|
522 "fls_subdegree f \<ge> 0 \<Longrightarrow> unit_factor (fls_regpart f) = fls_regpart (fls_base_factor f)" |
|
523 by (auto intro: fps_ext simp: fls_regpart_subdegree_conv) |
|
524 |
|
525 text \<open> |
|
526 The terms below the zeroth form a polynomial in the inverse of the implied variable, |
|
527 called the principle part. |
|
528 \<close> |
|
529 |
|
530 lift_definition fls_prpart :: "('a::zero) fls \<Rightarrow> 'a poly" |
|
531 is "\<lambda>f. Abs_poly (\<lambda>n. if n = 0 then 0 else f (- int n))" |
|
532 . |
|
533 |
|
534 lemma fls_prpart_coeff [simp]: "coeff (fls_prpart f) n = (if n = 0 then 0 else f $$ (- int n))" |
|
535 proof- |
|
536 have "{x. (if x = 0 then 0 else f $$ - int x) \<noteq> 0} \<subseteq> {x. f $$ - int x \<noteq> 0}" |
|
537 by auto |
|
538 hence "finite {x. (if x = 0 then 0 else f $$ - int x) \<noteq> 0}" |
|
539 using fls_finite_nonzero_neg_nth[of f] by (simp add: rev_finite_subset) |
|
540 hence "coeff (fls_prpart f) = (\<lambda>n. if n = 0 then 0 else f $$ (- int n))" |
|
541 using Abs_poly_inverse[OF CollectI, OF iffD2, OF eventually_cofinite] |
|
542 by (simp add: fls_prpart_def) |
|
543 thus ?thesis by simp |
|
544 qed |
|
545 |
|
546 lemma fls_prpart_eq0_iff: "(fls_prpart f = 0) \<longleftrightarrow> (fls_subdegree f \<ge> 0)" |
|
547 proof |
|
548 assume 1: "fls_prpart f = 0" |
|
549 show "fls_subdegree f \<ge> 0" |
|
550 proof (intro fls_subdegree_ge0I) |
|
551 fix k::int assume "k < 0" |
|
552 with 1 show "f $$ k = 0" using fls_prpart_coeff[of f "nat (-k)"] by simp |
|
553 qed |
|
554 qed (intro poly_eqI, simp) |
|
555 |
|
556 lemma fls_prpart0 [simp]: "fls_prpart 0 = 0" |
|
557 by (simp add: fls_prpart_eq0_iff) |
|
558 |
|
559 lemma fls_prpart_one [simp]: "fls_prpart 1 = 0" |
|
560 by (simp add: fls_prpart_eq0_iff) |
|
561 |
|
562 lemma fls_prpart_delta: |
|
563 "fls_prpart (Abs_fls (\<lambda>n. if n=a then b else 0)) = |
|
564 (if a<0 then Poly (replicate (nat (-a)) 0 @ [b]) else 0)" |
|
565 by (intro poly_eqI) (auto simp: nth_default_def nth_append) |
|
566 |
|
567 lemma fls_prpart_const [simp]: "fls_prpart (fls_const c) = 0" |
|
568 by (simp add: fls_prpart_eq0_iff) |
|
569 |
|
570 lemma fls_prpart_X [simp]: "fls_prpart fls_X = 0" |
|
571 by (intro poly_eqI) simp |
|
572 |
|
573 lemma fls_prpart_X_inv: "fls_prpart fls_X_inv = [:0,1:]" |
|
574 proof (intro poly_eqI) |
|
575 fix n show "coeff (fls_prpart fls_X_inv) n = coeff [:0,1:] n" |
|
576 proof (cases n) |
|
577 case (Suc i) thus ?thesis by (cases i) simp_all |
|
578 qed simp |
|
579 qed |
|
580 |
|
581 lemma degree_fls_prpart [simp]: |
|
582 "degree (fls_prpart f) = nat (-fls_subdegree f)" |
|
583 proof (cases "f=0") |
|
584 case False show ?thesis unfolding degree_def |
|
585 proof (intro Least_equality) |
|
586 fix N assume N: "\<forall>i>N. coeff (fls_prpart f) i = 0" |
|
587 have "\<forall>i < -int N. f $$ i = 0" |
|
588 proof clarify |
|
589 fix i assume i: "i < -int N" |
|
590 hence "nat (-i) > N" by simp |
|
591 with N i show "f $$ i = 0" using fls_prpart_coeff[of f "nat (-i)"] by auto |
|
592 qed |
|
593 with False have "fls_subdegree f \<ge> -int N" using fls_subdegree_geI by auto |
|
594 thus "nat (- fls_subdegree f) \<le> N" by simp |
|
595 qed auto |
|
596 qed simp |
|
597 |
|
598 lemma fls_prpart_shift: |
|
599 assumes "m \<le> 0" |
|
600 shows "fls_prpart (fls_shift m f) = pCons 0 (poly_shift (Suc (nat (-m))) (fls_prpart f))" |
|
601 proof (intro poly_eqI) |
|
602 fix n |
|
603 define LHS RHS |
|
604 where "LHS \<equiv> fls_prpart (fls_shift m f)" |
|
605 and "RHS \<equiv> pCons 0 (poly_shift (Suc (nat (-m))) (fls_prpart f))" |
|
606 show "coeff LHS n = coeff RHS n" |
|
607 proof (cases n) |
|
608 case (Suc k) |
|
609 from assms have 1: "-int (Suc k + nat (-m)) = -int (Suc k) + m" by simp |
|
610 have "coeff RHS n = f $$ (-int (Suc k) + m)" |
|
611 using arg_cong[OF 1, of "($$) f"] by (simp add: Suc RHS_def coeff_poly_shift) |
|
612 with Suc show ?thesis by (simp add: LHS_def) |
|
613 qed (simp add: LHS_def RHS_def) |
|
614 qed |
|
615 |
|
616 lemma fls_prpart_base_factor: "fls_prpart (fls_base_factor f) = 0" |
|
617 using fls_base_factor_subdegree[of f] by (simp add: fls_prpart_eq0_iff) |
|
618 |
|
619 text \<open>The essential data of a formal Laurant series resides from the subdegree up.\<close> |
|
620 |
|
621 abbreviation fls_base_factor_to_fps :: "('a::zero) fls \<Rightarrow> 'a fps" |
|
622 where "fls_base_factor_to_fps f \<equiv> fls_regpart (fls_base_factor f)" |
|
623 |
|
624 lemma fls_base_factor_to_fps_conv_fps_shift: |
|
625 assumes "fls_subdegree f \<ge> 0" |
|
626 shows "fls_base_factor_to_fps f = fps_shift (nat (fls_subdegree f)) (fls_regpart f)" |
|
627 by (simp add: assms fls_regpart_shift_conv_fps_shift) |
|
628 |
|
629 lemma fls_base_factor_to_fps_nth: |
|
630 "fls_base_factor_to_fps f $ n = f $$ (fls_subdegree f + int n)" |
|
631 by (simp add: algebra_simps) |
|
632 |
|
633 lemma fls_base_factor_to_fps_base: "f \<noteq> 0 \<Longrightarrow> fls_base_factor_to_fps f $ 0 \<noteq> 0" |
|
634 by simp |
|
635 |
|
636 lemma fls_base_factor_to_fps_nonzero: "f \<noteq> 0 \<Longrightarrow> fls_base_factor_to_fps f \<noteq> 0" |
|
637 using fps_nonzeroI[of "fls_base_factor_to_fps f" 0] fls_base_factor_to_fps_base by simp |
|
638 |
|
639 lemma fls_base_factor_to_fps_subdegree [simp]: "subdegree (fls_base_factor_to_fps f) = 0" |
|
640 by (cases "f=0") auto |
|
641 |
|
642 lemma fls_base_factor_to_fps_trivial: |
|
643 "fls_subdegree f = 0 \<Longrightarrow> fls_base_factor_to_fps f = fls_regpart f" |
|
644 by simp |
|
645 |
|
646 lemma fls_base_factor_to_fps_zero: "fls_base_factor_to_fps 0 = 0" |
|
647 by simp |
|
648 |
|
649 lemma fls_base_factor_to_fps_one: "fls_base_factor_to_fps 1 = 1" |
|
650 by simp |
|
651 |
|
652 lemma fls_base_factor_to_fps_delta: |
|
653 "fls_base_factor_to_fps (Abs_fls (\<lambda>n. if n=a then c else 0)) = fps_const c" |
|
654 using fls_base_factor_delta[of a c] by simp |
|
655 |
|
656 lemma fls_base_factor_to_fps_const: |
|
657 "fls_base_factor_to_fps (fls_const c) = fps_const c" |
|
658 by simp |
|
659 |
|
660 lemma fls_base_factor_to_fps_X: |
|
661 "fls_base_factor_to_fps (fls_X::'a::{zero_neq_one} fls) = 1" |
|
662 by simp |
|
663 |
|
664 lemma fls_base_factor_to_fps_X_inv: |
|
665 "fls_base_factor_to_fps (fls_X_inv::'a::{zero_neq_one} fls) = 1" |
|
666 by simp |
|
667 |
|
668 lemma fls_base_factor_to_fps_shift: |
|
669 "fls_base_factor_to_fps (fls_shift m f) = fls_base_factor_to_fps f" |
|
670 using fls_base_factor_shift[of m f] by simp |
|
671 |
|
672 lemma fls_base_factor_to_fps_base_factor: |
|
673 "fls_base_factor_to_fps (fls_base_factor f) = fls_base_factor_to_fps f" |
|
674 using fls_base_factor_to_fps_shift by simp |
|
675 |
|
676 lemma fps_unit_factor_fls_base_factor: |
|
677 "unit_factor (fls_base_factor_to_fps f) = fls_base_factor_to_fps f" |
|
678 using fls_base_factor_to_fps_subdegree[of f] by simp |
|
679 |
|
680 subsubsection \<open>Converting power to Laurent series\<close> |
|
681 |
|
682 text \<open>We can extend a power series by 0s below to create a Laurent series.\<close> |
|
683 |
|
684 definition fps_to_fls :: "('a::zero) fps \<Rightarrow> 'a fls" |
|
685 where "fps_to_fls f \<equiv> Abs_fls (\<lambda>k::int. if k<0 then 0 else f $ (nat k))" |
|
686 |
|
687 lemma fps_to_fls_nth [simp]: |
|
688 "(fps_to_fls f) $$ n = (if n < 0 then 0 else f$(nat n))" |
|
689 using nth_Abs_fls_lower_bound[of 0 "(\<lambda>k::int. if k<0 then 0 else f $ (nat k))"] |
|
690 unfolding fps_to_fls_def |
|
691 by simp |
|
692 |
|
693 lemma fps_to_fls_eq_imp_fps_eq: |
|
694 assumes "fps_to_fls f = fps_to_fls g" |
|
695 shows "f = g" |
|
696 proof (intro fps_ext) |
|
697 fix n |
|
698 have "f $ n = fps_to_fls g $$ int n" by (simp add: assms[symmetric]) |
|
699 thus "f $ n = g $ n" by simp |
|
700 qed |
|
701 |
|
702 lemma fps_zero_to_fls [simp]: "fps_to_fls 0 = 0" |
|
703 by (intro fls_zero_eqI) simp |
|
704 |
|
705 lemma fps_to_fls_nonzeroI: "f \<noteq> 0 \<Longrightarrow> fps_to_fls f \<noteq> 0" |
|
706 using fps_to_fls_eq_imp_fps_eq[of f 0] by auto |
|
707 |
|
708 lemma fps_one_to_fls [simp]: "fps_to_fls 1 = 1" |
|
709 by (intro fls_eqI) simp |
|
710 |
|
711 lemma fps_to_fls_Abs_fps: |
|
712 "fps_to_fls (Abs_fps F) = Abs_fls (\<lambda>n. if n<0 then 0 else F (nat n))" |
|
713 using nth_Abs_fls_lower_bound[of 0 "(\<lambda>n::int. if n<0 then 0 else F (nat n))"] |
|
714 by (intro fls_eqI) simp |
|
715 |
|
716 lemma fps_delta_to_fls: |
|
717 "fps_to_fls (Abs_fps (\<lambda>n. if n=a then b else 0)) = Abs_fls (\<lambda>n. if n=int a then b else 0)" |
|
718 using fls_eqI[of _ "Abs_fls (\<lambda>n. if n=int a then b else 0)"] by force |
|
719 |
|
720 lemma fps_const_to_fls [simp]: "fps_to_fls (fps_const c) = fls_const c" |
|
721 by (intro fls_eqI) simp |
|
722 |
|
723 lemma fps_X_to_fls [simp]: "fps_to_fls fps_X = fls_X" |
|
724 by (fastforce intro: fls_eqI) |
|
725 |
|
726 lemma fps_to_fls_eq_zero_iff: "(fps_to_fls f = 0) \<longleftrightarrow> (f=0)" |
|
727 using fps_to_fls_nonzeroI by auto |
|
728 |
|
729 lemma fls_subdegree_fls_to_fps_gt0: "fls_subdegree (fps_to_fls f) \<ge> 0" |
|
730 proof (cases "f=0") |
|
731 case False show ?thesis |
|
732 proof (rule fls_subdegree_geI, rule fls_nonzeroI) |
|
733 from False show "fps_to_fls f $$ int (subdegree f) \<noteq> 0" |
|
734 by simp |
|
735 qed simp |
|
736 qed simp |
|
737 |
|
738 lemma fls_subdegree_fls_to_fps: "fls_subdegree (fps_to_fls f) = int (subdegree f)" |
|
739 proof (cases "f=0") |
|
740 case False |
|
741 have "subdegree f = nat (fls_subdegree (fps_to_fls f))" |
|
742 proof (rule subdegreeI) |
|
743 from False show "f $ (nat (fls_subdegree (fps_to_fls f))) \<noteq> 0" |
|
744 using fls_subdegree_fls_to_fps_gt0[of f] nth_fls_subdegree_nonzero[of "fps_to_fls f"] |
|
745 fps_to_fls_nonzeroI[of f] |
|
746 by simp |
|
747 next |
|
748 fix k assume k: "k < nat (fls_subdegree (fps_to_fls f))" |
|
749 thus "f $ k = 0" |
|
750 using fls_eq0_below_subdegree[of "int k" "fps_to_fls f"] by simp |
|
751 qed |
|
752 thus ?thesis by (simp add: fls_subdegree_fls_to_fps_gt0) |
|
753 qed simp |
|
754 |
|
755 lemma fps_shift_to_fls [simp]: |
|
756 "n \<le> subdegree f \<Longrightarrow> fps_to_fls (fps_shift n f) = fls_shift (int n) (fps_to_fls f)" |
|
757 by (auto intro: fls_eqI simp: nat_add_distrib nth_less_subdegree_zero) |
|
758 |
|
759 lemma fls_base_factor_fps_to_fls: "fls_base_factor (fps_to_fls f) = fps_to_fls (unit_factor f)" |
|
760 using nth_less_subdegree_zero[of _ f] |
|
761 by (auto intro: fls_eqI simp: fls_subdegree_fls_to_fps nat_add_distrib) |
|
762 |
|
763 lemma fls_regpart_to_fls_trivial [simp]: |
|
764 "fls_subdegree f \<ge> 0 \<Longrightarrow> fps_to_fls (fls_regpart f) = f" |
|
765 by (intro fls_eqI) simp |
|
766 |
|
767 lemma fls_regpart_fps_trivial [simp]: "fls_regpart (fps_to_fls f) = f" |
|
768 by (intro fps_ext) simp |
|
769 |
|
770 lemma fps_to_fls_base_factor_to_fps: |
|
771 "fps_to_fls (fls_base_factor_to_fps f) = fls_base_factor f" |
|
772 by (intro fls_eqI) simp |
|
773 |
|
774 lemma fls_conv_base_factor_to_fps_shift_subdegree: |
|
775 "f = fls_shift (-fls_subdegree f) (fps_to_fls (fls_base_factor_to_fps f))" |
|
776 using fps_to_fls_base_factor_to_fps[of f] fps_to_fls_base_factor_to_fps[of f] by simp |
|
777 |
|
778 lemma fls_base_factor_to_fps_to_fls: |
|
779 "fls_base_factor_to_fps (fps_to_fls f) = unit_factor f" |
|
780 using fls_base_factor_fps_to_fls[of f] fls_regpart_fps_trivial[of "unit_factor f"] |
|
781 by simp |
|
782 |
|
783 abbreviation |
|
784 "fls_regpart_as_fls f \<equiv> fps_to_fls (fls_regpart f)" |
|
785 abbreviation |
|
786 "fls_prpart_as_fls f \<equiv> |
|
787 fls_shift (-fls_subdegree f) (fps_to_fls (fps_of_poly (reflect_poly (fls_prpart f))))" |
|
788 |
|
789 lemma fls_regpart_as_fls_nth: |
|
790 "fls_regpart_as_fls f $$ n = (if n < 0 then 0 else f $$ n)" |
|
791 by simp |
|
792 |
|
793 lemma fls_regpart_idem: |
|
794 "fls_regpart (fls_regpart_as_fls f) = fls_regpart f" |
|
795 by simp |
|
796 |
|
797 lemma fls_prpart_as_fls_nth: |
|
798 "fls_prpart_as_fls f $$ n = (if n < 0 then f $$ n else 0)" |
|
799 proof (cases "n < fls_subdegree f" "n < 0" rule: case_split[case_product case_split]) |
|
800 case False_True |
|
801 hence "nat (-fls_subdegree f) - nat (n - fls_subdegree f) = nat (-n)" by auto |
|
802 with False_True show ?thesis |
|
803 using coeff_reflect_poly[of "fls_prpart f" "nat (n - fls_subdegree f)"] by auto |
|
804 next |
|
805 case False_False thus ?thesis |
|
806 using coeff_reflect_poly[of "fls_prpart f" "nat (n - fls_subdegree f)"] by auto |
|
807 qed simp_all |
|
808 |
|
809 lemma fls_prpart_idem [simp]: "fls_prpart (fls_prpart_as_fls f) = fls_prpart f" |
|
810 using fls_prpart_as_fls_nth[of f] by (intro poly_eqI) simp |
|
811 |
|
812 lemma fls_regpart_prpart: "fls_regpart (fls_prpart_as_fls f) = 0" |
|
813 using fls_prpart_as_fls_nth[of f] by (intro fps_ext) simp |
|
814 |
|
815 lemma fls_prpart_regpart: "fls_prpart (fls_regpart_as_fls f) = 0" |
|
816 by (intro poly_eqI) simp |
|
817 |
|
818 |
|
819 subsection \<open>Algebraic structures\<close> |
|
820 |
|
821 subsubsection \<open>Addition\<close> |
|
822 |
|
823 instantiation fls :: (monoid_add) plus |
|
824 begin |
|
825 lift_definition plus_fls :: "'a fls \<Rightarrow> 'a fls \<Rightarrow> 'a fls" is "\<lambda>f g n. f n + g n" |
|
826 proof- |
|
827 fix f f' :: "int \<Rightarrow> 'a" |
|
828 assume "\<forall>\<^sub>\<infinity>n. f (- int n) = 0" "\<forall>\<^sub>\<infinity>n. f' (- int n) = 0" |
|
829 from this obtain N N' where "\<forall>n>N. f (-int n) = 0" "\<forall>n>N'. f' (-int n) = 0" |
|
830 by (auto simp: MOST_nat) |
|
831 hence "\<forall>n > max N N'. f (-int n) + f' (-int n) = 0" by auto |
|
832 hence "\<exists>K. \<forall>n>K. f (-int n) + f' (-int n) = 0" by fast |
|
833 thus "\<forall>\<^sub>\<infinity>n. f (- int n) + f' (-int n) = 0" by (simp add: MOST_nat) |
|
834 qed |
|
835 instance .. |
|
836 end |
|
837 |
|
838 lemma fls_plus_nth [simp]: "(f + g) $$ n = f $$ n + g $$ n" |
|
839 by transfer simp |
|
840 |
|
841 lemma fls_plus_const: "fls_const x + fls_const y = fls_const (x+y)" |
|
842 by (intro fls_eqI) simp |
|
843 |
|
844 lemma fls_plus_subdegree: |
|
845 "f + g \<noteq> 0 \<Longrightarrow> fls_subdegree (f + g) \<ge> min (fls_subdegree f) (fls_subdegree g)" |
|
846 by (auto intro: fls_subdegree_geI) |
|
847 |
|
848 lemma fls_shift_plus [simp]: |
|
849 "fls_shift m (f + g) = (fls_shift m f) + (fls_shift m g)" |
|
850 by (intro fls_eqI) simp |
|
851 |
|
852 lemma fls_regpart_plus [simp]: "fls_regpart (f + g) = fls_regpart f + fls_regpart g" |
|
853 by (intro fps_ext) simp |
|
854 |
|
855 lemma fls_prpart_plus [simp] : "fls_prpart (f + g) = fls_prpart f + fls_prpart g" |
|
856 by (intro poly_eqI) simp |
|
857 |
|
858 lemma fls_decompose_reg_pr_parts: |
|
859 fixes f :: "'a :: monoid_add fls" |
|
860 defines "R \<equiv> fls_regpart_as_fls f" |
|
861 and "P \<equiv> fls_prpart_as_fls f" |
|
862 shows "f = P + R" |
|
863 and "f = R + P" |
|
864 using fls_prpart_as_fls_nth[of f] |
|
865 by (auto intro: fls_eqI simp add: assms) |
|
866 |
|
867 lemma fps_to_fls_plus [simp]: "fps_to_fls (f + g) = fps_to_fls f + fps_to_fls g" |
|
868 by (intro fls_eqI) simp |
|
869 |
|
870 instance fls :: (monoid_add) monoid_add |
|
871 proof |
|
872 fix a b c :: "'a fls" |
|
873 show "a + b + c = a + (b + c)" by transfer (simp add: add.assoc) |
|
874 show "0 + a = a" by transfer simp |
|
875 show "a + 0 = a" by transfer simp |
|
876 qed |
|
877 |
|
878 instance fls :: (comm_monoid_add) comm_monoid_add |
|
879 by (standard, transfer, auto simp: add.commute) |
|
880 |
|
881 |
|
882 subsubsection \<open>Subtraction and negatives\<close> |
|
883 |
|
884 instantiation fls :: (group_add) minus |
|
885 begin |
|
886 lift_definition minus_fls :: "'a fls \<Rightarrow> 'a fls \<Rightarrow> 'a fls" is "\<lambda>f g n. f n - g n" |
|
887 proof- |
|
888 fix f f' :: "int \<Rightarrow> 'a" |
|
889 assume "\<forall>\<^sub>\<infinity>n. f (- int n) = 0" "\<forall>\<^sub>\<infinity>n. f' (- int n) = 0" |
|
890 from this obtain N N' where "\<forall>n>N. f (-int n) = 0" "\<forall>n>N'. f' (-int n) = 0" |
|
891 by (auto simp: MOST_nat) |
|
892 hence "\<forall>n > max N N'. f (-int n) - f' (-int n) = 0" by auto |
|
893 hence "\<exists>K. \<forall>n>K. f (-int n) - f' (-int n) = 0" by fast |
|
894 thus "\<forall>\<^sub>\<infinity>n. f (- int n) - f' (-int n) = 0" by (simp add: MOST_nat) |
|
895 qed |
|
896 instance .. |
|
897 end |
|
898 |
|
899 lemma fls_minus_nth [simp]: "(f - g) $$ n = f $$ n - g $$ n" |
|
900 by transfer simp |
|
901 |
|
902 lemma fls_minus_const: "fls_const x - fls_const y = fls_const (x-y)" |
|
903 by (intro fls_eqI) simp |
|
904 |
|
905 lemma fls_subdegree_minus: |
|
906 "f - g \<noteq> 0 \<Longrightarrow> fls_subdegree (f - g) \<ge> min (fls_subdegree f) (fls_subdegree g)" |
|
907 by (intro fls_subdegree_geI) simp_all |
|
908 |
|
909 lemma fls_shift_minus [simp]: "fls_shift m (f - g) = (fls_shift m f) - (fls_shift m g)" |
|
910 by (auto intro: fls_eqI) |
|
911 |
|
912 lemma fls_regpart_minus [simp]: "fls_regpart (f - g) = fls_regpart f - fls_regpart g" |
|
913 by (intro fps_ext) simp |
|
914 |
|
915 lemma fls_prpart_minus [simp] : "fls_prpart (f - g) = fls_prpart f - fls_prpart g" |
|
916 by (intro poly_eqI) simp |
|
917 |
|
918 lemma fps_to_fls_minus [simp]: "fps_to_fls (f - g) = fps_to_fls f - fps_to_fls g" |
|
919 by (intro fls_eqI) simp |
|
920 |
|
921 instantiation fls :: (group_add) uminus |
|
922 begin |
|
923 lift_definition uminus_fls :: "'a fls \<Rightarrow> 'a fls" is "\<lambda>f n. - f n" |
|
924 proof- |
|
925 fix f :: "int \<Rightarrow> 'a" assume "\<forall>\<^sub>\<infinity>n. f (- int n) = 0" |
|
926 from this obtain N where "\<forall>n>N. f (-int n) = 0" |
|
927 by (auto simp: MOST_nat) |
|
928 hence "\<forall>n>N. - f (-int n) = 0" by auto |
|
929 hence "\<exists>K. \<forall>n>K. - f (-int n) = 0" by fast |
|
930 thus "\<forall>\<^sub>\<infinity>n. - f (- int n) = 0" by (simp add: MOST_nat) |
|
931 qed |
|
932 instance .. |
|
933 end |
|
934 |
|
935 lemma fls_uminus_nth [simp]: "(-f) $$ n = - (f $$ n)" |
|
936 by transfer simp |
|
937 |
|
938 lemma fls_const_uminus[simp]: "fls_const (-x) = -fls_const x" |
|
939 by (intro fls_eqI) simp |
|
940 |
|
941 lemma fls_shift_uminus [simp]: "fls_shift m (- f) = - (fls_shift m f)" |
|
942 by (auto intro: fls_eqI) |
|
943 |
|
944 lemma fls_regpart_uminus [simp]: "fls_regpart (- f) = - fls_regpart f" |
|
945 by (intro fps_ext) simp |
|
946 |
|
947 lemma fls_prpart_uminus [simp] : "fls_prpart (- f) = - fls_prpart f" |
|
948 by (intro poly_eqI) simp |
|
949 |
|
950 lemma fps_to_fls_uminus [simp]: "fps_to_fls (- f) = - fps_to_fls f" |
|
951 by (intro fls_eqI) simp |
|
952 |
|
953 instance fls :: (group_add) group_add |
|
954 proof |
|
955 fix a b :: "'a fls" |
|
956 show "- a + a = 0" by transfer simp |
|
957 show "a + - b = a - b" by transfer simp |
|
958 qed |
|
959 |
|
960 instance fls :: (ab_group_add) ab_group_add |
|
961 proof |
|
962 fix a b :: "'a fls" |
|
963 show "- a + a = 0" by transfer simp |
|
964 show "a - b = a + - b" by transfer simp |
|
965 qed |
|
966 |
|
967 lemma fls_uminus_subdegree [simp]: "fls_subdegree (-f) = fls_subdegree f" |
|
968 by (cases "f=0") (auto intro: fls_subdegree_eqI) |
|
969 |
|
970 lemma fls_subdegree_minus_sym: "fls_subdegree (g - f) = fls_subdegree (f - g)" |
|
971 using fls_uminus_subdegree[of "g-f"] by (simp add: algebra_simps) |
|
972 |
|
973 lemma fls_regpart_sub_prpart: "fls_regpart (f - fls_prpart_as_fls f) = fls_regpart f" |
|
974 using fls_decompose_reg_pr_parts(2)[of f] |
|
975 add_diff_cancel[of "fls_regpart_as_fls f" "fls_prpart_as_fls f"] |
|
976 by simp |
|
977 |
|
978 lemma fls_prpart_sub_regpart: "fls_prpart (f - fls_regpart_as_fls f) = fls_prpart f" |
|
979 using fls_decompose_reg_pr_parts(1)[of f] |
|
980 add_diff_cancel[of "fls_prpart_as_fls f" "fls_regpart_as_fls f"] |
|
981 by simp |
|
982 |
|
983 |
|
984 subsubsection \<open>Multiplication\<close> |
|
985 |
|
986 instantiation fls :: ("{comm_monoid_add, times}") times |
|
987 begin |
|
988 definition fls_times_def: |
|
989 "(*) = (\<lambda>f g. |
|
990 fls_shift |
|
991 (- (fls_subdegree f + fls_subdegree g)) |
|
992 (fps_to_fls (fls_base_factor_to_fps f * fls_base_factor_to_fps g)) |
|
993 )" |
|
994 instance .. |
|
995 end |
|
996 |
|
997 lemma fls_times_nth_eq0: "n < fls_subdegree f + fls_subdegree g \<Longrightarrow> (f * g) $$ n = 0" |
|
998 by (simp add: fls_times_def) |
|
999 |
|
1000 lemma fls_times_nth: |
|
1001 fixes f df g dg |
|
1002 defines "df \<equiv> fls_subdegree f" and "dg \<equiv> fls_subdegree g" |
|
1003 shows "(f * g) $$ n = (\<Sum>i=df + dg..n. f $$ (i - dg) * g $$ (dg + n - i))" |
|
1004 and "(f * g) $$ n = (\<Sum>i=df..n - dg. f $$ i * g $$ (n - i))" |
|
1005 and "(f * g) $$ n = (\<Sum>i=dg..n - df. f $$ (df + i - dg) * g $$ (dg + n - df - i))" |
|
1006 and "(f * g) $$ n = (\<Sum>i=0..n - (df + dg). f $$ (df + i) * g $$ (n - df - i))" |
|
1007 proof- |
|
1008 |
|
1009 define dfg where "dfg \<equiv> df + dg" |
|
1010 |
|
1011 show 4: "(f * g) $$ n = (\<Sum>i=0..n - dfg. f $$ (df + i) * g $$ (n - df - i))" |
|
1012 proof (cases "n < dfg") |
|
1013 case False |
|
1014 from False assms have |
|
1015 "(f * g) $$ n = |
|
1016 (\<Sum>i = 0..nat (n - dfg). f $$ (df + int i) * g $$ (dg + int (nat (n - dfg) - i)))" |
|
1017 using fps_mult_nth[of "fls_base_factor_to_fps f" "fls_base_factor_to_fps g"] |
|
1018 fls_base_factor_to_fps_nth[of f] |
|
1019 fls_base_factor_to_fps_nth[of g] |
|
1020 by (simp add: dfg_def fls_times_def algebra_simps) |
|
1021 moreover from False have index: |
|
1022 "\<And>i. i \<in> {0..nat (n - dfg)} \<Longrightarrow> dg + int (nat (n - dfg) - i) = n - df - int i" |
|
1023 by (auto simp: dfg_def) |
|
1024 ultimately have |
|
1025 "(f * g) $$ n = (\<Sum>i=0..nat (n - dfg). f $$ (df + int i) * g $$ (n - df - int i))" |
|
1026 by simp |
|
1027 moreover have |
|
1028 "(\<Sum>i=0..nat (n - dfg). f $$ (df + int i) * g $$ (n - df - int i)) = |
|
1029 (\<Sum>i=0..n - dfg. f $$ (df + i) * g $$ (n - df - i))" |
|
1030 proof (intro sum.reindex_cong) |
|
1031 show "inj_on nat {0..n - dfg}" by standard auto |
|
1032 show "{0..nat (n - dfg)} = nat ` {0..n - dfg}" |
|
1033 proof |
|
1034 show "{0..nat (n - dfg)} \<subseteq> nat ` {0..n - dfg}" |
|
1035 proof |
|
1036 fix i assume "i \<in> {0..nat (n - dfg)}" |
|
1037 hence i: "i \<ge> 0" "i \<le> nat (n - dfg)" by auto |
|
1038 with False have "int i \<ge> 0" "int i \<le> n - dfg" by auto |
|
1039 hence "int i \<in> {0..n - dfg}" by simp |
|
1040 moreover from i(1) have "i = nat (int i)" by simp |
|
1041 ultimately show "i \<in> nat ` {0..n - dfg}" by fast |
|
1042 qed |
|
1043 qed (auto simp: False) |
|
1044 qed (simp add: False) |
|
1045 ultimately show "(f * g) $$ n = (\<Sum>i=0..n - dfg. f $$ (df + i) * g $$ (n - df - i))" |
|
1046 by simp |
|
1047 qed (simp add: fls_times_nth_eq0 assms dfg_def) |
|
1048 |
|
1049 have |
|
1050 "(\<Sum>i=dfg..n. f $$ (i - dg) * g $$ (dg + n - i)) = |
|
1051 (\<Sum>i=0..n - dfg. f $$ (df + i) * g $$ (n - df - i))" |
|
1052 proof (intro sum.reindex_cong) |
|
1053 define T where "T \<equiv> \<lambda>i. i + dfg" |
|
1054 show "inj_on T {0..n - dfg}" by standard (simp add: T_def) |
|
1055 qed (simp_all add: dfg_def algebra_simps) |
|
1056 with 4 show 1: "(f * g) $$ n = (\<Sum>i=dfg..n. f $$ (i - dg) * g $$ (dg + n - i))" |
|
1057 by simp |
|
1058 |
|
1059 have |
|
1060 "(\<Sum>i=dfg..n. f $$ (i - dg) * g $$ (dg + n - i)) = (\<Sum>i=df..n - dg. f $$ i * g $$ (n - i))" |
|
1061 proof (intro sum.reindex_cong) |
|
1062 define T where "T \<equiv> \<lambda>i. i + dg" |
|
1063 show "inj_on T {df..n - dg}" by standard (simp add: T_def) |
|
1064 qed (auto simp: dfg_def) |
|
1065 with 1 show "(f * g) $$ n = (\<Sum>i=df..n - dg. f $$ i * g $$ (n - i))" |
|
1066 by simp |
|
1067 |
|
1068 have |
|
1069 "(\<Sum>i=dfg..n. f $$ (i - dg) * g $$ (dg + n - i)) = |
|
1070 (\<Sum>i=dg..n - df. f $$ (df + i - dg) * g $$ (dg + n - df - i))" |
|
1071 proof (intro sum.reindex_cong) |
|
1072 define T where "T \<equiv> \<lambda>i. i + df" |
|
1073 show "inj_on T {dg..n - df}" by standard (simp add: T_def) |
|
1074 qed (simp_all add: dfg_def algebra_simps) |
|
1075 with 1 show "(f * g) $$ n = (\<Sum>i=dg..n - df. f $$ (df + i - dg) * g $$ (dg + n - df - i))" |
|
1076 by simp |
|
1077 |
|
1078 qed |
|
1079 |
|
1080 lemma fls_times_base [simp]: |
|
1081 "(f * g) $$ (fls_subdegree f + fls_subdegree g) = |
|
1082 (f $$ fls_subdegree f) * (g $$ fls_subdegree g)" |
|
1083 by (simp add: fls_times_nth(1)) |
|
1084 |
|
1085 instance fls :: ("{comm_monoid_add, mult_zero}") mult_zero |
|
1086 proof |
|
1087 fix a :: "'a fls" |
|
1088 have |
|
1089 "(0::'a fls) * a = |
|
1090 fls_shift (fls_subdegree a) (fps_to_fls ( (0::'a fps)*(fls_base_factor_to_fps a) ))" |
|
1091 by (simp add: fls_times_def) |
|
1092 moreover have |
|
1093 "a * (0::'a fls) = |
|
1094 fls_shift (fls_subdegree a) (fps_to_fls ( (fls_base_factor_to_fps a)*(0::'a fps) ))" |
|
1095 by (simp add: fls_times_def) |
|
1096 ultimately show "0 * a = (0::'a fls)" "a * 0 = (0::'a fls)" |
|
1097 by auto |
|
1098 qed |
|
1099 |
|
1100 lemma fls_mult_one: |
|
1101 fixes f :: "'a::{comm_monoid_add, mult_zero, monoid_mult} fls" |
|
1102 shows "1 * f = f" |
|
1103 and "f * 1 = f" |
|
1104 using fls_conv_base_factor_to_fps_shift_subdegree[of f] |
|
1105 by (simp_all add: fls_times_def fps_one_mult) |
|
1106 |
|
1107 lemma fls_mult_const_nth [simp]: |
|
1108 fixes f :: "'a::{comm_monoid_add, mult_zero} fls" |
|
1109 shows "(fls_const x * f) $$ n = x * f$$n" |
|
1110 and "(f * fls_const x ) $$ n = f$$n * x" |
|
1111 proof- |
|
1112 show "(fls_const x * f) $$ n = x * f$$n" |
|
1113 proof (cases "n<fls_subdegree f") |
|
1114 case False |
|
1115 hence "{fls_subdegree f..n} = insert (fls_subdegree f) {fls_subdegree f+1..n}" by auto |
|
1116 thus ?thesis by (simp add: fls_times_nth(1)) |
|
1117 qed (simp add: fls_times_nth_eq0) |
|
1118 show "(f * fls_const x ) $$ n = f$$n * x" |
|
1119 proof (cases "n<fls_subdegree f") |
|
1120 case False |
|
1121 hence "{fls_subdegree f..n} = insert n {fls_subdegree f..n-1}" by auto |
|
1122 thus ?thesis by (simp add: fls_times_nth(1)) |
|
1123 qed (simp add: fls_times_nth_eq0) |
|
1124 qed |
|
1125 |
|
1126 lemma fls_const_mult_const[simp]: |
|
1127 fixes x y :: "'a::{comm_monoid_add, mult_zero}" |
|
1128 shows "fls_const x * fls_const y = fls_const (x*y)" |
|
1129 by (intro fls_eqI) simp |
|
1130 |
|
1131 lemma fls_mult_subdegree_ge: |
|
1132 fixes f g :: "'a::{comm_monoid_add,mult_zero} fls" |
|
1133 assumes "f*g \<noteq> 0" |
|
1134 shows "fls_subdegree (f*g) \<ge> fls_subdegree f + fls_subdegree g" |
|
1135 by (auto intro: fls_subdegree_geI simp: assms fls_times_nth_eq0) |
|
1136 |
|
1137 lemma fls_mult_subdegree_ge_0: |
|
1138 fixes f g :: "'a::{comm_monoid_add,mult_zero} fls" |
|
1139 assumes "fls_subdegree f \<ge> 0" "fls_subdegree g \<ge> 0" |
|
1140 shows "fls_subdegree (f*g) \<ge> 0" |
|
1141 using assms fls_mult_subdegree_ge[of f g] |
|
1142 by fastforce |
|
1143 |
|
1144 lemma fls_mult_nonzero_base_subdegree_eq: |
|
1145 fixes f g :: "'a::{comm_monoid_add,mult_zero} fls" |
|
1146 assumes "f $$ (fls_subdegree f) * g $$ (fls_subdegree g) \<noteq> 0" |
|
1147 shows "fls_subdegree (f*g) = fls_subdegree f + fls_subdegree g" |
|
1148 proof- |
|
1149 from assms have "fls_subdegree (f*g) \<ge> fls_subdegree f + fls_subdegree g" |
|
1150 using fls_nonzeroI[of "f*g" "fls_subdegree f + fls_subdegree g"] |
|
1151 fls_mult_subdegree_ge[of f g] |
|
1152 by simp |
|
1153 moreover from assms have "fls_subdegree (f*g) \<le> fls_subdegree f + fls_subdegree g" |
|
1154 by (intro fls_subdegree_leI) simp |
|
1155 ultimately show ?thesis by simp |
|
1156 qed |
|
1157 |
|
1158 lemma fls_subdegree_mult [simp]: |
|
1159 fixes f g :: "'a::semiring_no_zero_divisors fls" |
|
1160 assumes "f \<noteq> 0" "g \<noteq> 0" |
|
1161 shows "fls_subdegree (f * g) = fls_subdegree f + fls_subdegree g" |
|
1162 using assms |
|
1163 by (auto intro: fls_subdegree_eqI simp: fls_times_nth_eq0) |
|
1164 |
|
1165 lemma fls_shifted_times_simps: |
|
1166 fixes f g :: "'a::{comm_monoid_add, mult_zero} fls" |
|
1167 shows "f * (fls_shift n g) = fls_shift n (f*g)" "(fls_shift n f) * g = fls_shift n (f*g)" |
|
1168 proof- |
|
1169 |
|
1170 show "f * (fls_shift n g) = fls_shift n (f*g)" |
|
1171 proof (cases "g=0") |
|
1172 case False |
|
1173 hence |
|
1174 "f * (fls_shift n g) = |
|
1175 fls_shift (- (fls_subdegree f + (fls_subdegree g - n))) |
|
1176 (fps_to_fls (fls_base_factor_to_fps f * fls_base_factor_to_fps g))" |
|
1177 unfolding fls_times_def by (simp add: fls_base_factor_to_fps_shift) |
|
1178 thus "f * (fls_shift n g) = fls_shift n (f*g)" |
|
1179 by (simp add: algebra_simps fls_times_def) |
|
1180 qed auto |
|
1181 |
|
1182 show "(fls_shift n f)*g = fls_shift n (f*g)" |
|
1183 proof (cases "f=0") |
|
1184 case False |
|
1185 hence |
|
1186 "(fls_shift n f)*g = |
|
1187 fls_shift (- ((fls_subdegree f - n) + fls_subdegree g)) |
|
1188 (fps_to_fls (fls_base_factor_to_fps f * fls_base_factor_to_fps g))" |
|
1189 unfolding fls_times_def by (simp add: fls_base_factor_to_fps_shift) |
|
1190 thus "(fls_shift n f) * g = fls_shift n (f*g)" |
|
1191 by (simp add: algebra_simps fls_times_def) |
|
1192 qed auto |
|
1193 |
|
1194 qed |
|
1195 |
|
1196 lemma fls_shifted_times_transfer: |
|
1197 fixes f g :: "'a::{comm_monoid_add, mult_zero} fls" |
|
1198 shows "fls_shift n f * g = f * fls_shift n g" |
|
1199 using fls_shifted_times_simps(1)[of f n g] fls_shifted_times_simps(2)[of n f g] |
|
1200 by simp |
|
1201 |
|
1202 lemma fls_times_both_shifted_simp: |
|
1203 fixes f g :: "'a::{comm_monoid_add, mult_zero} fls" |
|
1204 shows "(fls_shift m f) * (fls_shift n g) = fls_shift (m+n) (f*g)" |
|
1205 by (simp add: fls_shifted_times_simps) |
|
1206 |
|
1207 lemma fls_base_factor_mult_base_factor: |
|
1208 fixes f g :: "'a::{comm_monoid_add, mult_zero} fls" |
|
1209 shows "fls_base_factor (f * fls_base_factor g) = fls_base_factor (f * g)" |
|
1210 and "fls_base_factor (fls_base_factor f * g) = fls_base_factor (f * g)" |
|
1211 using fls_base_factor_shift[of "fls_subdegree g" "f*g"] |
|
1212 fls_base_factor_shift[of "fls_subdegree f" "f*g"] |
|
1213 by (simp_all add: fls_shifted_times_simps) |
|
1214 |
|
1215 lemma fls_base_factor_mult_both_base_factor: |
|
1216 fixes f g :: "'a::{comm_monoid_add,mult_zero} fls" |
|
1217 shows "fls_base_factor (fls_base_factor f * fls_base_factor g) = fls_base_factor (f * g)" |
|
1218 using fls_base_factor_mult_base_factor(1)[of "fls_base_factor f" g] |
|
1219 fls_base_factor_mult_base_factor(2)[of f g] |
|
1220 by simp |
|
1221 |
|
1222 lemma fls_base_factor_mult: |
|
1223 fixes f g :: "'a::semiring_no_zero_divisors fls" |
|
1224 shows "fls_base_factor (f * g) = fls_base_factor f * fls_base_factor g" |
|
1225 by (cases "f\<noteq>0 \<and> g\<noteq>0") |
|
1226 (auto simp: fls_times_both_shifted_simp) |
|
1227 |
|
1228 lemma fls_times_conv_base_factor_times: |
|
1229 fixes f g :: "'a::{comm_monoid_add, mult_zero} fls" |
|
1230 shows |
|
1231 "f * g = |
|
1232 fls_shift (-(fls_subdegree f + fls_subdegree g)) (fls_base_factor f * fls_base_factor g)" |
|
1233 by (simp add: fls_times_both_shifted_simp) |
|
1234 |
|
1235 lemma fls_times_base_factor_conv_shifted_times: |
|
1236 \<comment> \<open>Convenience form of lemma @{text "fls_times_both_shifted_simp"}.\<close> |
|
1237 fixes f g :: "'a::{comm_monoid_add, mult_zero} fls" |
|
1238 shows |
|
1239 "fls_base_factor f * fls_base_factor g = fls_shift (fls_subdegree f + fls_subdegree g) (f * g)" |
|
1240 by (simp add: fls_times_both_shifted_simp) |
|
1241 |
|
1242 lemma fls_times_conv_regpart: |
|
1243 fixes f g :: "'a::{comm_monoid_add,mult_zero} fls" |
|
1244 assumes "fls_subdegree f \<ge> 0" "fls_subdegree g \<ge> 0" |
|
1245 shows "fls_regpart (f * g) = fls_regpart f * fls_regpart g" |
|
1246 proof- |
|
1247 from assms have 1: |
|
1248 "f * g = |
|
1249 fls_shift (- (fls_subdegree f + fls_subdegree g)) ( |
|
1250 fps_to_fls ( |
|
1251 fps_shift (nat (fls_subdegree f) + nat (fls_subdegree g)) ( |
|
1252 fls_regpart f * fls_regpart g |
|
1253 ) |
|
1254 ) |
|
1255 )" |
|
1256 by (simp add: |
|
1257 fls_times_def fls_base_factor_to_fps_conv_fps_shift[symmetric] |
|
1258 fls_regpart_subdegree_conv fps_shift_mult_both[symmetric] |
|
1259 ) |
|
1260 show ?thesis |
|
1261 proof (cases "fls_regpart f * fls_regpart g = 0") |
|
1262 case False |
|
1263 with assms have |
|
1264 "subdegree (fls_regpart f * fls_regpart g) \<ge> |
|
1265 nat (fls_subdegree f) + nat (fls_subdegree g)" |
|
1266 by (simp add: fps_mult_subdegree_ge fls_regpart_subdegree_conv[symmetric]) |
|
1267 with 1 assms show ?thesis by simp |
|
1268 qed (simp add: 1) |
|
1269 qed |
|
1270 |
|
1271 lemma fls_base_factor_to_fps_mult_conv_unit_factor: |
|
1272 fixes f g :: "'a::{comm_monoid_add,mult_zero} fls" |
|
1273 shows |
|
1274 "fls_base_factor_to_fps (f * g) = |
|
1275 unit_factor (fls_base_factor_to_fps f * fls_base_factor_to_fps g)" |
|
1276 using fls_base_factor_mult_both_base_factor[of f g] |
|
1277 fps_unit_factor_fls_regpart[of "fls_base_factor f * fls_base_factor g"] |
|
1278 fls_base_factor_subdegree[of f] fls_base_factor_subdegree[of g] |
|
1279 fls_mult_subdegree_ge_0[of "fls_base_factor f" "fls_base_factor g"] |
|
1280 fls_times_conv_regpart[of "fls_base_factor f" "fls_base_factor g"] |
|
1281 by simp |
|
1282 |
|
1283 lemma fls_base_factor_to_fps_mult': |
|
1284 fixes f g :: "'a::{comm_monoid_add,mult_zero} fls" |
|
1285 assumes "(f $$ fls_subdegree f) * (g $$ fls_subdegree g) \<noteq> 0" |
|
1286 shows "fls_base_factor_to_fps (f * g) = fls_base_factor_to_fps f * fls_base_factor_to_fps g" |
|
1287 using assms fls_mult_nonzero_base_subdegree_eq[of f g] |
|
1288 fls_times_base_factor_conv_shifted_times[of f g] |
|
1289 fls_times_conv_regpart[of "fls_base_factor f" "fls_base_factor g"] |
|
1290 fls_base_factor_subdegree[of f] fls_base_factor_subdegree[of g] |
|
1291 by fastforce |
|
1292 |
|
1293 lemma fls_base_factor_to_fps_mult: |
|
1294 fixes f g :: "'a::semiring_no_zero_divisors fls" |
|
1295 shows "fls_base_factor_to_fps (f * g) = fls_base_factor_to_fps f * fls_base_factor_to_fps g" |
|
1296 using fls_base_factor_to_fps_mult'[of f g] |
|
1297 by (cases "f=0 \<or> g=0") auto |
|
1298 |
|
1299 lemma fls_times_conv_fps_times: |
|
1300 fixes f g :: "'a::{comm_monoid_add,mult_zero} fls" |
|
1301 assumes "fls_subdegree f \<ge> 0" "fls_subdegree g \<ge> 0" |
|
1302 shows "f * g = fps_to_fls (fls_regpart f * fls_regpart g)" |
|
1303 using assms fls_mult_subdegree_ge[of f g] |
|
1304 by (cases "f * g = 0") (simp_all add: fls_times_conv_regpart[symmetric]) |
|
1305 |
|
1306 lemma fps_times_conv_fls_times: |
|
1307 fixes f g :: "'a::{comm_monoid_add,mult_zero} fps" |
|
1308 shows "f * g = fls_regpart (fps_to_fls f * fps_to_fls g)" |
|
1309 using fls_subdegree_fls_to_fps_gt0 fls_times_conv_regpart[symmetric] |
|
1310 by fastforce |
|
1311 |
|
1312 lemma fls_times_fps_to_fls: |
|
1313 fixes f g :: "'a::{comm_monoid_add,mult_zero} fps" |
|
1314 shows "fps_to_fls (f * g) = fps_to_fls f * fps_to_fls g" |
|
1315 proof (intro fls_eq_conv_fps_eqI, rule fls_subdegree_fls_to_fps_gt0) |
|
1316 show "fls_subdegree (fps_to_fls f * fps_to_fls g) \<ge> 0" |
|
1317 proof (cases "fps_to_fls f * fps_to_fls g = 0") |
|
1318 case False thus ?thesis |
|
1319 using fls_mult_subdegree_ge fls_subdegree_fls_to_fps_gt0[of f] |
|
1320 fls_subdegree_fls_to_fps_gt0[of g] |
|
1321 by fastforce |
|
1322 qed simp |
|
1323 qed (simp add: fps_times_conv_fls_times) |
|
1324 |
|
1325 lemma fls_X_times_conv_shift: |
|
1326 fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls" |
|
1327 shows "fls_X * f = fls_shift (-1) f" "f * fls_X = fls_shift (-1) f" |
|
1328 by (simp_all add: fls_X_conv_shift_1 fls_mult_one fls_shifted_times_simps) |
|
1329 |
|
1330 lemmas fls_X_times_comm = trans_sym[OF fls_X_times_conv_shift] |
|
1331 |
|
1332 lemma fls_subdegree_mult_fls_X: |
|
1333 fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls" |
|
1334 assumes "f \<noteq> 0" |
|
1335 shows "fls_subdegree (fls_X * f) = fls_subdegree f + 1" |
|
1336 and "fls_subdegree (f * fls_X) = fls_subdegree f + 1" |
|
1337 by (auto simp: fls_X_times_conv_shift assms) |
|
1338 |
|
1339 lemma fls_mult_fls_X_nonzero: |
|
1340 fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls" |
|
1341 assumes "f \<noteq> 0" |
|
1342 shows "fls_X * f \<noteq> 0" |
|
1343 and "f * fls_X \<noteq> 0" |
|
1344 by (auto simp: fls_X_times_conv_shift fls_shift_eq0_iff assms) |
|
1345 |
|
1346 lemma fls_base_factor_mult_fls_X: |
|
1347 fixes f :: "'a::{comm_monoid_add,monoid_mult,mult_zero} fls" |
|
1348 shows "fls_base_factor (fls_X * f) = fls_base_factor f" |
|
1349 and "fls_base_factor (f * fls_X) = fls_base_factor f" |
|
1350 using fls_base_factor_shift[of "-1" f] |
|
1351 by (auto simp: fls_X_times_conv_shift) |
|
1352 |
|
1353 lemma fls_X_inv_times_conv_shift: |
|
1354 fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls" |
|
1355 shows "fls_X_inv * f = fls_shift 1 f" "f * fls_X_inv = fls_shift 1 f" |
|
1356 by (simp_all add: fls_X_inv_conv_shift_1 fls_mult_one fls_shifted_times_simps) |
|
1357 |
|
1358 lemmas fls_X_inv_times_comm = trans_sym[OF fls_X_inv_times_conv_shift] |
|
1359 |
|
1360 lemma fls_subdegree_mult_fls_X_inv: |
|
1361 fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls" |
|
1362 assumes "f \<noteq> 0" |
|
1363 shows "fls_subdegree (fls_X_inv * f) = fls_subdegree f - 1" |
|
1364 and "fls_subdegree (f * fls_X_inv) = fls_subdegree f - 1" |
|
1365 by (auto simp: fls_X_inv_times_conv_shift assms) |
|
1366 |
|
1367 lemma fls_mult_fls_X_inv_nonzero: |
|
1368 fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls" |
|
1369 assumes "f \<noteq> 0" |
|
1370 shows "fls_X_inv * f \<noteq> 0" |
|
1371 and "f * fls_X_inv \<noteq> 0" |
|
1372 by (auto simp: fls_X_inv_times_conv_shift fls_shift_eq0_iff assms) |
|
1373 |
|
1374 lemma fls_base_factor_mult_fls_X_inv: |
|
1375 fixes f :: "'a::{comm_monoid_add,monoid_mult,mult_zero} fls" |
|
1376 shows "fls_base_factor (fls_X_inv * f) = fls_base_factor f" |
|
1377 and "fls_base_factor (f * fls_X_inv) = fls_base_factor f" |
|
1378 using fls_base_factor_shift[of 1 f] |
|
1379 by (auto simp: fls_X_inv_times_conv_shift) |
|
1380 |
|
1381 lemma fls_mult_assoc_subdegree_ge_0: |
|
1382 fixes f g h :: "'a::semiring_0 fls" |
|
1383 assumes "fls_subdegree f \<ge> 0" "fls_subdegree g \<ge> 0" "fls_subdegree h \<ge> 0" |
|
1384 shows "f * g * h = f * (g * h)" |
|
1385 using assms |
|
1386 by (simp add: fls_times_conv_fps_times fls_subdegree_fls_to_fps_gt0 mult.assoc) |
|
1387 |
|
1388 lemma fls_mult_assoc_base_factor: |
|
1389 fixes a b c :: "'a::semiring_0 fls" |
|
1390 shows |
|
1391 "fls_base_factor a * fls_base_factor b * fls_base_factor c = |
|
1392 fls_base_factor a * (fls_base_factor b * fls_base_factor c)" |
|
1393 by (simp add: fls_mult_assoc_subdegree_ge_0 del: fls_base_factor_def) |
|
1394 |
|
1395 lemma fls_mult_distrib_subdegree_ge_0: |
|
1396 fixes f g h :: "'a::semiring_0 fls" |
|
1397 assumes "fls_subdegree f \<ge> 0" "fls_subdegree g \<ge> 0" "fls_subdegree h \<ge> 0" |
|
1398 shows "(f + g) * h = f * h + g * h" |
|
1399 and "h * (f + g) = h * f + h * g" |
|
1400 proof- |
|
1401 have "fls_subdegree (f+g) \<ge> 0" |
|
1402 proof (cases "f+g = 0") |
|
1403 case False |
|
1404 with assms(1,2) show ?thesis |
|
1405 using fls_plus_subdegree by fastforce |
|
1406 qed simp |
|
1407 with assms show "(f + g) * h = f * h + g * h" "h * (f + g) = h * f + h * g" |
|
1408 using distrib_right[of "fls_regpart f"] distrib_left[of "fls_regpart h"] |
|
1409 by (simp_all add: fls_times_conv_fps_times) |
|
1410 qed |
|
1411 |
|
1412 lemma fls_mult_distrib_base_factor: |
|
1413 fixes a b c :: "'a::semiring_0 fls" |
|
1414 shows |
|
1415 "fls_base_factor a * (fls_base_factor b + fls_base_factor c) = |
|
1416 fls_base_factor a * fls_base_factor b + fls_base_factor a * fls_base_factor c" |
|
1417 by (simp add: fls_mult_distrib_subdegree_ge_0 del: fls_base_factor_def) |
|
1418 |
|
1419 instance fls :: (semiring_0) semiring_0 |
|
1420 proof |
|
1421 |
|
1422 fix a b c :: "'a fls" |
|
1423 have |
|
1424 "a * b * c = |
|
1425 fls_shift (- (fls_subdegree a + fls_subdegree b + fls_subdegree c)) |
|
1426 (fls_base_factor a * fls_base_factor b * fls_base_factor c)" |
|
1427 by (simp add: fls_times_both_shifted_simp) |
|
1428 moreover have |
|
1429 "a * (b * c) = |
|
1430 fls_shift (- (fls_subdegree a + fls_subdegree b + fls_subdegree c)) |
|
1431 (fls_base_factor a * fls_base_factor b * fls_base_factor c)" |
|
1432 using fls_mult_assoc_base_factor[of a b c] by (simp add: fls_times_both_shifted_simp) |
|
1433 ultimately show "a * b * c = a * (b * c)" by simp |
|
1434 |
|
1435 have ab: |
|
1436 "fls_subdegree (fls_shift (min (fls_subdegree a) (fls_subdegree b)) a) \<ge> 0" |
|
1437 "fls_subdegree (fls_shift (min (fls_subdegree a) (fls_subdegree b)) b) \<ge> 0" |
|
1438 by (simp_all add: fls_shift_nonneg_subdegree) |
|
1439 have |
|
1440 "(a + b) * c = |
|
1441 fls_shift (- (min (fls_subdegree a) (fls_subdegree b) + fls_subdegree c)) ( |
|
1442 ( |
|
1443 fls_shift (min (fls_subdegree a) (fls_subdegree b)) a + |
|
1444 fls_shift (min (fls_subdegree a) (fls_subdegree b)) b |
|
1445 ) * fls_base_factor c)" |
|
1446 using fls_times_both_shifted_simp[of |
|
1447 "-min (fls_subdegree a) (fls_subdegree b)" |
|
1448 "fls_shift (min (fls_subdegree a) (fls_subdegree b)) a + |
|
1449 fls_shift (min (fls_subdegree a) (fls_subdegree b)) b" |
|
1450 "-fls_subdegree c" "fls_base_factor c" |
|
1451 ] |
|
1452 by simp |
|
1453 also have |
|
1454 "\<dots> = |
|
1455 fls_shift (-(min (fls_subdegree a) (fls_subdegree b) + fls_subdegree c)) |
|
1456 (fls_shift (min (fls_subdegree a) (fls_subdegree b)) a * fls_base_factor c) |
|
1457 + |
|
1458 fls_shift (-(min (fls_subdegree a) (fls_subdegree b) + fls_subdegree c)) |
|
1459 (fls_shift (min (fls_subdegree a) (fls_subdegree b)) b * fls_base_factor c)" |
|
1460 using ab |
|
1461 by (simp add: fls_mult_distrib_subdegree_ge_0(1) del: fls_base_factor_def) |
|
1462 finally show "(a + b) * c = a * c + b * c" by (simp add: fls_times_both_shifted_simp) |
|
1463 |
|
1464 have bc: |
|
1465 "fls_subdegree (fls_shift (min (fls_subdegree b) (fls_subdegree c)) b) \<ge> 0" |
|
1466 "fls_subdegree (fls_shift (min (fls_subdegree b) (fls_subdegree c)) c) \<ge> 0" |
|
1467 by (simp_all add: fls_shift_nonneg_subdegree) |
|
1468 have |
|
1469 "a * (b + c) = |
|
1470 fls_shift (- (fls_subdegree a + min (fls_subdegree b) (fls_subdegree c))) ( |
|
1471 fls_base_factor a * ( |
|
1472 fls_shift (min (fls_subdegree b) (fls_subdegree c)) b + |
|
1473 fls_shift (min (fls_subdegree b) (fls_subdegree c)) c |
|
1474 ) |
|
1475 ) |
|
1476 " |
|
1477 using fls_times_both_shifted_simp[of |
|
1478 "-fls_subdegree a" "fls_base_factor a" |
|
1479 "-min (fls_subdegree b) (fls_subdegree c)" |
|
1480 "fls_shift (min (fls_subdegree b) (fls_subdegree c)) b + |
|
1481 fls_shift (min (fls_subdegree b) (fls_subdegree c)) c" |
|
1482 ] |
|
1483 by simp |
|
1484 also have |
|
1485 "\<dots> = |
|
1486 fls_shift (-(fls_subdegree a + min (fls_subdegree b) (fls_subdegree c))) |
|
1487 (fls_base_factor a * fls_shift (min (fls_subdegree b) (fls_subdegree c)) b) |
|
1488 + |
|
1489 fls_shift (-(fls_subdegree a + min (fls_subdegree b) (fls_subdegree c))) |
|
1490 (fls_base_factor a * fls_shift (min (fls_subdegree b) (fls_subdegree c)) c) |
|
1491 " |
|
1492 using bc |
|
1493 by (simp add: fls_mult_distrib_subdegree_ge_0(2) del: fls_base_factor_def) |
|
1494 finally show "a * (b + c) = a * b + a * c" by (simp add: fls_times_both_shifted_simp) |
|
1495 |
|
1496 qed |
|
1497 |
|
1498 lemma fls_mult_commute_subdegree_ge_0: |
|
1499 fixes f g :: "'a::comm_semiring_0 fls" |
|
1500 assumes "fls_subdegree f \<ge> 0" "fls_subdegree g \<ge> 0" |
|
1501 shows "f * g = g * f" |
|
1502 using assms |
|
1503 by (simp add: fls_times_conv_fps_times mult.commute) |
|
1504 |
|
1505 lemma fls_mult_commute_base_factor: |
|
1506 fixes a b c :: "'a::comm_semiring_0 fls" |
|
1507 shows "fls_base_factor a * fls_base_factor b = fls_base_factor b * fls_base_factor a" |
|
1508 by (simp add: fls_mult_commute_subdegree_ge_0 del: fls_base_factor_def) |
|
1509 |
|
1510 instance fls :: (comm_semiring_0) comm_semiring_0 |
|
1511 proof |
|
1512 fix a b c :: "'a fls" |
|
1513 show "a * b = b * a" |
|
1514 using fls_times_conv_base_factor_times[of a b] fls_times_conv_base_factor_times[of b a] |
|
1515 fls_mult_commute_base_factor[of a b] |
|
1516 by (simp add: add.commute) |
|
1517 qed (simp add: distrib_right) |
|
1518 |
|
1519 instance fls :: (semiring_1) semiring_1 |
|
1520 by (standard, simp_all add: fls_mult_one) |
|
1521 |
|
1522 lemma fls_of_nat: "(of_nat n :: 'a::semiring_1 fls) = fls_const (of_nat n)" |
|
1523 by (induct n) (auto intro: fls_eqI) |
|
1524 |
|
1525 lemma fls_of_nat_nth: "of_nat n $$ k = (if k=0 then of_nat n else 0)" |
|
1526 by (simp add: fls_of_nat) |
|
1527 |
|
1528 lemma fls_mult_of_nat_nth [simp]: |
|
1529 shows "(of_nat k * f) $$ n = of_nat k * f$$n" |
|
1530 and "(f * of_nat k ) $$ n = f$$n * of_nat k" |
|
1531 by (simp_all add: fls_of_nat) |
|
1532 |
|
1533 lemma fls_subdegree_of_nat [simp]: "fls_subdegree (of_nat n) = 0" |
|
1534 by (simp add: fls_of_nat) |
|
1535 |
|
1536 lemma fls_shift_of_nat_nth: |
|
1537 "fls_shift k (of_nat a) $$ n = (if n=-k then of_nat a else 0)" |
|
1538 by (simp add: fls_of_nat fls_shift_const_nth) |
|
1539 |
|
1540 lemma fls_base_factor_of_nat [simp]: |
|
1541 "fls_base_factor (of_nat n :: 'a::semiring_1 fls) = (of_nat n :: 'a fls)" |
|
1542 by (simp add: fls_of_nat) |
|
1543 |
|
1544 lemma fls_regpart_of_nat [simp]: "fls_regpart (of_nat n) = (of_nat n :: 'a::semiring_1 fps)" |
|
1545 by (simp add: fls_of_nat fps_of_nat) |
|
1546 |
|
1547 lemma fls_prpart_of_nat [simp]: "fls_prpart (of_nat n) = 0" |
|
1548 by (simp add: fls_prpart_eq0_iff) |
|
1549 |
|
1550 lemma fls_base_factor_to_fps_of_nat: |
|
1551 "fls_base_factor_to_fps (of_nat n) = (of_nat n :: 'a::semiring_1 fps)" |
|
1552 by simp |
|
1553 |
|
1554 lemma fps_to_fls_of_nat: |
|
1555 "fps_to_fls (of_nat n) = (of_nat n :: 'a::semiring_1 fls)" |
|
1556 proof - |
|
1557 have "fps_to_fls (of_nat n) = fps_to_fls (fps_const (of_nat n))" |
|
1558 by (simp add: fps_of_nat) |
|
1559 thus ?thesis by (simp add: fls_of_nat) |
|
1560 qed |
|
1561 |
|
1562 instance fls :: (comm_semiring_1) comm_semiring_1 |
|
1563 by standard simp |
|
1564 |
|
1565 instance fls :: (ring) ring .. |
|
1566 |
|
1567 instance fls :: (comm_ring) comm_ring .. |
|
1568 |
|
1569 instance fls :: (ring_1) ring_1 .. |
|
1570 |
|
1571 lemma fls_of_int_nonneg: "(of_int (int n) :: 'a::ring_1 fls) = fls_const (of_int (int n))" |
|
1572 by (induct n) (auto intro: fls_eqI) |
|
1573 |
|
1574 lemma fls_of_int: "(of_int i :: 'a::ring_1 fls) = fls_const (of_int i)" |
|
1575 proof (induct i) |
|
1576 case (neg i) |
|
1577 have "of_int (int (Suc i)) = fls_const (of_int (int (Suc i)) :: 'a)" |
|
1578 using fls_of_int_nonneg[of "Suc i"] by simp |
|
1579 hence "- of_int (int (Suc i)) = - fls_const (of_int (int (Suc i)) :: 'a)" |
|
1580 by simp |
|
1581 thus ?case by (simp add: fls_const_uminus[symmetric]) |
|
1582 qed (rule fls_of_int_nonneg) |
|
1583 |
|
1584 lemma fls_of_int_nth: "of_int n $$ k = (if k=0 then of_int n else 0)" |
|
1585 by (simp add: fls_of_int) |
|
1586 |
|
1587 lemma fls_mult_of_int_nth [simp]: |
|
1588 shows "(of_int k * f) $$ n = of_int k * f$$n" |
|
1589 and "(f * of_int k ) $$ n = f$$n * of_int k" |
|
1590 by (simp_all add: fls_of_int) |
|
1591 |
|
1592 lemma fls_subdegree_of_int [simp]: "fls_subdegree (of_int i) = 0" |
|
1593 by (simp add: fls_of_int) |
|
1594 |
|
1595 lemma fls_shift_of_int_nth: |
|
1596 "fls_shift k (of_int i) $$ n = (if n=-k then of_int i else 0)" |
|
1597 by (simp add: fls_of_int_nth) |
|
1598 |
|
1599 lemma fls_base_factor_of_int [simp]: |
|
1600 "fls_base_factor (of_int i :: 'a::ring_1 fls) = (of_int i :: 'a fls)" |
|
1601 by (simp add: fls_of_int) |
|
1602 |
|
1603 lemma fls_regpart_of_int [simp]: |
|
1604 "fls_regpart (of_int i) = (of_int i :: 'a::ring_1 fps)" |
|
1605 by (simp add: fls_of_int fps_of_int) |
|
1606 |
|
1607 lemma fls_prpart_of_int [simp]: "fls_prpart (of_int n) = 0" |
|
1608 by (simp add: fls_prpart_eq0_iff) |
|
1609 |
|
1610 lemma fls_base_factor_to_fps_of_int: |
|
1611 "fls_base_factor_to_fps (of_int i) = (of_int i :: 'a::ring_1 fps)" |
|
1612 by simp |
|
1613 |
|
1614 lemma fps_to_fls_of_int: |
|
1615 "fps_to_fls (of_int i) = (of_int i :: 'a::ring_1 fls)" |
|
1616 proof - |
|
1617 have "fps_to_fls (of_int i) = fps_to_fls (fps_const (of_int i))" |
|
1618 by (simp add: fps_of_int) |
|
1619 thus ?thesis by (simp add: fls_of_int) |
|
1620 qed |
|
1621 |
|
1622 instance fls :: (comm_ring_1) comm_ring_1 .. |
|
1623 |
|
1624 instance fls :: (semiring_no_zero_divisors) semiring_no_zero_divisors |
|
1625 proof |
|
1626 fix a b :: "'a fls" |
|
1627 assume "a \<noteq> 0" and "b \<noteq> 0" |
|
1628 hence "(a * b) $$ (fls_subdegree a + fls_subdegree b) \<noteq> 0" by simp |
|
1629 thus "a * b \<noteq> 0" using fls_nonzeroI by fast |
|
1630 qed |
|
1631 |
|
1632 instance fls :: (semiring_1_no_zero_divisors) semiring_1_no_zero_divisors .. |
|
1633 |
|
1634 instance fls :: (ring_no_zero_divisors) ring_no_zero_divisors .. |
|
1635 |
|
1636 instance fls :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors .. |
|
1637 |
|
1638 instance fls :: (idom) idom .. |
|
1639 |
|
1640 |
|
1641 subsubsection \<open>Powers\<close> |
|
1642 |
|
1643 lemma fls_pow_subdegree_ge: |
|
1644 "f^n \<noteq> 0 \<Longrightarrow> fls_subdegree (f^n) \<ge> n * fls_subdegree f" |
|
1645 proof (induct n) |
|
1646 case (Suc n) thus ?case |
|
1647 using fls_mult_subdegree_ge[of f "f^n"] by (fastforce simp: algebra_simps) |
|
1648 qed simp |
|
1649 |
|
1650 lemma fls_pow_nth_below_subdegree: |
|
1651 "k < n * fls_subdegree f \<Longrightarrow> (f^n) $$ k = 0" |
|
1652 using fls_pow_subdegree_ge[of f n] by (cases "f^n = 0") auto |
|
1653 |
|
1654 lemma fls_pow_base [simp]: |
|
1655 "(f ^ n) $$ (n * fls_subdegree f) = (f $$ fls_subdegree f) ^ n" |
|
1656 proof (induct n) |
|
1657 case (Suc n) |
|
1658 show ?case |
|
1659 proof (cases "Suc n * fls_subdegree f < fls_subdegree f + fls_subdegree (f^n)") |
|
1660 case True with Suc show ?thesis |
|
1661 by (simp_all add: fls_times_nth_eq0 distrib_right) |
|
1662 next |
|
1663 case False |
|
1664 from False have |
|
1665 "{0..int n * fls_subdegree f - fls_subdegree (f ^ n)} = |
|
1666 insert 0 {1..int n * fls_subdegree f - fls_subdegree (f ^ n)}" |
|
1667 by (auto simp: algebra_simps) |
|
1668 with False Suc show ?thesis |
|
1669 by (simp add: algebra_simps fls_times_nth(4) fls_pow_nth_below_subdegree) |
|
1670 qed |
|
1671 qed simp |
|
1672 |
|
1673 lemma fls_pow_subdegree_eqI: |
|
1674 "(f $$ fls_subdegree f) ^ n \<noteq> 0 \<Longrightarrow> fls_subdegree (f^n) = n * fls_subdegree f" |
|
1675 using fls_pow_nth_below_subdegree by (fastforce intro: fls_subdegree_eqI) |
|
1676 |
|
1677 lemma fls_unit_base_subdegree_power: |
|
1678 "x * f $$ fls_subdegree f = 1 \<Longrightarrow> fls_subdegree (f ^ n) = n * fls_subdegree f" |
|
1679 "f $$ fls_subdegree f * y = 1 \<Longrightarrow> fls_subdegree (f ^ n) = n * fls_subdegree f" |
|
1680 proof- |
|
1681 show "x * f $$ fls_subdegree f = 1 \<Longrightarrow> fls_subdegree (f ^ n) = n * fls_subdegree f" |
|
1682 using left_right_inverse_power[of x "f $$ fls_subdegree f" n] |
|
1683 by (auto intro: fls_pow_subdegree_eqI) |
|
1684 show "f $$ fls_subdegree f * y = 1 \<Longrightarrow> fls_subdegree (f ^ n) = n * fls_subdegree f" |
|
1685 using left_right_inverse_power[of "f $$ fls_subdegree f" y n] |
|
1686 by (auto intro: fls_pow_subdegree_eqI) |
|
1687 qed |
|
1688 |
|
1689 lemma fls_base_dvd1_subdegree_power: |
|
1690 "f $$ fls_subdegree f dvd 1 \<Longrightarrow> fls_subdegree (f ^ n) = n * fls_subdegree f" |
|
1691 using fls_unit_base_subdegree_power unfolding dvd_def by auto |
|
1692 |
|
1693 lemma fls_pow_subdegree_ge0: |
|
1694 assumes "fls_subdegree f \<ge> 0" |
|
1695 shows "fls_subdegree (f^n) \<ge> 0" |
|
1696 proof (cases "f^n = 0") |
|
1697 case False |
|
1698 moreover from assms have "int n * fls_subdegree f \<ge> 0" by simp |
|
1699 ultimately show ?thesis using fls_pow_subdegree_ge by fastforce |
|
1700 qed simp |
|
1701 |
|
1702 lemma fls_subdegree_pow: |
|
1703 fixes f :: "'a::semiring_1_no_zero_divisors fls" |
|
1704 shows "fls_subdegree (f ^ n) = n * fls_subdegree f" |
|
1705 proof (cases "f=0") |
|
1706 case False thus ?thesis by (induct n) (simp_all add: algebra_simps) |
|
1707 qed (cases "n=0", auto simp: zero_power) |
|
1708 |
|
1709 lemma fls_shifted_pow: |
|
1710 "(fls_shift m f) ^ n = fls_shift (n*m) (f ^ n)" |
|
1711 by (induct n) (simp_all add: fls_times_both_shifted_simp algebra_simps) |
|
1712 |
|
1713 lemma fls_pow_conv_fps_pow: |
|
1714 assumes "fls_subdegree f \<ge> 0" |
|
1715 shows "f ^ n = fps_to_fls ( (fls_regpart f) ^ n )" |
|
1716 proof (induct n) |
|
1717 case (Suc n) with assms show ?case |
|
1718 using fls_pow_subdegree_ge0[of f n] |
|
1719 by (simp add: fls_times_conv_fps_times) |
|
1720 qed simp |
|
1721 |
|
1722 lemma fls_pow_conv_regpart: |
|
1723 "fls_subdegree f \<ge> 0 \<Longrightarrow> fls_regpart (f ^ n) = (fls_regpart f) ^ n" |
|
1724 using fls_pow_subdegree_ge0[of f n] fls_pow_conv_fps_pow[of f n] |
|
1725 by (intro fps_to_fls_eq_imp_fps_eq) simp |
|
1726 |
|
1727 text \<open>These two lemmas show that shifting 1 is equivalent to powers of the implied variable.\<close> |
|
1728 |
|
1729 lemma fls_X_power_conv_shift_1: "fls_X ^ n = fls_shift (-n) 1" |
|
1730 by (simp add: fls_X_conv_shift_1 fls_shifted_pow) |
|
1731 |
|
1732 lemma fls_X_inv_power_conv_shift_1: "fls_X_inv ^ n = fls_shift n 1" |
|
1733 by (simp add: fls_X_inv_conv_shift_1 fls_shifted_pow) |
|
1734 |
|
1735 abbreviation "fls_X_intpow \<equiv> (\<lambda>i. fls_shift (-i) 1)" |
|
1736 \<comment> \<open> |
|
1737 Unifies @{term fls_X} and @{term fls_X_inv} so that @{term "fls_X_intpow"} returns the equivalent |
|
1738 of the implied variable raised to the supplied integer argument of @{term "fls_X_intpow"}, whether |
|
1739 positive or negative. |
|
1740 \<close> |
|
1741 |
|
1742 lemma fls_X_intpow_nonzero[simp]: "(fls_X_intpow i :: 'a::zero_neq_one fls) \<noteq> 0" |
|
1743 by (simp add: fls_shift_eq0_iff) |
|
1744 |
|
1745 lemma fls_X_intpow_power: "(fls_X_intpow i) ^ n = fls_X_intpow (n * i)" |
|
1746 by (simp add: fls_shifted_pow) |
|
1747 |
|
1748 lemma fls_X_power_nth [simp]: "fls_X ^ n $$ k = (if k=n then 1 else 0)" |
|
1749 by (simp add: fls_X_power_conv_shift_1) |
|
1750 |
|
1751 lemma fls_X_inv_power_nth [simp]: "fls_X_inv ^ n $$ k = (if k=-n then 1 else 0)" |
|
1752 by (simp add: fls_X_inv_power_conv_shift_1) |
|
1753 |
|
1754 lemma fls_X_pow_nonzero[simp]: "(fls_X ^ n :: 'a :: semiring_1 fls) \<noteq> 0" |
|
1755 proof |
|
1756 assume "(fls_X ^ n :: 'a fls) = 0" |
|
1757 hence "(fls_X ^ n :: 'a fls) $$ n = 0" by simp |
|
1758 thus False by simp |
|
1759 qed |
|
1760 |
|
1761 lemma fls_X_inv_pow_nonzero[simp]: "(fls_X_inv ^ n :: 'a :: semiring_1 fls) \<noteq> 0" |
|
1762 proof |
|
1763 assume "(fls_X_inv ^ n :: 'a fls) = 0" |
|
1764 hence "(fls_X_inv ^ n :: 'a fls) $$ -n = 0" by simp |
|
1765 thus False by simp |
|
1766 qed |
|
1767 |
|
1768 lemma fls_subdegree_fls_X_pow [simp]: "fls_subdegree (fls_X ^ n) = n" |
|
1769 by (intro fls_subdegree_eqI) (simp_all add: fls_X_power_conv_shift_1) |
|
1770 |
|
1771 lemma fls_subdegree_fls_X_inv_pow [simp]: "fls_subdegree (fls_X_inv ^ n) = -n" |
|
1772 by (intro fls_subdegree_eqI) (simp_all add: fls_X_inv_power_conv_shift_1) |
|
1773 |
|
1774 lemma fls_subdegree_fls_X_intpow [simp]: |
|
1775 "fls_subdegree ((fls_X_intpow i) :: 'a::zero_neq_one fls) = i" |
|
1776 by simp |
|
1777 |
|
1778 lemma fls_X_pow_conv_fps_X_pow: "fls_regpart (fls_X ^ n) = fps_X ^ n" |
|
1779 by (simp add: fls_pow_conv_regpart) |
|
1780 |
|
1781 lemma fls_X_inv_pow_regpart: "n > 0 \<Longrightarrow> fls_regpart (fls_X_inv ^ n) = 0" |
|
1782 by (auto intro: fps_ext simp: fls_X_inv_power_conv_shift_1) |
|
1783 |
|
1784 lemma fls_X_intpow_regpart: |
|
1785 "fls_regpart (fls_X_intpow i) = (if i\<ge>0 then fps_X ^ nat i else 0)" |
|
1786 using fls_X_pow_conv_fps_X_pow[of "nat i"] |
|
1787 fls_regpart_shift_conv_fps_shift[of "-i" 1] |
|
1788 by (auto simp: fls_X_power_conv_shift_1 fps_shift_one) |
|
1789 |
|
1790 lemma fls_X_power_times_conv_shift: |
|
1791 "fls_X ^ n * f = fls_shift (-int n) f" "f * fls_X ^ n = fls_shift (-int n) f" |
|
1792 using fls_times_both_shifted_simp[of "-int n" 1 0 f] |
|
1793 fls_times_both_shifted_simp[of 0 f "-int n" 1] |
|
1794 by (simp_all add: fls_X_power_conv_shift_1) |
|
1795 |
|
1796 lemma fls_X_inv_power_times_conv_shift: |
|
1797 "fls_X_inv ^ n * f = fls_shift (int n) f" "f * fls_X_inv ^ n = fls_shift (int n) f" |
|
1798 using fls_times_both_shifted_simp[of "int n" 1 0 f] |
|
1799 fls_times_both_shifted_simp[of 0 f "int n" 1] |
|
1800 by (simp_all add: fls_X_inv_power_conv_shift_1) |
|
1801 |
|
1802 lemma fls_X_intpow_times_conv_shift: |
|
1803 fixes f :: "'a::semiring_1 fls" |
|
1804 shows "fls_X_intpow i * f = fls_shift (-i) f" "f * fls_X_intpow i = fls_shift (-i) f" |
|
1805 by (simp_all add: fls_shifted_times_simps) |
|
1806 |
|
1807 lemmas fls_X_power_times_comm = trans_sym[OF fls_X_power_times_conv_shift] |
|
1808 lemmas fls_X_inv_power_times_comm = trans_sym[OF fls_X_inv_power_times_conv_shift] |
|
1809 |
|
1810 lemma fls_X_intpow_times_comm: |
|
1811 fixes f :: "'a::semiring_1 fls" |
|
1812 shows "fls_X_intpow i * f = f * fls_X_intpow i" |
|
1813 by (simp add: fls_X_intpow_times_conv_shift) |
|
1814 |
|
1815 lemma fls_X_intpow_times_fls_X_intpow: |
|
1816 "(fls_X_intpow i :: 'a::semiring_1 fls) * fls_X_intpow j = fls_X_intpow (i+j)" |
|
1817 by (simp add: fls_times_both_shifted_simp) |
|
1818 |
|
1819 lemma fls_X_intpow_diff_conv_times: |
|
1820 "fls_X_intpow (i-j) = (fls_X_intpow i :: 'a::semiring_1 fls) * fls_X_intpow (-j)" |
|
1821 using fls_X_intpow_times_fls_X_intpow[of i "-j",symmetric] by simp |
|
1822 |
|
1823 lemma fls_mult_fls_X_power_nonzero: |
|
1824 assumes "f \<noteq> 0" |
|
1825 shows "fls_X ^ n * f \<noteq> 0" "f * fls_X ^ n \<noteq> 0" |
|
1826 by (auto simp: fls_X_power_times_conv_shift fls_shift_eq0_iff assms) |
|
1827 |
|
1828 lemma fls_mult_fls_X_inv_power_nonzero: |
|
1829 assumes "f \<noteq> 0" |
|
1830 shows "fls_X_inv ^ n * f \<noteq> 0" "f * fls_X_inv ^ n \<noteq> 0" |
|
1831 by (auto simp: fls_X_inv_power_times_conv_shift fls_shift_eq0_iff assms) |
|
1832 |
|
1833 lemma fls_mult_fls_X_intpow_nonzero: |
|
1834 fixes f :: "'a::semiring_1 fls" |
|
1835 assumes "f \<noteq> 0" |
|
1836 shows "fls_X_intpow i * f \<noteq> 0" "f * fls_X_intpow i \<noteq> 0" |
|
1837 by (auto simp: fls_X_intpow_times_conv_shift fls_shift_eq0_iff assms) |
|
1838 |
|
1839 lemma fls_subdegree_mult_fls_X_power: |
|
1840 assumes "f \<noteq> 0" |
|
1841 shows "fls_subdegree (fls_X ^ n * f) = fls_subdegree f + n" |
|
1842 and "fls_subdegree (f * fls_X ^ n) = fls_subdegree f + n" |
|
1843 by (auto simp: fls_X_power_times_conv_shift assms) |
|
1844 |
|
1845 lemma fls_subdegree_mult_fls_X_inv_power: |
|
1846 assumes "f \<noteq> 0" |
|
1847 shows "fls_subdegree (fls_X_inv ^ n * f) = fls_subdegree f - n" |
|
1848 and "fls_subdegree (f * fls_X_inv ^ n) = fls_subdegree f - n" |
|
1849 by (auto simp: fls_X_inv_power_times_conv_shift assms) |
|
1850 |
|
1851 lemma fls_subdegree_mult_fls_X_intpow: |
|
1852 fixes f :: "'a::semiring_1 fls" |
|
1853 assumes "f \<noteq> 0" |
|
1854 shows "fls_subdegree (fls_X_intpow i * f) = fls_subdegree f + i" |
|
1855 and "fls_subdegree (f * fls_X_intpow i) = fls_subdegree f + i" |
|
1856 by (auto simp: fls_X_intpow_times_conv_shift assms) |
|
1857 |
|
1858 lemma fls_X_shift: |
|
1859 "fls_shift (-int n) fls_X = fls_X ^ Suc n" |
|
1860 "fls_shift (int (Suc n)) fls_X = fls_X_inv ^ n" |
|
1861 using fls_X_power_conv_shift_1[of "Suc n", symmetric] |
|
1862 by (simp_all add: fls_X_conv_shift_1 fls_X_inv_power_conv_shift_1) |
|
1863 |
|
1864 lemma fls_X_inv_shift: |
|
1865 "fls_shift (int n) fls_X_inv = fls_X_inv ^ Suc n" |
|
1866 "fls_shift (- int (Suc n)) fls_X_inv = fls_X ^ n" |
|
1867 using fls_X_inv_power_conv_shift_1[of "Suc n", symmetric] |
|
1868 by (simp_all add: fls_X_inv_conv_shift_1 fls_X_power_conv_shift_1) |
|
1869 |
|
1870 lemma fls_X_power_base_factor: "fls_base_factor (fls_X ^ n) = 1" |
|
1871 by (simp add: fls_X_power_conv_shift_1) |
|
1872 |
|
1873 lemma fls_X_inv_power_base_factor: "fls_base_factor (fls_X_inv ^ n) = 1" |
|
1874 by (simp add: fls_X_inv_power_conv_shift_1) |
|
1875 |
|
1876 lemma fls_X_intpow_base_factor: "fls_base_factor (fls_X_intpow i) = 1" |
|
1877 using fls_base_factor_shift[of "-i" 1] by simp |
|
1878 |
|
1879 lemma fls_base_factor_mult_fls_X_power: |
|
1880 shows "fls_base_factor (fls_X ^ n * f) = fls_base_factor f" |
|
1881 and "fls_base_factor (f * fls_X ^ n) = fls_base_factor f" |
|
1882 using fls_base_factor_shift[of "-int n" f] |
|
1883 by (auto simp: fls_X_power_times_conv_shift) |
|
1884 |
|
1885 lemma fls_base_factor_mult_fls_X_inv_power: |
|
1886 shows "fls_base_factor (fls_X_inv ^ n * f) = fls_base_factor f" |
|
1887 and "fls_base_factor (f * fls_X_inv ^ n) = fls_base_factor f" |
|
1888 using fls_base_factor_shift[of "int n" f] |
|
1889 by (auto simp: fls_X_inv_power_times_conv_shift) |
|
1890 |
|
1891 lemma fls_base_factor_mult_fls_X_intpow: |
|
1892 fixes f :: "'a::semiring_1 fls" |
|
1893 shows "fls_base_factor (fls_X_intpow i * f) = fls_base_factor f" |
|
1894 and "fls_base_factor (f * fls_X_intpow i) = fls_base_factor f" |
|
1895 using fls_base_factor_shift[of "-i" f] |
|
1896 by (auto simp: fls_X_intpow_times_conv_shift) |
|
1897 |
|
1898 lemma fls_X_power_base_factor_to_fps: "fls_base_factor_to_fps (fls_X ^ n) = 1" |
|
1899 proof- |
|
1900 define X where "X \<equiv> fls_X :: 'a::semiring_1 fls" |
|
1901 hence "fls_base_factor (X ^ n) = 1" using fls_X_power_base_factor by simp |
|
1902 thus "fls_base_factor_to_fps (X^n) = 1" by simp |
|
1903 qed |
|
1904 |
|
1905 lemma fls_X_inv_power_base_factor_to_fps: "fls_base_factor_to_fps (fls_X_inv ^ n) = 1" |
|
1906 proof- |
|
1907 define iX where "iX \<equiv> fls_X_inv :: 'a::semiring_1 fls" |
|
1908 hence "fls_base_factor (iX ^ n) = 1" using fls_X_inv_power_base_factor by simp |
|
1909 thus "fls_base_factor_to_fps (iX^n) = 1" by simp |
|
1910 qed |
|
1911 |
|
1912 lemma fls_X_intpow_base_factor_to_fps: "fls_base_factor_to_fps (fls_X_intpow i) = 1" |
|
1913 proof- |
|
1914 define f :: "'a fls" where "f \<equiv> fls_X_intpow i" |
|
1915 moreover have "fls_base_factor (fls_X_intpow i) = 1" by (rule fls_X_intpow_base_factor) |
|
1916 ultimately have "fls_base_factor f = 1" by simp |
|
1917 thus "fls_base_factor_to_fps f = 1" by simp |
|
1918 qed |
|
1919 |
|
1920 lemma fls_base_factor_X_power_decompose: |
|
1921 fixes f :: "'a::semiring_1 fls" |
|
1922 shows "f = fls_base_factor f * fls_X_intpow (fls_subdegree f)" |
|
1923 and "f = fls_X_intpow (fls_subdegree f) * fls_base_factor f" |
|
1924 by (simp_all add: fls_times_both_shifted_simp) |
|
1925 |
|
1926 lemma fls_normalized_product_of_inverses: |
|
1927 assumes "f * g = 1" |
|
1928 shows "fls_base_factor f * fls_base_factor g = |
|
1929 fls_X ^ (nat (-(fls_subdegree f+fls_subdegree g)))" |
|
1930 and "fls_base_factor f * fls_base_factor g = |
|
1931 fls_X_intpow (-(fls_subdegree f+fls_subdegree g))" |
|
1932 using fls_mult_subdegree_ge[of f g] |
|
1933 fls_times_base_factor_conv_shifted_times[of f g] |
|
1934 by (simp_all add: assms fls_X_power_conv_shift_1 algebra_simps) |
|
1935 |
|
1936 lemma fls_fps_normalized_product_of_inverses: |
|
1937 assumes "f * g = 1" |
|
1938 shows "fls_base_factor_to_fps f * fls_base_factor_to_fps g = |
|
1939 fps_X ^ (nat (-(fls_subdegree f+fls_subdegree g)))" |
|
1940 using fls_times_conv_regpart[of "fls_base_factor f" "fls_base_factor g"] |
|
1941 fls_base_factor_subdegree[of f] fls_base_factor_subdegree[of g] |
|
1942 fls_normalized_product_of_inverses(1)[OF assms] |
|
1943 by (force simp: fls_X_pow_conv_fps_X_pow) |
|
1944 |
|
1945 |
|
1946 subsubsection \<open>Inverses\<close> |
|
1947 |
|
1948 \<comment> \<open>See lemma fls_left_inverse\<close> |
|
1949 abbreviation fls_left_inverse :: |
|
1950 "'a::{comm_monoid_add,uminus,times} fls \<Rightarrow> 'a \<Rightarrow> 'a fls" |
|
1951 where |
|
1952 "fls_left_inverse f x \<equiv> |
|
1953 fls_shift (fls_subdegree f) (fps_to_fls (fps_left_inverse (fls_base_factor_to_fps f) x))" |
|
1954 |
|
1955 \<comment> \<open>See lemma fls_right_inverse\<close> |
|
1956 abbreviation fls_right_inverse :: |
|
1957 "'a::{comm_monoid_add,uminus,times} fls \<Rightarrow> 'a \<Rightarrow> 'a fls" |
|
1958 where |
|
1959 "fls_right_inverse f y \<equiv> |
|
1960 fls_shift (fls_subdegree f) (fps_to_fls (fps_right_inverse (fls_base_factor_to_fps f) y))" |
|
1961 |
|
1962 instantiation fls :: ("{comm_monoid_add,uminus,times,inverse}") inverse |
|
1963 begin |
|
1964 definition fls_divide_def: |
|
1965 "f div g = |
|
1966 fls_shift (fls_subdegree g - fls_subdegree f) ( |
|
1967 fps_to_fls ((fls_base_factor_to_fps f) div (fls_base_factor_to_fps g)) |
|
1968 ) |
|
1969 " |
|
1970 definition fls_inverse_def: |
|
1971 "inverse f = fls_shift (fls_subdegree f) (fps_to_fls (inverse (fls_base_factor_to_fps f)))" |
|
1972 instance .. |
|
1973 end |
|
1974 |
|
1975 lemma fls_inverse_def': |
|
1976 "inverse f = fls_right_inverse f (inverse (f $$ fls_subdegree f))" |
|
1977 by (simp add: fls_inverse_def fps_inverse_def) |
|
1978 |
|
1979 lemma fls_lr_inverse_base: |
|
1980 "fls_left_inverse f x $$ (-fls_subdegree f) = x" |
|
1981 "fls_right_inverse f y $$ (-fls_subdegree f) = y" |
|
1982 by auto |
|
1983 |
|
1984 lemma fls_inverse_base: |
|
1985 "f \<noteq> 0 \<Longrightarrow> inverse f $$ (-fls_subdegree f) = inverse (f $$ fls_subdegree f)" |
|
1986 by (simp add: fls_inverse_def') |
|
1987 |
|
1988 lemma fls_lr_inverse_starting0: |
|
1989 fixes f :: "'a::{comm_monoid_add,mult_zero,uminus} fls" |
|
1990 and g :: "'b::{ab_group_add,mult_zero} fls" |
|
1991 shows "fls_left_inverse f 0 = 0" |
|
1992 and "fls_right_inverse g 0 = 0" |
|
1993 by (simp_all add: fps_lr_inverse_starting0) |
|
1994 |
|
1995 lemma fls_lr_inverse_eq0_imp_starting0: |
|
1996 "fls_left_inverse f x = 0 \<Longrightarrow> x = 0" |
|
1997 "fls_right_inverse f x = 0 \<Longrightarrow> x = 0" |
|
1998 proof- |
|
1999 assume "fls_left_inverse f x = 0" |
|
2000 hence "fps_left_inverse (fls_base_factor_to_fps f) x = 0" |
|
2001 using fls_shift_eq_iff fps_to_fls_eq_zero_iff by fastforce |
|
2002 thus "x = 0" using fps_lr_inverse_eq0_imp_starting0(1) by fast |
|
2003 next |
|
2004 assume "fls_right_inverse f x = 0" |
|
2005 hence "fps_right_inverse (fls_base_factor_to_fps f) x = 0" |
|
2006 using fls_shift_eq_iff fps_to_fls_eq_zero_iff by fastforce |
|
2007 thus "x = 0" using fps_lr_inverse_eq0_imp_starting0(2) by fast |
|
2008 qed |
|
2009 |
|
2010 lemma fls_lr_inverse_eq_0_iff: |
|
2011 fixes x :: "'a::{comm_monoid_add,mult_zero,uminus}" |
|
2012 and y :: "'b::{ab_group_add,mult_zero}" |
|
2013 shows "fls_left_inverse f x = 0 \<longleftrightarrow> x = 0" |
|
2014 and "fls_right_inverse g y = 0 \<longleftrightarrow> y = 0" |
|
2015 using fls_lr_inverse_starting0 fls_lr_inverse_eq0_imp_starting0 |
|
2016 by auto |
|
2017 |
|
2018 lemma fls_inverse_eq_0_iff': |
|
2019 fixes f :: "'a::{ab_group_add,inverse,mult_zero} fls" |
|
2020 shows "inverse f = 0 \<longleftrightarrow> (inverse (f $$ fls_subdegree f) = 0)" |
|
2021 using fls_lr_inverse_eq_0_iff(2)[of f "inverse (f $$ fls_subdegree f)"] |
|
2022 by (simp add: fls_inverse_def') |
|
2023 |
|
2024 lemma fls_inverse_eq_0_iff[simp]: |
|
2025 "inverse f = (0:: ('a::division_ring) fls) \<longleftrightarrow> f $$ fls_subdegree f = 0" |
|
2026 using fls_inverse_eq_0_iff'[of f] by (cases "f=0") auto |
|
2027 |
|
2028 lemmas fls_inverse_eq_0' = iffD2[OF fls_inverse_eq_0_iff'] |
|
2029 lemmas fls_inverse_eq_0 = iffD2[OF fls_inverse_eq_0_iff] |
|
2030 |
|
2031 lemma fls_lr_inverse_const: |
|
2032 fixes a :: "'a::{ab_group_add,mult_zero}" |
|
2033 and b :: "'b::{comm_monoid_add,mult_zero,uminus}" |
|
2034 shows "fls_left_inverse (fls_const a) x = fls_const x" |
|
2035 and "fls_right_inverse (fls_const b) y = fls_const y" |
|
2036 by (simp_all add: fps_const_lr_inverse) |
|
2037 |
|
2038 lemma fls_inverse_const: |
|
2039 fixes a :: "'a::{comm_monoid_add,inverse,mult_zero,uminus}" |
|
2040 shows "inverse (fls_const a) = fls_const (inverse a)" |
|
2041 using fls_lr_inverse_const(2) |
|
2042 by (auto simp: fls_inverse_def') |
|
2043 |
|
2044 lemma fls_lr_inverse_of_nat: |
|
2045 fixes x :: "'a::{ring_1,mult_zero}" |
|
2046 and y :: "'b::{semiring_1,uminus}" |
|
2047 shows "fls_left_inverse (of_nat n) x = fls_const x" |
|
2048 and "fls_right_inverse (of_nat n) y = fls_const y" |
|
2049 using fls_lr_inverse_const |
|
2050 by (auto simp: fls_of_nat) |
|
2051 |
|
2052 lemma fls_inverse_of_nat: |
|
2053 "inverse (of_nat n :: 'a :: {semiring_1,inverse,uminus} fls) = fls_const (inverse (of_nat n))" |
|
2054 by (simp add: fls_inverse_const fls_of_nat) |
|
2055 |
|
2056 lemma fls_lr_inverse_of_int: |
|
2057 fixes x :: "'a::{ring_1,mult_zero}" |
|
2058 shows "fls_left_inverse (of_int n) x = fls_const x" |
|
2059 and "fls_right_inverse (of_int n) x = fls_const x" |
|
2060 using fls_lr_inverse_const |
|
2061 by (auto simp: fls_of_int) |
|
2062 |
|
2063 lemma fls_inverse_of_int: |
|
2064 "inverse (of_int n :: 'a :: {ring_1,inverse,uminus} fls) = fls_const (inverse (of_int n))" |
|
2065 by (simp add: fls_inverse_const fls_of_int) |
|
2066 |
|
2067 lemma fls_lr_inverse_zero: |
|
2068 fixes x :: "'a::{ab_group_add,mult_zero}" |
|
2069 and y :: "'b::{comm_monoid_add,mult_zero,uminus}" |
|
2070 shows "fls_left_inverse 0 x = fls_const x" |
|
2071 and "fls_right_inverse 0 y = fls_const y" |
|
2072 using fls_lr_inverse_const[of 0] |
|
2073 by auto |
|
2074 |
|
2075 lemma fls_inverse_zero_conv_fls_const: |
|
2076 "inverse (0::'a::{comm_monoid_add,mult_zero,uminus,inverse} fls) = fls_const (inverse 0)" |
|
2077 using fls_lr_inverse_zero(2)[of "inverse (0::'a)"] by (simp add: fls_inverse_def') |
|
2078 |
|
2079 lemma fls_inverse_zero': |
|
2080 assumes "inverse (0::'a::{comm_monoid_add,inverse,mult_zero,uminus}) = 0" |
|
2081 shows "inverse (0::'a fls) = 0" |
|
2082 by (simp add: fls_inverse_zero_conv_fls_const assms) |
|
2083 |
|
2084 lemma fls_inverse_zero [simp]: "inverse (0::'a::division_ring fls) = 0" |
|
2085 by (rule fls_inverse_zero'[OF inverse_zero]) |
|
2086 |
|
2087 lemma fls_inverse_base2: |
|
2088 fixes f :: "'a::{comm_monoid_add,mult_zero,uminus,inverse} fls" |
|
2089 shows "inverse f $$ (-fls_subdegree f) = inverse (f $$ fls_subdegree f)" |
|
2090 by (cases "f=0") (simp_all add: fls_inverse_zero_conv_fls_const fls_inverse_def') |
|
2091 |
|
2092 lemma fls_lr_inverse_one: |
|
2093 fixes x :: "'a::{ab_group_add,mult_zero,one}" |
|
2094 and y :: "'b::{comm_monoid_add,mult_zero,uminus,one}" |
|
2095 shows "fls_left_inverse 1 x = fls_const x" |
|
2096 and "fls_right_inverse 1 y = fls_const y" |
|
2097 using fls_lr_inverse_const[of 1] |
|
2098 by auto |
|
2099 |
|
2100 lemma fls_lr_inverse_one_one: |
|
2101 "fls_left_inverse 1 1 = |
|
2102 (1::'a::{ab_group_add,mult_zero,one} fls)" |
|
2103 "fls_right_inverse 1 1 = |
|
2104 (1::'b::{comm_monoid_add,mult_zero,uminus,one} fls)" |
|
2105 using fls_lr_inverse_one[of 1] by auto |
|
2106 |
|
2107 lemma fls_inverse_one: |
|
2108 assumes "inverse (1::'a::{comm_monoid_add,inverse,mult_zero,uminus,one}) = 1" |
|
2109 shows "inverse (1::'a fls) = 1" |
|
2110 using assms fls_lr_inverse_one_one(2) |
|
2111 by (simp add: fls_inverse_def') |
|
2112 |
|
2113 lemma fls_left_inverse_delta: |
|
2114 fixes b :: "'a::{ab_group_add,mult_zero}" |
|
2115 assumes "b \<noteq> 0" |
|
2116 shows "fls_left_inverse (Abs_fls (\<lambda>n. if n=a then b else 0)) x = |
|
2117 Abs_fls (\<lambda>n. if n=-a then x else 0)" |
|
2118 proof (intro fls_eqI) |
|
2119 fix n from assms show |
|
2120 "fls_left_inverse (Abs_fls (\<lambda>n. if n=a then b else 0)) x $$ n |
|
2121 = Abs_fls (\<lambda>n. if n = - a then x else 0) $$ n" |
|
2122 using fls_base_factor_to_fps_delta[of a b] |
|
2123 fls_lr_inverse_const(1)[of b] |
|
2124 fls_shift_const |
|
2125 by simp |
|
2126 qed |
|
2127 |
|
2128 lemma fls_right_inverse_delta: |
|
2129 fixes b :: "'a::{comm_monoid_add,mult_zero,uminus}" |
|
2130 assumes "b \<noteq> 0" |
|
2131 shows "fls_right_inverse (Abs_fls (\<lambda>n. if n=a then b else 0)) x = |
|
2132 Abs_fls (\<lambda>n. if n=-a then x else 0)" |
|
2133 proof (intro fls_eqI) |
|
2134 fix n from assms show |
|
2135 "fls_right_inverse (Abs_fls (\<lambda>n. if n=a then b else 0)) x $$ n |
|
2136 = Abs_fls (\<lambda>n. if n = - a then x else 0) $$ n" |
|
2137 using fls_base_factor_to_fps_delta[of a b] |
|
2138 fls_lr_inverse_const(2)[of b] |
|
2139 fls_shift_const |
|
2140 by simp |
|
2141 qed |
|
2142 |
|
2143 lemma fls_inverse_delta_nonzero: |
|
2144 fixes b :: "'a::{comm_monoid_add,inverse,mult_zero,uminus}" |
|
2145 assumes "b \<noteq> 0" |
|
2146 shows "inverse (Abs_fls (\<lambda>n. if n=a then b else 0)) = |
|
2147 Abs_fls (\<lambda>n. if n=-a then inverse b else 0)" |
|
2148 using assms fls_nonzeroI[of "Abs_fls (\<lambda>n. if n=a then b else 0)" a] |
|
2149 by (simp add: fls_inverse_def' fls_right_inverse_delta[symmetric]) |
|
2150 |
|
2151 lemma fls_inverse_delta: |
|
2152 fixes b :: "'a::division_ring" |
|
2153 shows "inverse (Abs_fls (\<lambda>n. if n=a then b else 0)) = |
|
2154 Abs_fls (\<lambda>n. if n=-a then inverse b else 0)" |
|
2155 by (cases "b=0") (simp_all add: fls_inverse_delta_nonzero) |
|
2156 |
|
2157 lemma fls_lr_inverse_X: |
|
2158 fixes x :: "'a::{ab_group_add,mult_zero,zero_neq_one}" |
|
2159 and y :: "'b::{comm_monoid_add,uminus,mult_zero,zero_neq_one}" |
|
2160 shows "fls_left_inverse fls_X x = fls_shift 1 (fls_const x)" |
|
2161 and "fls_right_inverse fls_X y = fls_shift 1 (fls_const y)" |
|
2162 using fls_lr_inverse_one(1)[of x] fls_lr_inverse_one(2)[of y] |
|
2163 by auto |
|
2164 |
|
2165 lemma fls_lr_inverse_X': |
|
2166 fixes x :: "'a::{ab_group_add,mult_zero,zero_neq_one,monoid_mult}" |
|
2167 and y :: "'b::{comm_monoid_add,uminus,mult_zero,zero_neq_one,monoid_mult}" |
|
2168 shows "fls_left_inverse fls_X x = fls_const x * fls_X_inv" |
|
2169 and "fls_right_inverse fls_X y = fls_const y * fls_X_inv" |
|
2170 using fls_lr_inverse_X(1)[of x] fls_lr_inverse_X(2)[of y] |
|
2171 by (simp_all add: fls_X_inv_times_conv_shift(2)) |
|
2172 |
|
2173 lemma fls_inverse_X': |
|
2174 assumes "inverse 1 = (1::'a::{comm_monoid_add,inverse,mult_zero,uminus,zero_neq_one})" |
|
2175 shows "inverse (fls_X::'a fls) = fls_X_inv" |
|
2176 using assms fls_lr_inverse_X(2)[of "1::'a"] |
|
2177 by (simp add: fls_inverse_def' fls_X_inv_conv_shift_1) |
|
2178 |
|
2179 lemma fls_inverse_X: "inverse (fls_X::'a::division_ring fls) = fls_X_inv" |
|
2180 by (simp add: fls_inverse_X') |
|
2181 |
|
2182 lemma fls_lr_inverse_X_inv: |
|
2183 fixes x :: "'a::{ab_group_add,mult_zero,zero_neq_one}" |
|
2184 and y :: "'b::{comm_monoid_add,uminus,mult_zero,zero_neq_one}" |
|
2185 shows "fls_left_inverse fls_X_inv x = fls_shift (-1) (fls_const x)" |
|
2186 and "fls_right_inverse fls_X_inv y = fls_shift (-1) (fls_const y)" |
|
2187 using fls_lr_inverse_one(1)[of x] fls_lr_inverse_one(2)[of y] |
|
2188 by auto |
|
2189 |
|
2190 lemma fls_lr_inverse_X_inv': |
|
2191 fixes x :: "'a::{ab_group_add,mult_zero,zero_neq_one,monoid_mult}" |
|
2192 and y :: "'b::{comm_monoid_add,uminus,mult_zero,zero_neq_one,monoid_mult}" |
|
2193 shows "fls_left_inverse fls_X_inv x = fls_const x * fls_X" |
|
2194 and "fls_right_inverse fls_X_inv y = fls_const y * fls_X" |
|
2195 using fls_lr_inverse_X_inv(1)[of x] fls_lr_inverse_X_inv(2)[of y] |
|
2196 by (simp_all add: fls_X_times_conv_shift(2)) |
|
2197 |
|
2198 lemma fls_inverse_X_inv': |
|
2199 assumes "inverse 1 = (1::'a::{comm_monoid_add,inverse,mult_zero,uminus,zero_neq_one})" |
|
2200 shows "inverse (fls_X_inv::'a fls) = fls_X" |
|
2201 using assms fls_lr_inverse_X_inv(2)[of "1::'a"] |
|
2202 by (simp add: fls_inverse_def' fls_X_conv_shift_1) |
|
2203 |
|
2204 lemma fls_inverse_X_inv: "inverse (fls_X_inv::'a::division_ring fls) = fls_X" |
|
2205 by (simp add: fls_inverse_X_inv') |
|
2206 |
|
2207 lemma fls_lr_inverse_subdegree: |
|
2208 assumes "x \<noteq> 0" |
|
2209 shows "fls_subdegree (fls_left_inverse f x) = - fls_subdegree f" |
|
2210 and "fls_subdegree (fls_right_inverse f x) = - fls_subdegree f" |
|
2211 by (auto intro: fls_subdegree_eqI simp: assms) |
|
2212 |
|
2213 lemma fls_inverse_subdegree': |
|
2214 "inverse (f $$ fls_subdegree f) \<noteq> 0 \<Longrightarrow> fls_subdegree (inverse f) = - fls_subdegree f" |
|
2215 using fls_lr_inverse_subdegree(2)[of "inverse (f $$ fls_subdegree f)"] |
|
2216 by (simp add: fls_inverse_def') |
|
2217 |
|
2218 lemma fls_inverse_subdegree [simp]: |
|
2219 fixes f :: "'a::division_ring fls" |
|
2220 shows "fls_subdegree (inverse f) = - fls_subdegree f" |
|
2221 by (cases "f=0") |
|
2222 (auto intro: fls_inverse_subdegree' simp: nonzero_imp_inverse_nonzero) |
|
2223 |
|
2224 lemma fls_inverse_subdegree_base_nonzero: |
|
2225 assumes "f \<noteq> 0" "inverse (f $$ fls_subdegree f) \<noteq> 0" |
|
2226 shows "inverse f $$ (fls_subdegree (inverse f)) = inverse (f $$ fls_subdegree f)" |
|
2227 using assms fls_inverse_subdegree'[of f] fls_inverse_base[of f] |
|
2228 by simp |
|
2229 |
|
2230 lemma fls_inverse_subdegree_base: |
|
2231 fixes f :: "'a::{ab_group_add,inverse,mult_zero} fls" |
|
2232 shows "inverse f $$ (fls_subdegree (inverse f)) = inverse (f $$ fls_subdegree f)" |
|
2233 using fls_inverse_eq_0_iff'[of f] fls_inverse_subdegree_base_nonzero[of f] |
|
2234 by (cases "f=0 \<or> inverse (f $$ fls_subdegree f) = 0") |
|
2235 (auto simp: fls_inverse_zero_conv_fls_const) |
|
2236 |
|
2237 lemma fls_lr_inverse_subdegree_0: |
|
2238 assumes "fls_subdegree f = 0" |
|
2239 shows "fls_subdegree (fls_left_inverse f x) \<ge> 0" |
|
2240 and "fls_subdegree (fls_right_inverse f x) \<ge> 0" |
|
2241 using fls_subdegree_ge0I[of "fls_left_inverse f x"] |
|
2242 fls_subdegree_ge0I[of "fls_right_inverse f x"] |
|
2243 by (auto simp: assms) |
|
2244 |
|
2245 lemma fls_inverse_subdegree_0: |
|
2246 "fls_subdegree f = 0 \<Longrightarrow> fls_subdegree (inverse f) \<ge> 0" |
|
2247 using fls_lr_inverse_subdegree_0(2)[of f] by (simp add: fls_inverse_def') |
|
2248 |
|
2249 lemma fls_lr_inverse_shift_nonzero: |
|
2250 fixes f :: "'a::{comm_monoid_add,mult_zero,uminus} fls" |
|
2251 assumes "f \<noteq> 0" |
|
2252 shows "fls_left_inverse (fls_shift m f) x = fls_shift (-m) (fls_left_inverse f x)" |
|
2253 and "fls_right_inverse (fls_shift m f) x = fls_shift (-m) (fls_right_inverse f x)" |
|
2254 using assms fls_base_factor_to_fps_shift[of m f] fls_shift_subdegree |
|
2255 by auto |
|
2256 |
|
2257 lemma fls_inverse_shift_nonzero: |
|
2258 fixes f :: "'a::{comm_monoid_add,inverse,mult_zero,uminus} fls" |
|
2259 assumes "f \<noteq> 0" |
|
2260 shows "inverse (fls_shift m f) = fls_shift (-m) (inverse f)" |
|
2261 using assms fls_lr_inverse_shift_nonzero(2)[of f m "inverse (f $$ fls_subdegree f)"] |
|
2262 by (simp add: fls_inverse_def') |
|
2263 |
|
2264 lemma fls_inverse_shift: |
|
2265 fixes f :: "'a::division_ring fls" |
|
2266 shows "inverse (fls_shift m f) = fls_shift (-m) (inverse f)" |
|
2267 using fls_inverse_shift_nonzero |
|
2268 by (cases "f=0") simp_all |
|
2269 |
|
2270 lemma fls_left_inverse_base_factor: |
|
2271 fixes x :: "'a::{ab_group_add,mult_zero}" |
|
2272 assumes "x \<noteq> 0" |
|
2273 shows "fls_left_inverse (fls_base_factor f) x = fls_base_factor (fls_left_inverse f x)" |
|
2274 using assms fls_lr_inverse_zero(1)[of x] fls_lr_inverse_subdegree(1)[of x] |
|
2275 by (cases "f=0") auto |
|
2276 |
|
2277 lemma fls_right_inverse_base_factor: |
|
2278 fixes y :: "'a::{comm_monoid_add,mult_zero,uminus}" |
|
2279 assumes "y \<noteq> 0" |
|
2280 shows "fls_right_inverse (fls_base_factor f) y = fls_base_factor (fls_right_inverse f y)" |
|
2281 using assms fls_lr_inverse_zero(2)[of y] fls_lr_inverse_subdegree(2)[of y] |
|
2282 by (cases "f=0") auto |
|
2283 |
|
2284 lemma fls_inverse_base_factor': |
|
2285 fixes f :: "'a::{comm_monoid_add,inverse,mult_zero,uminus} fls" |
|
2286 assumes "inverse (f $$ fls_subdegree f) \<noteq> 0" |
|
2287 shows "inverse (fls_base_factor f) = fls_base_factor (inverse f)" |
|
2288 by (cases "f=0") |
|
2289 (simp_all add: |
|
2290 assms fls_inverse_shift_nonzero fls_inverse_subdegree' |
|
2291 fls_inverse_zero_conv_fls_const |
|
2292 ) |
|
2293 |
|
2294 lemma fls_inverse_base_factor: |
|
2295 fixes f :: "'a::{ab_group_add,inverse,mult_zero} fls" |
|
2296 shows "inverse (fls_base_factor f) = fls_base_factor (inverse f)" |
|
2297 using fls_base_factor_base[of f] fls_inverse_eq_0_iff'[of f] |
|
2298 fls_inverse_eq_0_iff'[of "fls_base_factor f"] fls_inverse_base_factor'[of f] |
|
2299 by (cases "inverse (f $$ fls_subdegree f) = 0") simp_all |
|
2300 |
|
2301 lemma fls_lr_inverse_regpart: |
|
2302 assumes "fls_subdegree f = 0" |
|
2303 shows "fls_regpart (fls_left_inverse f x) = fps_left_inverse (fls_regpart f) x" |
|
2304 and "fls_regpart (fls_right_inverse f y) = fps_right_inverse (fls_regpart f) y" |
|
2305 using assms |
|
2306 by auto |
|
2307 |
|
2308 lemma fls_inverse_regpart: |
|
2309 assumes "fls_subdegree f = 0" |
|
2310 shows "fls_regpart (inverse f) = inverse (fls_regpart f)" |
|
2311 by (simp add: assms fls_inverse_def) |
|
2312 |
|
2313 lemma fls_base_factor_to_fps_left_inverse: |
|
2314 fixes x :: "'a::{ab_group_add,mult_zero}" |
|
2315 shows "fls_base_factor_to_fps (fls_left_inverse f x) = |
|
2316 fps_left_inverse (fls_base_factor_to_fps f) x" |
|
2317 using fls_left_inverse_base_factor[of x f] fls_base_factor_subdegree[of f] |
|
2318 by (cases "x=0") (simp_all add: fls_lr_inverse_starting0(1) fps_lr_inverse_starting0(1)) |
|
2319 |
|
2320 lemma fls_base_factor_to_fps_right_inverse_nonzero: |
|
2321 fixes y :: "'a::{comm_monoid_add,mult_zero,uminus}" |
|
2322 assumes "y \<noteq> 0" |
|
2323 shows "fls_base_factor_to_fps (fls_right_inverse f y) = |
|
2324 fps_right_inverse (fls_base_factor_to_fps f) y" |
|
2325 using assms fls_right_inverse_base_factor[of y f] |
|
2326 fls_base_factor_subdegree[of f] |
|
2327 by simp |
|
2328 |
|
2329 lemma fls_base_factor_to_fps_right_inverse: |
|
2330 fixes y :: "'a::{ab_group_add,mult_zero}" |
|
2331 shows "fls_base_factor_to_fps (fls_right_inverse f y) = |
|
2332 fps_right_inverse (fls_base_factor_to_fps f) y" |
|
2333 using fls_base_factor_to_fps_right_inverse_nonzero[of y f] |
|
2334 by (cases "y=0") (simp_all add: fls_lr_inverse_starting0(2) fps_lr_inverse_starting0(2)) |
|
2335 |
|
2336 lemma fls_base_factor_to_fps_inverse_nonzero: |
|
2337 fixes f :: "'a::{comm_monoid_add,inverse,mult_zero,uminus} fls" |
|
2338 assumes "inverse (f $$ fls_subdegree f) \<noteq> 0" |
|
2339 shows "fls_base_factor_to_fps (inverse f) = inverse (fls_base_factor_to_fps f)" |
|
2340 using assms fls_base_factor_to_fps_right_inverse_nonzero |
|
2341 by (simp add: fls_inverse_def' fps_inverse_def) |
|
2342 |
|
2343 lemma fls_base_factor_to_fps_inverse: |
|
2344 fixes f :: "'a::{ab_group_add,inverse,mult_zero} fls" |
|
2345 shows "fls_base_factor_to_fps (inverse f) = inverse (fls_base_factor_to_fps f)" |
|
2346 using fls_base_factor_to_fps_right_inverse |
|
2347 by (simp add: fls_inverse_def' fps_inverse_def) |
|
2348 |
|
2349 lemma fls_lr_inverse_fps_to_fls: |
|
2350 assumes "subdegree f = 0" |
|
2351 shows "fls_left_inverse (fps_to_fls f) x = fps_to_fls (fps_left_inverse f x)" |
|
2352 and "fls_right_inverse (fps_to_fls f) x = fps_to_fls (fps_right_inverse f x)" |
|
2353 using assms fls_base_factor_to_fps_to_fls[of f] |
|
2354 by (simp_all add: fls_subdegree_fls_to_fps) |
|
2355 |
|
2356 lemma fls_inverse_fps_to_fls: |
|
2357 "subdegree f = 0 \<Longrightarrow> inverse (fps_to_fls f) = fps_to_fls (inverse f)" |
|
2358 using nth_subdegree_nonzero[of f] |
|
2359 by (cases "f=0") |
|
2360 (auto simp add: |
|
2361 fps_to_fls_nonzeroI fls_inverse_def' fls_subdegree_fls_to_fps fps_inverse_def |
|
2362 fls_lr_inverse_fps_to_fls(2) |
|
2363 ) |
|
2364 |
|
2365 lemma fls_lr_inverse_X_power: |
|
2366 fixes x :: "'a::ring_1" |
|
2367 and y :: "'b::{semiring_1,uminus}" |
|
2368 shows "fls_left_inverse (fls_X ^ n) x = fls_shift n (fls_const x)" |
|
2369 and "fls_right_inverse (fls_X ^ n) y = fls_shift n (fls_const y)" |
|
2370 using fls_lr_inverse_one(1)[of x] fls_lr_inverse_one(2)[of y] |
|
2371 by (simp_all add: fls_X_power_conv_shift_1) |
|
2372 |
|
2373 lemma fls_lr_inverse_X_power': |
|
2374 fixes x :: "'a::ring_1" |
|
2375 and y :: "'b::{semiring_1,uminus}" |
|
2376 shows "fls_left_inverse (fls_X ^ n) x = fls_const x * fls_X_inv ^ n" |
|
2377 and "fls_right_inverse (fls_X ^ n) y = fls_const y * fls_X_inv ^ n" |
|
2378 using fls_lr_inverse_X_power(1)[of n x] fls_lr_inverse_X_power(2)[of n y] |
|
2379 by (simp_all add: fls_X_inv_power_times_conv_shift(2)) |
|
2380 |
|
2381 lemma fls_inverse_X_power': |
|
2382 assumes "inverse 1 = (1::'a::{semiring_1,uminus,inverse})" |
|
2383 shows "inverse ((fls_X ^ n)::'a fls) = fls_X_inv ^ n" |
|
2384 using fls_lr_inverse_X_power'(2)[of n 1] |
|
2385 by (simp add: fls_inverse_def' assms ) |
|
2386 |
|
2387 lemma fls_inverse_X_power: |
|
2388 "inverse ((fls_X::'a::division_ring fls) ^ n) = fls_X_inv ^ n" |
|
2389 by (simp add: fls_inverse_X_power') |
|
2390 |
|
2391 lemma fls_lr_inverse_X_inv_power: |
|
2392 fixes x :: "'a::ring_1" |
|
2393 and y :: "'b::{semiring_1,uminus}" |
|
2394 shows "fls_left_inverse (fls_X_inv ^ n) x = fls_shift (-n) (fls_const x)" |
|
2395 and "fls_right_inverse (fls_X_inv ^ n) y = fls_shift (-n) (fls_const y)" |
|
2396 using fls_lr_inverse_one(1)[of x] fls_lr_inverse_one(2)[of y] |
|
2397 by (simp_all add: fls_X_inv_power_conv_shift_1) |
|
2398 |
|
2399 lemma fls_lr_inverse_X_inv_power': |
|
2400 fixes x :: "'a::ring_1" |
|
2401 and y :: "'b::{semiring_1,uminus}" |
|
2402 shows "fls_left_inverse (fls_X_inv ^ n) x = fls_const x * fls_X ^ n" |
|
2403 and "fls_right_inverse (fls_X_inv ^ n) y = fls_const y * fls_X ^ n" |
|
2404 using fls_lr_inverse_X_inv_power(1)[of n x] fls_lr_inverse_X_inv_power(2)[of n y] |
|
2405 by (simp_all add: fls_X_power_times_conv_shift(2)) |
|
2406 |
|
2407 lemma fls_inverse_X_inv_power': |
|
2408 assumes "inverse 1 = (1::'a::{semiring_1,uminus,inverse})" |
|
2409 shows "inverse ((fls_X_inv ^ n)::'a fls) = fls_X ^ n" |
|
2410 using fls_lr_inverse_X_inv_power'(2)[of n 1] |
|
2411 by (simp add: fls_inverse_def' assms) |
|
2412 |
|
2413 lemma fls_inverse_X_inv_power: |
|
2414 "inverse ((fls_X_inv::'a::division_ring fls) ^ n) = fls_X ^ n" |
|
2415 by (simp add: fls_inverse_X_inv_power') |
|
2416 |
|
2417 lemma fls_lr_inverse_X_intpow: |
|
2418 fixes x :: "'a::ring_1" |
|
2419 and y :: "'b::{semiring_1,uminus}" |
|
2420 shows "fls_left_inverse (fls_X_intpow i) x = fls_shift i (fls_const x)" |
|
2421 and "fls_right_inverse (fls_X_intpow i) y = fls_shift i (fls_const y)" |
|
2422 using fls_lr_inverse_one(1)[of x] fls_lr_inverse_one(2)[of y] |
|
2423 by auto |
|
2424 |
|
2425 lemma fls_lr_inverse_X_intpow': |
|
2426 fixes x :: "'a::ring_1" |
|
2427 and y :: "'b::{semiring_1,uminus}" |
|
2428 shows "fls_left_inverse (fls_X_intpow i) x = fls_const x * fls_X_intpow (-i)" |
|
2429 and "fls_right_inverse (fls_X_intpow i) y = fls_const y * fls_X_intpow (-i)" |
|
2430 using fls_lr_inverse_X_intpow(1)[of i x] fls_lr_inverse_X_intpow(2)[of i y] |
|
2431 by (simp_all add: fls_shifted_times_simps(1)) |
|
2432 |
|
2433 lemma fls_inverse_X_intpow': |
|
2434 assumes "inverse 1 = (1::'a::{semiring_1,uminus,inverse})" |
|
2435 shows "inverse (fls_X_intpow i :: 'a fls) = fls_X_intpow (-i)" |
|
2436 using fls_lr_inverse_X_intpow'(2)[of i 1] |
|
2437 by (simp add: fls_inverse_def' assms) |
|
2438 |
|
2439 lemma fls_inverse_X_intpow: |
|
2440 "inverse (fls_X_intpow i :: 'a::division_ring fls) = fls_X_intpow (-i)" |
|
2441 by (simp add: fls_inverse_X_intpow') |
|
2442 |
|
2443 lemma fls_left_inverse: |
|
2444 fixes f :: "'a::ring_1 fls" |
|
2445 assumes "x * f $$ fls_subdegree f = 1" |
|
2446 shows "fls_left_inverse f x * f = 1" |
|
2447 proof- |
|
2448 from assms have "x \<noteq> 0" "x * (fls_base_factor_to_fps f$0) = 1" by auto |
|
2449 thus ?thesis |
|
2450 using fls_base_factor_to_fps_left_inverse[of f x] |
|
2451 fls_lr_inverse_subdegree(1)[of x] fps_left_inverse |
|
2452 by (fastforce simp: fls_times_def) |
|
2453 qed |
|
2454 |
|
2455 lemma fls_right_inverse: |
|
2456 fixes f :: "'a::ring_1 fls" |
|
2457 assumes "f $$ fls_subdegree f * y = 1" |
|
2458 shows "f * fls_right_inverse f y = 1" |
|
2459 proof- |
|
2460 from assms have "y \<noteq> 0" "(fls_base_factor_to_fps f$0) * y = 1" by auto |
|
2461 thus ?thesis |
|
2462 using fls_base_factor_to_fps_right_inverse[of f y] |
|
2463 fls_lr_inverse_subdegree(2)[of y] fps_right_inverse |
|
2464 by (fastforce simp: fls_times_def) |
|
2465 qed |
|
2466 |
|
2467 \<comment> \<open> |
|
2468 It is possible in a ring for an element to have a left inverse but not a right inverse, or |
|
2469 vice versa. But when an element has both, they must be the same. |
|
2470 \<close> |
|
2471 lemma fls_left_inverse_eq_fls_right_inverse: |
|
2472 fixes f :: "'a::ring_1 fls" |
|
2473 assumes "x * f $$ fls_subdegree f = 1" "f $$ fls_subdegree f * y = 1" |
|
2474 \<comment> \<open>These assumptions imply x equals y, but no need to assume that.\<close> |
|
2475 shows "fls_left_inverse f x = fls_right_inverse f y" |
|
2476 using assms |
|
2477 by (simp add: fps_left_inverse_eq_fps_right_inverse) |
|
2478 |
|
2479 lemma fls_left_inverse_eq_inverse: |
|
2480 fixes f :: "'a::division_ring fls" |
|
2481 shows "fls_left_inverse f (inverse (f $$ fls_subdegree f)) = inverse f" |
|
2482 proof (cases "f=0") |
|
2483 case True |
|
2484 hence "fls_left_inverse f (inverse (f $$ fls_subdegree f)) = fls_const (0::'a)" |
|
2485 by (simp add: fls_lr_inverse_zero(1)[symmetric]) |
|
2486 with True show ?thesis by simp |
|
2487 next |
|
2488 case False thus ?thesis |
|
2489 using fls_left_inverse_eq_fls_right_inverse[of "inverse (f $$ fls_subdegree f)"] |
|
2490 by (auto simp add: fls_inverse_def') |
|
2491 qed |
|
2492 |
|
2493 lemma fls_right_inverse_eq_inverse: |
|
2494 fixes f :: "'a::division_ring fls" |
|
2495 shows "fls_right_inverse f (inverse (f $$ fls_subdegree f)) = inverse f" |
|
2496 proof (cases "f=0") |
|
2497 case True |
|
2498 hence "fls_right_inverse f (inverse (f $$ fls_subdegree f)) = fls_const (0::'a)" |
|
2499 by (simp add: fls_lr_inverse_zero(2)[symmetric]) |
|
2500 with True show ?thesis by simp |
|
2501 qed (simp add: fls_inverse_def') |
|
2502 |
|
2503 lemma fls_left_inverse_eq_fls_right_inverse_comm: |
|
2504 fixes f :: "'a::comm_ring_1 fls" |
|
2505 assumes "x * f $$ fls_subdegree f = 1" |
|
2506 shows "fls_left_inverse f x = fls_right_inverse f x" |
|
2507 using assms fls_left_inverse_eq_fls_right_inverse[of x f x] |
|
2508 by (simp add: mult.commute) |
|
2509 |
|
2510 lemma fls_left_inverse': |
|
2511 fixes f :: "'a::ring_1 fls" |
|
2512 assumes "x * f $$ fls_subdegree f = 1" "f $$ fls_subdegree f * y = 1" |
|
2513 \<comment> \<open>These assumptions imply x equals y, but no need to assume that.\<close> |
|
2514 shows "fls_right_inverse f y * f = 1" |
|
2515 using assms fls_left_inverse_eq_fls_right_inverse[of x f y] fls_left_inverse[of x f] |
|
2516 by simp |
|
2517 |
|
2518 lemma fls_right_inverse': |
|
2519 fixes f :: "'a::ring_1 fls" |
|
2520 assumes "x * f $$ fls_subdegree f = 1" "f $$ fls_subdegree f * y = 1" |
|
2521 \<comment> \<open>These assumptions imply x equals y, but no need to assume that.\<close> |
|
2522 shows "f * fls_left_inverse f x = 1" |
|
2523 using assms fls_left_inverse_eq_fls_right_inverse[of x f y] fls_right_inverse[of f y] |
|
2524 by simp |
|
2525 |
|
2526 lemma fls_mult_left_inverse_base_factor: |
|
2527 fixes f :: "'a::ring_1 fls" |
|
2528 assumes "x * (f $$ fls_subdegree f) = 1" |
|
2529 shows "fls_left_inverse (fls_base_factor f) x * f = fls_X_intpow (fls_subdegree f)" |
|
2530 using assms fls_base_factor_to_fps_base_factor[of f] fls_base_factor_subdegree[of f] |
|
2531 fls_shifted_times_simps(2)[of "-fls_subdegree f" "fls_left_inverse f x" f] |
|
2532 fls_left_inverse[of x f] |
|
2533 by simp |
|
2534 |
|
2535 lemma fls_mult_right_inverse_base_factor: |
|
2536 fixes f :: "'a::ring_1 fls" |
|
2537 assumes "(f $$ fls_subdegree f) * y = 1" |
|
2538 shows "f * fls_right_inverse (fls_base_factor f) y = fls_X_intpow (fls_subdegree f)" |
|
2539 using assms fls_base_factor_to_fps_base_factor[of f] fls_base_factor_subdegree[of f] |
|
2540 fls_shifted_times_simps(1)[of f "-fls_subdegree f" "fls_right_inverse f y"] |
|
2541 fls_right_inverse[of f y] |
|
2542 by simp |
|
2543 |
|
2544 lemma fls_mult_inverse_base_factor: |
|
2545 fixes f :: "'a::division_ring fls" |
|
2546 assumes "f \<noteq> 0" |
|
2547 shows "f * inverse (fls_base_factor f) = fls_X_intpow (fls_subdegree f)" |
|
2548 using fls_mult_right_inverse_base_factor[of f "inverse (f $$ fls_subdegree f)"] |
|
2549 fls_base_factor_base[of f] |
|
2550 by (simp add: assms fls_right_inverse_eq_inverse[symmetric]) |
|
2551 |
|
2552 lemma fls_left_inverse_idempotent_ring1: |
|
2553 fixes f :: "'a::ring_1 fls" |
|
2554 assumes "x * f $$ fls_subdegree f = 1" "y * x = 1" |
|
2555 \<comment> \<open>These assumptions imply y equals f $$ fls_subdegree f, but no need to assume that.\<close> |
|
2556 shows "fls_left_inverse (fls_left_inverse f x) y = f" |
|
2557 proof- |
|
2558 from assms(1) have |
|
2559 "fls_left_inverse (fls_left_inverse f x) y * fls_left_inverse f x * f = |
|
2560 fls_left_inverse (fls_left_inverse f x) y" |
|
2561 using fls_left_inverse[of x f] |
|
2562 by (simp add: mult.assoc) |
|
2563 moreover have |
|
2564 "fls_left_inverse (fls_left_inverse f x) y * fls_left_inverse f x = 1" |
|
2565 using assms fls_lr_inverse_subdegree(1)[of x f] fls_lr_inverse_base(1)[of f x] |
|
2566 by (fastforce intro: fls_left_inverse) |
|
2567 ultimately show ?thesis by simp |
|
2568 qed |
|
2569 |
|
2570 lemma fls_left_inverse_idempotent_comm_ring1: |
|
2571 fixes f :: "'a::comm_ring_1 fls" |
|
2572 assumes "x * f $$ fls_subdegree f = 1" |
|
2573 shows "fls_left_inverse (fls_left_inverse f x) (f $$ fls_subdegree f) = f" |
|
2574 using assms fls_left_inverse_idempotent_ring1[of x f "f $$ fls_subdegree f"] |
|
2575 by (simp add: mult.commute) |
|
2576 |
|
2577 lemma fls_right_inverse_idempotent_ring1: |
|
2578 fixes f :: "'a::ring_1 fls" |
|
2579 assumes "f $$ fls_subdegree f * x = 1" "x * y = 1" |
|
2580 \<comment> \<open>These assumptions imply y equals f $$ fls_subdegree f, but no need to assume that.\<close> |
|
2581 shows "fls_right_inverse (fls_right_inverse f x) y = f" |
|
2582 proof- |
|
2583 from assms(1) have |
|
2584 "f * (fls_right_inverse f x * fls_right_inverse (fls_right_inverse f x) y) = |
|
2585 fls_right_inverse (fls_right_inverse f x) y" |
|
2586 using fls_right_inverse [of f] |
|
2587 by (simp add: mult.assoc[symmetric]) |
|
2588 moreover have |
|
2589 "fls_right_inverse f x * fls_right_inverse (fls_right_inverse f x) y = 1" |
|
2590 using assms fls_lr_inverse_subdegree(2)[of x f] fls_lr_inverse_base(2)[of f x] |
|
2591 by (fastforce intro: fls_right_inverse) |
|
2592 ultimately show ?thesis by simp |
|
2593 qed |
|
2594 |
|
2595 lemma fls_right_inverse_idempotent_comm_ring1: |
|
2596 fixes f :: "'a::comm_ring_1 fls" |
|
2597 assumes "f $$ fls_subdegree f * x = 1" |
|
2598 shows "fls_right_inverse (fls_right_inverse f x) (f $$ fls_subdegree f) = f" |
|
2599 using assms fls_right_inverse_idempotent_ring1[of f x "f $$ fls_subdegree f"] |
|
2600 by (simp add: mult.commute) |
|
2601 |
|
2602 lemma fls_lr_inverse_unique_ring1: |
|
2603 fixes f g :: "'a :: ring_1 fls" |
|
2604 assumes fg: "f * g = 1" "g $$ fls_subdegree g * f $$ fls_subdegree f = 1" |
|
2605 shows "fls_left_inverse g (f $$ fls_subdegree f) = f" |
|
2606 and "fls_right_inverse f (g $$ fls_subdegree g) = g" |
|
2607 proof- |
|
2608 |
|
2609 have "f $$ fls_subdegree f * g $$ fls_subdegree g \<noteq> 0" |
|
2610 proof |
|
2611 assume "f $$ fls_subdegree f * g $$ fls_subdegree g = 0" |
|
2612 hence "f $$ fls_subdegree f * (g $$ fls_subdegree g * f $$ fls_subdegree f) = 0" |
|
2613 by (simp add: mult.assoc[symmetric]) |
|
2614 with fg(2) show False by simp |
|
2615 qed |
|
2616 with fg(1) have subdeg_sum: "fls_subdegree f + fls_subdegree g = 0" |
|
2617 using fls_mult_nonzero_base_subdegree_eq[of f g] by simp |
|
2618 hence subdeg_sum': |
|
2619 "fls_subdegree f = -fls_subdegree g" "fls_subdegree g = -fls_subdegree f" |
|
2620 by auto |
|
2621 |
|
2622 from fg(1) have f_ne_0: "f\<noteq>0" by auto |
|
2623 moreover have |
|
2624 "fps_left_inverse (fls_base_factor_to_fps g) (fls_regpart (fls_shift (-fls_subdegree g) f)$0) |
|
2625 = fls_regpart (fls_shift (-fls_subdegree g) f)" |
|
2626 proof (intro fps_lr_inverse_unique_ring1(1)) |
|
2627 from fg(1) show |
|
2628 "fls_regpart (fls_shift (-fls_subdegree g) f) * fls_base_factor_to_fps g = 1" |
|
2629 using f_ne_0 fls_times_conv_regpart[of "fls_shift (-fls_subdegree g) f" "fls_base_factor g"] |
|
2630 fls_base_factor_subdegree[of g] |
|
2631 by (simp add: fls_times_both_shifted_simp subdeg_sum) |
|
2632 from fg(2) show |
|
2633 "fls_base_factor_to_fps g $ 0 * fls_regpart (fls_shift (-fls_subdegree g) f) $ 0 = 1" |
|
2634 by (simp add: subdeg_sum'(2)) |
|
2635 qed |
|
2636 ultimately show "fls_left_inverse g (f $$ fls_subdegree f) = f" |
|
2637 by (simp add: subdeg_sum'(2)) |
|
2638 |
|
2639 from fg(1) have g_ne_0: "g\<noteq>0" by auto |
|
2640 moreover have |
|
2641 "fps_right_inverse (fls_base_factor_to_fps f) (fls_regpart (fls_shift (-fls_subdegree f) g)$0) |
|
2642 = fls_regpart (fls_shift (-fls_subdegree f) g)" |
|
2643 proof (intro fps_lr_inverse_unique_ring1(2)) |
|
2644 from fg(1) show |
|
2645 "fls_base_factor_to_fps f * fls_regpart (fls_shift (-fls_subdegree f) g) = 1" |
|
2646 using g_ne_0 fls_times_conv_regpart[of "fls_base_factor f" "fls_shift (-fls_subdegree f) g"] |
|
2647 fls_base_factor_subdegree[of f] |
|
2648 by (simp add: fls_times_both_shifted_simp subdeg_sum add.commute) |
|
2649 from fg(2) show |
|
2650 "fls_regpart (fls_shift (-fls_subdegree f) g) $ 0 * fls_base_factor_to_fps f $ 0 = 1" |
|
2651 by (simp add: subdeg_sum'(1)) |
|
2652 qed |
|
2653 ultimately show "fls_right_inverse f (g $$ fls_subdegree g) = g" |
|
2654 by (simp add: subdeg_sum'(2)) |
|
2655 |
|
2656 qed |
|
2657 |
|
2658 lemma fls_lr_inverse_unique_divring: |
|
2659 fixes f g :: "'a ::division_ring fls" |
|
2660 assumes fg: "f * g = 1" |
|
2661 shows "fls_left_inverse g (f $$ fls_subdegree f) = f" |
|
2662 and "fls_right_inverse f (g $$ fls_subdegree g) = g" |
|
2663 proof- |
|
2664 from fg have "f \<noteq>0" "g \<noteq> 0" by auto |
|
2665 with fg have "fls_subdegree f + fls_subdegree g = 0" using fls_subdegree_mult by force |
|
2666 with fg have "f $$ fls_subdegree f * g $$ fls_subdegree g = 1" |
|
2667 using fls_times_base[of f g] by simp |
|
2668 hence "g $$ fls_subdegree g * f $$ fls_subdegree f = 1" |
|
2669 using inverse_unique[of "f $$ fls_subdegree f"] left_inverse[of "f $$ fls_subdegree f"] |
|
2670 by force |
|
2671 thus |
|
2672 "fls_left_inverse g (f $$ fls_subdegree f) = f" |
|
2673 "fls_right_inverse f (g $$ fls_subdegree g) = g" |
|
2674 using fg fls_lr_inverse_unique_ring1 |
|
2675 by auto |
|
2676 qed |
|
2677 |
|
2678 lemma fls_lr_inverse_minus: |
|
2679 fixes f :: "'a::ring_1 fls" |
|
2680 shows "fls_left_inverse (-f) (-x) = - fls_left_inverse f x" |
|
2681 and "fls_right_inverse (-f) (-x) = - fls_right_inverse f x" |
|
2682 by (simp_all add: fps_lr_inverse_minus) |
|
2683 |
|
2684 lemma fls_inverse_minus [simp]: "inverse (-f) = -inverse (f :: 'a :: division_ring fls)" |
|
2685 using fls_lr_inverse_minus(2)[of f] by (simp add: fls_inverse_def') |
|
2686 |
|
2687 lemma fls_lr_inverse_mult_ring1: |
|
2688 fixes f g :: "'a::ring_1 fls" |
|
2689 assumes x: "x * f $$ fls_subdegree f = 1" "f $$ fls_subdegree f * x = 1" |
|
2690 and y: "y * g $$ fls_subdegree g = 1" "g $$ fls_subdegree g * y = 1" |
|
2691 shows "fls_left_inverse (f * g) (y*x) = fls_left_inverse g y * fls_left_inverse f x" |
|
2692 and "fls_right_inverse (f * g) (y*x) = fls_right_inverse g y * fls_right_inverse f x" |
|
2693 proof- |
|
2694 from x(1) y(2) have "x * (f $$ fls_subdegree f * g $$ fls_subdegree g) * y = 1" |
|
2695 by (simp add: mult.assoc) |
|
2696 hence base_prod: "f $$ fls_subdegree f * g $$ fls_subdegree g \<noteq> 0" by auto |
|
2697 hence subdegrees: "fls_subdegree (f*g) = fls_subdegree f + fls_subdegree g" |
|
2698 using fls_mult_nonzero_base_subdegree_eq[of f g] by simp |
|
2699 |
|
2700 have norm: |
|
2701 "fls_base_factor_to_fps (f * g) = fls_base_factor_to_fps f * fls_base_factor_to_fps g" |
|
2702 using base_prod fls_base_factor_to_fps_mult'[of f g] by simp |
|
2703 |
|
2704 have |
|
2705 "fls_left_inverse (f * g) (y*x) = |
|
2706 fls_shift (fls_subdegree (f * g)) ( |
|
2707 fps_to_fls ( |
|
2708 fps_left_inverse (fls_base_factor_to_fps f * fls_base_factor_to_fps g) (y*x) |
|
2709 ) |
|
2710 ) |
|
2711 " |
|
2712 using norm |
|
2713 by simp |
|
2714 thus "fls_left_inverse (f * g) (y*x) = fls_left_inverse g y * fls_left_inverse f x" |
|
2715 using x y |
|
2716 fps_lr_inverse_mult_ring1(1)[of |
|
2717 x "fls_base_factor_to_fps f" y "fls_base_factor_to_fps g" |
|
2718 ] |
|
2719 by (simp add: |
|
2720 fls_times_both_shifted_simp fls_times_fps_to_fls subdegrees algebra_simps |
|
2721 ) |
|
2722 |
|
2723 have |
|
2724 "fls_right_inverse (f * g) (y*x) = |
|
2725 fls_shift (fls_subdegree (f * g)) ( |
|
2726 fps_to_fls ( |
|
2727 fps_right_inverse (fls_base_factor_to_fps f * fls_base_factor_to_fps g) (y*x) |
|
2728 ) |
|
2729 ) |
|
2730 " |
|
2731 using norm |
|
2732 by simp |
|
2733 thus "fls_right_inverse (f * g) (y*x) = fls_right_inverse g y * fls_right_inverse f x" |
|
2734 using x y |
|
2735 fps_lr_inverse_mult_ring1(2)[of |
|
2736 x "fls_base_factor_to_fps f" y "fls_base_factor_to_fps g" |
|
2737 ] |
|
2738 by (simp add: |
|
2739 fls_times_both_shifted_simp fls_times_fps_to_fls subdegrees algebra_simps |
|
2740 ) |
|
2741 |
|
2742 qed |
|
2743 |
|
2744 lemma fls_lr_inverse_power_ring1: |
|
2745 fixes f :: "'a::ring_1 fls" |
|
2746 assumes x: "x * f $$ fls_subdegree f = 1" "f $$ fls_subdegree f * x = 1" |
|
2747 shows "fls_left_inverse (f ^ n) (x ^ n) = (fls_left_inverse f x) ^ n" |
|
2748 "fls_right_inverse (f ^ n) (x ^ n) = (fls_right_inverse f x) ^ n" |
|
2749 proof- |
|
2750 |
|
2751 show "fls_left_inverse (f ^ n) (x ^ n) = (fls_left_inverse f x) ^ n" |
|
2752 proof (induct n) |
|
2753 case 0 show ?case using fls_lr_inverse_one(1)[of 1] by simp |
|
2754 next |
|
2755 case (Suc n) with assms show ?case |
|
2756 using fls_lr_inverse_mult_ring1(1)[of x f "x^n" "f^n"] |
|
2757 by (simp add: |
|
2758 power_Suc2[symmetric] fls_unit_base_subdegree_power(1) left_right_inverse_power |
|
2759 ) |
|
2760 qed |
|
2761 |
|
2762 show "fls_right_inverse (f ^ n) (x ^ n) = (fls_right_inverse f x) ^ n" |
|
2763 proof (induct n) |
|
2764 case 0 show ?case using fls_lr_inverse_one(2)[of 1] by simp |
|
2765 next |
|
2766 case (Suc n) with assms show ?case |
|
2767 using fls_lr_inverse_mult_ring1(2)[of x f "x^n" "f^n"] |
|
2768 by (simp add: |
|
2769 power_Suc2[symmetric] fls_unit_base_subdegree_power(1) left_right_inverse_power |
|
2770 ) |
|
2771 qed |
|
2772 |
|
2773 qed |
|
2774 |
|
2775 lemma fls_divide_convert_times_inverse: |
|
2776 fixes f g :: "'a::{comm_monoid_add,inverse,mult_zero,uminus} fls" |
|
2777 shows "f / g = f * inverse g" |
|
2778 using fls_base_factor_to_fps_subdegree[of g] fps_to_fls_base_factor_to_fps[of f] |
|
2779 fls_times_both_shifted_simp[of "-fls_subdegree f" "fls_base_factor f"] |
|
2780 by (simp add: |
|
2781 fls_divide_def fps_divide_unit' fls_times_fps_to_fls |
|
2782 fls_conv_base_factor_shift_subdegree fls_inverse_def |
|
2783 ) |
|
2784 |
|
2785 instance fls :: (division_ring) division_ring |
|
2786 proof |
|
2787 fix a b :: "'a fls" |
|
2788 show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" |
|
2789 using fls_left_inverse'[of "inverse (a $$ fls_subdegree a)" a] |
|
2790 by (simp add: fls_inverse_def') |
|
2791 show "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1" |
|
2792 using fls_right_inverse[of a] |
|
2793 by (simp add: fls_inverse_def') |
|
2794 show "a / b = a * inverse b" using fls_divide_convert_times_inverse by fast |
|
2795 show "inverse (0::'a fls) = 0" by simp |
|
2796 qed |
|
2797 |
|
2798 lemma fls_lr_inverse_mult_divring: |
|
2799 fixes f g :: "'a::division_ring fls" |
|
2800 and df dg :: int |
|
2801 defines "df \<equiv> fls_subdegree f" |
|
2802 and "dg \<equiv> fls_subdegree g" |
|
2803 shows "fls_left_inverse (f*g) (inverse ((f*g)$$(df+dg))) = |
|
2804 fls_left_inverse g (inverse (g$$dg)) * fls_left_inverse f (inverse (f$$df))" |
|
2805 and "fls_right_inverse (f*g) (inverse ((f*g)$$(df+dg))) = |
|
2806 fls_right_inverse g (inverse (g$$dg)) * fls_right_inverse f (inverse (f$$df))" |
|
2807 proof - |
|
2808 show |
|
2809 "fls_left_inverse (f*g) (inverse ((f*g)$$(df+dg))) = |
|
2810 fls_left_inverse g (inverse (g$$dg)) * fls_left_inverse f (inverse (f$$df))" |
|
2811 proof (cases "f=0 \<or> g=0") |
|
2812 case True thus ?thesis |
|
2813 using fls_lr_inverse_zero(1)[of "inverse (0::'a)"] by (auto simp add: assms) |
|
2814 next |
|
2815 case False thus ?thesis |
|
2816 using fls_left_inverse_eq_inverse[of "f*g"] nonzero_inverse_mult_distrib[of f g] |
|
2817 fls_left_inverse_eq_inverse[of g] fls_left_inverse_eq_inverse[of f] |
|
2818 by (simp add: assms) |
|
2819 qed |
|
2820 show |
|
2821 "fls_right_inverse (f*g) (inverse ((f*g)$$(df+dg))) = |
|
2822 fls_right_inverse g (inverse (g$$dg)) * fls_right_inverse f (inverse (f$$df))" |
|
2823 proof (cases "f=0 \<or> g=0") |
|
2824 case True thus ?thesis |
|
2825 using fls_lr_inverse_zero(2)[of "inverse (0::'a)"] by (auto simp add: assms) |
|
2826 next |
|
2827 case False thus ?thesis |
|
2828 using fls_inverse_def'[of "f*g"] nonzero_inverse_mult_distrib[of f g] |
|
2829 fls_inverse_def'[of g] fls_inverse_def'[of f] |
|
2830 by (simp add: assms) |
|
2831 qed |
|
2832 qed |
|
2833 |
|
2834 lemma fls_lr_inverse_power_divring: |
|
2835 fixes f :: "'a::division_ring fls" |
|
2836 shows "fls_left_inverse (f ^ n) ((inverse (f $$ fls_subdegree f)) ^ n) = |
|
2837 (fls_left_inverse f (inverse (f $$ fls_subdegree f))) ^ n" |
|
2838 "fls_right_inverse (f ^ n) ((inverse (f $$ fls_subdegree f)) ^ n) = |
|
2839 (fls_right_inverse f (inverse (f $$ fls_subdegree f))) ^ n" |
|
2840 proof - |
|
2841 have |
|
2842 "fls_right_inverse (f ^ n) ((inverse (f $$ fls_subdegree f)) ^ n) = |
|
2843 inverse f ^ n" |
|
2844 "fls_left_inverse (f ^ n) ((inverse (f $$ fls_subdegree f)) ^ n) = |
|
2845 inverse f ^ n" |
|
2846 using fls_left_inverse_eq_inverse[of "f^n"] fls_right_inverse_eq_inverse[of "f^n"] |
|
2847 by (auto simp add: divide_simps fls_subdegree_pow) |
|
2848 thus |
|
2849 "fls_left_inverse (f ^ n) ((inverse (f $$ fls_subdegree f)) ^ n) = |
|
2850 (fls_left_inverse f (inverse (f $$ fls_subdegree f))) ^ n" |
|
2851 "fls_right_inverse (f ^ n) ((inverse (f $$ fls_subdegree f)) ^ n) = |
|
2852 (fls_right_inverse f (inverse (f $$ fls_subdegree f))) ^ n" |
|
2853 using fls_left_inverse_eq_inverse[of f] fls_right_inverse_eq_inverse[of f] |
|
2854 by auto |
|
2855 qed |
|
2856 |
|
2857 instance fls :: (field) field |
|
2858 by (standard, simp_all add: field_simps) |
|
2859 |
|
2860 |
|
2861 subsubsection \<open>Division\<close> |
|
2862 |
|
2863 lemma fls_divide_nth_below: |
|
2864 fixes f g :: "'a::{comm_monoid_add,uminus,times,inverse} fls" |
|
2865 shows "n < fls_subdegree f - fls_subdegree g \<Longrightarrow> (f div g) $$ n = 0" |
|
2866 by (simp add: fls_divide_def) |
|
2867 |
|
2868 lemma fls_divide_nth_base: |
|
2869 fixes f g :: "'a::division_ring fls" |
|
2870 shows |
|
2871 "(f div g) $$ (fls_subdegree f - fls_subdegree g) = |
|
2872 f $$ fls_subdegree f / g $$ fls_subdegree g" |
|
2873 using fps_divide_nth_0'[of "fls_base_factor_to_fps g" "fls_base_factor_to_fps f"] |
|
2874 fls_base_factor_to_fps_subdegree[of g] |
|
2875 by (simp add: fls_divide_def) |
|
2876 |
|
2877 lemma fls_div_zero [simp]: |
|
2878 "0 div (g :: 'a :: {comm_monoid_add,inverse,mult_zero,uminus} fls) = 0" |
|
2879 by (simp add: fls_divide_def) |
|
2880 |
|
2881 lemma fls_div_by_zero: |
|
2882 fixes g :: "'a::{comm_monoid_add,inverse,mult_zero,uminus} fls" |
|
2883 assumes "inverse (0::'a) = 0" |
|
2884 shows "g div 0 = 0" |
|
2885 by (simp add: fls_divide_def assms fps_div_by_zero') |
|
2886 |
|
2887 lemma fls_divide_times: |
|
2888 fixes f g :: "'a::{semiring_0,inverse,uminus} fls" |
|
2889 shows "(f * g) / h = f * (g / h)" |
|
2890 by (simp add: fls_divide_convert_times_inverse mult.assoc) |
|
2891 |
|
2892 lemma fls_divide_times2: |
|
2893 fixes f g :: "'a::{comm_semiring_0,inverse,uminus} fls" |
|
2894 shows "(f * g) / h = (f / h) * g" |
|
2895 using fls_divide_times[of g f h] |
|
2896 by (simp add: mult.commute) |
|
2897 |
|
2898 lemma fls_divide_subdegree_ge: |
|
2899 fixes f g :: "'a::{comm_monoid_add,uminus,times,inverse} fls" |
|
2900 assumes "f / g \<noteq> 0" |
|
2901 shows "fls_subdegree (f / g) \<ge> fls_subdegree f - fls_subdegree g" |
|
2902 using assms fls_divide_nth_below |
|
2903 by (intro fls_subdegree_geI) simp |
|
2904 |
|
2905 lemma fls_divide_subdegree: |
|
2906 fixes f g :: "'a::division_ring fls" |
|
2907 assumes "f \<noteq> 0" "g \<noteq> 0" |
|
2908 shows "fls_subdegree (f / g) = fls_subdegree f - fls_subdegree g" |
|
2909 proof (intro antisym) |
|
2910 from assms have "f $$ fls_subdegree f / g $$ fls_subdegree g \<noteq> 0" by (simp add: field_simps) |
|
2911 thus "fls_subdegree (f/g) \<le> fls_subdegree f - fls_subdegree g" |
|
2912 using fls_divide_nth_base[of f g] by (intro fls_subdegree_leI) simp |
|
2913 from assms have "f / g \<noteq> 0" by (simp add: field_simps) |
|
2914 thus "fls_subdegree (f/g) \<ge> fls_subdegree f - fls_subdegree g" |
|
2915 using fls_divide_subdegree_ge by fast |
|
2916 qed |
|
2917 |
|
2918 lemma fls_divide_shift_numer_nonzero: |
|
2919 fixes f g :: "'a :: {comm_monoid_add,inverse,times,uminus} fls" |
|
2920 assumes "f \<noteq> 0" |
|
2921 shows "fls_shift m f / g = fls_shift m (f/g)" |
|
2922 using assms fls_base_factor_to_fps_shift[of m f] |
|
2923 by (simp add: fls_divide_def algebra_simps) |
|
2924 |
|
2925 lemma fls_divide_shift_numer: |
|
2926 fixes f g :: "'a :: {comm_monoid_add,inverse,mult_zero,uminus} fls" |
|
2927 shows "fls_shift m f / g = fls_shift m (f/g)" |
|
2928 using fls_divide_shift_numer_nonzero |
|
2929 by (cases "f=0") auto |
|
2930 |
|
2931 lemma fls_divide_shift_denom_nonzero: |
|
2932 fixes f g :: "'a :: {comm_monoid_add,inverse,times,uminus} fls" |
|
2933 assumes "g \<noteq> 0" |
|
2934 shows "f / fls_shift m g = fls_shift (-m) (f/g)" |
|
2935 using assms fls_base_factor_to_fps_shift[of m g] |
|
2936 by (simp add: fls_divide_def algebra_simps) |
|
2937 |
|
2938 lemma fls_divide_shift_denom: |
|
2939 fixes f g :: "'a :: division_ring fls" |
|
2940 shows "f / fls_shift m g = fls_shift (-m) (f/g)" |
|
2941 using fls_divide_shift_denom_nonzero |
|
2942 by (cases "g=0") auto |
|
2943 |
|
2944 lemma fls_divide_shift_both_nonzero: |
|
2945 fixes f g :: "'a :: {comm_monoid_add,inverse,times,uminus} fls" |
|
2946 assumes "f \<noteq> 0" "g \<noteq> 0" |
|
2947 shows "fls_shift n f / fls_shift m g = fls_shift (n-m) (f/g)" |
|
2948 by (simp add: assms fls_divide_shift_numer_nonzero fls_divide_shift_denom_nonzero) |
|
2949 |
|
2950 lemma fls_divide_shift_both [simp]: |
|
2951 fixes f g :: "'a :: division_ring fls" |
|
2952 shows "fls_shift n f / fls_shift m g = fls_shift (n-m) (f/g)" |
|
2953 using fls_divide_shift_both_nonzero |
|
2954 by (cases "f=0 \<or> g=0") auto |
|
2955 |
|
2956 lemma fls_divide_base_factor_numer: |
|
2957 "fls_base_factor f / g = fls_shift (fls_subdegree f) (f/g)" |
|
2958 using fls_base_factor_to_fps_base_factor[of f] |
|
2959 fls_base_factor_subdegree[of f] |
|
2960 by (simp add: fls_divide_def algebra_simps) |
|
2961 |
|
2962 lemma fls_divide_base_factor_denom: |
|
2963 "f / fls_base_factor g = fls_shift (-fls_subdegree g) (f/g)" |
|
2964 using fls_base_factor_to_fps_base_factor[of g] |
|
2965 fls_base_factor_subdegree[of g] |
|
2966 by (simp add: fls_divide_def) |
|
2967 |
|
2968 lemma fls_divide_base_factor': |
|
2969 "fls_base_factor f / fls_base_factor g = fls_shift (fls_subdegree f - fls_subdegree g) (f/g)" |
|
2970 using fls_divide_base_factor_numer[of f "fls_base_factor g"] |
|
2971 fls_divide_base_factor_denom[of f g] |
|
2972 by simp |
|
2973 |
|
2974 lemma fls_divide_base_factor: |
|
2975 fixes f g :: "'a :: division_ring fls" |
|
2976 shows "fls_base_factor f / fls_base_factor g = fls_base_factor (f/g)" |
|
2977 using fls_divide_subdegree[of f g] fls_divide_base_factor' |
|
2978 by fastforce |
|
2979 |
|
2980 lemma fls_divide_regpart: |
|
2981 fixes f g :: "'a::{inverse,comm_monoid_add,uminus,mult_zero} fls" |
|
2982 assumes "fls_subdegree f \<ge> 0" "fls_subdegree g \<ge> 0" |
|
2983 shows "fls_regpart (f / g) = fls_regpart f / fls_regpart g" |
|
2984 proof - |
|
2985 have deg0: |
|
2986 "\<And>g. fls_subdegree g = 0 \<Longrightarrow> |
|
2987 fls_regpart (f / g) = fls_regpart f / fls_regpart g" |
|
2988 by (simp add: |
|
2989 assms(1) fls_divide_convert_times_inverse fls_inverse_subdegree_0 |
|
2990 fls_times_conv_regpart fls_inverse_regpart fls_regpart_subdegree_conv fps_divide_unit' |
|
2991 ) |
|
2992 show ?thesis |
|
2993 proof (cases "fls_subdegree g = 0") |
|
2994 case False |
|
2995 hence "fls_base_factor g \<noteq> 0" using fls_base_factor_nonzero[of g] by force |
|
2996 with assms(2) show ?thesis |
|
2997 using fls_divide_shift_denom_nonzero[of "fls_base_factor g" f "-fls_subdegree g"] |
|
2998 fps_shift_fls_regpart_conv_fls_shift[of |
|
2999 "nat (fls_subdegree g)" "f / fls_base_factor g" |
|
3000 ] |
|
3001 fls_base_factor_subdegree[of g] deg0 |
|
3002 fls_regpart_subdegree_conv[of g] fps_unit_factor_fls_regpart[of g] |
|
3003 by (simp add: |
|
3004 fls_conv_base_factor_shift_subdegree fls_regpart_subdegree_conv fps_divide_def |
|
3005 ) |
|
3006 qed (rule deg0) |
|
3007 qed |
|
3008 |
|
3009 lemma fls_divide_fls_base_factor_to_fps': |
|
3010 fixes f g :: "'a::{comm_monoid_add,uminus,inverse,mult_zero} fls" |
|
3011 shows |
|
3012 "fls_base_factor_to_fps f / fls_base_factor_to_fps g = |
|
3013 fls_regpart (fls_shift (fls_subdegree f - fls_subdegree g) (f / g))" |
|
3014 using fls_base_factor_subdegree[of f] fls_base_factor_subdegree[of g] |
|
3015 fls_divide_regpart[of "fls_base_factor f" "fls_base_factor g"] |
|
3016 fls_divide_base_factor'[of f g] |
|
3017 by simp |
|
3018 |
|
3019 lemma fls_divide_fls_base_factor_to_fps: |
|
3020 fixes f g :: "'a::division_ring fls" |
|
3021 shows "fls_base_factor_to_fps f / fls_base_factor_to_fps g = fls_base_factor_to_fps (f / g)" |
|
3022 using fls_divide_fls_base_factor_to_fps' fls_divide_subdegree[of f g] |
|
3023 by fastforce |
|
3024 |
|
3025 lemma fls_divide_fps_to_fls: |
|
3026 fixes f g :: "'a::{inverse,ab_group_add,mult_zero} fps" |
|
3027 assumes "subdegree f \<ge> subdegree g" |
|
3028 shows "fps_to_fls f / fps_to_fls g = fps_to_fls (f/g)" |
|
3029 proof- |
|
3030 have 1: |
|
3031 "fps_to_fls f / fps_to_fls g = |
|
3032 fls_shift (int (subdegree g)) (fps_to_fls (f * inverse (unit_factor g)))" |
|
3033 using fls_base_factor_to_fps_to_fls[of f] fls_base_factor_to_fps_to_fls[of g] |
|
3034 fls_subdegree_fls_to_fps[of f] fls_subdegree_fls_to_fps[of g] |
|
3035 fps_divide_def[of "unit_factor f" "unit_factor g"] |
|
3036 fls_times_fps_to_fls[of "unit_factor f" "inverse (unit_factor g)"] |
|
3037 fls_shifted_times_simps(2)[of "-int (subdegree f)" "fps_to_fls (unit_factor f)"] |
|
3038 fls_times_fps_to_fls[of f "inverse (unit_factor g)"] |
|
3039 by (simp add: fls_divide_def) |
|
3040 with assms show ?thesis |
|
3041 using fps_mult_subdegree_ge[of f "inverse (unit_factor g)"] |
|
3042 fps_shift_to_fls[of "subdegree g" "f * inverse (unit_factor g)"] |
|
3043 by (cases "f * inverse (unit_factor g) = 0") (simp_all add: fps_divide_def) |
|
3044 qed |
|
3045 |
|
3046 lemma fls_divide_1': |
|
3047 fixes f :: "'a::{comm_monoid_add,inverse,mult_zero,uminus,zero_neq_one,monoid_mult} fls" |
|
3048 assumes "inverse (1::'a) = 1" |
|
3049 shows "f / 1 = f" |
|
3050 using assms fls_conv_base_factor_to_fps_shift_subdegree[of f] |
|
3051 by (simp add: fls_divide_def fps_divide_1') |
|
3052 |
|
3053 lemma fls_divide_1 [simp]: "a / 1 = (a::'a::division_ring fls)" |
|
3054 by (rule fls_divide_1'[OF inverse_1]) |
|
3055 |
|
3056 lemma fls_const_divide_const: |
|
3057 fixes x y :: "'a::division_ring" |
|
3058 shows "fls_const x / fls_const y = fls_const (x/y)" |
|
3059 by (simp add: fls_divide_def fls_base_factor_to_fps_const fps_const_divide) |
|
3060 |
|
3061 lemma fls_divide_X': |
|
3062 fixes f :: "'a::{comm_monoid_add,inverse,mult_zero,uminus,zero_neq_one,monoid_mult} fls" |
|
3063 assumes "inverse (1::'a) = 1" |
|
3064 shows "f / fls_X = fls_shift 1 f" |
|
3065 proof- |
|
3066 from assms have |
|
3067 "f / fls_X = |
|
3068 fls_shift 1 (fls_shift (-fls_subdegree f) (fps_to_fls (fls_base_factor_to_fps f)))" |
|
3069 by (simp add: fls_divide_def fps_divide_1') |
|
3070 also have "\<dots> = fls_shift 1 f" |
|
3071 using fls_conv_base_factor_to_fps_shift_subdegree[of f] |
|
3072 by simp |
|
3073 finally show ?thesis by simp |
|
3074 qed |
|
3075 |
|
3076 lemma fls_divide_X [simp]: |
|
3077 fixes f :: "'a::division_ring fls" |
|
3078 shows "f / fls_X = fls_shift 1 f" |
|
3079 by (rule fls_divide_X'[OF inverse_1]) |
|
3080 |
|
3081 lemma fls_divide_X_power': |
|
3082 fixes f :: "'a::{semiring_1,inverse,uminus} fls" |
|
3083 assumes "inverse (1::'a) = 1" |
|
3084 shows "f / (fls_X ^ n) = fls_shift n f" |
|
3085 proof- |
|
3086 have "fls_base_factor_to_fps ((fls_X::'a fls) ^ n) = 1" by (rule fls_X_power_base_factor_to_fps) |
|
3087 with assms have |
|
3088 "f / (fls_X ^ n) = |
|
3089 fls_shift n (fls_shift (-fls_subdegree f) (fps_to_fls (fls_base_factor_to_fps f)))" |
|
3090 by (simp add: fls_divide_def fps_divide_1') |
|
3091 also have "\<dots> = fls_shift n f" |
|
3092 using fls_conv_base_factor_to_fps_shift_subdegree[of f] by simp |
|
3093 finally show ?thesis by simp |
|
3094 qed |
|
3095 |
|
3096 lemma fls_divide_X_power [simp]: |
|
3097 fixes f :: "'a::division_ring fls" |
|
3098 shows "f / (fls_X ^ n) = fls_shift n f" |
|
3099 by (rule fls_divide_X_power'[OF inverse_1]) |
|
3100 |
|
3101 lemma fls_divide_X_inv': |
|
3102 fixes f :: "'a::{comm_monoid_add,inverse,mult_zero,uminus,zero_neq_one,monoid_mult} fls" |
|
3103 assumes "inverse (1::'a) = 1" |
|
3104 shows "f / fls_X_inv = fls_shift (-1) f" |
|
3105 proof- |
|
3106 from assms have |
|
3107 "f / fls_X_inv = |
|
3108 fls_shift (-1) (fls_shift (-fls_subdegree f) (fps_to_fls (fls_base_factor_to_fps f)))" |
|
3109 by (simp add: fls_divide_def fps_divide_1' algebra_simps) |
|
3110 also have "\<dots> = fls_shift (-1) f" |
|
3111 using fls_conv_base_factor_to_fps_shift_subdegree[of f] |
|
3112 by simp |
|
3113 finally show ?thesis by simp |
|
3114 qed |
|
3115 |
|
3116 lemma fls_divide_X_inv [simp]: |
|
3117 fixes f :: "'a::division_ring fls" |
|
3118 shows "f / fls_X_inv = fls_shift (-1) f" |
|
3119 by (rule fls_divide_X_inv'[OF inverse_1]) |
|
3120 |
|
3121 lemma fls_divide_X_inv_power': |
|
3122 fixes f :: "'a::{semiring_1,inverse,uminus} fls" |
|
3123 assumes "inverse (1::'a) = 1" |
|
3124 shows "f / (fls_X_inv ^ n) = fls_shift (-int n) f" |
|
3125 proof- |
|
3126 have "fls_base_factor_to_fps ((fls_X_inv::'a fls) ^ n) = 1" |
|
3127 by (rule fls_X_inv_power_base_factor_to_fps) |
|
3128 with assms have |
|
3129 "f / (fls_X_inv ^ n) = |
|
3130 fls_shift (-int n + -fls_subdegree f) (fps_to_fls (fls_base_factor_to_fps f))" |
|
3131 by (simp add: fls_divide_def fps_divide_1') |
|
3132 also have |
|
3133 "\<dots> = fls_shift (-int n) (fls_shift (-fls_subdegree f) (fps_to_fls (fls_base_factor_to_fps f)))" |
|
3134 by (simp add: add.commute) |
|
3135 also have "\<dots> = fls_shift (-int n) f" |
|
3136 using fls_conv_base_factor_to_fps_shift_subdegree[of f] by simp |
|
3137 finally show ?thesis by simp |
|
3138 qed |
|
3139 |
|
3140 lemma fls_divide_X_inv_power [simp]: |
|
3141 fixes f :: "'a::division_ring fls" |
|
3142 shows "f / (fls_X_inv ^ n) = fls_shift (-int n) f" |
|
3143 by (rule fls_divide_X_inv_power'[OF inverse_1]) |
|
3144 |
|
3145 lemma fls_divide_X_intpow': |
|
3146 fixes f :: "'a::{semiring_1,inverse,uminus} fls" |
|
3147 assumes "inverse (1::'a) = 1" |
|
3148 shows "f / (fls_X_intpow i) = fls_shift i f" |
|
3149 using assms |
|
3150 by (simp add: fls_divide_shift_denom_nonzero fls_divide_1') |
|
3151 |
|
3152 lemma fls_divide_X_intpow_conv_times': |
|
3153 fixes f :: "'a::{semiring_1,inverse,uminus} fls" |
|
3154 assumes "inverse (1::'a) = 1" |
|
3155 shows "f / (fls_X_intpow i) = f * fls_X_intpow (-i)" |
|
3156 using assms fls_X_intpow_times_conv_shift(2)[of f "-i"] |
|
3157 by (simp add: fls_divide_X_intpow') |
|
3158 |
|
3159 lemma fls_divide_X_intpow: |
|
3160 fixes f :: "'a::division_ring fls" |
|
3161 shows "f / (fls_X_intpow i) = fls_shift i f" |
|
3162 by (rule fls_divide_X_intpow'[OF inverse_1]) |
|
3163 |
|
3164 lemma fls_divide_X_intpow_conv_times: |
|
3165 fixes f :: "'a::division_ring fls" |
|
3166 shows "f / (fls_X_intpow i) = f * fls_X_intpow (-i)" |
|
3167 by (rule fls_divide_X_intpow_conv_times'[OF inverse_1]) |
|
3168 |
|
3169 lemma fls_X_intpow_div_fls_X_intpow_semiring1: |
|
3170 assumes "inverse (1::'a::{semiring_1,inverse,uminus}) = 1" |
|
3171 shows "(fls_X_intpow i :: 'a fls) / fls_X_intpow j = fls_X_intpow (i-j)" |
|
3172 by (simp add: assms fls_divide_shift_both_nonzero fls_divide_1') |
|
3173 |
|
3174 lemma fls_X_intpow_div_fls_X_intpow: |
|
3175 "(fls_X_intpow i :: 'a::division_ring fls) / fls_X_intpow j = fls_X_intpow (i-j)" |
|
3176 by (rule fls_X_intpow_div_fls_X_intpow_semiring1[OF inverse_1]) |
|
3177 |
|
3178 lemma fls_divide_add: |
|
3179 fixes f g h :: "'a::{semiring_0,inverse,uminus} fls" |
|
3180 shows "(f + g) / h = f / h + g / h" |
|
3181 by (simp add: fls_divide_convert_times_inverse algebra_simps) |
|
3182 |
|
3183 lemma fls_divide_diff: |
|
3184 fixes f g h :: "'a::{ring,inverse} fls" |
|
3185 shows "(f - g) / h = f / h - g / h" |
|
3186 by (simp add: fls_divide_convert_times_inverse algebra_simps) |
|
3187 |
|
3188 lemma fls_divide_uminus: |
|
3189 fixes f g h :: "'a::{ring,inverse} fls" |
|
3190 shows "(- f) / g = - (f / g)" |
|
3191 by (simp add: fls_divide_convert_times_inverse) |
|
3192 |
|
3193 lemma fls_divide_uminus': |
|
3194 fixes f g h :: "'a::division_ring fls" |
|
3195 shows "f / (- g) = - (f / g)" |
|
3196 by (simp add: fls_divide_convert_times_inverse) |
|
3197 |
|
3198 |
|
3199 subsubsection \<open>Units\<close> |
|
3200 |
|
3201 lemma fls_is_left_unit_iff_base_is_left_unit: |
|
3202 fixes f :: "'a :: ring_1_no_zero_divisors fls" |
|
3203 shows "(\<exists>g. 1 = f * g) \<longleftrightarrow> (\<exists>k. 1 = f $$ fls_subdegree f * k)" |
|
3204 proof |
|
3205 assume "\<exists>g. 1 = f * g" |
|
3206 then obtain g where "1 = f * g" by fast |
|
3207 hence "1 = (f $$ fls_subdegree f) * (g $$ fls_subdegree g)" |
|
3208 using fls_subdegree_mult[of f g] fls_times_base[of f g] by fastforce |
|
3209 thus "\<exists>k. 1 = f $$ fls_subdegree f * k" by fast |
|
3210 next |
|
3211 assume "\<exists>k. 1 = f $$ fls_subdegree f * k" |
|
3212 then obtain k where "1 = f $$ fls_subdegree f * k" by fast |
|
3213 hence "1 = f * fls_right_inverse f k" |
|
3214 using fls_right_inverse by simp |
|
3215 thus "\<exists>g. 1 = f * g" by fast |
|
3216 qed |
|
3217 |
|
3218 lemma fls_is_right_unit_iff_base_is_right_unit: |
|
3219 fixes f :: "'a :: ring_1_no_zero_divisors fls" |
|
3220 shows "(\<exists>g. 1 = g * f) \<longleftrightarrow> (\<exists>k. 1 = k * f $$ fls_subdegree f)" |
|
3221 proof |
|
3222 assume "\<exists>g. 1 = g * f" |
|
3223 then obtain g where "1 = g * f" by fast |
|
3224 hence "1 = (g $$ fls_subdegree g) * (f $$ fls_subdegree f)" |
|
3225 using fls_subdegree_mult[of g f] fls_times_base[of g f] by fastforce |
|
3226 thus "\<exists>k. 1 = k * f $$ fls_subdegree f" by fast |
|
3227 next |
|
3228 assume "\<exists>k. 1 = k * f $$ fls_subdegree f" |
|
3229 then obtain k where "1 = k * f $$ fls_subdegree f" by fast |
|
3230 hence "1 = fls_left_inverse f k * f" |
|
3231 using fls_left_inverse by simp |
|
3232 thus "\<exists>g. 1 = g * f" by fast |
|
3233 qed |
|
3234 |
|
3235 |
|
3236 subsection \<open>Formal differentiation and integration\<close> |
|
3237 |
|
3238 |
|
3239 subsubsection \<open>Derivative definition and basic properties\<close> |
|
3240 |
|
3241 definition "fls_deriv f = Abs_fls (\<lambda>n. of_int (n+1) * f$$(n+1))" |
|
3242 |
|
3243 lemma fls_deriv_nth[simp]: "fls_deriv f $$ n = of_int (n+1) * f$$(n+1)" |
|
3244 proof- |
|
3245 obtain N where "\<forall>n<N. f$$n = 0" by (elim fls_nth_vanishes_belowE) |
|
3246 hence "\<forall>n<N-1. of_int (n+1) * f$$(n+1) = 0" by auto |
|
3247 thus ?thesis using nth_Abs_fls_lower_bound unfolding fls_deriv_def by simp |
|
3248 qed |
|
3249 |
|
3250 lemma fls_deriv_residue: "fls_deriv f $$ -1 = 0" |
|
3251 by simp |
|
3252 |
|
3253 lemma fls_deriv_const[simp]: "fls_deriv (fls_const x) = 0" |
|
3254 proof (intro fls_eqI) |
|
3255 fix n show "fls_deriv (fls_const x) $$ n = 0$$n" |
|
3256 by (cases "n+1=0") auto |
|
3257 qed |
|
3258 |
|
3259 lemma fls_deriv_of_nat[simp]: "fls_deriv (of_nat n) = 0" |
|
3260 by (simp add: fls_of_nat) |
|
3261 |
|
3262 lemma fls_deriv_of_int[simp]: "fls_deriv (of_int i) = 0" |
|
3263 by (simp add: fls_of_int) |
|
3264 |
|
3265 lemma fls_deriv_zero[simp]: "fls_deriv 0 = 0" |
|
3266 using fls_deriv_const[of 0] by simp |
|
3267 |
|
3268 lemma fls_deriv_one[simp]: "fls_deriv 1 = 0" |
|
3269 using fls_deriv_const[of 1] by simp |
|
3270 |
|
3271 lemma fls_deriv_subdegree': |
|
3272 assumes "of_int (fls_subdegree f) * f $$ fls_subdegree f \<noteq> 0" |
|
3273 shows "fls_subdegree (fls_deriv f) = fls_subdegree f - 1" |
|
3274 by (auto intro: fls_subdegree_eqI simp: assms) |
|
3275 |
|
3276 lemma fls_deriv_subdegree0: |
|
3277 assumes "fls_subdegree f = 0" |
|
3278 shows "fls_subdegree (fls_deriv f) \<ge> 0" |
|
3279 proof (cases "fls_deriv f = 0") |
|
3280 case False |
|
3281 show ?thesis |
|
3282 proof (intro fls_subdegree_geI, rule False) |
|
3283 fix k :: int assume "k < 0" |
|
3284 with assms show "fls_deriv f $$ k = 0" by (cases "k=-1") auto |
|
3285 qed |
|
3286 qed simp |
|
3287 |
|
3288 lemma fls_subdegree_deriv': |
|
3289 fixes f :: "'a::ring_1_no_zero_divisors fls" |
|
3290 assumes "(of_int (fls_subdegree f) :: 'a) \<noteq> 0" |
|
3291 shows "fls_subdegree (fls_deriv f) = fls_subdegree f - 1" |
|
3292 using assms nth_fls_subdegree_zero_iff[of f] |
|
3293 by (auto intro: fls_deriv_subdegree') |
|
3294 |
|
3295 lemma fls_subdegree_deriv: |
|
3296 fixes f :: "'a::{ring_1_no_zero_divisors,ring_char_0} fls" |
|
3297 assumes "fls_subdegree f \<noteq> 0" |
|
3298 shows "fls_subdegree (fls_deriv f) = fls_subdegree f - 1" |
|
3299 by (auto intro: fls_subdegree_deriv' simp: assms) |
|
3300 |
|
3301 text \<open> |
|
3302 Shifting is like multiplying by a power of the implied variable, and so satisfies a product-like |
|
3303 rule. |
|
3304 \<close> |
|
3305 |
|
3306 lemma fls_deriv_shift: |
|
3307 "fls_deriv (fls_shift n f) = of_int (-n) * fls_shift (n+1) f + fls_shift n (fls_deriv f)" |
|
3308 by (intro fls_eqI) (simp flip: fls_shift_fls_shift add: algebra_simps) |
|
3309 |
|
3310 lemma fls_deriv_X [simp]: "fls_deriv fls_X = 1" |
|
3311 by (intro fls_eqI) simp |
|
3312 |
|
3313 lemma fls_deriv_X_inv [simp]: "fls_deriv fls_X_inv = - (fls_X_inv\<^sup>2)" |
|
3314 proof- |
|
3315 have "fls_deriv fls_X_inv = - (fls_shift 2 1)" |
|
3316 by (simp add: fls_X_inv_conv_shift_1 fls_deriv_shift) |
|
3317 thus ?thesis by (simp add: fls_X_inv_power_conv_shift_1) |
|
3318 qed |
|
3319 |
|
3320 lemma fls_deriv_delta: |
|
3321 "fls_deriv (Abs_fls (\<lambda>n. if n=m then c else 0)) = |
|
3322 Abs_fls (\<lambda>n. if n=m-1 then of_int m * c else 0)" |
|
3323 proof- |
|
3324 have |
|
3325 "fls_deriv (Abs_fls (\<lambda>n. if n=m then c else 0)) = fls_shift (1-m) (fls_const (of_int m * c))" |
|
3326 using fls_deriv_shift[of "-m" "fls_const c"] |
|
3327 by (simp |
|
3328 add: fls_shift_const fls_of_int fls_shifted_times_simps(1)[symmetric] |
|
3329 fls_const_mult_const[symmetric] |
|
3330 del: fls_const_mult_const |
|
3331 ) |
|
3332 thus ?thesis by (simp add: fls_shift_const) |
|
3333 qed |
|
3334 |
|
3335 lemma fls_deriv_base_factor: |
|
3336 "fls_deriv (fls_base_factor f) = |
|
3337 of_int (-fls_subdegree f) * fls_shift (fls_subdegree f + 1) f + |
|
3338 fls_shift (fls_subdegree f) (fls_deriv f)" |
|
3339 by (simp add: fls_deriv_shift) |
|
3340 |
|
3341 lemma fls_regpart_deriv: "fls_regpart (fls_deriv f) = fps_deriv (fls_regpart f)" |
|
3342 proof (intro fps_ext) |
|
3343 fix n |
|
3344 have 1: "(of_nat n :: 'a) + 1 = of_nat (n+1)" |
|
3345 and 2: "int n + 1 = int (n + 1)" |
|
3346 by auto |
|
3347 show "fls_regpart (fls_deriv f) $ n = fps_deriv (fls_regpart f) $ n" by (simp add: 1 2) |
|
3348 qed |
|
3349 |
|
3350 lemma fls_prpart_deriv: |
|
3351 fixes f :: "'a :: {comm_ring_1,ring_no_zero_divisors} fls" |
|
3352 \<comment> \<open>Commutivity and no zero divisors are required by the definition of @{const pderiv}.\<close> |
|
3353 shows "fls_prpart (fls_deriv f) = - pCons 0 (pCons 0 (pderiv (fls_prpart f)))" |
|
3354 proof (intro poly_eqI) |
|
3355 fix n |
|
3356 show |
|
3357 "coeff (fls_prpart (fls_deriv f)) n = |
|
3358 coeff (- pCons 0 (pCons 0 (pderiv (fls_prpart f)))) n" |
|
3359 proof (cases n) |
|
3360 case (Suc m) |
|
3361 hence n: "n = Suc m" by fast |
|
3362 show ?thesis |
|
3363 proof (cases m) |
|
3364 case (Suc k) |
|
3365 with n have |
|
3366 "coeff (- pCons 0 (pCons 0 (pderiv (fls_prpart f)))) n = |
|
3367 - coeff (pderiv (fls_prpart f)) k" |
|
3368 by (simp flip: coeff_minus) |
|
3369 with Suc n show ?thesis by (simp add: coeff_pderiv algebra_simps) |
|
3370 qed (simp add: n) |
|
3371 qed simp |
|
3372 qed |
|
3373 |
|
3374 lemma pderiv_fls_prpart: |
|
3375 "pderiv (fls_prpart f) = - poly_shift 2 (fls_prpart (fls_deriv f))" |
|
3376 by (intro poly_eqI) (simp add: coeff_pderiv coeff_poly_shift algebra_simps) |
|
3377 |
|
3378 lemma fls_deriv_fps_to_fls: "fls_deriv (fps_to_fls f) = fps_to_fls (fps_deriv f)" |
|
3379 proof (intro fls_eqI) |
|
3380 fix n |
|
3381 show "fls_deriv (fps_to_fls f) $$ n = fps_to_fls (fps_deriv f) $$ n" |
|
3382 proof (cases "n\<ge>0") |
|
3383 case True |
|
3384 from True have 1: "nat (n + 1) = nat n + 1" by simp |
|
3385 from True have 2: "(of_int (n + 1) :: 'a) = of_nat (nat (n+1))" by simp |
|
3386 from True show ?thesis using arg_cong[OF 2, of "\<lambda>x. x * f $ (nat n+1)"] by (simp add: 1) |
|
3387 next |
|
3388 case False thus ?thesis by (cases "n=-1") auto |
|
3389 qed |
|
3390 qed |
|
3391 |
|
3392 |
|
3393 subsubsection \<open>Algebra rules of the derivative\<close> |
|
3394 |
|
3395 lemma fls_deriv_add [simp]: "fls_deriv (f+g) = fls_deriv f + fls_deriv g" |
|
3396 by (auto intro: fls_eqI simp: algebra_simps) |
|
3397 |
|
3398 lemma fls_deriv_sub [simp]: "fls_deriv (f-g) = fls_deriv f - fls_deriv g" |
|
3399 by (auto intro: fls_eqI simp: algebra_simps) |
|
3400 |
|
3401 lemma fls_deriv_neg [simp]: "fls_deriv (-f) = - fls_deriv f" |
|
3402 using fls_deriv_sub[of 0 f] by simp |
|
3403 |
|
3404 lemma fls_deriv_mult [simp]: |
|
3405 "fls_deriv (f*g) = f * fls_deriv g + fls_deriv f * g" |
|
3406 proof- |
|
3407 define df dg :: int |
|
3408 where "df \<equiv> fls_subdegree f" |
|
3409 and "dg \<equiv> fls_subdegree g" |
|
3410 define uf ug :: "'a fls" |
|
3411 where "uf \<equiv> fls_base_factor f" |
|
3412 and "ug \<equiv> fls_base_factor g" |
|
3413 have |
|
3414 "f * fls_deriv g = |
|
3415 of_int dg * fls_shift (1 - dg) (f * ug) + fls_shift (-dg) (f * fls_deriv ug)" |
|
3416 "fls_deriv f * g = |
|
3417 of_int df * fls_shift (1 - df) (uf * g) + fls_shift (-df) (fls_deriv uf * g)" |
|
3418 using fls_deriv_shift[of "-df" uf] fls_deriv_shift[of "-dg" ug] |
|
3419 mult_of_int_commute[of dg f] |
|
3420 mult.assoc[of "of_int dg" f] |
|
3421 fls_shifted_times_simps(1)[of f "1 - dg" ug] |
|
3422 fls_shifted_times_simps(1)[of f "-dg" "fls_deriv ug"] |
|
3423 fls_shifted_times_simps(2)[of "1 - df" uf g] |
|
3424 fls_shifted_times_simps(2)[of "-df" "fls_deriv uf" g] |
|
3425 by (auto simp add: algebra_simps df_def dg_def uf_def ug_def) |
|
3426 moreover have |
|
3427 "fls_deriv (f*g) = |
|
3428 ( of_int dg * fls_shift (1 - dg) (f * ug) + fls_shift (-dg) (f * fls_deriv ug) ) + |
|
3429 ( of_int df * fls_shift (1 - df) (uf * g) + fls_shift (-df) (fls_deriv uf * g) ) |
|
3430 " |
|
3431 using fls_deriv_shift[of |
|
3432 "- (df + dg)" "fps_to_fls (fls_base_factor_to_fps f * fls_base_factor_to_fps g)" |
|
3433 ] |
|
3434 fls_deriv_fps_to_fls[of "fls_base_factor_to_fps f * fls_base_factor_to_fps g"] |
|
3435 fps_deriv_mult[of "fls_base_factor_to_fps f" "fls_base_factor_to_fps g"] |
|
3436 distrib_right[of |
|
3437 "of_int df" "of_int dg" |
|
3438 "fls_shift (1 - (df + dg)) ( |
|
3439 fps_to_fls (fls_base_factor_to_fps f * fls_base_factor_to_fps g) |
|
3440 )" |
|
3441 ] |
|
3442 fls_times_conv_fps_times[of uf ug] |
|
3443 fls_base_factor_subdegree[of f] fls_base_factor_subdegree[of g] |
|
3444 fls_regpart_deriv[of ug] |
|
3445 fls_times_conv_fps_times[of uf "fls_deriv ug"] |
|
3446 fls_deriv_subdegree0[of ug] |
|
3447 fls_regpart_deriv[of uf] |
|
3448 fls_times_conv_fps_times[of "fls_deriv uf" ug] |
|
3449 fls_deriv_subdegree0[of uf] |
|
3450 fls_shifted_times_simps(1)[of uf "-dg" ug] |
|
3451 fls_shifted_times_simps(1)[of "fls_deriv uf" "-dg" ug] |
|
3452 fls_shifted_times_simps(2)[of "-df" uf ug] |
|
3453 fls_shifted_times_simps(2)[of "-df" uf "fls_deriv ug"] |
|
3454 by (simp add: fls_times_def algebra_simps df_def dg_def uf_def ug_def) |
|
3455 ultimately show ?thesis by simp |
|
3456 qed |
|
3457 |
|
3458 lemma fls_deriv_mult_const_left: |
|
3459 "fls_deriv (fls_const c * f) = fls_const c * fls_deriv f" |
|
3460 by simp |
|
3461 |
|
3462 lemma fls_deriv_linear: |
|
3463 "fls_deriv (fls_const a * f + fls_const b * g) = |
|
3464 fls_const a * fls_deriv f + fls_const b * fls_deriv g" |
|
3465 by simp |
|
3466 |
|
3467 lemma fls_deriv_mult_const_right: |
|
3468 "fls_deriv (f * fls_const c) = fls_deriv f * fls_const c" |
|
3469 by simp |
|
3470 |
|
3471 lemma fls_deriv_linear2: |
|
3472 "fls_deriv (f * fls_const a + g * fls_const b) = |
|
3473 fls_deriv f * fls_const a + fls_deriv g * fls_const b" |
|
3474 by simp |
|
3475 |
|
3476 lemma fls_deriv_sum: |
|
3477 "fls_deriv (sum f S) = sum (\<lambda>i. fls_deriv (f i)) S" |
|
3478 proof (cases "finite S") |
|
3479 case True show ?thesis |
|
3480 by (induct rule: finite_induct [OF True]) simp_all |
|
3481 qed simp |
|
3482 |
|
3483 lemma fls_deriv_power: |
|
3484 fixes f :: "'a::comm_ring_1 fls" |
|
3485 shows "fls_deriv (f^n) = of_nat n * f^(n-1) * fls_deriv f" |
|
3486 proof (cases n) |
|
3487 case (Suc m) |
|
3488 have "fls_deriv (f^Suc m) = of_nat (Suc m) * f^m * fls_deriv f" |
|
3489 by (induct m) (simp_all add: algebra_simps) |
|
3490 with Suc show ?thesis by simp |
|
3491 qed simp |
|
3492 |
|
3493 lemma fls_deriv_X_power: |
|
3494 "fls_deriv (fls_X ^ n) = of_nat n * fls_X ^ (n-1)" |
|
3495 proof (cases n) |
|
3496 case (Suc m) |
|
3497 have "fls_deriv (fls_X^Suc m) = of_nat (Suc m) * fls_X^m" |
|
3498 by (induct m) (simp_all add: mult_of_nat_commute algebra_simps) |
|
3499 with Suc show ?thesis by simp |
|
3500 qed simp |
|
3501 |
|
3502 lemma fls_deriv_X_inv_power: |
|
3503 "fls_deriv (fls_X_inv ^ n) = - of_nat n * fls_X_inv ^ (Suc n)" |
|
3504 proof (cases n) |
|
3505 case (Suc m) |
|
3506 define iX :: "'a fls" where "iX \<equiv> fls_X_inv" |
|
3507 have "fls_deriv (iX ^ Suc m) = - of_nat (Suc m) * iX ^ (Suc (Suc m))" |
|
3508 proof (induct m) |
|
3509 case (Suc m) |
|
3510 have "- of_nat (Suc m + 1) * iX ^ Suc (Suc (Suc m)) = |
|
3511 iX * (-of_nat (Suc m) * iX ^ Suc (Suc m)) + |
|
3512 - (iX ^ 2 * iX ^ Suc m)" |
|
3513 using distrib_right[of "-of_nat (Suc m)" "-(1::'a fls)" "fls_X_inv ^ Suc (Suc (Suc m))"] |
|
3514 by (simp add: algebra_simps mult_of_nat_commute power2_eq_square Suc iX_def) |
|
3515 thus ?case using Suc by (simp add: iX_def) |
|
3516 qed (simp add: numeral_2_eq_2 iX_def) |
|
3517 with Suc show ?thesis by (simp add: iX_def) |
|
3518 qed simp |
|
3519 |
|
3520 lemma fls_deriv_X_intpow: |
|
3521 "fls_deriv (fls_X_intpow i) = of_int i * fls_X_intpow (i-1)" |
|
3522 by (simp add: fls_deriv_shift) |
|
3523 |
|
3524 lemma fls_deriv_lr_inverse: |
|
3525 assumes "x * f $$ fls_subdegree f = 1" "f $$ fls_subdegree f * y = 1" |
|
3526 \<comment> \<open>These assumptions imply x equals y, but no need to assume that.\<close> |
|
3527 shows "fls_deriv (fls_left_inverse f x) = |
|
3528 - fls_left_inverse f x * fls_deriv f * fls_left_inverse f x" |
|
3529 and "fls_deriv (fls_right_inverse f y) = |
|
3530 - fls_right_inverse f y * fls_deriv f * fls_right_inverse f y" |
|
3531 proof- |
|
3532 |
|
3533 define L where "L \<equiv> fls_left_inverse f x" |
|
3534 hence "fls_deriv (L * f) = 0" using fls_left_inverse[OF assms(1)] by simp |
|
3535 with assms show "fls_deriv L = - L * fls_deriv f * L" |
|
3536 using fls_right_inverse'[OF assms] |
|
3537 by (simp add: minus_unique mult.assoc L_def) |
|
3538 |
|
3539 define R where "R \<equiv> fls_right_inverse f y" |
|
3540 hence "fls_deriv (f * R) = 0" using fls_right_inverse[OF assms(2)] by simp |
|
3541 hence 1: "f * fls_deriv R + fls_deriv f * R = 0" by simp |
|
3542 have "R * f * fls_deriv R = - R * fls_deriv f * R" |
|
3543 using iffD2[OF eq_neg_iff_add_eq_0, OF 1] by (simp add: mult.assoc) |
|
3544 thus "fls_deriv R = - R * fls_deriv f * R" |
|
3545 using fls_left_inverse'[OF assms] by (simp add: R_def) |
|
3546 |
|
3547 qed |
|
3548 |
|
3549 lemma fls_deriv_lr_inverse_comm: |
|
3550 fixes x y :: "'a::comm_ring_1" |
|
3551 assumes "x * f $$ fls_subdegree f = 1" |
|
3552 shows "fls_deriv (fls_left_inverse f x) = - fls_deriv f * (fls_left_inverse f x)\<^sup>2" |
|
3553 and "fls_deriv (fls_right_inverse f x) = - fls_deriv f * (fls_right_inverse f x)\<^sup>2" |
|
3554 using assms fls_deriv_lr_inverse[of x f x] |
|
3555 by (simp_all add: mult.commute power2_eq_square) |
|
3556 |
|
3557 lemma fls_inverse_deriv_divring: |
|
3558 fixes a :: "'a::division_ring fls" |
|
3559 shows "fls_deriv (inverse a) = - inverse a * fls_deriv a * inverse a" |
|
3560 proof (cases "a=0") |
|
3561 case False thus ?thesis |
|
3562 using fls_deriv_lr_inverse(2)[of |
|
3563 "inverse (a $$ fls_subdegree a)" a "inverse (a $$ fls_subdegree a)" |
|
3564 ] |
|
3565 by (auto simp add: fls_inverse_def') |
|
3566 qed simp |
|
3567 |
|
3568 lemma fls_inverse_deriv: |
|
3569 fixes a :: "'a::field fls" |
|
3570 shows "fls_deriv (inverse a) = - fls_deriv a * (inverse a)\<^sup>2" |
|
3571 by (simp add: fls_inverse_deriv_divring power2_eq_square) |
|
3572 |
|
3573 lemma fls_inverse_deriv': |
|
3574 fixes a :: "'a::field fls" |
|
3575 shows "fls_deriv (inverse a) = - fls_deriv a / a\<^sup>2" |
|
3576 using fls_inverse_deriv[of a] |
|
3577 by (simp add: field_simps) |
|
3578 |
|
3579 |
|
3580 subsubsection \<open>Equality of derivatives\<close> |
|
3581 |
|
3582 lemma fls_deriv_eq_0_iff: |
|
3583 "fls_deriv f = 0 \<longleftrightarrow> f = fls_const (f$$0 :: 'a::{ring_1_no_zero_divisors,ring_char_0})" |
|
3584 proof |
|
3585 assume f: "fls_deriv f = 0" |
|
3586 show "f = fls_const (f$$0)" |
|
3587 proof (intro fls_eqI) |
|
3588 fix n |
|
3589 from f have "of_int n * f$$ n = 0" using fls_deriv_nth[of f "n-1"] by simp |
|
3590 thus "f$$n = fls_const (f$$0) $$ n" by (cases "n=0") auto |
|
3591 qed |
|
3592 next |
|
3593 show "f = fls_const (f$$0) \<Longrightarrow> fls_deriv f = 0" using fls_deriv_const[of "f$$0"] by simp |
|
3594 qed |
|
3595 |
|
3596 lemma fls_deriv_eq_iff: |
|
3597 fixes f g :: "'a::{ring_1_no_zero_divisors,ring_char_0} fls" |
|
3598 shows "fls_deriv f = fls_deriv g \<longleftrightarrow> (f = fls_const(f$$0 - g$$0) + g)" |
|
3599 proof - |
|
3600 have "fls_deriv f = fls_deriv g \<longleftrightarrow> fls_deriv (f - g) = 0" |
|
3601 by simp |
|
3602 also have "\<dots> \<longleftrightarrow> f - g = fls_const ((f - g) $$ 0)" |
|
3603 unfolding fls_deriv_eq_0_iff .. |
|
3604 finally show ?thesis |
|
3605 by (simp add: field_simps) |
|
3606 qed |
|
3607 |
|
3608 lemma fls_deriv_eq_iff_ex: |
|
3609 fixes f g :: "'a::{ring_1_no_zero_divisors,ring_char_0} fls" |
|
3610 shows "(fls_deriv f = fls_deriv g) \<longleftrightarrow> (\<exists>c. f = fls_const c + g)" |
|
3611 by (auto simp: fls_deriv_eq_iff) |
|
3612 |
|
3613 |
|
3614 subsubsection \<open>Residues\<close> |
|
3615 |
|
3616 definition fls_residue_def[simp]: "fls_residue f \<equiv> f $$ -1" |
|
3617 |
|
3618 lemma fls_residue_deriv: "fls_residue (fls_deriv f) = 0" |
|
3619 by simp |
|
3620 |
|
3621 lemma fls_residue_add: "fls_residue (f+g) = fls_residue f + fls_residue g" |
|
3622 by simp |
|
3623 |
|
3624 lemma fls_residue_times_deriv: |
|
3625 "fls_residue (fls_deriv f * g) = - fls_residue (f * fls_deriv g)" |
|
3626 using fls_residue_deriv[of "f*g"] minus_unique[of "fls_residue (f * fls_deriv g)"] |
|
3627 by simp |
|
3628 |
|
3629 lemma fls_residue_power_series: "fls_subdegree f \<ge> 0 \<Longrightarrow> fls_residue f = 0" |
|
3630 by simp |
|
3631 |
|
3632 lemma fls_residue_fls_X_intpow: |
|
3633 "fls_residue (fls_X_intpow i) = (if i=-1 then 1 else 0)" |
|
3634 by simp |
|
3635 |
|
3636 lemma fls_residue_shift_nth: |
|
3637 fixes f :: "'a::semiring_1 fls" |
|
3638 shows "f$$n = fls_residue (fls_X_intpow (-n-1) * f)" |
|
3639 by (simp add: fls_shifted_times_transfer) |
|
3640 |
|
3641 lemma fls_residue_fls_const_times: |
|
3642 fixes f :: "'a::{comm_monoid_add, mult_zero} fls" |
|
3643 shows "fls_residue (fls_const c * f) = c * fls_residue f" |
|
3644 and "fls_residue (f * fls_const c) = fls_residue f * c" |
|
3645 by simp_all |
|
3646 |
|
3647 lemma fls_residue_of_int_times: |
|
3648 fixes f :: "'a::ring_1 fls" |
|
3649 shows "fls_residue (of_int i * f) = of_int i * fls_residue f" |
|
3650 and "fls_residue (f * of_int i) = fls_residue f * of_int i" |
|
3651 by (simp_all add: fls_residue_fls_const_times fls_of_int) |
|
3652 |
|
3653 lemma fls_residue_deriv_times_lr_inverse_eq_subdegree: |
|
3654 fixes f g :: "'a::ring_1 fls" |
|
3655 assumes "y * (f $$ fls_subdegree f) = 1" "(f $$ fls_subdegree f) * y = 1" |
|
3656 shows "fls_residue (fls_deriv f * fls_right_inverse f y) = of_int (fls_subdegree f)" |
|
3657 and "fls_residue (fls_deriv f * fls_left_inverse f y) = of_int (fls_subdegree f)" |
|
3658 and "fls_residue (fls_left_inverse f y * fls_deriv f) = of_int (fls_subdegree f)" |
|
3659 and "fls_residue (fls_right_inverse f y * fls_deriv f) = of_int (fls_subdegree f)" |
|
3660 proof- |
|
3661 define df :: int where "df \<equiv> fls_subdegree f" |
|
3662 define B X :: "'a fls" |
|
3663 where "B \<equiv> fls_base_factor f" |
|
3664 and "X \<equiv> (fls_X_intpow df :: 'a fls)" |
|
3665 define D L R :: "'a fls" |
|
3666 where "D \<equiv> fls_deriv B" |
|
3667 and "L \<equiv> fls_left_inverse B y" |
|
3668 and "R \<equiv> fls_right_inverse B y" |
|
3669 have intpow_diff: "fls_X_intpow (df - 1) = X * fls_X_inv" |
|
3670 using fls_X_intpow_diff_conv_times[of df 1] by (simp add: X_def fls_X_inv_conv_shift_1) |
|
3671 |
|
3672 |
|
3673 show "fls_residue (fls_deriv f * fls_right_inverse f y) = of_int df" |
|
3674 proof- |
|
3675 have subdegree_DR: "fls_subdegree (D * R) \<ge> 0" |
|
3676 using fls_base_factor_subdegree[of f] fls_base_factor_subdegree[of "fls_right_inverse f y"] |
|
3677 assms(1) fls_right_inverse_base_factor[of y f] fls_mult_subdegree_ge_0[of D R] |
|
3678 by (force simp: fls_deriv_subdegree0 D_def R_def B_def) |
|
3679 have decomp: "f = X * B" |
|
3680 unfolding X_def B_def df_def by (rule fls_base_factor_X_power_decompose(2)[of f]) |
|
3681 hence "fls_deriv f = X * D + of_int df * X * fls_X_inv * B" |
|
3682 using intpow_diff fls_deriv_mult[of X B] |
|
3683 by (simp add: fls_deriv_X_intpow X_def B_def D_def mult.assoc) |
|
3684 moreover from assms have "fls_right_inverse (X * B) y = R * fls_right_inverse X 1" |
|
3685 using fls_base_factor_base[of f] fls_lr_inverse_mult_ring1(2)[of 1 X] |
|
3686 by (simp add: X_def B_def R_def) |
|
3687 ultimately have |
|
3688 "fls_deriv f * fls_right_inverse f y = |
|
3689 (D + of_int df * fls_X_inv * B) * R * (X * fls_right_inverse X 1)" |
|
3690 by (simp add: decomp algebra_simps X_def fls_X_intpow_times_comm) |
|
3691 also have "\<dots> = D * R + of_int df * fls_X_inv" |
|
3692 using fls_right_inverse[of X 1] |
|
3693 assms fls_base_factor_base[of f] fls_right_inverse[of B y] |
|
3694 by (simp add: X_def distrib_right mult.assoc B_def R_def) |
|
3695 finally show ?thesis using subdegree_DR by simp |
|
3696 qed |
|
3697 |
|
3698 with assms show "fls_residue (fls_deriv f * fls_left_inverse f y) = of_int df" |
|
3699 using fls_left_inverse_eq_fls_right_inverse[of y f] by simp |
|
3700 |
|
3701 show "fls_residue (fls_left_inverse f y * fls_deriv f) = of_int df" |
|
3702 proof- |
|
3703 have subdegree_LD: "fls_subdegree (L * D) \<ge> 0" |
|
3704 using fls_base_factor_subdegree[of f] fls_base_factor_subdegree[of "fls_left_inverse f y"] |
|
3705 assms(1) fls_left_inverse_base_factor[of y f] fls_mult_subdegree_ge_0[of L D] |
|
3706 by (force simp: fls_deriv_subdegree0 D_def L_def B_def) |
|
3707 have decomp: "f = B * X" |
|
3708 unfolding X_def B_def df_def by (rule fls_base_factor_X_power_decompose(1)[of f]) |
|
3709 hence "fls_deriv f = D * X + B * of_int df * X * fls_X_inv" |
|
3710 using intpow_diff fls_deriv_mult[of B X] |
|
3711 by (simp add: fls_deriv_X_intpow X_def D_def B_def mult.assoc) |
|
3712 moreover from assms have "fls_left_inverse (B * X) y = fls_left_inverse X 1 * L" |
|
3713 using fls_base_factor_base[of f] fls_lr_inverse_mult_ring1(1)[of _ _ 1 X] |
|
3714 by (simp add: X_def B_def L_def) |
|
3715 ultimately have |
|
3716 "fls_left_inverse f y * fls_deriv f = |
|
3717 fls_left_inverse X 1 * X * L * (D + B * (of_int df * fls_X_inv))" |
|
3718 by (simp add: decomp algebra_simps X_def fls_X_intpow_times_comm) |
|
3719 also have "\<dots> = L * D + of_int df * fls_X_inv" |
|
3720 using assms fls_left_inverse[of 1 X] fls_base_factor_base[of f] fls_left_inverse[of y B] |
|
3721 by (simp add: X_def distrib_left mult.assoc[symmetric] L_def B_def) |
|
3722 finally show ?thesis using subdegree_LD by simp |
|
3723 qed |
|
3724 |
|
3725 with assms show "fls_residue (fls_right_inverse f y * fls_deriv f) = of_int df" |
|
3726 using fls_left_inverse_eq_fls_right_inverse[of y f] by simp |
|
3727 |
|
3728 qed |
|
3729 |
|
3730 lemma fls_residue_deriv_times_inverse_eq_subdegree: |
|
3731 fixes f g :: "'a::division_ring fls" |
|
3732 shows "fls_residue (fls_deriv f * inverse f) = of_int (fls_subdegree f)" |
|
3733 and "fls_residue (inverse f * fls_deriv f) = of_int (fls_subdegree f)" |
|
3734 proof- |
|
3735 show "fls_residue (fls_deriv f * inverse f) = of_int (fls_subdegree f)" |
|
3736 using fls_residue_deriv_times_lr_inverse_eq_subdegree(1)[of _ f] |
|
3737 by (cases "f=0") (auto simp: fls_inverse_def') |
|
3738 show "fls_residue (inverse f * fls_deriv f) = of_int (fls_subdegree f)" |
|
3739 using fls_residue_deriv_times_lr_inverse_eq_subdegree(4)[of _ f] |
|
3740 by (cases "f=0") (auto simp: fls_inverse_def') |
|
3741 qed |
|
3742 |
|
3743 |
|
3744 subsubsection \<open>Integral definition and basic properties\<close> |
|
3745 |
|
3746 \<comment> \<open>To incorporate a constant of integration, just add an fps_const.\<close> |
|
3747 definition fls_integral :: "'a::{ring_1,inverse} fls \<Rightarrow> 'a fls" |
|
3748 where "fls_integral a = Abs_fls (\<lambda>n. if n=0 then 0 else inverse (of_int n) * a$$(n - 1))" |
|
3749 |
|
3750 lemma fls_integral_nth [simp]: |
|
3751 "fls_integral a $$ n = (if n=0 then 0 else inverse (of_int n) * a$$(n-1))" |
|
3752 proof- |
|
3753 define F where "F \<equiv> (\<lambda>n. if n=0 then 0 else inverse (of_int n) * a$$(n - 1))" |
|
3754 obtain N where "\<forall>n<N. a$$n = 0" by (elim fls_nth_vanishes_belowE) |
|
3755 hence "\<forall>n<N. F n = 0" by (auto simp add: F_def) |
|
3756 thus ?thesis using nth_Abs_fls_lower_bound[of N F] unfolding fls_integral_def F_def by simp |
|
3757 qed |
|
3758 |
|
3759 lemma fls_integral_conv_fps_zeroth_integral: |
|
3760 assumes "fls_subdegree a \<ge> 0" |
|
3761 shows "fls_integral a = fps_to_fls (fps_integral0 (fls_regpart a))" |
|
3762 proof (rule fls_eqI) |
|
3763 fix n |
|
3764 show "fls_integral a $$ n = fps_to_fls (fps_integral0 (fls_regpart a)) $$ n" |
|
3765 proof (cases "n>0") |
|
3766 case False with assms show ?thesis by simp |
|
3767 next |
|
3768 case True |
|
3769 hence "int ((nat n) - 1) = n - 1" by simp |
|
3770 with True show ?thesis by (simp add: fps_integral_def) |
|
3771 qed |
|
3772 qed |
|
3773 |
|
3774 lemma fls_integral_zero [simp]: "fls_integral 0 = 0" |
|
3775 by (intro fls_eqI) simp |
|
3776 |
|
3777 lemma fls_integral_const': |
|
3778 fixes x :: "'a::{ring_1,inverse}" |
|
3779 assumes "inverse (1::'a) = 1" |
|
3780 shows "fls_integral (fls_const x) = fls_const x * fls_X" |
|
3781 by (intro fls_eqI) (simp add: assms) |
|
3782 |
|
3783 lemma fls_integral_const: |
|
3784 fixes x :: "'a::division_ring" |
|
3785 shows "fls_integral (fls_const x) = fls_const x * fls_X" |
|
3786 by (rule fls_integral_const'[OF inverse_1]) |
|
3787 |
|
3788 lemma fls_integral_of_nat': |
|
3789 assumes "inverse (1::'a::{ring_1,inverse}) = 1" |
|
3790 shows "fls_integral (of_nat n :: 'a fls) = of_nat n * fls_X" |
|
3791 by (simp add: assms fls_integral_const' fls_of_nat) |
|
3792 |
|
3793 lemma fls_integral_of_nat: |
|
3794 "fls_integral (of_nat n :: 'a::division_ring fls) = of_nat n * fls_X" |
|
3795 by (rule fls_integral_of_nat'[OF inverse_1]) |
|
3796 |
|
3797 lemma fls_integral_of_int': |
|
3798 assumes "inverse (1::'a::{ring_1,inverse}) = 1" |
|
3799 shows "fls_integral (of_int i :: 'a fls) = of_int i * fls_X" |
|
3800 by (simp add: assms fls_integral_const' fls_of_int) |
|
3801 |
|
3802 lemma fls_integral_of_int: |
|
3803 "fls_integral (of_int i :: 'a::division_ring fls) = of_int i * fls_X" |
|
3804 by (rule fls_integral_of_int'[OF inverse_1]) |
|
3805 |
|
3806 lemma fls_integral_one': |
|
3807 assumes "inverse (1::'a::{ring_1,inverse}) = 1" |
|
3808 shows "fls_integral (1::'a fls) = fls_X" |
|
3809 using fls_integral_const'[of 1] |
|
3810 by (force simp: assms) |
|
3811 |
|
3812 lemma fls_integral_one: "fls_integral (1::'a::division_ring fls) = fls_X" |
|
3813 by (rule fls_integral_one'[OF inverse_1]) |
|
3814 |
|
3815 lemma fls_subdegree_integral_ge: |
|
3816 "fls_integral f \<noteq> 0 \<Longrightarrow> fls_subdegree (fls_integral f) \<ge> fls_subdegree f + 1" |
|
3817 by (intro fls_subdegree_geI) simp_all |
|
3818 |
|
3819 lemma fls_subdegree_integral: |
|
3820 fixes f :: "'a::{division_ring,ring_char_0} fls" |
|
3821 assumes "f \<noteq> 0" "fls_subdegree f \<noteq> -1" |
|
3822 shows "fls_subdegree (fls_integral f) = fls_subdegree f + 1" |
|
3823 using assms of_int_0_eq_iff[of "fls_subdegree f + 1"] fls_subdegree_integral_ge |
|
3824 by (intro fls_subdegree_eqI) simp_all |
|
3825 |
|
3826 lemma fls_integral_X [simp]: |
|
3827 "fls_integral (fls_X::'a::{ring_1,inverse} fls) = |
|
3828 fls_const (inverse (of_int 2)) * fls_X\<^sup>2" |
|
3829 proof (intro fls_eqI) |
|
3830 fix n |
|
3831 show "fls_integral (fls_X::'a fls) $$ n = (fls_const (inverse (of_int 2)) * fls_X\<^sup>2) $$ n" |
|
3832 using arg_cong[OF fls_X_power_nth, of "\<lambda>x. inverse (of_int 2) * x", of 2 n, symmetric] |
|
3833 by (auto simp add: ) |
|
3834 qed |
|
3835 |
|
3836 lemma fls_integral_X_power: |
|
3837 "fls_integral (fls_X ^ n ::'a :: {ring_1,inverse} fls) = |
|
3838 fls_const (inverse (of_nat (Suc n))) * fls_X ^ Suc n" |
|
3839 proof (intro fls_eqI) |
|
3840 fix k |
|
3841 have "(fls_X :: 'a fls) ^ Suc n $$ k = (if k=Suc n then 1 else 0)" |
|
3842 by (rule fls_X_power_nth) |
|
3843 thus |
|
3844 "fls_integral ((fls_X::'a fls) ^ n) $$ k = |
|
3845 (fls_const (inverse (of_nat (Suc n))) * (fls_X::'a fls) ^ Suc n) $$ k" |
|
3846 by simp |
|
3847 qed |
|
3848 |
|
3849 lemma fls_integral_X_power_char0: |
|
3850 "fls_integral (fls_X ^ n :: 'a :: {ring_char_0,inverse} fls) = |
|
3851 inverse (of_nat (Suc n)) * fls_X ^ Suc n" |
|
3852 proof - |
|
3853 have "(of_nat (Suc n) :: 'a) \<noteq> 0" by (rule of_nat_neq_0) |
|
3854 hence "fls_const (inverse (of_nat (Suc n) :: 'a)) = inverse (fls_const (of_nat (Suc n)))" |
|
3855 by (simp add: fls_inverse_const) |
|
3856 moreover have |
|
3857 "fls_integral ((fls_X::'a fls) ^ n) = fls_const (inverse (of_nat (Suc n))) * fls_X ^ Suc n" |
|
3858 by (rule fls_integral_X_power) |
|
3859 ultimately show ?thesis by (simp add: fls_of_nat) |
|
3860 qed |
|
3861 |
|
3862 lemma fls_integral_X_inv [simp]: "fls_integral (fls_X_inv::'a::{ring_1,inverse} fls) = 0" |
|
3863 by (intro fls_eqI) simp |
|
3864 |
|
3865 lemma fls_integral_X_inv_power: |
|
3866 assumes "n \<ge> 2" |
|
3867 shows |
|
3868 "fls_integral (fls_X_inv ^ n :: 'a :: {ring_1,inverse} fls) = |
|
3869 fls_const (inverse (of_int (1 - int n))) * fls_X_inv ^ (n-1)" |
|
3870 proof (rule fls_eqI) |
|
3871 fix k show |
|
3872 "fls_integral (fls_X_inv ^ n :: 'a fls) $$ k= |
|
3873 (fls_const (inverse (of_int (1 - int n))) * fls_X_inv ^ (n-1)) $$ k" |
|
3874 proof (cases "k=0") |
|
3875 case True with assms show ?thesis by simp |
|
3876 next |
|
3877 case False |
|
3878 from assms have "int (n-1) = int n - 1" by simp |
|
3879 hence |
|
3880 "(fls_const (inverse (of_int (1 - int n))) * (fls_X_inv:: 'a fls) ^ (n-1)) $$ k = |
|
3881 (if k = 1 - int n then inverse (of_int k) else 0)" |
|
3882 by (simp add: fls_X_inv_power_times_conv_shift(2)) |
|
3883 with False show ?thesis by (simp add: algebra_simps) |
|
3884 qed |
|
3885 qed |
|
3886 |
|
3887 lemma fls_integral_X_inv_power_char0: |
|
3888 assumes "n \<ge> 2" |
|
3889 shows |
|
3890 "fls_integral (fls_X_inv ^ n :: 'a :: {ring_char_0,inverse} fls) = |
|
3891 inverse (of_int (1 - int n)) * fls_X_inv ^ (n-1)" |
|
3892 proof- |
|
3893 from assms have "(of_int (1 - int n) :: 'a) \<noteq> 0" by simp |
|
3894 hence |
|
3895 "fls_const (inverse (of_int (1 - int n) :: 'a)) = inverse (fls_const (of_int (1 - int n)))" |
|
3896 by (simp add: fls_inverse_const) |
|
3897 moreover have |
|
3898 "fls_integral (fls_X_inv ^ n :: 'a fls) = |
|
3899 fls_const (inverse (of_int (1 - int n))) * fls_X_inv ^ (n-1)" |
|
3900 using assms by (rule fls_integral_X_inv_power) |
|
3901 ultimately show ?thesis by (simp add: fls_of_int) |
|
3902 qed |
|
3903 |
|
3904 lemma fls_integral_X_inv_power': |
|
3905 assumes "n \<ge> 1" |
|
3906 shows |
|
3907 "fls_integral (fls_X_inv ^ n :: 'a :: division_ring fls) = |
|
3908 - fls_const (inverse (of_nat (n-1))) * fls_X_inv ^ (n-1)" |
|
3909 proof (cases "n = 1") |
|
3910 case False |
|
3911 with assms have n: "n \<ge> 2" by simp |
|
3912 hence |
|
3913 "fls_integral (fls_X_inv ^ n :: 'a fls) = |
|
3914 fls_const (inverse (- of_nat (nat (int n - 1)))) * fls_X_inv ^ (n-1)" |
|
3915 by (simp add: fls_integral_X_inv_power) |
|
3916 moreover from n have "nat (int n - 1) = n - 1" by simp |
|
3917 ultimately show ?thesis |
|
3918 using inverse_minus_eq[of "of_nat (n-1) :: 'a"] by simp |
|
3919 qed simp |
|
3920 |
|
3921 lemma fls_integral_X_inv_power_char0': |
|
3922 assumes "n \<ge> 1" |
|
3923 shows |
|
3924 "fls_integral (fls_X_inv ^ n :: 'a :: {division_ring,ring_char_0} fls) = |
|
3925 - inverse (of_nat (n-1)) * fls_X_inv ^ (n-1)" |
|
3926 proof (cases "n=1") |
|
3927 case False with assms show ?thesis |
|
3928 by (simp add: fls_integral_X_inv_power' fls_inverse_const fls_of_nat) |
|
3929 qed simp |
|
3930 |
|
3931 lemma fls_integral_delta: |
|
3932 assumes "m \<noteq> -1" |
|
3933 shows |
|
3934 "fls_integral (Abs_fls (\<lambda>n. if n=m then c else 0)) = |
|
3935 Abs_fls (\<lambda>n. if n=m+1 then inverse (of_int (m+1)) * c else 0)" |
|
3936 using assms |
|
3937 by (intro fls_eqI) auto |
|
3938 |
|
3939 lemma fls_regpart_integral: |
|
3940 "fls_regpart (fls_integral f) = fps_integral0 (fls_regpart f)" |
|
3941 proof (rule fps_ext) |
|
3942 fix n |
|
3943 show "fls_regpart (fls_integral f) $ n = fps_integral0 (fls_regpart f) $ n" |
|
3944 by (cases n) (simp_all add: fps_integral_def) |
|
3945 qed |
|
3946 |
|
3947 lemma fls_integral_fps_to_fls: |
|
3948 "fls_integral (fps_to_fls f) = fps_to_fls (fps_integral0 f)" |
|
3949 proof (intro fls_eqI) |
|
3950 fix n :: int |
|
3951 show "fls_integral (fps_to_fls f) $$ n = fps_to_fls (fps_integral0 f) $$ n" |
|
3952 proof (cases "n<1") |
|
3953 case True thus ?thesis by simp |
|
3954 next |
|
3955 case False |
|
3956 hence "nat (n-1) = nat n - 1" by simp |
|
3957 with False show ?thesis by (cases "nat n") auto |
|
3958 qed |
|
3959 qed |
|
3960 |
|
3961 |
|
3962 subsubsection \<open>Algebra rules of the integral\<close> |
|
3963 |
|
3964 lemma fls_integral_add [simp]: "fls_integral (f+g) = fls_integral f + fls_integral g" |
|
3965 by (intro fls_eqI) (simp add: algebra_simps) |
|
3966 |
|
3967 lemma fls_integral_sub [simp]: "fls_integral (f-g) = fls_integral f - fls_integral g" |
|
3968 by (intro fls_eqI) (simp add: algebra_simps) |
|
3969 |
|
3970 lemma fls_integral_neg [simp]: "fls_integral (-f) = - fls_integral f" |
|
3971 using fls_integral_sub[of 0 f] by simp |
|
3972 |
|
3973 lemma fls_integral_mult_const_left: |
|
3974 "fls_integral (fls_const c * f) = fls_const c * fls_integral (f :: 'a::division_ring fls)" |
|
3975 by (intro fls_eqI) (simp add: mult.assoc mult_inverse_of_int_commute) |
|
3976 |
|
3977 lemma fls_integral_mult_const_left_comm: |
|
3978 fixes f :: "'a::{comm_ring_1,inverse} fls" |
|
3979 shows "fls_integral (fls_const c * f) = fls_const c * fls_integral f" |
|
3980 by (intro fls_eqI) (simp add: mult.assoc mult.commute) |
|
3981 |
|
3982 lemma fls_integral_linear: |
|
3983 fixes f g :: "'a::division_ring fls" |
|
3984 shows |
|
3985 "fls_integral (fls_const a * f + fls_const b * g) = |
|
3986 fls_const a * fls_integral f + fls_const b * fls_integral g" |
|
3987 by (simp add: fls_integral_mult_const_left) |
|
3988 |
|
3989 lemma fls_integral_linear_comm: |
|
3990 fixes f g :: "'a::{comm_ring_1,inverse} fls" |
|
3991 shows |
|
3992 "fls_integral (fls_const a * f + fls_const b * g) = |
|
3993 fls_const a * fls_integral f + fls_const b * fls_integral g" |
|
3994 by (simp add: fls_integral_mult_const_left_comm) |
|
3995 |
|
3996 lemma fls_integral_mult_const_right: |
|
3997 "fls_integral (f * fls_const c) = fls_integral f * fls_const c" |
|
3998 by (intro fls_eqI) (simp add: mult.assoc) |
|
3999 |
|
4000 lemma fls_integral_linear2: |
|
4001 "fls_integral (f * fls_const a + g * fls_const b) = |
|
4002 fls_integral f * fls_const a + fls_integral g * fls_const b" |
|
4003 by (simp add: fls_integral_mult_const_right) |
|
4004 |
|
4005 lemma fls_integral_sum: |
|
4006 "fls_integral (sum f S) = sum (\<lambda>i. fls_integral (f i)) S" |
|
4007 proof (cases "finite S") |
|
4008 case True show ?thesis |
|
4009 by (induct rule: finite_induct [OF True]) simp_all |
|
4010 qed simp |
|
4011 |
|
4012 |
|
4013 subsubsection \<open>Derivatives of integrals and vice versa\<close> |
|
4014 |
|
4015 lemma fls_integral_fls_deriv: |
|
4016 fixes a :: "'a::{division_ring,ring_char_0} fls" |
|
4017 shows "fls_integral (fls_deriv a) + fls_const (a$$0) = a" |
|
4018 by (intro fls_eqI) (simp add: mult.assoc[symmetric]) |
|
4019 |
|
4020 lemma fls_deriv_fls_integral: |
|
4021 fixes a :: "'a::{division_ring,ring_char_0} fls" |
|
4022 assumes "fls_residue a = 0" |
|
4023 shows "fls_deriv (fls_integral a) = a" |
|
4024 proof (intro fls_eqI) |
|
4025 fix n :: int |
|
4026 show "fls_deriv (fls_integral a) $$ n = a $$ n" |
|
4027 proof (cases "n=-1") |
|
4028 case True with assms show ?thesis by simp |
|
4029 next |
|
4030 case False |
|
4031 hence "(of_int (n+1) :: 'a) \<noteq> 0" using of_int_eq_0_iff[of "n+1"] by simp |
|
4032 hence "(of_int (n+1) :: 'a) * inverse (of_int (n+1) :: 'a) = (1::'a)" |
|
4033 using of_int_eq_0_iff[of "n+1"] by simp |
|
4034 moreover have |
|
4035 "fls_deriv (fls_integral a) $$ n = |
|
4036 (if n=-1 then 0 else of_int (n+1) * inverse (of_int (n+1)) * a$$n)" |
|
4037 by (simp add: mult.assoc) |
|
4038 ultimately show ?thesis |
|
4039 by (simp add: False) |
|
4040 qed |
|
4041 qed |
|
4042 |
|
4043 text \<open>Series with zero residue are precisely the derivatives.\<close> |
|
4044 |
|
4045 lemma fls_residue_nonzero_ex_antiderivative: |
|
4046 fixes f :: "'a::{division_ring,ring_char_0} fls" |
|
4047 assumes "fls_residue f = 0" |
|
4048 shows "\<exists>F. fls_deriv F = f" |
|
4049 using assms fls_deriv_fls_integral |
|
4050 by auto |
|
4051 |
|
4052 lemma fls_ex_antiderivative_residue_nonzero: |
|
4053 assumes "\<exists>F. fls_deriv F = f" |
|
4054 shows "fls_residue f = 0" |
|
4055 using assms fls_residue_deriv |
|
4056 by auto |
|
4057 |
|
4058 lemma fls_residue_nonzero_ex_anitderivative_iff: |
|
4059 fixes f :: "'a::{division_ring,ring_char_0} fls" |
|
4060 shows "fls_residue f = 0 \<longleftrightarrow> (\<exists>F. fls_deriv F = f)" |
|
4061 using fls_residue_nonzero_ex_antiderivative fls_ex_antiderivative_residue_nonzero |
|
4062 by fast |
|
4063 |
|
4064 |
|
4065 subsection \<open>Topology\<close> |
|
4066 |
|
4067 instantiation fls :: (group_add) metric_space |
|
4068 begin |
|
4069 |
|
4070 definition |
|
4071 dist_fls_def: |
|
4072 "dist (a :: 'a fls) b = |
|
4073 (if a = b |
|
4074 then 0 |
|
4075 else if fls_subdegree (a-b) \<ge> 0 |
|
4076 then inverse (2 ^ nat (fls_subdegree (a-b))) |
|
4077 else 2 ^ nat (-fls_subdegree (a-b)) |
|
4078 )" |
|
4079 |
|
4080 lemma dist_fls_ge0: "dist (a :: 'a fls) b \<ge> 0" |
|
4081 by (simp add: dist_fls_def) |
|
4082 |
|
4083 definition uniformity_fls_def [code del]: |
|
4084 "(uniformity :: ('a fls \<times> 'a fls) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})" |
|
4085 |
|
4086 definition open_fls_def' [code del]: |
|
4087 "open (U :: 'a fls set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)" |
|
4088 |
|
4089 lemma dist_fls_sym: "dist (a :: 'a fls) b = dist b a" |
|
4090 by (cases "a\<noteq>b", cases "fls_subdegree (a-b) \<ge> 0") |
|
4091 (simp_all add: fls_subdegree_minus_sym dist_fls_def) |
|
4092 |
|
4093 context |
|
4094 begin |
|
4095 |
|
4096 private lemma instance_helper: |
|
4097 fixes a b c :: "'a fls" |
|
4098 assumes neq: "a\<noteq>b" "a\<noteq>c" |
|
4099 and dist_ineq: "dist a b > dist a c" |
|
4100 shows "fls_subdegree (a - b) < fls_subdegree (a - c)" |
|
4101 proof ( |
|
4102 cases "fls_subdegree (a-b) \<ge> 0" "fls_subdegree (a-c) \<ge> 0" |
|
4103 rule: case_split[case_product case_split] |
|
4104 ) |
|
4105 case True_True with neq dist_ineq show ?thesis by (simp add: dist_fls_def) |
|
4106 next |
|
4107 case False_True with dist_ineq show ?thesis by (simp add: dist_fls_def) |
|
4108 next |
|
4109 case False_False with neq dist_ineq show ?thesis by (simp add: dist_fls_def) |
|
4110 next |
|
4111 case True_False |
|
4112 with neq |
|
4113 have "(1::real) > 2 ^ (nat (fls_subdegree (a-b)) + nat (-fls_subdegree (a-c)))" |
|
4114 and "nat (fls_subdegree (a-b)) + nat (-fls_subdegree (a-c)) = |
|
4115 nat (fls_subdegree (a-b) - fls_subdegree (a-c))" |
|
4116 using dist_ineq |
|
4117 by (simp_all add: dist_fls_def field_simps power_add) |
|
4118 hence "\<not> (1::real) < 2 ^ (nat (fls_subdegree (a-b) - fls_subdegree (a-c)))" by simp |
|
4119 hence "\<not> (0 < nat (fls_subdegree (a - b) - fls_subdegree (a - c)))" by auto |
|
4120 hence "fls_subdegree (a - b) \<le> fls_subdegree (a - c)" by simp |
|
4121 with True_False show ?thesis by simp |
|
4122 qed |
|
4123 |
|
4124 instance |
|
4125 proof |
|
4126 show th: "dist a b = 0 \<longleftrightarrow> a = b" for a b :: "'a fls" |
|
4127 by (simp add: dist_fls_def split: if_split_asm) |
|
4128 then have th'[simp]: "dist a a = 0" for a :: "'a fls" by simp |
|
4129 |
|
4130 fix a b c :: "'a fls" |
|
4131 consider "a = b" | "c = a \<or> c = b" | "a \<noteq> b" "a \<noteq> c" "b \<noteq> c" by blast |
|
4132 then show "dist a b \<le> dist a c + dist b c" |
|
4133 proof cases |
|
4134 case 1 |
|
4135 then show ?thesis by (simp add: dist_fls_def) |
|
4136 next |
|
4137 case 2 |
|
4138 then show ?thesis |
|
4139 by (cases "c = a") (simp_all add: th dist_fls_sym) |
|
4140 next |
|
4141 case neq: 3 |
|
4142 have False if "dist a b > dist a c + dist b c" |
|
4143 proof - |
|
4144 from neq have "dist a b > 0" "dist b c > 0" "dist a c > 0" by (simp_all add: dist_fls_def) |
|
4145 with that have dist_ineq: "dist a b > dist a c" "dist a b > dist b c" by simp_all |
|
4146 have "fls_subdegree (a - b) < fls_subdegree (a - c)" |
|
4147 and "fls_subdegree (a - b) < fls_subdegree (b - c)" |
|
4148 using instance_helper[of a b c] instance_helper[of b a c] neq dist_ineq |
|
4149 by (simp_all add: dist_fls_sym fls_subdegree_minus_sym) |
|
4150 hence "(a - c) $$ fls_subdegree (a - b) = 0" and "(b - c) $$ fls_subdegree (a - b) = 0" |
|
4151 by (simp_all only: fls_eq0_below_subdegree) |
|
4152 hence "(a - b) $$ fls_subdegree (a - b) = 0" by simp |
|
4153 moreover from neq have "(a - b) $$ fls_subdegree (a - b) \<noteq> 0" |
|
4154 by (intro nth_fls_subdegree_nonzero) simp |
|
4155 ultimately show False by contradiction |
|
4156 qed |
|
4157 thus ?thesis by (auto simp: not_le[symmetric]) |
|
4158 qed |
|
4159 qed (rule open_fls_def' uniformity_fls_def)+ |
|
4160 |
|
4161 end |
|
4162 end |
|
4163 |
|
4164 lemma open_fls_def: |
|
4165 "open (S :: 'a::group_add fls set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> {y. dist y a < r} \<subseteq> S)" |
|
4166 unfolding open_dist subset_eq by simp |
|
4167 |
|
4168 |
|
4169 subsection \<open>Notation bundle\<close> |
|
4170 |
|
4171 no_notation fls_nth (infixl "$$" 75) |
|
4172 |
|
4173 bundle fls_notation |
|
4174 begin |
|
4175 notation fls_nth (infixl "$$" 75) |
|
4176 end |
|
4177 |
|
4178 end |