src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 changeset 60698 29e8bdc41f90 parent 60580 7e741e22d7fc child 61166 5976fe402824
```     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jul 09 00:39:49 2015 +0200
1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jul 09 00:40:57 2015 +0200
1.3 @@ -8,7 +8,7 @@
1.4  imports Complex_Main Rat_Pair Polynomial_List
1.5  begin
1.6
1.7 -subsection\<open>Datatype of polynomial expressions\<close>
1.8 +subsection \<open>Datatype of polynomial expressions\<close>
1.9
1.10  datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly
1.11    | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
1.12 @@ -66,7 +66,7 @@
1.13  | "decrpoly a = a"
1.14
1.15
1.16 -subsection\<open>Degrees and heads and coefficients\<close>
1.17 +subsection \<open>Degrees and heads and coefficients\<close>
1.18
1.19  fun degree :: "poly \<Rightarrow> nat"
1.20  where
1.21 @@ -78,7 +78,8 @@
1.22    "head (CN c 0 p) = head p"
1.23  | "head p = p"
1.24
1.25 -(* More general notions of degree and head *)
1.26 +text \<open>More general notions of degree and head.\<close>
1.27 +
1.28  fun degreen :: "poly \<Rightarrow> nat \<Rightarrow> nat"
1.29  where
1.30    "degreen (CN c n p) = (\<lambda>m. if n = m then 1 + degreen p n else 0)"
1.31 @@ -110,7 +111,7 @@
1.32  | "headconst (C n) = n"
1.33
1.34
1.35 -subsection\<open>Operations for normalization\<close>
1.36 +subsection \<open>Operations for normalization\<close>
1.37
1.38  declare if_cong[fundef_cong del]
1.39  declare let_cong[fundef_cong del]
1.40 @@ -179,7 +180,7 @@
1.41  | "polynate (Pw p n) = polynate p ^\<^sub>p n"
1.42  | "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))"
1.43  | "polynate (C c) = C (normNum c)"
1.44 -by pat_completeness auto
1.45 +  by pat_completeness auto
1.46  termination by (relation "measure polysize") auto
1.47
1.48  fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly"
1.49 @@ -233,7 +234,7 @@
1.50  | "poly_deriv p = 0\<^sub>p"
1.51
1.52
1.53 -subsection\<open>Semantics of the polynomial representation\<close>
1.54 +subsection \<open>Semantics of the polynomial representation\<close>
1.55
1.56  primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field,power}"
1.57  where
1.58 @@ -246,8 +247,7 @@
1.59  | "Ipoly bs (Pw t n) = Ipoly bs t ^ n"
1.60  | "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p"
1.61
1.62 -abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field,power}"
1.63 -    ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
1.64 +abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field,power}"  ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
1.65    where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
1.66
1.67  lemma Ipoly_CInt: "Ipoly bs (C (i, 1)) = of_int i"
1.68 @@ -273,14 +273,14 @@
1.69  definition isnpoly :: "poly \<Rightarrow> bool"
1.70    where "isnpoly p = isnpolyh p 0"
1.71
1.72 -text\<open>polyadd preserves normal forms\<close>
1.73 +text \<open>polyadd preserves normal forms\<close>
1.74
1.75  lemma polyadd_normh: "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (polyadd p q) (min n0 n1)"
1.76  proof (induct p q arbitrary: n0 n1 rule: polyadd.induct)
1.77    case (2 ab c' n' p' n0 n1)
1.78    from 2 have  th1: "isnpolyh (C ab) (Suc n')"
1.79      by simp
1.80 -  from 2(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1"
1.81 +  from 2(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1"
1.82      by simp_all
1.83    with isnpolyh_mono have cp: "isnpolyh c' (Suc n')"
1.84      by simp
1.85 @@ -314,11 +314,11 @@
1.86      by simp
1.87    from 4 have n'gen1: "n' \<ge> n1"
1.88      by simp
1.89 -  have "n < n' \<or> n' < n \<or> n = n'"
1.90 -    by auto
1.91 -  moreover
1.92 -  {
1.93 -    assume eq: "n = n'"
1.94 +  consider (eq) "n = n'" | (lt) "n < n'" | (gt) "n > n'"
1.95 +    by arith
1.96 +  then show ?case
1.97 +  proof cases
1.98 +    case eq
1.99      with "4.hyps"(3)[OF nc nc']
1.100      have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)"
1.101        by auto
1.102 @@ -329,12 +329,10 @@
1.103        by simp
1.104      have minle: "min n0 n1 \<le> n'"
1.105        using ngen0 n'gen1 eq by simp
1.106 -    from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' have ?case
1.107 +    from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' show ?thesis
1.108        by (simp add: Let_def)
1.109 -  }
1.110 -  moreover
1.111 -  {
1.112 -    assume lt: "n < n'"
1.113 +  next
1.114 +    case lt
1.115      have "min n0 n1 \<le> n0"
1.116        by simp
1.117      with 4 lt have th1:"min n0 n1 \<le> n"
1.118 @@ -347,12 +345,10 @@
1.119        by arith
1.120      from "4.hyps"(1)[OF th21 th22] have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)"
1.121        using th23 by simp
1.122 -    with 4 lt th1 have ?case
1.123 +    with 4 lt th1 show ?thesis
1.124        by simp
1.125 -  }
1.126 -  moreover
1.127 -  {
1.128 -    assume gt: "n' < n"
1.129 +  next
1.130 +    case gt
1.131      then have gt': "n' < n \<and> \<not> n < n'"
1.132        by simp
1.133      have "min n0 n1 \<le> n1"
1.134 @@ -367,10 +363,9 @@
1.135        by arith
1.136      from "4.hyps"(2)[OF th22 th21] have "isnpolyh (polyadd (CN c n p) c') (Suc n')"
1.137        using th23 by simp
1.138 -    with 4 gt th1 have ?case
1.139 +    with 4 gt th1 show ?thesis
1.140        by simp
1.141 -  }
1.142 -  ultimately show ?case by blast
1.143 +  qed
1.144  qed auto
1.145
1.146  lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
1.147 @@ -378,9 +373,9 @@
1.148       (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left_NO_MATCH)
1.149
1.150  lemma polyadd_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polyadd p q)"
1.151 -  using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
1.152 +  using polyadd_normh[of p 0 q 0] isnpoly_def by simp
1.153
1.154 -text\<open>The degree of addition and other general lemmas needed for the normal form of polymul\<close>
1.155 +text \<open>The degree of addition and other general lemmas needed for the normal form of polymul.\<close>
1.156
1.157  lemma polyadd_different_degreen:
1.158    assumes "isnpolyh p n0"
1.159 @@ -391,17 +386,13 @@
1.160    using assms
1.161  proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct)
1.162    case (4 c n p c' n' p' m n0 n1)
1.163 -  have "n' = n \<or> n < n' \<or> n' < n" by arith
1.164 -  then show ?case
1.165 -  proof (elim disjE)
1.166 -    assume [simp]: "n' = n"
1.167 -    from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
1.168 +  show ?case
1.169 +  proof (cases "n = n'")
1.170 +    case True
1.171 +    with 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
1.172      show ?thesis by (auto simp: Let_def)
1.173    next
1.174 -    assume "n < n'"
1.175 -    with 4 show ?thesis by auto
1.176 -  next
1.177 -    assume "n' < n"
1.178 +    case False
1.179      with 4 show ?thesis by auto
1.180    qed
1.181  qed auto
1.182 @@ -441,13 +432,15 @@
1.183      by (cases n) auto
1.184  next
1.185    case (4 c n p c' n' p' n0 n1 m)
1.186 -  have "n' = n \<or> n < n' \<or> n' < n" by arith
1.187 -  then show ?case
1.188 -  proof (elim disjE)
1.189 -    assume [simp]: "n' = n"
1.190 -    from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
1.191 +  show ?case
1.192 +  proof (cases "n = n'")
1.193 +    case True
1.194 +    with 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
1.195      show ?thesis by (auto simp: Let_def)
1.196 -  qed simp_all
1.197 +  next
1.198 +    case False
1.199 +    then show ?thesis by simp
1.200 +  qed
1.201  qed auto
1.202
1.203  lemma polyadd_eq_const_degreen:
1.204 @@ -458,26 +451,16 @@
1.205    using assms
1.206  proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
1.207    case (4 c n p c' n' p' m n0 n1 x)
1.208 -  {
1.209 -    assume nn': "n' < n"
1.210 -    then have ?case using 4 by simp
1.211 -  }
1.212 -  moreover
1.213 -  {
1.214 -    assume nn': "\<not> n' < n"
1.215 -    then have "n < n' \<or> n = n'" by arith
1.216 -    moreover { assume "n < n'" with 4 have ?case by simp }
1.217 -    moreover
1.218 -    {
1.219 -      assume eq: "n = n'"
1.220 -      then have ?case using 4
1.221 -        apply (cases "p +\<^sub>p p' = 0\<^sub>p")
1.222 -        apply (auto simp add: Let_def)
1.223 -        done
1.224 -    }
1.225 -    ultimately have ?case by blast
1.226 -  }
1.227 -  ultimately show ?case by blast
1.228 +  consider "n = n'" | "n > n' \<or> n < n'" by arith
1.229 +  then show ?case
1.230 +  proof cases
1.231 +    case 1
1.232 +    with 4 show ?thesis
1.233 +      by (cases "p +\<^sub>p p' = 0\<^sub>p") (auto simp add: Let_def)
1.234 +  next
1.235 +    case 2
1.236 +    with 4 show ?thesis by auto
1.237 +  qed
1.238  qed simp_all
1.239
1.240  lemma polymul_properties:
1.241 @@ -500,7 +483,7 @@
1.242      then show ?case by auto
1.243    next
1.244      case (3 n0 n1)
1.245 -    then show ?case  using "2.hyps" by auto
1.246 +    then show ?case using "2.hyps" by auto
1.247    }
1.248  next
1.249    case (3 c n p c')
1.250 @@ -720,7 +703,7 @@
1.251  qed
1.252
1.253
1.254 -text\<open>polyneg is a negation and preserves normal forms\<close>
1.255 +text \<open>polyneg is a negation and preserves normal forms\<close>
1.256
1.257  lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
1.258    by (induct p rule: polyneg.induct) auto
1.259 @@ -738,7 +721,7 @@
1.260    using isnpoly_def polyneg_normh by simp
1.261
1.262
1.263 -text\<open>polysub is a substraction and preserves normal forms\<close>
1.264 +text \<open>polysub is a substraction and preserves normal forms\<close>
1.265
1.266  lemma polysub[simp]: "Ipoly bs (polysub p q) = Ipoly bs p - Ipoly bs q"
1.267    by (simp add: polysub_def)
1.268 @@ -762,7 +745,7 @@
1.269    by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
1.270      (auto simp: Nsub0[simplified Nsub_def] Let_def)
1.271
1.272 -text\<open>polypow is a power function and preserves normal forms\<close>
1.273 +text \<open>polypow is a power function and preserves normal forms\<close>
1.274
1.275  lemma polypow[simp]:
1.276    "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n"
1.277 @@ -830,7 +813,7 @@
1.278    shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
1.279    by (simp add: polypow_normh isnpoly_def)
1.280
1.281 -text\<open>Finally the whole normalization\<close>
1.282 +text \<open>Finally the whole normalization\<close>
1.283
1.284  lemma polynate [simp]:
1.285    "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})"
1.286 @@ -843,7 +826,7 @@
1.287       (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
1.288        simp_all add: isnpoly_def)
1.289
1.290 -text\<open>shift1\<close>
1.291 +text \<open>shift1\<close>
1.292
1.293
1.294  lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"
1.295 @@ -1254,7 +1237,7 @@
1.296  qed
1.297
1.298
1.299 -text\<open>consequences of unicity on the algorithms for polynomial normalization\<close>
1.300 +text \<open>consequences of unicity on the algorithms for polynomial normalization\<close>
1.301
1.302  lemma polyadd_commute:
1.303    assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.304 @@ -1328,7 +1311,7 @@
1.305    unfolding poly_nate_polypoly' by auto
1.306
1.307
1.308 -subsection\<open>heads, degrees and all that\<close>
1.309 +subsection \<open>heads, degrees and all that\<close>
1.310
1.311  lemma degree_eq_degreen0: "degree p = degreen p 0"
1.312    by (induct p rule: degree.induct) simp_all
```