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