src/HOL/Library/Formal_Power_Series.thy
author eberlm <eberlm@in.tum.de>
Tue, 04 Apr 2017 09:01:19 +0200
changeset 65396 b42167902f57
parent 64786 340db65fd2c1
child 65398 a14fa655b48c
permissions -rw-r--r--
moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 39302
diff changeset
     1
(*  Title:      HOL/Library/Formal_Power_Series.thy
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
     2
    Author:     Amine Chaieb, University of Cambridge
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
     3
*)
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
     4
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
     5
section \<open>A formalization of formal power series\<close>
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
     6
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
     7
theory Formal_Power_Series
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
     8
imports Complex_Main "~~/src/HOL/Number_Theory/Euclidean_Algorithm"
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
     9
begin
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    10
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
    11
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
    12
subsection \<open>The type of formal power series\<close>
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    13
49834
b27bbb021df1 discontinued obsolete typedef (open) syntax;
wenzelm
parents: 48757
diff changeset
    14
typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    15
  morphisms fps_nth Abs_fps
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    16
  by simp
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    17
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    18
notation fps_nth (infixl "$" 75)
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    19
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    20
lemma expand_fps_eq: "p = q \<longleftrightarrow> (\<forall>n. p $ n = q $ n)"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
    21
  by (simp add: fps_nth_inject [symmetric] fun_eq_iff)
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    22
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    23
lemma fps_ext: "(\<And>n. p $ n = q $ n) \<Longrightarrow> p = q"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    24
  by (simp add: expand_fps_eq)
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    25
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    26
lemma fps_nth_Abs_fps [simp]: "Abs_fps f $ n = f n"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    27
  by (simp add: Abs_fps_inverse)
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    28
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
    29
text \<open>Definition of the basic elements 0 and 1 and the basic operations of addition,
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
    30
  negation and multiplication.\<close>
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    31
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36350
diff changeset
    32
instantiation fps :: (zero) zero
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    33
begin
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
    34
  definition fps_zero_def: "0 = Abs_fps (\<lambda>n. 0)"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
    35
  instance ..
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    36
end
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    37
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    38
lemma fps_zero_nth [simp]: "0 $ n = 0"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    39
  unfolding fps_zero_def by simp
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    40
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36350
diff changeset
    41
instantiation fps :: ("{one, zero}") one
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    42
begin
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
    43
  definition fps_one_def: "1 = Abs_fps (\<lambda>n. if n = 0 then 1 else 0)"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
    44
  instance ..
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    45
end
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    46
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30273
diff changeset
    47
lemma fps_one_nth [simp]: "1 $ n = (if n = 0 then 1 else 0)"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    48
  unfolding fps_one_def by simp
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    49
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
    50
instantiation fps :: (plus) plus
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    51
begin
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
    52
  definition fps_plus_def: "op + = (\<lambda>f g. Abs_fps (\<lambda>n. f $ n + g $ n))"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
    53
  instance ..
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    54
end
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    55
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    56
lemma fps_add_nth [simp]: "(f + g) $ n = f $ n + g $ n"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    57
  unfolding fps_plus_def by simp
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    58
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    59
instantiation fps :: (minus) minus
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    60
begin
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
    61
  definition fps_minus_def: "op - = (\<lambda>f g. Abs_fps (\<lambda>n. f $ n - g $ n))"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
    62
  instance ..
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    63
end
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    64
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    65
lemma fps_sub_nth [simp]: "(f - g) $ n = f $ n - g $ n"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    66
  unfolding fps_minus_def by simp
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    67
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    68
instantiation fps :: (uminus) uminus
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    69
begin
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
    70
  definition fps_uminus_def: "uminus = (\<lambda>f. Abs_fps (\<lambda>n. - (f $ n)))"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
    71
  instance ..
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    72
end
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    73
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    74
lemma fps_neg_nth [simp]: "(- f) $ n = - (f $ n)"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    75
  unfolding fps_uminus_def by simp
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    76
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
    77
instantiation fps :: ("{comm_monoid_add, times}") times
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    78
begin
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
    79
  definition fps_times_def: "op * = (\<lambda>f g. Abs_fps (\<lambda>n. \<Sum>i=0..n. f $ i * g $ (n - i)))"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
    80
  instance ..
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    81
end
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    82
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    83
lemma fps_mult_nth: "(f * g) $ n = (\<Sum>i=0..n. f$i * g$(n - i))"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
    84
  unfolding fps_times_def by simp
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    85
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
    86
lemma fps_mult_nth_0 [simp]: "(f * g) $ 0 = f $ 0 * g $ 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
    87
  unfolding fps_times_def by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
    88
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
    89
declare atLeastAtMost_iff [presburger]
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
    90
declare Bex_def [presburger]
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
    91
declare Ball_def [presburger]
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
    92
29913
89eadbe71e97 add mult_delta lemmas; simplify some proofs
huffman
parents: 29912
diff changeset
    93
lemma mult_delta_left:
89eadbe71e97 add mult_delta lemmas; simplify some proofs
huffman
parents: 29912
diff changeset
    94
  fixes x y :: "'a::mult_zero"
89eadbe71e97 add mult_delta lemmas; simplify some proofs
huffman
parents: 29912
diff changeset
    95
  shows "(if b then x else 0) * y = (if b then x * y else 0)"
89eadbe71e97 add mult_delta lemmas; simplify some proofs
huffman
parents: 29912
diff changeset
    96
  by simp
89eadbe71e97 add mult_delta lemmas; simplify some proofs
huffman
parents: 29912
diff changeset
    97
89eadbe71e97 add mult_delta lemmas; simplify some proofs
huffman
parents: 29912
diff changeset
    98
lemma mult_delta_right:
89eadbe71e97 add mult_delta lemmas; simplify some proofs
huffman
parents: 29912
diff changeset
    99
  fixes x y :: "'a::mult_zero"
89eadbe71e97 add mult_delta lemmas; simplify some proofs
huffman
parents: 29912
diff changeset
   100
  shows "x * (if b then y else 0) = (if b then x * y else 0)"
89eadbe71e97 add mult_delta lemmas; simplify some proofs
huffman
parents: 29912
diff changeset
   101
  by simp
89eadbe71e97 add mult_delta lemmas; simplify some proofs
huffman
parents: 29912
diff changeset
   102
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   103
lemma cond_value_iff: "f (if b then x else y) = (if b then f x else f y)"
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   104
  by auto
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   105
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   106
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   107
  by auto
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   108
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   109
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   110
subsection \<open>Formal power series form a commutative ring with unity, if the range of sequences
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   111
  they represent is a commutative ring with unity\<close>
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   112
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   113
instance fps :: (semigroup_add) semigroup_add
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   114
proof
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   115
  fix a b c :: "'a fps"
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   116
  show "a + b + c = a + (b + c)"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57418
diff changeset
   117
    by (simp add: fps_ext add.assoc)
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   118
qed
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   119
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   120
instance fps :: (ab_semigroup_add) ab_semigroup_add
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   121
proof
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   122
  fix a b :: "'a fps"
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   123
  show "a + b = b + a"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57418
diff changeset
   124
    by (simp add: fps_ext add.commute)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   125
qed
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   126
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   127
lemma fps_mult_assoc_lemma:
53195
e4b18828a817 tuned proofs;
wenzelm
parents: 53077
diff changeset
   128
  fixes k :: nat
e4b18828a817 tuned proofs;
wenzelm
parents: 53077
diff changeset
   129
    and f :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   130
  shows "(\<Sum>j=0..k. \<Sum>i=0..j. f i (j - i) (n - j)) =
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   131
         (\<Sum>j=0..k. \<Sum>i=0..k - j. f j i (n - j - i))"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   132
  by (induct k) (simp_all add: Suc_diff_le sum.distrib add.assoc)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   133
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   134
instance fps :: (semiring_0) semigroup_mult
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   135
proof
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   136
  fix a b c :: "'a fps"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   137
  show "(a * b) * c = a * (b * c)"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   138
  proof (rule fps_ext)
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   139
    fix n :: nat
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   140
    have "(\<Sum>j=0..n. \<Sum>i=0..j. a$i * b$(j - i) * c$(n - j)) =
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   141
          (\<Sum>j=0..n. \<Sum>i=0..n - j. a$j * b$i * c$(n - j - i))"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   142
      by (rule fps_mult_assoc_lemma)
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   143
    then show "((a * b) * c) $ n = (a * (b * c)) $ n"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   144
      by (simp add: fps_mult_nth sum_distrib_left sum_distrib_right mult.assoc)
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   145
  qed
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   146
qed
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   147
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   148
lemma fps_mult_commute_lemma:
52903
6c89225ddeba tuned proofs;
wenzelm
parents: 52902
diff changeset
   149
  fixes n :: nat
6c89225ddeba tuned proofs;
wenzelm
parents: 52902
diff changeset
   150
    and f :: "nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   151
  shows "(\<Sum>i=0..n. f i (n - i)) = (\<Sum>i=0..n. f (n - i) i)"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   152
  by (rule sum.reindex_bij_witness[where i="op - n" and j="op - n"]) auto
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   153
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   154
instance fps :: (comm_semiring_0) ab_semigroup_mult
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   155
proof
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   156
  fix a b :: "'a fps"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   157
  show "a * b = b * a"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   158
  proof (rule fps_ext)
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   159
    fix n :: nat
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   160
    have "(\<Sum>i=0..n. a$i * b$(n - i)) = (\<Sum>i=0..n. a$(n - i) * b$i)"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   161
      by (rule fps_mult_commute_lemma)
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   162
    then show "(a * b) $ n = (b * a) $ n"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57418
diff changeset
   163
      by (simp add: fps_mult_nth mult.commute)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   164
  qed
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   165
qed
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   166
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   167
instance fps :: (monoid_add) monoid_add
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   168
proof
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   169
  fix a :: "'a fps"
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   170
  show "0 + a = a" by (simp add: fps_ext)
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   171
  show "a + 0 = a" by (simp add: fps_ext)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   172
qed
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   173
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   174
instance fps :: (comm_monoid_add) comm_monoid_add
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   175
proof
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   176
  fix a :: "'a fps"
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   177
  show "0 + a = a" by (simp add: fps_ext)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   178
qed
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   179
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   180
instance fps :: (semiring_1) monoid_mult
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   181
proof
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   182
  fix a :: "'a fps"
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   183
  show "1 * a = a"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   184
    by (simp add: fps_ext fps_mult_nth mult_delta_left sum.delta)
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   185
  show "a * 1 = a"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   186
    by (simp add: fps_ext fps_mult_nth mult_delta_right sum.delta')
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   187
qed
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   188
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   189
instance fps :: (cancel_semigroup_add) cancel_semigroup_add
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   190
proof
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   191
  fix a b c :: "'a fps"
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   192
  show "b = c" if "a + b = a + c"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   193
    using that by (simp add: expand_fps_eq)
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   194
  show "b = c" if "b + a = c + a"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   195
    using that by (simp add: expand_fps_eq)
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   196
qed
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   197
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   198
instance fps :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   199
proof
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   200
  fix a b c :: "'a fps"
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   201
  show "a + b - a = b"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   202
    by (simp add: expand_fps_eq)
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   203
  show "a - b - c = a - (b + c)"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   204
    by (simp add: expand_fps_eq diff_diff_eq)
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   205
qed
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   206
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   207
instance fps :: (cancel_comm_monoid_add) cancel_comm_monoid_add ..
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   208
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   209
instance fps :: (group_add) group_add
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   210
proof
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   211
  fix a b :: "'a fps"
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   212
  show "- a + a = 0" by (simp add: fps_ext)
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 53374
diff changeset
   213
  show "a + - b = a - b" by (simp add: fps_ext)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   214
qed
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   215
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   216
instance fps :: (ab_group_add) ab_group_add
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   217
proof
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   218
  fix a b :: "'a fps"
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   219
  show "- a + a = 0" by (simp add: fps_ext)
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   220
  show "a - b = a + - b" by (simp add: fps_ext)
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   221
qed
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   222
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   223
instance fps :: (zero_neq_one) zero_neq_one
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60567
diff changeset
   224
  by standard (simp add: expand_fps_eq)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   225
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   226
instance fps :: (semiring_0) semiring
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   227
proof
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   228
  fix a b c :: "'a fps"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   229
  show "(a + b) * c = a * c + b * c"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   230
    by (simp add: expand_fps_eq fps_mult_nth distrib_right sum.distrib)
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   231
  show "a * (b + c) = a * b + a * c"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   232
    by (simp add: expand_fps_eq fps_mult_nth distrib_left sum.distrib)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   233
qed
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   234
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   235
instance fps :: (semiring_0) semiring_0
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   236
proof
53195
e4b18828a817 tuned proofs;
wenzelm
parents: 53077
diff changeset
   237
  fix a :: "'a fps"
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   238
  show "0 * a = 0"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   239
    by (simp add: fps_ext fps_mult_nth)
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   240
  show "a * 0 = 0"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   241
    by (simp add: fps_ext fps_mult_nth)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   242
qed
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   243
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   244
instance fps :: (semiring_0_cancel) semiring_0_cancel ..
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   245
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60679
diff changeset
   246
instance fps :: (semiring_1) semiring_1 ..
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60679
diff changeset
   247
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   248
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   249
subsection \<open>Selection of the nth power of the implicit variable in the infinite sum\<close>
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   250
63317
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   251
lemma fps_square_nth: "(f^2) $ n = (\<Sum>k\<le>n. f $ k * f $ (n - k))"
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   252
  by (simp add: power2_eq_square fps_mult_nth atLeast0AtMost)
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   253
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   254
lemma fps_nonzero_nth: "f \<noteq> 0 \<longleftrightarrow> (\<exists> n. f $n \<noteq> 0)"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   255
  by (simp add: expand_fps_eq)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   256
52902
7196e1ce1cd8 tuned proofs;
wenzelm
parents: 52891
diff changeset
   257
lemma fps_nonzero_nth_minimal: "f \<noteq> 0 \<longleftrightarrow> (\<exists>n. f $ n \<noteq> 0 \<and> (\<forall>m < n. f $ m = 0))"
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   258
  (is "?lhs \<longleftrightarrow> ?rhs")
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   259
proof
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   260
  let ?n = "LEAST n. f $ n \<noteq> 0"
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   261
  show ?rhs if ?lhs
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   262
  proof -
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   263
    from that have "\<exists>n. f $ n \<noteq> 0"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   264
      by (simp add: fps_nonzero_nth)
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   265
    then have "f $ ?n \<noteq> 0"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   266
      by (rule LeastI_ex)
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   267
    moreover have "\<forall>m<?n. f $ m = 0"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   268
      by (auto dest: not_less_Least)
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   269
    ultimately have "f $ ?n \<noteq> 0 \<and> (\<forall>m<?n. f $ m = 0)" ..
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   270
    then show ?thesis ..
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   271
  qed
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   272
  show ?lhs if ?rhs
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   273
    using that by (auto simp add: expand_fps_eq)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   274
qed
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   275
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   276
lemma fps_eq_iff: "f = g \<longleftrightarrow> (\<forall>n. f $ n = g $n)"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   277
  by (rule expand_fps_eq)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   278
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   279
lemma fps_sum_nth: "sum f S $ n = sum (\<lambda>k. (f k) $ n) S"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   280
proof (cases "finite S")
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   281
  case True
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   282
  then show ?thesis by (induct set: finite) auto
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   283
next
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   284
  case False
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   285
  then show ?thesis by simp
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   286
qed
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   287
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   288
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   289
subsection \<open>Injection of the basic ring elements and multiplication by scalars\<close>
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   290
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   291
definition "fps_const c = Abs_fps (\<lambda>n. if n = 0 then c else 0)"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   292
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   293
lemma fps_nth_fps_const [simp]: "fps_const c $ n = (if n = 0 then c else 0)"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   294
  unfolding fps_const_def by simp
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   295
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   296
lemma fps_const_0_eq_0 [simp]: "fps_const 0 = 0"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   297
  by (simp add: fps_ext)
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   298
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   299
lemma fps_const_1_eq_1 [simp]: "fps_const 1 = 1"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   300
  by (simp add: fps_ext)
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   301
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   302
lemma fps_const_neg [simp]: "- (fps_const (c::'a::ring)) = fps_const (- c)"
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   303
  by (simp add: fps_ext)
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   304
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   305
lemma fps_const_add [simp]: "fps_const (c::'a::monoid_add) + fps_const d = fps_const (c + d)"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   306
  by (simp add: fps_ext)
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   307
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   308
lemma fps_const_sub [simp]: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
31369
8b460fd12100 Reverses idempotent; radical of E; generalized logarithm;
chaieb
parents: 31199
diff changeset
   309
  by (simp add: fps_ext)
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   310
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   311
lemma fps_const_mult[simp]: "fps_const (c::'a::ring) * fps_const d = fps_const (c * d)"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   312
  by (simp add: fps_eq_iff fps_mult_nth sum.neutral)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   313
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   314
lemma fps_const_add_left: "fps_const (c::'a::monoid_add) + f =
48757
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
   315
    Abs_fps (\<lambda>n. if n = 0 then c + f$0 else f$n)"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   316
  by (simp add: fps_ext)
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   317
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   318
lemma fps_const_add_right: "f + fps_const (c::'a::monoid_add) =
48757
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
   319
    Abs_fps (\<lambda>n. if n = 0 then f$0 + c else f$n)"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   320
  by (simp add: fps_ext)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   321
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   322
lemma fps_const_mult_left: "fps_const (c::'a::semiring_0) * f = Abs_fps (\<lambda>n. c * f$n)"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   323
  unfolding fps_eq_iff fps_mult_nth
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   324
  by (simp add: fps_const_def mult_delta_left sum.delta)
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   325
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   326
lemma fps_const_mult_right: "f * fps_const (c::'a::semiring_0) = Abs_fps (\<lambda>n. f$n * c)"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   327
  unfolding fps_eq_iff fps_mult_nth
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   328
  by (simp add: fps_const_def mult_delta_right sum.delta')
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   329
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   330
lemma fps_mult_left_const_nth [simp]: "(fps_const (c::'a::semiring_1) * f)$n = c* f$n"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   331
  by (simp add: fps_mult_nth mult_delta_left sum.delta)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   332
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   333
lemma fps_mult_right_const_nth [simp]: "(f * fps_const (c::'a::semiring_1))$n = f$n * c"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   334
  by (simp add: fps_mult_nth mult_delta_right sum.delta')
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   335
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   336
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   337
subsection \<open>Formal power series form an integral domain\<close>
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   338
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   339
instance fps :: (ring) ring ..
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   340
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   341
instance fps :: (ring_1) ring_1
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 53374
diff changeset
   342
  by (intro_classes, auto simp add: distrib_right)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   343
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   344
instance fps :: (comm_ring_1) comm_ring_1
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 53374
diff changeset
   345
  by (intro_classes, auto simp add: distrib_right)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   346
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   347
instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   348
proof
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   349
  fix a b :: "'a fps"
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   350
  assume "a \<noteq> 0" and "b \<noteq> 0"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   351
  then obtain i j where i: "a $ i \<noteq> 0" "\<forall>k<i. a $ k = 0" and j: "b $ j \<noteq> 0" "\<forall>k<j. b $ k =0"
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   352
    unfolding fps_nonzero_nth_minimal
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   353
    by blast+
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   354
  have "(a * b) $ (i + j) = (\<Sum>k=0..i+j. a $ k * b $ (i + j - k))"
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   355
    by (rule fps_mult_nth)
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   356
  also have "\<dots> = (a $ i * b $ (i + j - i)) + (\<Sum>k\<in>{0..i+j} - {i}. a $ k * b $ (i + j - k))"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   357
    by (rule sum.remove) simp_all
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   358
  also have "(\<Sum>k\<in>{0..i+j}-{i}. a $ k * b $ (i + j - k)) = 0"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   359
  proof (rule sum.neutral [rule_format])
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   360
    fix k assume "k \<in> {0..i+j} - {i}"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   361
    then have "k < i \<or> i+j-k < j"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   362
      by auto
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   363
    then show "a $ k * b $ (i + j - k) = 0"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   364
      using i j by auto
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   365
  qed
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   366
  also have "a $ i * b $ (i + j - i) + 0 = a $ i * b $ j"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   367
    by simp
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   368
  also have "a $ i * b $ j \<noteq> 0"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   369
    using i j by simp
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   370
  finally have "(a*b) $ (i+j) \<noteq> 0" .
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   371
  then show "a * b \<noteq> 0"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   372
    unfolding fps_nonzero_nth by blast
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   373
qed
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   374
36311
ed3a87a7f977 epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
haftmann
parents: 36309
diff changeset
   375
instance fps :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
ed3a87a7f977 epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
haftmann
parents: 36309
diff changeset
   376
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   377
instance fps :: (idom) idom ..
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   378
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46757
diff changeset
   379
lemma numeral_fps_const: "numeral k = fps_const (numeral k)"
48757
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
   380
  by (induct k) (simp_all only: numeral.simps fps_const_1_eq_1
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46757
diff changeset
   381
    fps_const_add [symmetric])
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46757
diff changeset
   382
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60679
diff changeset
   383
lemma neg_numeral_fps_const:
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60679
diff changeset
   384
  "(- numeral k :: 'a :: ring_1 fps) = fps_const (- numeral k)"
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60679
diff changeset
   385
  by (simp add: numeral_fps_const)
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46757
diff changeset
   386
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   387
lemma fps_numeral_nth: "numeral n $ i = (if i = 0 then numeral n else 0)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   388
  by (simp add: numeral_fps_const)
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   389
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   390
lemma fps_numeral_nth_0 [simp]: "numeral n $ 0 = numeral n"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   391
  by (simp add: numeral_fps_const)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   392
63317
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   393
lemma fps_of_nat: "fps_const (of_nat c) = of_nat c"
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   394
  by (induction c) (simp_all add: fps_const_add [symmetric] del: fps_const_add)
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   395
65396
b42167902f57 moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
eberlm <eberlm@in.tum.de>
parents: 64786
diff changeset
   396
lemma numeral_neq_fps_zero [simp]: "(numeral f :: 'a :: field_char_0 fps) \<noteq> 0"
b42167902f57 moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
eberlm <eberlm@in.tum.de>
parents: 64786
diff changeset
   397
proof
b42167902f57 moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
eberlm <eberlm@in.tum.de>
parents: 64786
diff changeset
   398
  assume "numeral f = (0 :: 'a fps)"
b42167902f57 moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
eberlm <eberlm@in.tum.de>
parents: 64786
diff changeset
   399
  from arg_cong[of _ _ "\<lambda>F. F $ 0", OF this] show False by simp
b42167902f57 moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
eberlm <eberlm@in.tum.de>
parents: 64786
diff changeset
   400
qed 
63317
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   401
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   402
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   403
subsection \<open>The eXtractor series X\<close>
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   404
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   405
lemma minus_one_power_iff: "(- (1::'a::comm_ring_1)) ^ n = (if even n then 1 else - 1)"
48757
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
   406
  by (induct n) auto
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   407
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   408
definition "X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)"
53195
e4b18828a817 tuned proofs;
wenzelm
parents: 53077
diff changeset
   409
e4b18828a817 tuned proofs;
wenzelm
parents: 53077
diff changeset
   410
lemma X_mult_nth [simp]:
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   411
  "(X * (f :: 'a::semiring_1 fps)) $n = (if n = 0 then 0 else f $ (n - 1))"
53195
e4b18828a817 tuned proofs;
wenzelm
parents: 53077
diff changeset
   412
proof (cases "n = 0")
e4b18828a817 tuned proofs;
wenzelm
parents: 53077
diff changeset
   413
  case False
e4b18828a817 tuned proofs;
wenzelm
parents: 53077
diff changeset
   414
  have "(X * f) $n = (\<Sum>i = 0..n. X $ i * f $ (n - i))"
e4b18828a817 tuned proofs;
wenzelm
parents: 53077
diff changeset
   415
    by (simp add: fps_mult_nth)
e4b18828a817 tuned proofs;
wenzelm
parents: 53077
diff changeset
   416
  also have "\<dots> = f $ (n - 1)"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   417
    using False by (simp add: X_def mult_delta_left sum.delta)
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   418
  finally show ?thesis
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   419
    using False by simp
53195
e4b18828a817 tuned proofs;
wenzelm
parents: 53077
diff changeset
   420
next
e4b18828a817 tuned proofs;
wenzelm
parents: 53077
diff changeset
   421
  case True
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   422
  then show ?thesis
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   423
    by (simp add: fps_mult_nth X_def)
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   424
qed
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   425
48757
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
   426
lemma X_mult_right_nth[simp]:
63317
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   427
  "((a::'a::semiring_1 fps) * X) $ n = (if n = 0 then 0 else a $ (n - 1))"
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   428
proof -
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   429
  have "(a * X) $ n = (\<Sum>i = 0..n. a $ i * (if n - i = Suc 0 then 1 else 0))"
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   430
    by (simp add: fps_times_def X_def)
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   431
  also have "\<dots> = (\<Sum>i = 0..n. if i = n - 1 then if n = 0 then 0 else a $ i else 0)"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   432
    by (intro sum.cong) auto
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   433
  also have "\<dots> = (if n = 0 then 0 else a $ (n - 1))" by (simp add: sum.delta)
63317
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   434
  finally show ?thesis .
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   435
qed
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   436
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   437
lemma fps_mult_X_commute: "X * (a :: 'a :: semiring_1 fps) = a * X" 
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
   438
  by (simp add: fps_eq_iff)
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   439
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   440
lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then 1::'a::comm_ring_1 else 0)"
52902
7196e1ce1cd8 tuned proofs;
wenzelm
parents: 52891
diff changeset
   441
proof (induct k)
7196e1ce1cd8 tuned proofs;
wenzelm
parents: 52891
diff changeset
   442
  case 0
54452
f3090621446e tuned proofs;
wenzelm
parents: 54263
diff changeset
   443
  then show ?case by (simp add: X_def fps_eq_iff)
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   444
next
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   445
  case (Suc k)
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   446
  have "(X^Suc k) $ m = (if m = Suc k then 1::'a else 0)" for m
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   447
  proof -
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   448
    have "(X^Suc k) $ m = (if m = 0 then 0 else (X^k) $ (m - 1))"
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   449
      by (simp del: One_nat_def)
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   450
    then show ?thesis
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   451
      using Suc.hyps by (auto cong del: if_weak_cong)
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   452
  qed
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   453
  then show ?case
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   454
    by (simp add: fps_eq_iff)
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   455
qed
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   456
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   457
lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   458
  by (simp add: X_def)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   459
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   460
lemma X_power_nth[simp]: "(X^k) $n = (if n = k then 1 else 0::'a::comm_ring_1)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   461
  by (simp add: X_power_iff)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   462
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   463
lemma X_power_mult_nth: "(X^k * (f :: 'a::comm_ring_1 fps)) $n = (if n < k then 0 else f $ (n - k))"
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   464
  apply (induct k arbitrary: n)
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   465
  apply simp
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57418
diff changeset
   466
  unfolding power_Suc mult.assoc
48757
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
   467
  apply (case_tac n)
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
   468
  apply auto
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
   469
  done
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
   470
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
   471
lemma X_power_mult_right_nth:
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   472
    "((f :: 'a::comm_ring_1 fps) * X^k) $n = (if n < k then 0 else f $ (n - k))"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57418
diff changeset
   473
  by (metis X_power_mult_nth mult.commute)
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   474
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   475
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   476
lemma X_neq_fps_const [simp]: "(X :: 'a :: zero_neq_one fps) \<noteq> fps_const c"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   477
proof
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   478
  assume "(X::'a fps) = fps_const (c::'a)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   479
  hence "X$1 = (fps_const (c::'a))$1" by (simp only:)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   480
  thus False by auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   481
qed
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   482
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   483
lemma X_neq_zero [simp]: "(X :: 'a :: zero_neq_one fps) \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   484
  by (simp only: fps_const_0_eq_0[symmetric] X_neq_fps_const) simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   485
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   486
lemma X_neq_one [simp]: "(X :: 'a :: zero_neq_one fps) \<noteq> 1"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   487
  by (simp only: fps_const_1_eq_1[symmetric] X_neq_fps_const) simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   488
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   489
lemma X_neq_numeral [simp]: "(X :: 'a :: {semiring_1,zero_neq_one} fps) \<noteq> numeral c"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   490
  by (simp only: numeral_fps_const X_neq_fps_const) simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   491
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   492
lemma X_pow_eq_X_pow_iff [simp]:
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   493
  "(X :: ('a :: {comm_ring_1}) fps) ^ m = X ^ n \<longleftrightarrow> m = n"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   494
proof
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   495
  assume "(X :: 'a fps) ^ m = X ^ n"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   496
  hence "(X :: 'a fps) ^ m $ m = X ^ n $ m" by (simp only:)
62390
842917225d56 more canonical names
nipkow
parents: 62343
diff changeset
   497
  thus "m = n" by (simp split: if_split_asm)
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   498
qed simp_all
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   499
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   500
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   501
subsection \<open>Subdegrees\<close>
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   502
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   503
definition subdegree :: "('a::zero) fps \<Rightarrow> nat" where
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   504
  "subdegree f = (if f = 0 then 0 else LEAST n. f$n \<noteq> 0)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   505
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   506
lemma subdegreeI:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   507
  assumes "f $ d \<noteq> 0" and "\<And>i. i < d \<Longrightarrow> f $ i = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   508
  shows   "subdegree f = d"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   509
proof-
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   510
  from assms(1) have "f \<noteq> 0" by auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   511
  moreover from assms(1) have "(LEAST i. f $ i \<noteq> 0) = d"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   512
  proof (rule Least_equality)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   513
    fix e assume "f $ e \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   514
    with assms(2) have "\<not>(e < d)" by blast
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   515
    thus "e \<ge> d" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   516
  qed
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   517
  ultimately show ?thesis unfolding subdegree_def by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   518
qed
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   519
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   520
lemma nth_subdegree_nonzero [simp,intro]: "f \<noteq> 0 \<Longrightarrow> f $ subdegree f \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   521
proof-
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   522
  assume "f \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   523
  hence "subdegree f = (LEAST n. f $ n \<noteq> 0)" by (simp add: subdegree_def)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   524
  also from \<open>f \<noteq> 0\<close> have "\<exists>n. f$n \<noteq> 0" using fps_nonzero_nth by blast
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   525
  from LeastI_ex[OF this] have "f $ (LEAST n. f $ n \<noteq> 0) \<noteq> 0" .
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   526
  finally show ?thesis .
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   527
qed
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   528
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   529
lemma nth_less_subdegree_zero [dest]: "n < subdegree f \<Longrightarrow> f $ n = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   530
proof (cases "f = 0")
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   531
  assume "f \<noteq> 0" and less: "n < subdegree f"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   532
  note less
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   533
  also from \<open>f \<noteq> 0\<close> have "subdegree f = (LEAST n. f $ n \<noteq> 0)" by (simp add: subdegree_def)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   534
  finally show "f $ n = 0" using not_less_Least by blast
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   535
qed simp_all
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   536
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   537
lemma subdegree_geI:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   538
  assumes "f \<noteq> 0" "\<And>i. i < n \<Longrightarrow> f$i = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   539
  shows   "subdegree f \<ge> n"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   540
proof (rule ccontr)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   541
  assume "\<not>(subdegree f \<ge> n)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   542
  with assms(2) have "f $ subdegree f = 0" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   543
  moreover from assms(1) have "f $ subdegree f \<noteq> 0" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   544
  ultimately show False by contradiction
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   545
qed
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   546
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   547
lemma subdegree_greaterI:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   548
  assumes "f \<noteq> 0" "\<And>i. i \<le> n \<Longrightarrow> f$i = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   549
  shows   "subdegree f > n"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   550
proof (rule ccontr)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   551
  assume "\<not>(subdegree f > n)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   552
  with assms(2) have "f $ subdegree f = 0" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   553
  moreover from assms(1) have "f $ subdegree f \<noteq> 0" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   554
  ultimately show False by contradiction
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   555
qed
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   556
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   557
lemma subdegree_leI:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   558
  "f $ n \<noteq> 0 \<Longrightarrow> subdegree f \<le> n"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   559
  by (rule leI) auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   560
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   561
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   562
lemma subdegree_0 [simp]: "subdegree 0 = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   563
  by (simp add: subdegree_def)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   564
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   565
lemma subdegree_1 [simp]: "subdegree (1 :: ('a :: zero_neq_one) fps) = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   566
  by (auto intro!: subdegreeI)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   567
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   568
lemma subdegree_X [simp]: "subdegree (X :: ('a :: zero_neq_one) fps) = 1"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   569
  by (auto intro!: subdegreeI simp: X_def)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   570
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   571
lemma subdegree_fps_const [simp]: "subdegree (fps_const c) = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   572
  by (cases "c = 0") (auto intro!: subdegreeI)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   573
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   574
lemma subdegree_numeral [simp]: "subdegree (numeral n) = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   575
  by (simp add: numeral_fps_const)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   576
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   577
lemma subdegree_eq_0_iff: "subdegree f = 0 \<longleftrightarrow> f = 0 \<or> f $ 0 \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   578
proof (cases "f = 0")
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   579
  assume "f \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   580
  thus ?thesis
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   581
    using nth_subdegree_nonzero[OF \<open>f \<noteq> 0\<close>] by (fastforce intro!: subdegreeI)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   582
qed simp_all
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   583
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   584
lemma subdegree_eq_0 [simp]: "f $ 0 \<noteq> 0 \<Longrightarrow> subdegree f = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   585
  by (simp add: subdegree_eq_0_iff)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   586
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   587
lemma nth_subdegree_mult [simp]:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   588
  fixes f g :: "('a :: {mult_zero,comm_monoid_add}) fps"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   589
  shows "(f * g) $ (subdegree f + subdegree g) = f $ subdegree f * g $ subdegree g"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   590
proof-
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   591
  let ?n = "subdegree f + subdegree g"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   592
  have "(f * g) $ ?n = (\<Sum>i=0..?n. f$i * g$(?n-i))"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   593
    by (simp add: fps_mult_nth)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   594
  also have "... = (\<Sum>i=0..?n. if i = subdegree f then f$i * g$(?n-i) else 0)"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   595
  proof (intro sum.cong)
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   596
    fix x assume x: "x \<in> {0..?n}"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   597
    hence "x = subdegree f \<or> x < subdegree f \<or> ?n - x < subdegree g" by auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   598
    thus "f $ x * g $ (?n - x) = (if x = subdegree f then f $ x * g $ (?n - x) else 0)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   599
      by (elim disjE conjE) auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   600
  qed auto
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   601
  also have "... = f $ subdegree f * g $ subdegree g" by (simp add: sum.delta)
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   602
  finally show ?thesis .
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   603
qed
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   604
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   605
lemma subdegree_mult [simp]:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   606
  assumes "f \<noteq> 0" "g \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   607
  shows "subdegree ((f :: ('a :: {ring_no_zero_divisors}) fps) * g) = subdegree f + subdegree g"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   608
proof (rule subdegreeI)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   609
  let ?n = "subdegree f + subdegree g"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   610
  have "(f * g) $ ?n = (\<Sum>i=0..?n. f$i * g$(?n-i))" by (simp add: fps_mult_nth)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   611
  also have "... = (\<Sum>i=0..?n. if i = subdegree f then f$i * g$(?n-i) else 0)"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   612
  proof (intro sum.cong)
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   613
    fix x assume x: "x \<in> {0..?n}"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   614
    hence "x = subdegree f \<or> x < subdegree f \<or> ?n - x < subdegree g" by auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   615
    thus "f $ x * g $ (?n - x) = (if x = subdegree f then f $ x * g $ (?n - x) else 0)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   616
      by (elim disjE conjE) auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   617
  qed auto
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   618
  also have "... = f $ subdegree f * g $ subdegree g" by (simp add: sum.delta)
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   619
  also from assms have "... \<noteq> 0" by auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   620
  finally show "(f * g) $ (subdegree f + subdegree g) \<noteq> 0" .
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   621
next
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   622
  fix m assume m: "m < subdegree f + subdegree g"
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   623
  have "(f * g) $ m = (\<Sum>i=0..m. f$i * g$(m-i))" by (simp add: fps_mult_nth)
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   624
  also have "... = (\<Sum>i=0..m. 0)"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   625
  proof (rule sum.cong)
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   626
    fix i assume "i \<in> {0..m}"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   627
    with m have "i < subdegree f \<or> m - i < subdegree g" by auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   628
    thus "f$i * g$(m-i) = 0" by (elim disjE) auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   629
  qed auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   630
  finally show "(f * g) $ m = 0" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   631
qed
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   632
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   633
lemma subdegree_power [simp]:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   634
  "subdegree ((f :: ('a :: ring_1_no_zero_divisors) fps) ^ n) = n * subdegree f"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   635
  by (cases "f = 0"; induction n) simp_all
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   636
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   637
lemma subdegree_uminus [simp]:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   638
  "subdegree (-(f::('a::group_add) fps)) = subdegree f"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   639
  by (simp add: subdegree_def)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   640
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   641
lemma subdegree_minus_commute [simp]:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   642
  "subdegree (f-(g::('a::group_add) fps)) = subdegree (g - f)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   643
proof -
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   644
  have "f - g = -(g - f)" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   645
  also have "subdegree ... = subdegree (g - f)" by (simp only: subdegree_uminus)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   646
  finally show ?thesis .
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   647
qed
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   648
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   649
lemma subdegree_add_ge:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   650
  assumes "f \<noteq> -(g :: ('a :: {group_add}) fps)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   651
  shows   "subdegree (f + g) \<ge> min (subdegree f) (subdegree g)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   652
proof (rule subdegree_geI)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   653
  from assms show "f + g \<noteq> 0" by (subst (asm) eq_neg_iff_add_eq_0)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   654
next
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   655
  fix i assume "i < min (subdegree f) (subdegree g)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   656
  hence "f $ i = 0" and "g $ i = 0" by auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   657
  thus "(f + g) $ i = 0" by force
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   658
qed
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   659
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   660
lemma subdegree_add_eq1:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   661
  assumes "f \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   662
  assumes "subdegree f < subdegree (g :: ('a :: {group_add}) fps)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   663
  shows   "subdegree (f + g) = subdegree f"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   664
proof (rule antisym[OF subdegree_leI])
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   665
  from assms show "subdegree (f + g) \<ge> subdegree f"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   666
    by (intro order.trans[OF min.boundedI subdegree_add_ge]) auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   667
  from assms have "f $ subdegree f \<noteq> 0" "g $ subdegree f = 0" by auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   668
  thus "(f + g) $ subdegree f \<noteq> 0" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   669
qed
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   670
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   671
lemma subdegree_add_eq2:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   672
  assumes "g \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   673
  assumes "subdegree g < subdegree (f :: ('a :: {ab_group_add}) fps)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   674
  shows   "subdegree (f + g) = subdegree g"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   675
  using subdegree_add_eq1[OF assms] by (simp add: add.commute)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   676
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   677
lemma subdegree_diff_eq1:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   678
  assumes "f \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   679
  assumes "subdegree f < subdegree (g :: ('a :: {ab_group_add}) fps)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   680
  shows   "subdegree (f - g) = subdegree f"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   681
  using subdegree_add_eq1[of f "-g"] assms by (simp add: add.commute)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   682
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   683
lemma subdegree_diff_eq2:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   684
  assumes "g \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   685
  assumes "subdegree g < subdegree (f :: ('a :: {ab_group_add}) fps)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   686
  shows   "subdegree (f - g) = subdegree g"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   687
  using subdegree_add_eq2[of "-g" f] assms by (simp add: add.commute)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   688
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   689
lemma subdegree_diff_ge [simp]:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   690
  assumes "f \<noteq> (g :: ('a :: {group_add}) fps)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   691
  shows   "subdegree (f - g) \<ge> min (subdegree f) (subdegree g)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   692
  using assms subdegree_add_ge[of f "-g"] by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   693
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   694
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   695
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   696
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   697
subsection \<open>Shifting and slicing\<close>
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   698
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   699
definition fps_shift :: "nat \<Rightarrow> 'a fps \<Rightarrow> 'a fps" where
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   700
  "fps_shift n f = Abs_fps (\<lambda>i. f $ (i + n))"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   701
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   702
lemma fps_shift_nth [simp]: "fps_shift n f $ i = f $ (i + n)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   703
  by (simp add: fps_shift_def)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   704
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   705
lemma fps_shift_0 [simp]: "fps_shift 0 f = f"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   706
  by (intro fps_ext) (simp add: fps_shift_def)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   707
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   708
lemma fps_shift_zero [simp]: "fps_shift n 0 = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   709
  by (intro fps_ext) (simp add: fps_shift_def)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   710
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   711
lemma fps_shift_one: "fps_shift n 1 = (if n = 0 then 1 else 0)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   712
  by (intro fps_ext) (simp add: fps_shift_def)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   713
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   714
lemma fps_shift_fps_const: "fps_shift n (fps_const c) = (if n = 0 then fps_const c else 0)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   715
  by (intro fps_ext) (simp add: fps_shift_def)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   716
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   717
lemma fps_shift_numeral: "fps_shift n (numeral c) = (if n = 0 then numeral c else 0)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   718
  by (simp add: numeral_fps_const fps_shift_fps_const)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   719
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   720
lemma fps_shift_X_power [simp]:
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   721
  "n \<le> m \<Longrightarrow> fps_shift n (X ^ m) = (X ^ (m - n) ::'a::comm_ring_1 fps)"
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   722
  by (intro fps_ext) (auto simp: fps_shift_def )
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   723
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   724
lemma fps_shift_times_X_power:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   725
  "n \<le> subdegree f \<Longrightarrow> fps_shift n f * X ^ n = (f :: 'a :: comm_ring_1 fps)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   726
  by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   727
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   728
lemma fps_shift_times_X_power' [simp]:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   729
  "fps_shift n (f * X^n) = (f :: 'a :: comm_ring_1 fps)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   730
  by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   731
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   732
lemma fps_shift_times_X_power'':
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   733
  "m \<le> n \<Longrightarrow> fps_shift n (f * X^m) = fps_shift (n - m) (f :: 'a :: comm_ring_1 fps)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   734
  by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   735
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   736
lemma fps_shift_subdegree [simp]:
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   737
  "n \<le> subdegree f \<Longrightarrow> subdegree (fps_shift n f) = subdegree (f :: 'a :: comm_ring_1 fps) - n"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   738
  by (cases "f = 0") (force intro: nth_less_subdegree_zero subdegreeI)+
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   739
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   740
lemma subdegree_decompose:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   741
  "f = fps_shift (subdegree f) f * X ^ subdegree (f :: ('a :: comm_ring_1) fps)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   742
  by (rule fps_ext) (auto simp: X_power_mult_right_nth)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   743
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   744
lemma subdegree_decompose':
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   745
  "n \<le> subdegree (f :: ('a :: comm_ring_1) fps) \<Longrightarrow> f = fps_shift n f * X^n"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   746
  by (rule fps_ext) (auto simp: X_power_mult_right_nth intro!: nth_less_subdegree_zero)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   747
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   748
lemma fps_shift_fps_shift:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   749
  "fps_shift (m + n) f = fps_shift m (fps_shift n f)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   750
  by (rule fps_ext) (simp add: add_ac)
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   751
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   752
lemma fps_shift_add:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   753
  "fps_shift n (f + g) = fps_shift n f + fps_shift n g"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   754
  by (simp add: fps_eq_iff)
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   755
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   756
lemma fps_shift_mult:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   757
  assumes "n \<le> subdegree (g :: 'b :: {comm_ring_1} fps)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   758
  shows   "fps_shift n (h*g) = h * fps_shift n g"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   759
proof -
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   760
  from assms have "g = fps_shift n g * X^n" by (rule subdegree_decompose')
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   761
  also have "h * ... = (h * fps_shift n g) * X^n" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   762
  also have "fps_shift n ... = h * fps_shift n g" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   763
  finally show ?thesis .
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   764
qed
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   765
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   766
lemma fps_shift_mult_right:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   767
  assumes "n \<le> subdegree (g :: 'b :: {comm_ring_1} fps)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   768
  shows   "fps_shift n (g*h) = h * fps_shift n g"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   769
  by (subst mult.commute, subst fps_shift_mult) (simp_all add: assms)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   770
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   771
lemma nth_subdegree_zero_iff [simp]: "f $ subdegree f = 0 \<longleftrightarrow> f = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   772
  by (cases "f = 0") auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   773
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   774
lemma fps_shift_subdegree_zero_iff [simp]:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   775
  "fps_shift (subdegree f) f = 0 \<longleftrightarrow> f = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   776
  by (subst (1) nth_subdegree_zero_iff[symmetric], cases "f = 0")
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   777
     (simp_all del: nth_subdegree_zero_iff)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   778
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   779
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   780
definition "fps_cutoff n f = Abs_fps (\<lambda>i. if i < n then f$i else 0)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   781
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   782
lemma fps_cutoff_nth [simp]: "fps_cutoff n f $ i = (if i < n then f$i else 0)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   783
  unfolding fps_cutoff_def by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   784
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   785
lemma fps_cutoff_zero_iff: "fps_cutoff n f = 0 \<longleftrightarrow> (f = 0 \<or> n \<le> subdegree f)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   786
proof
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   787
  assume A: "fps_cutoff n f = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   788
  thus "f = 0 \<or> n \<le> subdegree f"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   789
  proof (cases "f = 0")
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   790
    assume "f \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   791
    with A have "n \<le> subdegree f"
62390
842917225d56 more canonical names
nipkow
parents: 62343
diff changeset
   792
      by (intro subdegree_geI) (auto simp: fps_eq_iff split: if_split_asm)
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   793
    thus ?thesis ..
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   794
  qed simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   795
qed (auto simp: fps_eq_iff intro: nth_less_subdegree_zero)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   796
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   797
lemma fps_cutoff_0 [simp]: "fps_cutoff 0 f = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   798
  by (simp add: fps_eq_iff)
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   799
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   800
lemma fps_cutoff_zero [simp]: "fps_cutoff n 0 = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   801
  by (simp add: fps_eq_iff)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   802
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   803
lemma fps_cutoff_one: "fps_cutoff n 1 = (if n = 0 then 0 else 1)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   804
  by (simp add: fps_eq_iff)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   805
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   806
lemma fps_cutoff_fps_const: "fps_cutoff n (fps_const c) = (if n = 0 then 0 else fps_const c)"
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   807
  by (simp add: fps_eq_iff)
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   808
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   809
lemma fps_cutoff_numeral: "fps_cutoff n (numeral c) = (if n = 0 then 0 else numeral c)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   810
  by (simp add: numeral_fps_const fps_cutoff_fps_const)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   811
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   812
lemma fps_shift_cutoff:
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   813
  "fps_shift n (f :: ('a :: comm_ring_1) fps) * X^n + fps_cutoff n f = f"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   814
  by (simp add: fps_eq_iff X_power_mult_right_nth)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   815
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   816
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   817
subsection \<open>Formal Power series form a metric space\<close>
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   818
52902
7196e1ce1cd8 tuned proofs;
wenzelm
parents: 52891
diff changeset
   819
definition (in dist) "ball x r = {y. dist y x < r}"
48757
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
   820
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   821
instantiation fps :: (comm_ring_1) dist
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   822
begin
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   823
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   824
definition
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   825
  dist_fps_def: "dist (a :: 'a fps) b = (if a = b then 0 else inverse (2 ^ subdegree (a - b)))"
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   826
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   827
lemma dist_fps_ge0: "dist (a :: 'a fps) b \<ge> 0"
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   828
  by (simp add: dist_fps_def)
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   829
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   830
lemma dist_fps_sym: "dist (a :: 'a fps) b = dist b a"
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   831
  by (simp add: dist_fps_def)
48757
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
   832
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   833
instance ..
48757
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
   834
30746
d6915b738bd9 fps made instance of number_ring
chaieb
parents: 30488
diff changeset
   835
end
d6915b738bd9 fps made instance of number_ring
chaieb
parents: 30488
diff changeset
   836
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   837
instantiation fps :: (comm_ring_1) metric_space
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   838
begin
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   839
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61969
diff changeset
   840
definition uniformity_fps_def [code del]:
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61969
diff changeset
   841
  "(uniformity :: ('a fps \<times> 'a fps) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61969
diff changeset
   842
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61969
diff changeset
   843
definition open_fps_def' [code del]:
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61969
diff changeset
   844
  "open (U :: 'a fps set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   845
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   846
instance
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   847
proof
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   848
  show th: "dist a b = 0 \<longleftrightarrow> a = b" for a b :: "'a fps"
62390
842917225d56 more canonical names
nipkow
parents: 62343
diff changeset
   849
    by (simp add: dist_fps_def split: if_split_asm)
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   850
  then have th'[simp]: "dist a a = 0" for a :: "'a fps" by simp
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   851
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   852
  fix a b c :: "'a fps"
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   853
  consider "a = b" | "c = a \<or> c = b" | "a \<noteq> b" "a \<noteq> c" "b \<noteq> c" by blast
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   854
  then show "dist a b \<le> dist a c + dist b c"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   855
  proof cases
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   856
    case 1
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   857
    then show ?thesis by (simp add: dist_fps_def)
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   858
  next
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   859
    case 2
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   860
    then show ?thesis
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   861
      by (cases "c = a") (simp_all add: th dist_fps_sym)
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   862
  next
60567
19c277ea65ae tuned proofs -- less digits;
wenzelm
parents: 60558
diff changeset
   863
    case neq: 3
60558
4fcc6861e64f tuned proofs;
wenzelm
parents: 60504
diff changeset
   864
    have False if "dist a b > dist a c + dist b c"
4fcc6861e64f tuned proofs;
wenzelm
parents: 60504
diff changeset
   865
    proof -
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   866
      let ?n = "subdegree (a - b)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   867
      from neq have "dist a b > 0" "dist b c > 0" and "dist a c > 0" by (simp_all add: dist_fps_def)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   868
      with that have "dist a b > dist a c" and "dist a b > dist b c" by simp_all
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   869
      with neq have "?n < subdegree (a - c)" and "?n < subdegree (b - c)"
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   870
        by (simp_all add: dist_fps_def field_simps)
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   871
      hence "(a - c) $ ?n = 0" and "(b - c) $ ?n = 0"
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   872
        by (simp_all only: nth_less_subdegree_zero)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   873
      hence "(a - b) $ ?n = 0" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   874
      moreover from neq have "(a - b) $ ?n \<noteq> 0" by (intro nth_subdegree_nonzero) simp_all
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   875
      ultimately show False by contradiction
60558
4fcc6861e64f tuned proofs;
wenzelm
parents: 60504
diff changeset
   876
    qed
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   877
    thus ?thesis by (auto simp add: not_le[symmetric])
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   878
  qed
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61969
diff changeset
   879
qed (rule open_fps_def' uniformity_fps_def)+
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   880
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   881
end
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   882
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   883
declare uniformity_Abort[where 'a="'a :: comm_ring_1 fps", code]
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   884
62101
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61969
diff changeset
   885
lemma open_fps_def: "open (S :: 'a::comm_ring_1 fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)"
26c0a70f78a3 add uniform spaces
hoelzl
parents: 61969
diff changeset
   886
  unfolding open_dist ball_def subset_eq by simp
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   887
60558
4fcc6861e64f tuned proofs;
wenzelm
parents: 60504
diff changeset
   888
text \<open>The infinite sums and justification of the notation in textbooks.\<close>
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   889
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   890
lemma reals_power_lt_ex:
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   891
  fixes x y :: real
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   892
  assumes xp: "x > 0"
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   893
    and y1: "y > 1"
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   894
  shows "\<exists>k>0. (1/y)^k < x"
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   895
proof -
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   896
  have yp: "y > 0"
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   897
    using y1 by simp
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   898
  from reals_Archimedean2[of "max 0 (- log y x) + 1"]
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   899
  obtain k :: nat where k: "real k > max 0 (- log y x) + 1"
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   900
    by blast
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   901
  from k have kp: "k > 0"
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   902
    by simp
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   903
  from k have "real k > - log y x"
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   904
    by simp
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   905
  then have "ln y * real k > - ln x"
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   906
    unfolding log_def
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   907
    using ln_gt_zero_iff[OF yp] y1
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   908
    by (simp add: minus_divide_left field_simps del: minus_divide_left[symmetric])
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   909
  then have "ln y * real k + ln x > 0"
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   910
    by simp
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   911
  then have "exp (real k * ln y + ln x) > exp 0"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
   912
    by (simp add: ac_simps)
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   913
  then have "y ^ k * x > 1"
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   914
    unfolding exp_zero exp_add exp_real_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   915
    by simp
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   916
  then have "x > (1 / y)^k" using yp
60867
86e7560e07d0 slight cleanup of lemmas
haftmann
parents: 60679
diff changeset
   917
    by (simp add: field_simps)
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   918
  then show ?thesis
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   919
    using kp by blast
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   920
qed
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   921
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   922
lemma fps_sum_rep_nth: "(sum (\<lambda>i. fps_const(a$i)*X^i) {0..m})$n =
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   923
    (if n \<le> m then a$n else 0::'a::comm_ring_1)"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   924
  apply (auto simp add: fps_sum_nth cond_value_iff cong del: if_weak_cong)
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   925
  apply (simp add: sum.delta')
48757
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
   926
  done
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   927
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   928
lemma fps_notation: "(\<lambda>n. sum (\<lambda>i. fps_const(a$i) * X^i) {0..n}) \<longlonglongrightarrow> a"
61969
e01015e49041 more symbols;
wenzelm
parents: 61943
diff changeset
   929
  (is "?s \<longlonglongrightarrow> a")
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   930
proof -
60558
4fcc6861e64f tuned proofs;
wenzelm
parents: 60504
diff changeset
   931
  have "\<exists>n0. \<forall>n \<ge> n0. dist (?s n) a < r" if "r > 0" for r
4fcc6861e64f tuned proofs;
wenzelm
parents: 60504
diff changeset
   932
  proof -
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   933
    obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   934
      using reals_power_lt_ex[OF \<open>r > 0\<close>, of 2] by auto
60558
4fcc6861e64f tuned proofs;
wenzelm
parents: 60504
diff changeset
   935
    show ?thesis
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   936
    proof -
60558
4fcc6861e64f tuned proofs;
wenzelm
parents: 60504
diff changeset
   937
      have "dist (?s n) a < r" if nn0: "n \<ge> n0" for n
4fcc6861e64f tuned proofs;
wenzelm
parents: 60504
diff changeset
   938
      proof -
4fcc6861e64f tuned proofs;
wenzelm
parents: 60504
diff changeset
   939
        from that have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0"
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   940
          by (simp add: divide_simps)
60558
4fcc6861e64f tuned proofs;
wenzelm
parents: 60504
diff changeset
   941
        show ?thesis
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   942
        proof (cases "?s n = a")
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   943
          case True
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   944
          then show ?thesis
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   945
            unfolding dist_eq_0_iff[of "?s n" a, symmetric]
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   946
            using \<open>r > 0\<close> by (simp del: dist_eq_0_iff)
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   947
        next
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   948
          case False
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   949
          from False have dth: "dist (?s n) a = (1/2)^subdegree (?s n - a)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   950
            by (simp add: dist_fps_def field_simps)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   951
          from False have kn: "subdegree (?s n - a) > n"
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   952
            by (intro subdegree_greaterI) (simp_all add: fps_sum_rep_nth)
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   953
          then have "dist (?s n) a < (1/2)^n"
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   954
            by (simp add: field_simps dist_fps_def)
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   955
          also have "\<dots> \<le> (1/2)^n0"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   956
            using nn0 by (simp add: divide_simps)
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   957
          also have "\<dots> < r"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   958
            using n0 by simp
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   959
          finally show ?thesis .
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   960
        qed
60558
4fcc6861e64f tuned proofs;
wenzelm
parents: 60504
diff changeset
   961
      qed
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   962
      then show ?thesis by blast
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   963
    qed
60558
4fcc6861e64f tuned proofs;
wenzelm
parents: 60504
diff changeset
   964
  qed
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   965
  then show ?thesis
60017
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59867
diff changeset
   966
    unfolding lim_sequentially by blast
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   967
qed
31968
0314441a53a6 FPS form a metric space, which justifies the infinte sum notation
chaieb
parents: 31790
diff changeset
   968
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   969
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   970
subsection \<open>Inverses of formal power series\<close>
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   971
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   972
declare sum.cong[fundef_cong]
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   973
60558
4fcc6861e64f tuned proofs;
wenzelm
parents: 60504
diff changeset
   974
instantiation fps :: ("{comm_monoid_add,inverse,times,uminus}") inverse
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   975
begin
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   976
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   977
fun natfun_inverse:: "'a fps \<Rightarrow> nat \<Rightarrow> 'a"
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   978
where
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   979
  "natfun_inverse f 0 = inverse (f$0)"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
   980
| "natfun_inverse f n = - inverse (f$0) * sum (\<lambda>i. f$i * natfun_inverse f (n - i)) {1..n}"
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   981
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   982
definition fps_inverse_def: "inverse f = (if f $ 0 = 0 then 0 else Abs_fps (natfun_inverse f))"
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
   983
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   984
definition fps_divide_def:
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
   985
  "f div g = (if g = 0 then 0 else
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   986
     let n = subdegree g; h = fps_shift n g
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
   987
     in  fps_shift n (f * inverse h))"
36311
ed3a87a7f977 epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
haftmann
parents: 36309
diff changeset
   988
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   989
instance ..
36311
ed3a87a7f977 epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
haftmann
parents: 36309
diff changeset
   990
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   991
end
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   992
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   993
lemma fps_inverse_zero [simp]:
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
   994
  "inverse (0 :: 'a::{comm_monoid_add,inverse,times,uminus} fps) = 0"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   995
  by (simp add: fps_ext fps_inverse_def)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
   996
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   997
lemma fps_inverse_one [simp]: "inverse (1 :: 'a::{division_ring,zero_neq_one} fps) = 1"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
   998
  apply (auto simp add: expand_fps_eq fps_inverse_def)
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
   999
  apply (case_tac n)
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
  1000
  apply auto
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
  1001
  done
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
  1002
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
  1003
lemma inverse_mult_eq_1 [intro]:
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
  1004
  assumes f0: "f$0 \<noteq> (0::'a::field)"
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1005
  shows "inverse f * f = 1"
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
  1006
proof -
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1007
  have c: "inverse f * f = f * inverse f"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57418
diff changeset
  1008
    by (simp add: mult.commute)
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30273
diff changeset
  1009
  from f0 have ifn: "\<And>n. inverse f $ n = natfun_inverse f n"
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1010
    by (simp add: fps_inverse_def)
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1011
  from f0 have th0: "(inverse f * f) $ 0 = 1"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
  1012
    by (simp add: fps_mult_nth fps_inverse_def)
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
  1013
  have "(inverse f * f)$n = 0" if np: "n > 0" for n
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
  1014
  proof -
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1015
    from np have eq: "{0..n} = {0} \<union> {1 .. n}"
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1016
      by auto
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1017
    have d: "{0} \<inter> {1 .. n} = {}"
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1018
      by auto
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
  1019
    from f0 np have th0: "- (inverse f $ n) =
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
  1020
      (sum (\<lambda>i. f$i * natfun_inverse f (n - i)) {1..n}) / (f$0)"
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
  1021
      by (cases n) (simp_all add: divide_inverse fps_inverse_def)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1022
    from th0[symmetric, unfolded nonzero_divide_eq_eq[OF f0]]
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
  1023
    have th1: "sum (\<lambda>i. f$i * natfun_inverse f (n - i)) {1..n} = - (f$0) * (inverse f)$n"
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36311
diff changeset
  1024
      by (simp add: field_simps)
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30273
diff changeset
  1025
    have "(f * inverse f) $ n = (\<Sum>i = 0..n. f $i * natfun_inverse f (n - i))"
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1026
      unfolding fps_mult_nth ifn ..
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
  1027
    also have "\<dots> = f$0 * natfun_inverse f n + (\<Sum>i = 1..n. f$i * natfun_inverse f (n-i))"
46757
ad878aff9c15 removing finiteness goals
bulwahn
parents: 46131
diff changeset
  1028
      by (simp add: eq)
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1029
    also have "\<dots> = 0"
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1030
      unfolding th1 ifn by simp
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
  1031
    finally show ?thesis unfolding c .
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
  1032
  qed
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1033
  with th0 show ?thesis
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1034
    by (simp add: fps_eq_iff)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1035
qed
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1036
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
  1037
lemma fps_inverse_0_iff[simp]: "(inverse f) $ 0 = (0::'a::division_ring) \<longleftrightarrow> f $ 0 = 0"
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
  1038
  by (simp add: fps_inverse_def nonzero_imp_inverse_nonzero)
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
  1039
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1040
lemma fps_inverse_nth_0 [simp]: "inverse f $ 0 = inverse (f $ 0 :: 'a :: division_ring)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1041
  by (simp add: fps_inverse_def)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1042
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1043
lemma fps_inverse_eq_0_iff[simp]: "inverse f = (0:: ('a::division_ring) fps) \<longleftrightarrow> f $ 0 = 0"
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
  1044
proof
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1045
  assume A: "inverse f = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1046
  have "0 = inverse f $ 0" by (subst A) simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1047
  thus "f $ 0 = 0" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1048
qed (simp add: fps_inverse_def)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1049
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1050
lemma fps_inverse_idempotent[intro, simp]:
48757
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
  1051
  assumes f0: "f$0 \<noteq> (0::'a::field)"
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1052
  shows "inverse (inverse f) = f"
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
  1053
proof -
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1054
  from f0 have if0: "inverse f $ 0 \<noteq> 0" by simp
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30273
diff changeset
  1055
  from inverse_mult_eq_1[OF f0] inverse_mult_eq_1[OF if0]
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
  1056
  have "inverse f * f = inverse f * inverse (inverse f)"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
  1057
    by (simp add: ac_simps)
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1058
  then show ?thesis
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1059
    using f0 unfolding mult_cancel_left by simp
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1060
qed
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1061
48757
1232760e208e tuned proofs;
wenzelm
parents: 47217
diff changeset
  1062
lemma fps_inverse_unique:
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1063
  assumes fg: "(f :: 'a :: field fps) * g = 1"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1064
  shows   "inverse f = g"
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
  1065
proof -
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1066
  have f0: "f $ 0 \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1067
  proof
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1068
    assume "f $ 0 = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1069
    hence "0 = (f * g) $ 0" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1070
    also from fg have "(f * g) $ 0 = 1" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1071
    finally show False by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1072
  qed
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1073
  from inverse_mult_eq_1[OF this] fg
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1074
  have th0: "inverse f * f = g * f"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
  1075
    by (simp add: ac_simps)
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1076
  then show ?thesis
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1077
    using f0
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1078
    unfolding mult_cancel_right
29911
c790a70a3d19 declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents: 29906
diff changeset
  1079
    by (auto simp add: expand_fps_eq)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1080
qed
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1081
63317
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
  1082
lemma fps_inverse_eq_0: "f$0 = 0 \<Longrightarrow> inverse (f :: 'a :: division_ring fps) = 0"
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
  1083
  by simp
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63040
diff changeset
  1084
  
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
  1085
lemma sum_zero_lemma:
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
  1086
  fixes n::nat
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
  1087
  assumes "0 < n"
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
  1088
  shows "(\<Sum>i = 0..n. if n = i then 1 else if n - i = 1 then - 1 else 0) = (0::'a::field)"
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1089
proof -
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
  1090
  let ?f = "\<lambda>i. if n = i then 1 else if n - i = 1 then - 1 else 0"
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
  1091
  let ?g = "\<lambda>i. if i = n then 1 else if i = n - 1 then - 1 else 0"
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1092
  let ?h = "\<lambda>i. if i=n - 1 then - 1 else 0"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
  1093
  have th1: "sum ?f {0..n} = sum ?g {0..n}"
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
  1094
    by (rule sum.cong) auto
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
  1095
  have th2: "sum ?g {0..n - 1} = sum ?h {0..n - 1}"
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
  1096
    apply (rule sum.cong)
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
  1097
    using assms
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1098
    apply auto
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1099
    done
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1100
  have eq: "{0 .. n} = {0.. n - 1} \<union> {n}"
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1101
    by auto
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
  1102
  from assms have d: "{0.. n - 1} \<inter> {n} = {}"
54681
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1103
    by auto
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1104
  have f: "finite {0.. n - 1}" "finite {n}"
8a8e6db7f391 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1105
    by auto
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
  1106
  show ?thesis
30488
5c4c3a9e9102 remove trailing spaces
huffman
parents: 30273
diff changeset
  1107
    unfolding th1
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
  1108
    apply (simp add: sum.union_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def)
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1109
    unfolding th2
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
  1110
    apply (simp add: sum.delta)
52891
b8dede3a4f1d tuned proofs;
wenzelm
parents: 51542
diff changeset
  1111
    done
29687
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1112
qed
4d934a895d11 A formalization of formal power series
chaieb
parents:
diff changeset
  1113
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1114
lemma fps_inverse_mult: "inverse (f * g :: 'a::field fps) = inverse f * inverse g"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1115
proof (cases "f$0 = 0 \<or> g$0 = 0")
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1116
  assume "\<not>(f$0 = 0 \<or> g$0 = 0)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1117
  hence [simp]: "f$0 \<noteq> 0" "g$0 \<noteq> 0" by simp_all
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1118
  show ?thesis
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1119
  proof (rule fps_inverse_unique)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1120
    have "f * g * (inverse f * inverse g) = (inverse f * f) * (inverse g * g)" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1121
    also have "... = 1" by (subst (1 2) inverse_mult_eq_1) simp_all
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1122
    finally show "f * g * (inverse f * inverse g) = 1" .
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1123
  qed
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1124
next
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1125
  assume A: "f$0 = 0 \<or> g$0 = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1126
  hence "inverse (f * g) = 0" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1127
  also from A have "... = inverse f * inverse g" by auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1128
  finally show "inverse (f * g) = inverse f * inverse g" .
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1129
qed
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
  1130
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1131
60501
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
  1132
lemma fps_inverse_gp: "inverse (Abs_fps(\<lambda>n. (1::'a::field))) =
839169c70e92 tuned proofs;
wenzelm
parents: 60500
diff changeset
  1133
    Abs_fps (\<lambda>n. if n= 0 then 1 else if n=1 then - 1 else 0)"
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
  1134
  apply (rule fps_inverse_unique)
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64242
diff changeset
  1135
  apply (simp_all add: fps_eq_iff fps_mult_nth sum_zero_lemma)
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
  1136
  done
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
  1137
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1138
lemma subdegree_inverse [simp]: "subdegree (inverse (f::'a::field fps)) = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1139
proof (cases "f$0 = 0")
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1140
  assume nz: "f$0 \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1141
  hence "subdegree (inverse f) + subdegree f = subdegree (inverse f * f)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1142
    by (subst subdegree_mult) auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1143
  also from nz have "subdegree f = 0" by (simp add: subdegree_eq_0_iff)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1144
  also from nz have "inverse f * f = 1" by (rule inverse_mult_eq_1)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1145
  finally show "subdegree (inverse f) = 0" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1146
qed (simp_all add: fps_inverse_def)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1147
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1148
lemma fps_is_unit_iff [simp]: "(f :: 'a :: field fps) dvd 1 \<longleftrightarrow> f $ 0 \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1149
proof
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1150
  assume "f dvd 1"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1151
  then obtain g where "1 = f * g" by (elim dvdE)
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1152
  from this[symmetric] have "(f*g) $ 0 = 1" by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1153
  thus "f $ 0 \<noteq> 0" by auto
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1154
next
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1155
  assume A: "f $ 0 \<noteq> 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1156
  thus "f dvd 1" by (simp add: inverse_mult_eq_1[OF A, symmetric])
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1157
qed
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1158
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1159
lemma subdegree_eq_0' [simp]: "(f :: 'a :: field fps) dvd 1 \<Longrightarrow> subdegree f = 0"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1160
  by simp
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1161
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1162
lemma fps_unit_dvd [simp]: "(f $ 0 :: 'a :: field) \<noteq> 0 \<Longrightarrow> f dvd g"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1163
  by (rule dvd_trans, subst fps_is_unit_iff) simp_all
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1164
64592
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1165
instantiation fps :: (field) normalization_semidom
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1166
begin
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1167
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1168
definition fps_unit_factor_def [simp]:
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1169
  "unit_factor f = fps_shift (subdegree f) f"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1170
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1171
definition fps_normalize_def [simp]:
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1172
  "normalize f = (if f = 0 then 0 else X ^ subdegree f)"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1173
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1174
instance proof
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1175
  fix f :: "'a fps"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1176
  show "unit_factor f * normalize f = f"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1177
    by (simp add: fps_shift_times_X_power)
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1178
next
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1179
  fix f g :: "'a fps"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1180
  show "unit_factor (f * g) = unit_factor f * unit_factor g"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1181
  proof (cases "f = 0 \<or> g = 0")
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1182
    assume "\<not>(f = 0 \<or> g = 0)"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1183
    thus "unit_factor (f * g) = unit_factor f * unit_factor g"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1184
    unfolding fps_unit_factor_def
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1185
      by (auto simp: fps_shift_fps_shift fps_shift_mult fps_shift_mult_right)
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1186
  qed auto
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1187
next
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1188
  fix f g :: "'a fps"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1189
  assume "g \<noteq> 0"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1190
  then have "f * (fps_shift (subdegree g) g * inverse (fps_shift (subdegree g) g)) = f"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1191
    by (metis add_cancel_right_left fps_shift_nth inverse_mult_eq_1 mult.commute mult_cancel_left2 nth_subdegree_nonzero)
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1192
  then have "fps_shift (subdegree g) (g * (f * inverse (fps_shift (subdegree g) g))) = f"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1193
    by (simp add: fps_shift_mult_right mult.commute)
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1194
  with \<open>g \<noteq> 0\<close> show "f * g / g = f"
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1195
    by (simp add: fps_divide_def Let_def ac_simps)
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1196
qed (auto simp add: fps_divide_def Let_def)
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1197
7759f1766189 more fine-grained type class hierarchy for div and mod
haftmann
parents: 64272
diff changeset
  1198
end
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1199
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1200
instantiation fps :: (field) ring_div
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1201
begin
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1202
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1203
definition fps_mod_def:
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1204
  "f mod g = (if g = 0 then f else
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
  1205
     let n = subdegree g; h = fps_shift n g
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1206
     in  fps_cutoff n (f * inverse h) * h)"
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1207
62102
877463945ce9 fix code generation for uniformity: uniformity is a non-computable pure data.
hoelzl
parents: 62101
diff changeset
  1208
lemma fps_mod_eq_zero:
61608
a0487caabb4a subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents: 61585
diff changeset
  1209
  assumes "g \<noteq> 0" and "subdegree f \<ge> subdegree g"