src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
author wenzelm
Mon, 10 Mar 2014 23:03:15 +0100
changeset 56043 0b25c3d34b77
parent 56009 dda076a32aea
child 56066 cce36efe32eb
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
     1
(*  Title:      HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
     2
    Author:     Amine Chaieb
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
     3
*)
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
     4
35046
1266f04f42ec tuned header
haftmann
parents: 34915
diff changeset
     5
header {* Implementation and verification of multivariate polynomials *}
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
     6
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
     7
theory Reflected_Multivariate_Polynomial
54220
0e6645622f22 more convenient place for a theory in solitariness
haftmann
parents: 53374
diff changeset
     8
imports Complex_Main Rat_Pair Polynomial_List
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
     9
begin
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    10
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
    11
subsection{* Datatype of polynomial expressions *}
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    12
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
    13
datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    14
  | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    15
35054
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 35046
diff changeset
    16
abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)"
50282
fe4d4bb9f4c2 more robust syntax that survives collapse of \<^isub> and \<^sub>;
wenzelm
parents: 49962
diff changeset
    17
abbreviation poly_p :: "int \<Rightarrow> poly" ("'((_)')\<^sub>p") where "(i)\<^sub>p \<equiv> C (i)\<^sub>N"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    18
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
    19
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    20
subsection{* Boundedness, substitution and all that *}
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
    21
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
    22
primrec polysize:: "poly \<Rightarrow> nat"
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
    23
where
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    24
  "polysize (C c) = 1"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
    25
| "polysize (Bound n) = 1"
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
    26
| "polysize (Neg p) = 1 + polysize p"
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
    27
| "polysize (Add p q) = 1 + polysize p + polysize q"
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
    28
| "polysize (Sub p q) = 1 + polysize p + polysize q"
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
    29
| "polysize (Mul p q) = 1 + polysize p + polysize q"
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
    30
| "polysize (Pw p n) = 1 + polysize p"
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
    31
| "polysize (CN c n p) = 4 + polysize c + polysize p"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    32
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
    33
primrec polybound0:: "poly \<Rightarrow> bool" -- {* a poly is INDEPENDENT of Bound 0 *}
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
    34
where
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    35
  "polybound0 (C c) \<longleftrightarrow> True"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    36
| "polybound0 (Bound n) \<longleftrightarrow> n > 0"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    37
| "polybound0 (Neg a) \<longleftrightarrow> polybound0 a"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    38
| "polybound0 (Add a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    39
| "polybound0 (Sub a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    40
| "polybound0 (Mul a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    41
| "polybound0 (Pw p n) \<longleftrightarrow> polybound0 p"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    42
| "polybound0 (CN c n p) \<longleftrightarrow> n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
    43
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
    44
primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" -- {* substitute a poly into a poly for Bound 0 *}
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
    45
where
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    46
  "polysubst0 t (C c) = C c"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    47
| "polysubst0 t (Bound n) = (if n = 0 then t else Bound n)"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
    48
| "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
    49
| "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
    50
| "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
    51
| "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
    52
| "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    53
| "polysubst0 t (CN c n p) =
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    54
    (if n = 0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    55
     else CN (polysubst0 t c) n (polysubst0 t p))"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    56
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
    57
fun decrpoly:: "poly \<Rightarrow> poly"
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    58
where
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    59
  "decrpoly (Bound n) = Bound (n - 1)"
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    60
| "decrpoly (Neg a) = Neg (decrpoly a)"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    61
| "decrpoly (Add a b) = Add (decrpoly a) (decrpoly b)"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    62
| "decrpoly (Sub a b) = Sub (decrpoly a) (decrpoly b)"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    63
| "decrpoly (Mul a b) = Mul (decrpoly a) (decrpoly b)"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    64
| "decrpoly (Pw p n) = Pw (decrpoly p) n"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    65
| "decrpoly (CN c n p) = CN (decrpoly c) (n - 1) (decrpoly p)"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    66
| "decrpoly a = a"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    67
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
    68
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    69
subsection{* Degrees and heads and coefficients *}
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    70
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    71
fun degree:: "poly \<Rightarrow> nat"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    72
where
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    73
  "degree (CN c 0 p) = 1 + degree p"
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    74
| "degree p = 0"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    75
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    76
fun head:: "poly \<Rightarrow> poly"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    77
where
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    78
  "head (CN c 0 p) = head p"
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    79
| "head p = p"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    80
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    81
(* More general notions of degree and head *)
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    82
fun degreen:: "poly \<Rightarrow> nat \<Rightarrow> nat"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    83
where
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    84
  "degreen (CN c n p) = (\<lambda>m. if n = m then 1 + degreen p n else 0)"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    85
| "degreen p = (\<lambda>m. 0)"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    86
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    87
fun headn:: "poly \<Rightarrow> nat \<Rightarrow> poly"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    88
where
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    89
  "headn (CN c n p) = (\<lambda>m. if n \<le> m then headn p m else CN c n p)"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    90
| "headn p = (\<lambda>m. p)"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    91
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    92
fun coefficients:: "poly \<Rightarrow> poly list"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    93
where
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
    94
  "coefficients (CN c 0 p) = c # coefficients p"
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    95
| "coefficients p = [p]"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
    96
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    97
fun isconstant:: "poly \<Rightarrow> bool"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    98
where
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
    99
  "isconstant (CN c 0 p) = False"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   100
| "isconstant p = True"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   101
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   102
fun behead:: "poly \<Rightarrow> poly"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   103
where
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   104
  "behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   105
| "behead p = 0\<^sub>p"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   106
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   107
fun headconst:: "poly \<Rightarrow> Num"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   108
where
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   109
  "headconst (CN c n p) = headconst p"
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   110
| "headconst (C n) = n"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   111
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   112
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   113
subsection{* Operations for normalization *}
41812
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   114
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   115
declare if_cong[fundef_cong del]
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   116
declare let_cong[fundef_cong del]
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   117
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   118
fun polyadd :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   119
where
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   120
  "polyadd (C c) (C c') = C (c +\<^sub>N c')"
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   121
| "polyadd (C c) (CN c' n' p') = CN (polyadd (C c) c') n' p'"
41812
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   122
| "polyadd (CN c n p) (C c') = CN (polyadd c (C c')) n p"
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   123
| "polyadd (CN c n p) (CN c' n' p') =
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   124
    (if n < n' then CN (polyadd c (CN c' n' p')) n p
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   125
     else if n' < n then CN (polyadd (CN c n p) c') n' p'
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   126
     else
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   127
      let
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   128
        cc' = polyadd c c';
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   129
        pp' = polyadd p p'
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   130
      in if pp' = 0\<^sub>p then cc' else CN cc' n pp')"
41812
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   131
| "polyadd a b = Add a b"
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   132
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   133
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   134
fun polyneg :: "poly \<Rightarrow> poly" ("~\<^sub>p")
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   135
where
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   136
  "polyneg (C c) = C (~\<^sub>N c)"
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   137
| "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   138
| "polyneg a = Neg a"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   139
41814
3848eb635eab modernized specification; curried
krauss
parents: 41813
diff changeset
   140
definition polysub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   141
  where "p -\<^sub>p q = polyadd p (polyneg q)"
41813
4eb43410d2fa recdef -> fun; curried
krauss
parents: 41812
diff changeset
   142
4eb43410d2fa recdef -> fun; curried
krauss
parents: 41812
diff changeset
   143
fun polymul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
4eb43410d2fa recdef -> fun; curried
krauss
parents: 41812
diff changeset
   144
where
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   145
  "polymul (C c) (C c') = C (c *\<^sub>N c')"
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   146
| "polymul (C c) (CN c' n' p') =
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   147
    (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul (C c) c') n' (polymul (C c) p'))"
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   148
| "polymul (CN c n p) (C c') =
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   149
    (if c' = 0\<^sub>N  then 0\<^sub>p else CN (polymul c (C c')) n (polymul p (C c')))"
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   150
| "polymul (CN c n p) (CN c' n' p') =
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   151
    (if n < n' then CN (polymul c (CN c' n' p')) n (polymul p (CN c' n' p'))
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   152
     else if n' < n then CN (polymul (CN c n p) c') n' (polymul (CN c n p) p')
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   153
     else polyadd (polymul (CN c n p) c') (CN 0\<^sub>p n' (polymul (CN c n p) p')))"
41813
4eb43410d2fa recdef -> fun; curried
krauss
parents: 41812
diff changeset
   154
| "polymul a b = Mul a b"
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   155
41812
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   156
declare if_cong[fundef_cong]
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   157
declare let_cong[fundef_cong]
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   158
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   159
fun polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   160
where
50282
fe4d4bb9f4c2 more robust syntax that survives collapse of \<^isub> and \<^sub>;
wenzelm
parents: 49962
diff changeset
   161
  "polypow 0 = (\<lambda>p. (1)\<^sub>p)"
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   162
| "polypow n =
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   163
    (\<lambda>p.
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   164
      let
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   165
        q = polypow (n div 2) p;
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   166
        d = polymul q q
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   167
      in if even n then d else polymul p d)"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   168
35054
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 35046
diff changeset
   169
abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 35046
diff changeset
   170
  where "a ^\<^sub>p k \<equiv> polypow k a"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   171
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   172
function polynate :: "poly \<Rightarrow> poly"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   173
where
50282
fe4d4bb9f4c2 more robust syntax that survives collapse of \<^isub> and \<^sub>;
wenzelm
parents: 49962
diff changeset
   174
  "polynate (Bound n) = CN 0\<^sub>p n (1)\<^sub>p"
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   175
| "polynate (Add p q) = polynate p +\<^sub>p polynate q"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   176
| "polynate (Sub p q) = polynate p -\<^sub>p polynate q"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   177
| "polynate (Mul p q) = polynate p *\<^sub>p polynate q"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   178
| "polynate (Neg p) = ~\<^sub>p (polynate p)"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   179
| "polynate (Pw p n) = polynate p ^\<^sub>p n"
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   180
| "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   181
| "polynate (C c) = C (normNum c)"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   182
by pat_completeness auto
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   183
termination by (relation "measure polysize") auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   184
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   185
fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly"
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   186
where
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   187
  "poly_cmul y (C x) = C (y *\<^sub>N x)"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   188
| "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   189
| "poly_cmul y p = C y *\<^sub>p p"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   190
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   191
definition monic :: "poly \<Rightarrow> poly \<times> bool"
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   192
where
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   193
  "monic p =
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   194
    (let h = headconst p
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   195
     in if h = 0\<^sub>N then (p, False) else (C (Ninv h) *\<^sub>p p, 0>\<^sub>N h))"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   196
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   197
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   198
subsection {* Pseudo-division *}
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   199
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   200
definition shift1 :: "poly \<Rightarrow> poly"
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   201
  where "shift1 p = CN 0\<^sub>p 0 p"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   202
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   203
abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   204
  where "funpow \<equiv> compow"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
   205
41403
7eba049f7310 partial_function (tailrec) replaces function (tailrec);
krauss
parents: 39246
diff changeset
   206
partial_function (tailrec) polydivide_aux :: "poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<times> poly"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   207
where
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   208
  "polydivide_aux a n p k s =
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   209
    (if s = 0\<^sub>p then (k, s)
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   210
     else
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   211
      let
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   212
        b = head s;
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   213
        m = degree s
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   214
      in
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   215
        if m < n then (k,s)
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   216
        else
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   217
          let p' = funpow (m - n) shift1 p
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   218
          in
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   219
            if a = b then polydivide_aux a n p k (s -\<^sub>p p')
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   220
            else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   221
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   222
definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> nat \<times> poly"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   223
  where "polydivide s p = polydivide_aux (head p) (degree p) p 0 s"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   224
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   225
fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly"
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   226
where
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   227
  "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   228
| "poly_deriv_aux n p = poly_cmul ((int n)\<^sub>N) p"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   229
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   230
fun poly_deriv :: "poly \<Rightarrow> poly"
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   231
where
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   232
  "poly_deriv (CN c 0 p) = poly_deriv_aux 1 p"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   233
| "poly_deriv p = 0\<^sub>p"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   234
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   235
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   236
subsection{* Semantics of the polynomial representation *}
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   237
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   238
primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field_inverse_zero,power}"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   239
where
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   240
  "Ipoly bs (C c) = INum c"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
   241
| "Ipoly bs (Bound n) = bs!n"
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
   242
| "Ipoly bs (Neg a) = - Ipoly bs a"
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
   243
| "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
   244
| "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
   245
| "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   246
| "Ipoly bs (Pw t n) = Ipoly bs t ^ n"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   247
| "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
   248
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   249
abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field_inverse_zero,power}"
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   250
    ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
35054
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 35046
diff changeset
   251
  where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   252
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   253
lemma Ipoly_CInt: "Ipoly bs (C (i, 1)) = of_int i"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   254
  by (simp add: INum_def)
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   255
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   256
lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   257
  by (simp  add: INum_def)
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   258
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   259
lemmas RIpoly_eqs = Ipoly.simps(2-7) Ipoly_CInt Ipoly_CRat
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   260
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   261
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   262
subsection {* Normal form and normalization *}
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   263
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   264
fun isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool"
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   265
where
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   266
  "isnpolyh (C c) = (\<lambda>k. isnormNum c)"
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   267
| "isnpolyh (CN c n p) = (\<lambda>k. n \<ge> k \<and> isnpolyh c (Suc n) \<and> isnpolyh p n \<and> p \<noteq> 0\<^sub>p)"
41808
9f436d00248f recdef -> function
krauss
parents: 41763
diff changeset
   268
| "isnpolyh p = (\<lambda>k. False)"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   269
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   270
lemma isnpolyh_mono: "n' \<le> n \<Longrightarrow> isnpolyh p n \<Longrightarrow> isnpolyh p n'"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   271
  by (induct p rule: isnpolyh.induct) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   272
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   273
definition isnpoly :: "poly \<Rightarrow> bool"
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   274
  where "isnpoly p = isnpolyh p 0"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   275
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   276
text{* polyadd preserves normal forms *}
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   277
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   278
lemma polyadd_normh: "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (polyadd p q) (min n0 n1)"
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   279
proof (induct p q arbitrary: n0 n1 rule: polyadd.induct)
41812
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   280
  case (2 ab c' n' p' n0 n1)
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   281
  from 2 have  th1: "isnpolyh (C ab) (Suc n')"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   282
    by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   283
  from 2(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   284
    by simp_all
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   285
  with isnpolyh_mono have cp: "isnpolyh c' (Suc n')"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   286
    by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   287
  with 2(1)[OF th1 th2] have th3:"isnpolyh (C ab +\<^sub>p c') (Suc n')"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   288
    by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   289
  from nplen1 have n01len1: "min n0 n1 \<le> n'"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   290
    by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   291
  then show ?case using 2 th3
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   292
    by simp
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   293
next
41812
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   294
  case (3 c' n' p' ab n1 n0)
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   295
  from 3 have  th1: "isnpolyh (C ab) (Suc n')"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   296
    by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   297
  from 3(2) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   298
    by simp_all
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   299
  with isnpolyh_mono have cp: "isnpolyh c' (Suc n')"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   300
    by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   301
  with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C ab) (Suc n')"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   302
    by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   303
  from nplen1 have n01len1: "min n0 n1 \<le> n'"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   304
    by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   305
  then show ?case using 3 th3
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   306
    by simp
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   307
next
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   308
  case (4 c n p c' n' p' n0 n1)
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   309
  then have nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   310
    by simp_all
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   311
  from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   312
    by simp_all
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   313
  from 4 have ngen0: "n \<ge> n0"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   314
    by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   315
  from 4 have n'gen1: "n' \<ge> n1"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   316
    by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   317
  have "n < n' \<or> n' < n \<or> n = n'"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   318
    by auto
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   319
  moreover
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   320
  {
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   321
    assume eq: "n = n'"
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   322
    with "4.hyps"(3)[OF nc nc']
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   323
    have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   324
      by auto
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   325
    then have ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   326
      using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   327
      by auto
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   328
    from eq "4.hyps"(4)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   329
      by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   330
    have minle: "min n0 n1 \<le> n'"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   331
      using ngen0 n'gen1 eq by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   332
    from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' have ?case
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   333
      by (simp add: Let_def)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   334
  }
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   335
  moreover
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   336
  {
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   337
    assume lt: "n < n'"
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   338
    have "min n0 n1 \<le> n0"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   339
      by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   340
    with 4 lt have th1:"min n0 n1 \<le> n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   341
      by auto
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   342
    from 4 have th21: "isnpolyh c (Suc n)"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   343
      by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   344
    from 4 have th22: "isnpolyh (CN c' n' p') n'"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   345
      by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   346
    from lt have th23: "min (Suc n) n' = Suc n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   347
      by arith
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   348
    from "4.hyps"(1)[OF th21 th22] have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   349
      using th23 by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   350
    with 4 lt th1 have ?case
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   351
      by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   352
  }
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   353
  moreover
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   354
  {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   355
    assume gt: "n' < n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   356
    then have gt': "n' < n \<and> \<not> n < n'"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   357
      by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   358
    have "min n0 n1 \<le> n1"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   359
      by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   360
    with 4 gt have th1: "min n0 n1 \<le> n'"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   361
      by auto
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   362
    from 4 have th21: "isnpolyh c' (Suc n')"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   363
      by simp_all
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   364
    from 4 have th22: "isnpolyh (CN c n p) n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   365
      by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   366
    from gt have th23: "min n (Suc n') = Suc n'"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   367
      by arith
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   368
    from "4.hyps"(2)[OF th22 th21] have "isnpolyh (polyadd (CN c n p) c') (Suc n')"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   369
      using th23 by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   370
    with 4 gt th1 have ?case
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   371
      by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   372
  }
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   373
  ultimately show ?case by blast
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   374
qed auto
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   375
41812
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   376
lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   377
  by (induct p q rule: polyadd.induct)
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   378
    (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   379
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   380
lemma polyadd_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polyadd p q)"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   381
  using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   382
41404
aae9f912cca8 dropped duplicate unused lemmas;
krauss
parents: 41403
diff changeset
   383
text{* The degree of addition and other general lemmas needed for the normal form of polymul *}
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   384
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   385
lemma polyadd_different_degreen:
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   386
  assumes "isnpolyh p n0"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   387
    and "isnpolyh q n1"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   388
    and "degreen p m \<noteq> degreen q m"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   389
    and "m \<le> min n0 n1"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   390
  shows "degreen (polyadd p q) m = max (degreen p m) (degreen q m)"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   391
  using assms
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   392
proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct)
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   393
  case (4 c n p c' n' p' m n0 n1)
41763
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   394
  have "n' = n \<or> n < n' \<or> n' < n" by arith
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   395
  then show ?case
41763
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   396
  proof (elim disjE)
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   397
    assume [simp]: "n' = n"
41812
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   398
    from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
41763
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   399
    show ?thesis by (auto simp: Let_def)
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   400
  next
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   401
    assume "n < n'"
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   402
    with 4 show ?thesis by auto
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   403
  next
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   404
    assume "n' < n"
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   405
    with 4 show ?thesis by auto
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   406
  qed
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   407
qed auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   408
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   409
lemma headnz[simp]: "isnpolyh p n \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> headn p m \<noteq> 0\<^sub>p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   410
  by (induct p arbitrary: n rule: headn.induct) auto
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   411
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   412
lemma degree_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> degree p = 0"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   413
  by (induct p arbitrary: n rule: degree.induct) auto
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   414
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   415
lemma degreen_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> degreen p m = 0"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   416
  by (induct p arbitrary: n rule: degreen.induct) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   417
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   418
lemma degree_isnpolyh_Suc': "n > 0 \<Longrightarrow> isnpolyh p n \<Longrightarrow> degree p = 0"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   419
  by (induct p arbitrary: n rule: degree.induct) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   420
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   421
lemma degree_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degree c = 0"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   422
  using degree_isnpolyh_Suc by auto
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   423
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   424
lemma degreen_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degreen c n = 0"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   425
  using degreen_0 by auto
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   426
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   427
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   428
lemma degreen_polyadd:
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   429
  assumes np: "isnpolyh p n0"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   430
    and nq: "isnpolyh q n1"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   431
    and m: "m \<le> max n0 n1"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   432
  shows "degreen (p +\<^sub>p q) m \<le> max (degreen p m) (degreen q m)"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   433
  using np nq m
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   434
proof (induct p q arbitrary: n0 n1 m rule: polyadd.induct)
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   435
  case (2 c c' n' p' n0 n1)
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   436
  then show ?case
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   437
    by (cases n') simp_all
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   438
next
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   439
  case (3 c n p c' n0 n1)
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   440
  then show ?case
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   441
    by (cases n) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   442
next
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   443
  case (4 c n p c' n' p' n0 n1 m)
41763
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   444
  have "n' = n \<or> n < n' \<or> n' < n" by arith
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   445
  then show ?case
41763
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   446
  proof (elim disjE)
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   447
    assume [simp]: "n' = n"
41812
d46c2908a838 recdef -> fun; curried
krauss
parents: 41811
diff changeset
   448
    from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
41763
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   449
    show ?thesis by (auto simp: Let_def)
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   450
  qed simp_all
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   451
qed auto
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   452
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   453
lemma polyadd_eq_const_degreen:
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   454
  assumes "isnpolyh p n0"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   455
    and "isnpolyh q n1"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   456
    and "polyadd p q = C c"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   457
  shows "degreen p m = degreen q m"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   458
  using assms
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   459
proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   460
  case (4 c n p c' n' p' m n0 n1 x)
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   461
  {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   462
    assume nn': "n' < n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   463
    then have ?case using 4 by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   464
  }
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   465
  moreover
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   466
  {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   467
    assume nn': "\<not> n' < n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   468
    then have "n < n' \<or> n = n'" by arith
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   469
    moreover { assume "n < n'" with 4 have ?case by simp }
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   470
    moreover
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   471
    {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   472
      assume eq: "n = n'"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   473
      then have ?case using 4
41763
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   474
        apply (cases "p +\<^sub>p p' = 0\<^sub>p")
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   475
        apply (auto simp add: Let_def)
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   476
        apply blast
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   477
        done
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   478
    }
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   479
    ultimately have ?case by blast
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   480
  }
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   481
  ultimately show ?case by blast
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   482
qed simp_all
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   483
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   484
lemma polymul_properties:
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   485
  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   486
    and np: "isnpolyh p n0"
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   487
    and nq: "isnpolyh q n1"
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   488
    and m: "m \<le> min n0 n1"
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   489
  shows "isnpolyh (p *\<^sub>p q) (min n0 n1)"
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   490
    and "p *\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p \<or> q = 0\<^sub>p"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   491
    and "degreen (p *\<^sub>p q) m = (if p = 0\<^sub>p \<or> q = 0\<^sub>p then 0 else degreen p m + degreen q m)"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   492
  using np nq m
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   493
proof (induct p q arbitrary: n0 n1 m rule: polymul.induct)
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   494
  case (2 c c' n' p')
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   495
  {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   496
    case (1 n0 n1)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   497
    with "2.hyps"(4-6)[of n' n' n'] and "2.hyps"(1-3)[of "Suc n'" "Suc n'" n']
41811
7e338ccabff0 strengthened polymul.induct
krauss
parents: 41810
diff changeset
   498
    show ?case by (auto simp add: min_def)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   499
  next
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   500
    case (2 n0 n1)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   501
    then show ?case by auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   502
  next
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   503
    case (3 n0 n1)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   504
    then show ?case  using "2.hyps" by auto
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   505
  }
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   506
next
41813
4eb43410d2fa recdef -> fun; curried
krauss
parents: 41812
diff changeset
   507
  case (3 c n p c')
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   508
  {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   509
    case (1 n0 n1)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   510
    with "3.hyps"(4-6)[of n n n] and "3.hyps"(1-3)[of "Suc n" "Suc n" n]
41811
7e338ccabff0 strengthened polymul.induct
krauss
parents: 41810
diff changeset
   511
    show ?case by (auto simp add: min_def)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   512
  next
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   513
    case (2 n0 n1)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   514
    then show ?case by auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   515
  next
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   516
    case (3 n0 n1)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   517
    then show ?case  using "3.hyps" by auto
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   518
  }
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   519
next
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   520
  case (4 c n p c' n' p')
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   521
  let ?cnp = "CN c n p" let ?cnp' = "CN c' n' p'"
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   522
  {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   523
    case (1 n0 n1)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   524
    then have cnp: "isnpolyh ?cnp n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   525
      and cnp': "isnpolyh ?cnp' n'"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   526
      and np: "isnpolyh p n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   527
      and nc: "isnpolyh c (Suc n)"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   528
      and np': "isnpolyh p' n'"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   529
      and nc': "isnpolyh c' (Suc n')"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   530
      and nn0: "n \<ge> n0"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   531
      and nn1: "n' \<ge> n1"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   532
      by simp_all
41811
7e338ccabff0 strengthened polymul.induct
krauss
parents: 41810
diff changeset
   533
    {
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   534
      assume "n < n'"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   535
      with "4.hyps"(4-5)[OF np cnp', of n] and "4.hyps"(1)[OF nc cnp', of n] nn0 cnp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   536
      have ?case by (simp add: min_def)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   537
    } moreover {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   538
      assume "n' < n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   539
      with "4.hyps"(16-17)[OF cnp np', of "n'"] and "4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp'
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   540
      have ?case by (cases "Suc n' = n") (simp_all add: min_def)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   541
    } moreover {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   542
      assume "n' = n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   543
      with "4.hyps"(16-17)[OF cnp np', of n] and "4.hyps"(13)[OF cnp nc', of n] cnp cnp' nn1 nn0
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   544
      have ?case
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   545
        apply (auto intro!: polyadd_normh)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   546
        apply (simp_all add: min_def isnpolyh_mono[OF nn0])
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   547
        done
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   548
    }
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   549
    ultimately show ?case by arith
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   550
  next
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   551
    fix n0 n1 m
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   552
    assume np: "isnpolyh ?cnp n0"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   553
    assume np':"isnpolyh ?cnp' n1"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   554
    assume m: "m \<le> min n0 n1"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   555
    let ?d = "degreen (?cnp *\<^sub>p ?cnp') m"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   556
    let ?d1 = "degreen ?cnp m"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   557
    let ?d2 = "degreen ?cnp' m"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   558
    let ?eq = "?d = (if ?cnp = 0\<^sub>p \<or> ?cnp' = 0\<^sub>p then 0  else ?d1 + ?d2)"
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   559
    have "n' < n \<or> n < n' \<or> n' = n" by auto
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   560
    moreover
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   561
    {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   562
      assume "n' < n \<or> n < n'"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   563
      with "4.hyps"(3,6,18) np np' m have ?eq
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   564
        by auto
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   565
    }
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   566
    moreover
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   567
    {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   568
      assume nn': "n' = n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   569
      then have nn: "\<not> n' < n \<and> \<not> n < n'" by arith
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   570
      from "4.hyps"(16,18)[of n n' n]
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   571
        "4.hyps"(13,14)[of n "Suc n'" n]
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   572
        np np' nn'
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   573
      have norm:
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   574
        "isnpolyh ?cnp n"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   575
        "isnpolyh c' (Suc n)"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   576
        "isnpolyh (?cnp *\<^sub>p c') n"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   577
        "isnpolyh p' n"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   578
        "isnpolyh (?cnp *\<^sub>p p') n"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   579
        "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   580
        "?cnp *\<^sub>p c' = 0\<^sub>p \<longleftrightarrow> c' = 0\<^sub>p"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   581
        "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   582
        by (auto simp add: min_def)
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   583
      {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   584
        assume mn: "m = n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   585
        from "4.hyps"(17,18)[OF norm(1,4), of n]
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   586
          "4.hyps"(13,15)[OF norm(1,2), of n] norm nn' mn
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   587
        have degs:
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   588
          "degreen (?cnp *\<^sub>p c') n = (if c' = 0\<^sub>p then 0 else ?d1 + degreen c' n)"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   589
          "degreen (?cnp *\<^sub>p p') n = ?d1  + degreen p' n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   590
          by (simp_all add: min_def)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   591
        from degs norm have th1: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   592
          by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   593
        then have neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   594
          by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   595
        have nmin: "n \<le> min n n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   596
          by (simp add: min_def)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   597
        from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   598
        have deg: "degreen (CN c n p *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n =
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   599
            degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   600
          by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   601
        from "4.hyps"(16-18)[OF norm(1,4), of n]
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   602
          "4.hyps"(13-15)[OF norm(1,2), of n]
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   603
          mn norm m nn' deg
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   604
        have ?eq by simp
41811
7e338ccabff0 strengthened polymul.induct
krauss
parents: 41810
diff changeset
   605
      }
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   606
      moreover
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   607
      {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   608
        assume mn: "m \<noteq> n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   609
        then have mn': "m < n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   610
          using m np by auto
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   611
        from nn' m np have max1: "m \<le> max n n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   612
          by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   613
        then have min1: "m \<le> min n n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   614
          by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   615
        then have min2: "m \<le> min n (Suc n)"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   616
          by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   617
        from "4.hyps"(16-18)[OF norm(1,4) min1]
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   618
          "4.hyps"(13-15)[OF norm(1,2) min2]
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   619
          degreen_polyadd[OF norm(3,6) max1]
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   620
        have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m \<le>
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   621
            max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   622
          using mn nn' np np' by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   623
        with "4.hyps"(16-18)[OF norm(1,4) min1]
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   624
          "4.hyps"(13-15)[OF norm(1,2) min2]
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   625
          degreen_0[OF norm(3) mn']
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   626
        have ?eq using nn' mn np np' by clarsimp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   627
      }
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   628
      ultimately have ?eq by blast
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   629
    }
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   630
    ultimately show ?eq by blast
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   631
  }
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   632
  {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   633
    case (2 n0 n1)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   634
    then have np: "isnpolyh ?cnp n0"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   635
      and np': "isnpolyh ?cnp' n1"
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   636
      and m: "m \<le> min n0 n1"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   637
      by simp_all
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   638
    then have mn: "m \<le> n" by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   639
    let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   640
    {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   641
      assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   642
      then have nn: "\<not> n' < n \<and> \<not> n < n'"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   643
        by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   644
      from "4.hyps"(16-18) [of n n n]
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   645
        "4.hyps"(13-15)[of n "Suc n" n]
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   646
        np np' C(2) mn
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   647
      have norm:
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   648
        "isnpolyh ?cnp n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   649
        "isnpolyh c' (Suc n)"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   650
        "isnpolyh (?cnp *\<^sub>p c') n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   651
        "isnpolyh p' n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   652
        "isnpolyh (?cnp *\<^sub>p p') n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   653
        "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   654
        "?cnp *\<^sub>p c' = 0\<^sub>p \<longleftrightarrow> c' = 0\<^sub>p"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   655
        "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   656
        "degreen (?cnp *\<^sub>p c') n = (if c' = 0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   657
        "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   658
        by (simp_all add: min_def)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   659
      from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   660
        by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   661
      have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   662
        using norm by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   663
      from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"] degneq
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   664
      have False by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   665
    }
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   666
    then show ?case using "4.hyps" by clarsimp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   667
  }
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   668
qed auto
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   669
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   670
lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = Ipoly bs p * Ipoly bs q"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   671
  by (induct p q rule: polymul.induct) (auto simp add: field_simps)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   672
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   673
lemma polymul_normh:
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   674
  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   675
  shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   676
  using polymul_properties(1) by blast
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   677
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   678
lemma polymul_eq0_iff:
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   679
  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   680
  shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p *\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p \<or> q = 0\<^sub>p"
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   681
  using polymul_properties(2) by blast
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   682
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   683
lemma polymul_degreen:  (* FIXME duplicate? *)
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   684
  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   685
  shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> m \<le> min n0 n1 \<Longrightarrow>
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   686
    degreen (p *\<^sub>p q) m = (if p = 0\<^sub>p \<or> q = 0\<^sub>p then 0 else degreen p m + degreen q m)"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   687
  using polymul_properties(3) by blast
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   688
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   689
lemma polymul_norm:
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   690
  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   691
  shows "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polymul p q)"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   692
  using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   693
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   694
lemma headconst_zero: "isnpolyh p n0 \<Longrightarrow> headconst p = 0\<^sub>N \<longleftrightarrow> p = 0\<^sub>p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   695
  by (induct p arbitrary: n0 rule: headconst.induct) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   696
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   697
lemma headconst_isnormNum: "isnpolyh p n0 \<Longrightarrow> isnormNum (headconst p)"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   698
  by (induct p arbitrary: n0) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   699
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   700
lemma monic_eqI:
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   701
  assumes np: "isnpolyh p n0"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   702
  shows "INum (headconst p) * Ipoly bs (fst (monic p)) =
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   703
    (Ipoly bs p ::'a::{field_char_0,field_inverse_zero, power})"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   704
  unfolding monic_def Let_def
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   705
proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   706
  let ?h = "headconst p"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   707
  assume pz: "p \<noteq> 0\<^sub>p"
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   708
  {
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   709
    assume hz: "INum ?h = (0::'a)"
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   710
    from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   711
      by simp_all
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   712
    from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   713
      by simp
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   714
    with headconst_zero[OF np] have "p = 0\<^sub>p"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   715
      by blast
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   716
    with pz have False
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   717
      by blast
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   718
  }
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   719
  then show "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   720
    by blast
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   721
qed
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   722
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   723
41404
aae9f912cca8 dropped duplicate unused lemmas;
krauss
parents: 41403
diff changeset
   724
text{* polyneg is a negation and preserves normal forms *}
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   725
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   726
lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   727
  by (induct p rule: polyneg.induct) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   728
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   729
lemma polyneg0: "isnpolyh p n \<Longrightarrow> (~\<^sub>p p) = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   730
  by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: Nneg_def)
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   731
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   732
lemma polyneg_polyneg: "isnpolyh p n0 \<Longrightarrow> ~\<^sub>p (~\<^sub>p p) = p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   733
  by (induct p arbitrary: n0 rule: polyneg.induct) auto
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   734
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   735
lemma polyneg_normh: "isnpolyh p n \<Longrightarrow> isnpolyh (polyneg p) n"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   736
  by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: polyneg0)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   737
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   738
lemma polyneg_norm: "isnpoly p \<Longrightarrow> isnpoly (polyneg p)"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   739
  using isnpoly_def polyneg_normh by simp
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   740
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   741
41404
aae9f912cca8 dropped duplicate unused lemmas;
krauss
parents: 41403
diff changeset
   742
text{* polysub is a substraction and preserves normal forms *}
aae9f912cca8 dropped duplicate unused lemmas;
krauss
parents: 41403
diff changeset
   743
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   744
lemma polysub[simp]: "Ipoly bs (polysub p q) = Ipoly bs p - Ipoly bs q"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   745
  by (simp add: polysub_def)
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   746
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   747
lemma polysub_normh: "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (polysub p q) (min n0 n1)"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   748
  by (simp add: polysub_def polyneg_normh polyadd_normh)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   749
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   750
lemma polysub_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polysub p q)"
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   751
  using polyadd_norm polyneg_norm by (simp add: polysub_def)
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   752
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   753
lemma polysub_same_0[simp]:
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   754
  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
41814
3848eb635eab modernized specification; curried
krauss
parents: 41813
diff changeset
   755
  shows "isnpolyh p n0 \<Longrightarrow> polysub p p = 0\<^sub>p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   756
  unfolding polysub_def split_def fst_conv snd_conv
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   757
  by (induct p arbitrary: n0) (auto simp add: Let_def Nsub0[simplified Nsub_def])
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   758
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   759
lemma polysub_0:
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   760
  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   761
  shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p -\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = q"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   762
  unfolding polysub_def split_def fst_conv snd_conv
41763
8ce56536fda7 strengthened induction rule;
krauss
parents: 41413
diff changeset
   763
  by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   764
    (auto simp: Nsub0[simplified Nsub_def] Let_def)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   765
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   766
text{* polypow is a power function and preserves normal forms *}
41404
aae9f912cca8 dropped duplicate unused lemmas;
krauss
parents: 41403
diff changeset
   767
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   768
lemma polypow[simp]:
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   769
  "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field_inverse_zero}) ^ n"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   770
proof (induct n rule: polypow.induct)
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   771
  case 1
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   772
  then show ?case
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   773
    by simp
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   774
next
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   775
  case (2 n)
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   776
  let ?q = "polypow ((Suc n) div 2) p"
41813
4eb43410d2fa recdef -> fun; curried
krauss
parents: 41812
diff changeset
   777
  let ?d = "polymul ?q ?q"
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   778
  have "odd (Suc n) \<or> even (Suc n)"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   779
    by simp
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   780
  moreover
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   781
  {
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   782
    assume odd: "odd (Suc n)"
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   783
    have th: "(Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0)))) = Suc n div 2 + Suc n div 2 + 1"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   784
      by arith
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   785
    from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   786
      by (simp add: Let_def)
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   787
    also have "\<dots> = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2) * (Ipoly bs p)^(Suc n div 2)"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   788
      using "2.hyps" by simp
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   789
    also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   790
      by (simp only: power_add power_one_right) simp
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   791
    also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   792
      by (simp only: th)
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   793
    finally have ?case
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   794
    using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   795
  }
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   796
  moreover
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   797
  {
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   798
    assume even: "even (Suc n)"
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   799
    have th: "(Suc (Suc 0)) * (Suc n div Suc (Suc 0)) = Suc n div 2 + Suc n div 2"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   800
      by arith
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   801
    from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   802
      by (simp add: Let_def)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   803
    also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)"
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   804
      using "2.hyps" by (simp only: power_add) simp
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   805
    finally have ?case using even_nat_div_two_times_two[OF even]
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   806
      by (simp only: th)
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   807
  }
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   808
  ultimately show ?case by blast
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   809
qed
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   810
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   811
lemma polypow_normh:
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   812
  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   813
  shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   814
proof (induct k arbitrary: n rule: polypow.induct)
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   815
  case 1
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   816
  then show ?case by auto
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   817
next
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   818
  case (2 k n)
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   819
  let ?q = "polypow (Suc k div 2) p"
41813
4eb43410d2fa recdef -> fun; curried
krauss
parents: 41812
diff changeset
   820
  let ?d = "polymul ?q ?q"
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   821
  from 2 have th1: "isnpolyh ?q n" and th2: "isnpolyh p n"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   822
    by blast+
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   823
  from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   824
    by simp
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   825
  from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   826
    by simp
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   827
  from dn on show ?case
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   828
    by (simp add: Let_def)
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   829
qed
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   830
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   831
lemma polypow_norm:
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   832
  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   833
  shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   834
  by (simp add: polypow_normh isnpoly_def)
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   835
41404
aae9f912cca8 dropped duplicate unused lemmas;
krauss
parents: 41403
diff changeset
   836
text{* Finally the whole normalization *}
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   837
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   838
lemma polynate [simp]:
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   839
  "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field_inverse_zero})"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   840
  by (induct p rule:polynate.induct) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   841
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   842
lemma polynate_norm[simp]:
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   843
  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   844
  shows "isnpoly (polynate p)"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   845
  by (induct p rule: polynate.induct)
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   846
     (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   847
      simp_all add: isnpoly_def)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   848
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   849
text{* shift1 *}
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   850
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   851
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   852
lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   853
  by (simp add: shift1_def)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   854
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   855
lemma shift1_isnpoly:
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   856
  assumes pn: "isnpoly p"
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   857
    and pnz: "p \<noteq> 0\<^sub>p"
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   858
  shows "isnpoly (shift1 p) "
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   859
  using pn pnz by (simp add: shift1_def isnpoly_def)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   860
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   861
lemma shift1_nz[simp]:"shift1 p \<noteq> 0\<^sub>p"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   862
  by (simp add: shift1_def)
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   863
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   864
lemma funpow_shift1_isnpoly: "isnpoly p \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> isnpoly (funpow n shift1 p)"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 36409
diff changeset
   865
  by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   866
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   867
lemma funpow_isnpolyh:
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   868
  assumes f: "\<And>p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   869
    and np: "isnpolyh p n"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   870
  shows "isnpolyh (funpow k f p) n"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   871
  using f np by (induct k arbitrary: p) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   872
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   873
lemma funpow_shift1:
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   874
  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) =
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   875
    Ipoly bs (Mul (Pw (Bound 0) n) p)"
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   876
  by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   877
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   878
lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   879
  using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   880
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   881
lemma funpow_shift1_1:
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   882
  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) =
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   883
    Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   884
  by (simp add: funpow_shift1)
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   885
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   886
lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
45129
1fce03e3e8ad tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
wenzelm
parents: 41842
diff changeset
   887
  by (induct p rule: poly_cmul.induct) (auto simp add: field_simps)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   888
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   889
lemma behead:
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   890
  assumes np: "isnpolyh p n"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   891
  shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) =
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   892
    (Ipoly bs p :: 'a :: {field_char_0,field_inverse_zero})"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   893
  using np
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   894
proof (induct p arbitrary: n rule: behead.induct)
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   895
  case (1 c p n)
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   896
  then have pn: "isnpolyh p n" by simp
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   897
  from 1(1)[OF pn]
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   898
  have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" .
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   899
  then show ?case using "1.hyps"
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   900
    apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   901
    apply (simp_all add: th[symmetric] field_simps)
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   902
    done
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   903
qed (auto simp add: Let_def)
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   904
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   905
lemma behead_isnpolyh:
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   906
  assumes np: "isnpolyh p n"
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   907
  shows "isnpolyh (behead p) n"
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   908
  using np by (induct p rule: behead.induct) (auto simp add: Let_def isnpolyh_mono)
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   909
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   910
41404
aae9f912cca8 dropped duplicate unused lemmas;
krauss
parents: 41403
diff changeset
   911
subsection{* Miscellaneous lemmas about indexes, decrementation, substitution  etc ... *}
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   912
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   913
lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   914
proof (induct p arbitrary: n rule: poly.induct, auto)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   915
  case (goal1 c n p n')
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   916
  then have "n = Suc (n - 1)"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   917
    by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   918
  then have "isnpolyh p (Suc (n - 1))"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   919
    using `isnpolyh p n` by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   920
  with goal1(2) show ?case
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   921
    by simp
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   922
qed
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   923
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   924
lemma isconstant_polybound0: "isnpolyh p n0 \<Longrightarrow> isconstant p \<longleftrightarrow> polybound0 p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   925
  by (induct p arbitrary: n0 rule: isconstant.induct) (auto simp add: isnpolyh_polybound0)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   926
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   927
lemma decrpoly_zero[simp]: "decrpoly p = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p"
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   928
  by (induct p) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   929
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   930
lemma decrpoly_normh: "isnpolyh p n0 \<Longrightarrow> polybound0 p \<Longrightarrow> isnpolyh (decrpoly p) (n0 - 1)"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   931
  apply (induct p arbitrary: n0)
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   932
  apply auto
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   933
  apply atomize
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   934
  apply (erule_tac x = "Suc nat" in allE)
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   935
  apply auto
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   936
  done
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   937
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   938
lemma head_polybound0: "isnpolyh p n0 \<Longrightarrow> polybound0 (head p)"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   939
  by (induct p  arbitrary: n0 rule: head.induct) (auto intro: isnpolyh_polybound0)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   940
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   941
lemma polybound0_I:
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   942
  assumes nb: "polybound0 a"
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   943
  shows "Ipoly (b # bs) a = Ipoly (b' # bs) a"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   944
  using nb
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   945
  by (induct a rule: poly.induct) auto
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   946
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   947
lemma polysubst0_I: "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b # bs) a) # bs) t"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   948
  by (induct t) simp_all
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   949
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   950
lemma polysubst0_I':
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   951
  assumes nb: "polybound0 a"
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   952
  shows "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b' # bs) a) # bs) t"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   953
  by (induct t) (simp_all add: polybound0_I[OF nb, where b="b" and b'="b'"])
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   954
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   955
lemma decrpoly:
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   956
  assumes nb: "polybound0 t"
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   957
  shows "Ipoly (x # bs) t = Ipoly bs (decrpoly t)"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   958
  using nb by (induct t rule: decrpoly.induct) simp_all
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   959
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   960
lemma polysubst0_polybound0:
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   961
  assumes nb: "polybound0 t"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   962
  shows "polybound0 (polysubst0 t a)"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   963
  using nb by (induct a rule: poly.induct) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   964
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   965
lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   966
  by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   967
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   968
primrec maxindex :: "poly \<Rightarrow> nat"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   969
where
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   970
  "maxindex (Bound n) = n + 1"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   971
| "maxindex (CN c n p) = max  (n + 1) (max (maxindex c) (maxindex p))"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   972
| "maxindex (Add p q) = max (maxindex p) (maxindex q)"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   973
| "maxindex (Sub p q) = max (maxindex p) (maxindex q)"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   974
| "maxindex (Mul p q) = max (maxindex p) (maxindex q)"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   975
| "maxindex (Neg p) = maxindex p"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   976
| "maxindex (Pw p n) = maxindex p"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   977
| "maxindex (C x) = 0"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   978
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   979
definition wf_bs :: "'a list \<Rightarrow> poly \<Rightarrow> bool"
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
   980
  where "wf_bs bs p \<longleftrightarrow> length bs \<ge> maxindex p"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   981
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   982
lemma wf_bs_coefficients: "wf_bs bs p \<Longrightarrow> \<forall>c \<in> set (coefficients p). wf_bs bs c"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
   983
proof (induct p rule: coefficients.induct)
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   984
  case (1 c p)
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   985
  show ?case
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
   986
  proof
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   987
    fix x
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   988
    assume xc: "x \<in> set (coefficients (CN c 0 p))"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   989
    then have "x = c \<or> x \<in> set (coefficients p)"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   990
      by simp
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
   991
    moreover
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   992
    {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   993
      assume "x = c"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   994
      then have "wf_bs bs x"
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
   995
        using "1.prems" unfolding wf_bs_def by simp
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   996
    }
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   997
    moreover
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   998
    {
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
   999
      assume H: "x \<in> set (coefficients p)"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1000
      from "1.prems" have "wf_bs bs p"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1001
        unfolding wf_bs_def by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1002
      with "1.hyps" H have "wf_bs bs x"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1003
        by blast
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1004
    }
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1005
    ultimately  show "wf_bs bs x"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1006
      by blast
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1007
  qed
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1008
qed simp_all
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1009
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1010
lemma maxindex_coefficients: "\<forall>c \<in> set (coefficients p). maxindex c \<le> maxindex p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1011
  by (induct p rule: coefficients.induct) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1012
56000
899ad5a3ad00 tuned proofs;
wenzelm
parents: 54489
diff changeset
  1013
lemma wf_bs_I: "wf_bs bs p \<Longrightarrow> Ipoly (bs @ bs') p = Ipoly bs p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1014
  unfolding wf_bs_def by (induct p) (auto simp add: nth_append)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1015
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1016
lemma take_maxindex_wf:
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
  1017
  assumes wf: "wf_bs bs p"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1018
  shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p"
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1019
proof -
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1020
  let ?ip = "maxindex p"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1021
  let ?tbs = "take ?ip bs"
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1022
  from wf have "length ?tbs = ?ip"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1023
    unfolding wf_bs_def by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1024
  then have wf': "wf_bs ?tbs p"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1025
    unfolding wf_bs_def by  simp
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1026
  have eq: "bs = ?tbs @ drop ?ip bs"
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1027
    by simp
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1028
  from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1029
    using eq by simp
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1030
qed
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1031
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1032
lemma decr_maxindex: "polybound0 p \<Longrightarrow> maxindex (decrpoly p) = maxindex p - 1"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1033
  by (induct p) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1034
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1035
lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1036
  unfolding wf_bs_def by simp
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1037
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1038
lemma wf_bs_insensitive': "wf_bs (x#bs) p = wf_bs (y#bs) p"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1039
  unfolding wf_bs_def by simp
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1040
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1041
lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x#bs) p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1042
  by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def)
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1043
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1044
lemma coefficients_Nil[simp]: "coefficients p \<noteq> []"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1045
  by (induct p rule: coefficients.induct) simp_all
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1046
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1047
lemma coefficients_head: "last (coefficients p) = head p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1048
  by (induct p rule: coefficients.induct) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1049
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1050
lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \<Longrightarrow> wf_bs (x#bs) p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1051
  unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1052
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1053
lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists>ys. length (xs @ ys) = n"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1054
  apply (rule exI[where x="replicate (n - length xs) z"])
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1055
  apply simp
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1056
  done
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1057
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1058
lemma isnpolyh_Suc_const: "isnpolyh p (Suc n) \<Longrightarrow> isconstant p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1059
  apply (cases p)
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1060
  apply auto
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1061
  apply (case_tac "nat")
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1062
  apply simp_all
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1063
  done
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1064
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1065
lemma wf_bs_polyadd: "wf_bs bs p \<and> wf_bs bs q \<longrightarrow> wf_bs bs (p +\<^sub>p q)"
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
  1066
  unfolding wf_bs_def
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1067
  apply (induct p q rule: polyadd.induct)
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1068
  apply (auto simp add: Let_def)
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1069
  done
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1070
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1071
lemma wf_bs_polyul: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p *\<^sub>p q)"
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
  1072
  unfolding wf_bs_def
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
  1073
  apply (induct p q arbitrary: bs rule: polymul.induct)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1074
  apply (simp_all add: wf_bs_polyadd)
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1075
  apply clarsimp
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1076
  apply (rule wf_bs_polyadd[unfolded wf_bs_def, rule_format])
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1077
  apply auto
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1078
  done
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1079
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1080
lemma wf_bs_polyneg: "wf_bs bs p \<Longrightarrow> wf_bs bs (~\<^sub>p p)"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1081
  unfolding wf_bs_def by (induct p rule: polyneg.induct) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1082
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1083
lemma wf_bs_polysub: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p -\<^sub>p q)"
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1084
  unfolding polysub_def split_def fst_conv snd_conv
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1085
  using wf_bs_polyadd wf_bs_polyneg by blast
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1086
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1087
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1088
subsection {* Canonicity of polynomial representation, see lemma isnpolyh_unique *}
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1089
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1090
definition "polypoly bs p = map (Ipoly bs) (coefficients p)"
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1091
definition "polypoly' bs p = map (Ipoly bs \<circ> decrpoly) (coefficients p)"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1092
definition "poly_nate bs p = map (Ipoly bs \<circ> decrpoly) (coefficients (polynate p))"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1093
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1094
lemma coefficients_normh: "isnpolyh p n0 \<Longrightarrow> \<forall>q \<in> set (coefficients p). isnpolyh q n0"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1095
proof (induct p arbitrary: n0 rule: coefficients.induct)
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1096
  case (1 c p n0)
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1097
  have cp: "isnpolyh (CN c 0 p) n0"
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1098
    by fact
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1099
  then have norm: "isnpolyh c 0" "isnpolyh p 0" "p \<noteq> 0\<^sub>p" "n0 = 0"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1100
    by (auto simp add: isnpolyh_mono[where n'=0])
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1101
  from "1.hyps"[OF norm(2)] norm(1) norm(4) show ?case
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1102
    by simp
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1103
qed auto
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1104
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1105
lemma coefficients_isconst: "isnpolyh p n \<Longrightarrow> \<forall>q \<in> set (coefficients p). isconstant q"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1106
  by (induct p arbitrary: n rule: coefficients.induct) (auto simp add: isnpolyh_Suc_const)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1107
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1108
lemma polypoly_polypoly':
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1109
  assumes np: "isnpolyh p n0"
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1110
  shows "polypoly (x # bs) p = polypoly' bs p"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1111
proof -
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1112
  let ?cf = "set (coefficients p)"
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1113
  from coefficients_normh[OF np] have cn_norm: "\<forall> q\<in> ?cf. isnpolyh q n0" .
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1114
  {
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1115
    fix q
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1116
    assume q: "q \<in> ?cf"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1117
    from q cn_norm have th: "isnpolyh q n0"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1118
      by blast
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1119
    from coefficients_isconst[OF np] q have "isconstant q"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1120
      by blast
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1121
    with isconstant_polybound0[OF th] have "polybound0 q"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1122
      by blast
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1123
  }
56009
dda076a32aea tuned proofs;
wenzelm
parents: 56000
diff changeset
  1124
  then have "\<forall>q \<in> ?cf. polybound0 q" ..
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1125
  then have "\<forall>q \<in> ?cf. Ipoly (x # bs) q = Ipoly bs (decrpoly q)"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1126
    using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs]
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1127
    by auto
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1128
  then show ?thesis
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1129
    unfolding polypoly_def polypoly'_def by simp
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1130
qed
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1131
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1132
lemma polypoly_poly:
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1133
  assumes "isnpolyh p n0"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1134
  shows "Ipoly (x # bs) p = poly (polypoly (x # bs) p) x"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1135
  using assms
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1136
  by (induct p arbitrary: n0 bs rule: coefficients.induct) (auto simp add: polypoly_def)
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1137
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
  1138
lemma polypoly'_poly:
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1139
  assumes "isnpolyh p n0"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1140
  shows "\<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x"
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1141
  using polypoly_poly[OF assms, simplified polypoly_polypoly'[OF assms]] .
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1142
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1143
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1144
lemma polypoly_poly_polybound0:
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1145
  assumes "isnpolyh p n0"
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1146
    and "polybound0 p"
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1147
  shows "polypoly bs p = [Ipoly bs p]"
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1148
  using assms
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1149
  unfolding polypoly_def
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1150
  apply (cases p)
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1151
  apply auto
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1152
  apply (case_tac nat)
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1153
  apply auto
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1154
  done
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1155
52803
bcaa5bbf7e6b tuned proofs;
wenzelm
parents: 52658
diff changeset
  1156
lemma head_isnpolyh: "isnpolyh p n0 \<Longrightarrow> isnpolyh (head p) n0"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1157
  by (induct p rule: head.induct) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1158
56043
0b25c3d34b77 tuned proofs;
wenzelm
parents: 56009
diff changeset
  1159
lemma headn_nz[simp]: "isnpolyh p n0 \<Longrightarrow> headn p m = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p"
52658
1e7896c7f781 tuned specifications and proofs;
wenzelm
parents: 50282
diff changeset
  1160
  by (cases p) auto
33154
daa6ddece9f0 Multivariate polynomials library over fields
chaieb
parents:
diff changeset
  1161
daa6ddece9f0 Multivariate polynomials library over fields
cha