src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 changeset 41813 4eb43410d2fa parent 41812 d46c2908a838 child 41814 3848eb635eab
```     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 21 23:14:36 2011 +0100
1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 21 23:14:36 2011 +0100
1.3 @@ -109,10 +109,7 @@
1.4
1.5  consts
1.6    polysub :: "poly\<times>poly \<Rightarrow> poly"
1.7 -  polymul :: "poly\<times>poly \<Rightarrow> poly"
1.8
1.9 -abbreviation poly_mul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
1.10 -  where "a *\<^sub>p b \<equiv> polymul (a,b)"
1.11  abbreviation poly_sub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
1.12    where "a -\<^sub>p b \<equiv> polysub (a,b)"
1.13
1.14 @@ -141,19 +138,20 @@
1.15
1.16  defs polysub_def[code]: "polysub \<equiv> \<lambda> (p,q). polyadd p (polyneg q)"
1.17
1.18 -recdef polymul "measure (\<lambda>(a,b). size a + size b)"
1.19 -  "polymul(C c, C c') = C (c*\<^sub>Nc')"
1.20 -  "polymul(C c, CN c' n' p') =
1.21 -      (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul(C c,c')) n' (polymul(C c, p')))"
1.22 -  "polymul(CN c n p, C c') =
1.23 -      (if c' = 0\<^sub>N  then 0\<^sub>p else CN (polymul(c,C c')) n (polymul(p, C c')))"
1.24 -  "polymul(CN c n p, CN c' n' p') =
1.25 -  (if n<n' then CN (polymul(c,CN c' n' p')) n (polymul(p,CN c' n' p'))
1.26 +
1.27 +fun polymul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
1.28 +where
1.29 +  "polymul (C c) (C c') = C (c*\<^sub>Nc')"
1.30 +| "polymul (C c) (CN c' n' p') =
1.31 +      (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul (C c) c') n' (polymul (C c) p'))"
1.32 +| "polymul (CN c n p) (C c') =
1.33 +      (if c' = 0\<^sub>N  then 0\<^sub>p else CN (polymul c (C c')) n (polymul p (C c')))"
1.34 +| "polymul (CN c n p) (CN c' n' p') =
1.35 +  (if n<n' then CN (polymul c (CN c' n' p')) n (polymul p (CN c' n' p'))
1.36    else if n' < n
1.37 -  then CN (polymul(CN c n p,c')) n' (polymul(CN c n p,p'))
1.38 -  else polyadd (polymul(CN c n p, c')) (CN 0\<^sub>p n' (polymul(CN c n p, p'))))"
1.39 -  "polymul (a,b) = Mul a b"
1.40 -(hints recdef_cong del: if_cong)
1.41 +  then CN (polymul (CN c n p) c') n' (polymul (CN c n p) p')
1.42 +  else polyadd (polymul (CN c n p) c') (CN 0\<^sub>p n' (polymul (CN c n p) p')))"
1.43 +| "polymul a b = Mul a b"
1.44
1.45  declare if_cong[fundef_cong]
1.46  declare let_cong[fundef_cong]
1.47 @@ -161,8 +159,8 @@
1.48  fun polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
1.49  where
1.50    "polypow 0 = (\<lambda>p. 1\<^sub>p)"
1.51 -| "polypow n = (\<lambda>p. let q = polypow (n div 2) p ; d = polymul(q,q) in
1.52 -                    if even n then d else polymul(p,d))"
1.53 +| "polypow n = (\<lambda>p. let q = polypow (n div 2) p ; d = polymul q q in
1.54 +                    if even n then d else polymul p d)"
1.55
1.56  abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
1.57    where "a ^\<^sub>p k \<equiv> polypow k a"
1.58 @@ -404,22 +402,20 @@
1.59                               else degreen p m + degreen q m)"
1.60    using np nq m
1.61  proof(induct p q arbitrary: n0 n1 m rule: polymul.induct)
1.62 -  case (2 a b c' n' p')
1.63 -  let ?c = "(a,b)"
1.64 +  case (2 c c' n' p')
1.65    { case (1 n0 n1)
1.66 -    with "2.hyps"(1-3)[of n' n' n']
1.67 -      and "2.hyps"(4-6)[of "Suc n'" "Suc n'" n']
1.68 +    with "2.hyps"(4-6)[of n' n' n']
1.69 +      and "2.hyps"(1-3)[of "Suc n'" "Suc n'" n']
1.70      show ?case by (auto simp add: min_def)
1.71    next
1.72      case (2 n0 n1) thus ?case by auto
1.73    next
1.74      case (3 n0 n1) thus ?case  using "2.hyps" by auto }
1.75  next
1.76 -  case (3 c n p a b)
1.77 -  let ?c' = "(a,b)"
1.78 +  case (3 c n p c')
1.79    { case (1 n0 n1)
1.80 -    with "3.hyps"(1-3)[of n n n]
1.81 -      "3.hyps"(4-6)[of "Suc n" "Suc n" n]
1.82 +    with "3.hyps"(4-6)[of n n n]
1.83 +      "3.hyps"(1-3)[of "Suc n" "Suc n" n]
1.84      show ?case by (auto simp add: min_def)
1.85    next
1.86      case (2 n0 n1) thus ?case by auto
1.87 @@ -436,19 +432,19 @@
1.88          and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1"
1.89          by simp_all
1.90        { assume "n < n'"
1.91 -        with "4.hyps"(13-14)[OF np cnp', of n]
1.92 -          "4.hyps"(16)[OF nc cnp', of n] nn0 cnp
1.93 +        with "4.hyps"(4-5)[OF np cnp', of n]
1.94 +          "4.hyps"(1)[OF nc cnp', of n] nn0 cnp
1.95          have ?case by (simp add: min_def)
1.96        } moreover {
1.97          assume "n' < n"
1.98 -        with "4.hyps"(1-2)[OF cnp np', of "n'"]
1.99 -          "4.hyps"(4)[OF cnp nc', of "Suc n'"] nn1 cnp'
1.100 +        with "4.hyps"(16-17)[OF cnp np', of "n'"]
1.101 +          "4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp'
1.102          have ?case
1.103            by (cases "Suc n' = n", simp_all add: min_def)
1.104        } moreover {
1.105          assume "n' = n"
1.106 -        with "4.hyps"(1-2)[OF cnp np', of n]
1.107 -          "4.hyps"(4)[OF cnp nc', of n] cnp cnp' nn1 nn0
1.108 +        with "4.hyps"(16-17)[OF cnp np', of n]
1.109 +          "4.hyps"(13)[OF cnp nc', of n] cnp cnp' nn1 nn0
1.110          have ?case
1.111            apply (auto intro!: polyadd_normh)
1.112            apply (simp_all add: min_def isnpolyh_mono[OF nn0])
1.113 @@ -466,20 +462,20 @@
1.114        have "n'<n \<or> n < n' \<or> n' = n" by auto
1.115        moreover
1.116        {assume "n' < n \<or> n < n'"
1.117 -        with "4.hyps"(3,15,18) np np' m
1.118 +        with "4.hyps"(3,6,18) np np' m
1.119          have ?eq by auto }
1.120        moreover
1.121        {assume nn': "n' = n" hence nn:"\<not> n' < n \<and> \<not> n < n'" by arith
1.122 -        from "4.hyps"(1,3)[of n n' n]
1.123 -          "4.hyps"(4,5)[of n "Suc n'" n]
1.124 +        from "4.hyps"(16,18)[of n n' n]
1.125 +          "4.hyps"(13,14)[of n "Suc n'" n]
1.126            np np' nn'
1.127          have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
1.128            "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
1.129            "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
1.130            "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
1.131          {assume mn: "m = n"
1.132 -          from "4.hyps"(2,3)[OF norm(1,4), of n]
1.133 -            "4.hyps"(4,6)[OF norm(1,2), of n] norm nn' mn
1.134 +          from "4.hyps"(17,18)[OF norm(1,4), of n]
1.135 +            "4.hyps"(13,15)[OF norm(1,2), of n] norm nn' mn
1.136            have degs:  "degreen (?cnp *\<^sub>p c') n =
1.137              (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"
1.138              "degreen (?cnp *\<^sub>p p') n = ?d1  + degreen p' n" by (simp_all add: min_def)
1.139 @@ -490,8 +486,8 @@
1.140            have nmin: "n \<le> min n n" by (simp add: min_def)
1.141            from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
1.142            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 = degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
1.143 -          from "4.hyps"(1-3)[OF norm(1,4), of n]
1.144 -            "4.hyps"(4-6)[OF norm(1,2), of n]
1.145 +          from "4.hyps"(16-18)[OF norm(1,4), of n]
1.146 +            "4.hyps"(13-15)[OF norm(1,2), of n]
1.147              mn norm m nn' deg
1.148            have ?eq by simp}
1.149          moreover
1.150 @@ -499,15 +495,15 @@
1.151            from nn' m np have max1: "m \<le> max n n"  by simp
1.152            hence min1: "m \<le> min n n" by simp
1.153            hence min2: "m \<le> min n (Suc n)" by simp
1.154 -          from "4.hyps"(1-3)[OF norm(1,4) min1]
1.155 -            "4.hyps"(4-6)[OF norm(1,2) min2]
1.156 +          from "4.hyps"(16-18)[OF norm(1,4) min1]
1.157 +            "4.hyps"(13-15)[OF norm(1,2) min2]
1.158              degreen_polyadd[OF norm(3,6) max1]
1.159
1.160            have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m
1.161              \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
1.162              using mn nn' np np' by simp
1.163 -          with "4.hyps"(1-3)[OF norm(1,4) min1]
1.164 -            "4.hyps"(4-6)[OF norm(1,2) min2]
1.165 +          with "4.hyps"(16-18)[OF norm(1,4) min1]
1.166 +            "4.hyps"(13-15)[OF norm(1,2) min2]
1.167              degreen_0[OF norm(3) mn']
1.168            have ?eq using nn' mn np np' by clarsimp}
1.169          ultimately have ?eq by blast}
1.170 @@ -519,8 +515,8 @@
1.171        let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
1.172        {assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
1.173          hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp
1.174 -        from "4.hyps"(1-3) [of n n n]
1.175 -          "4.hyps"(4-6)[of n "Suc n" n]
1.176 +        from "4.hyps"(16-18) [of n n n]
1.177 +          "4.hyps"(13-15)[of n "Suc n" n]
1.178            np np' C(2) mn
1.179          have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
1.180            "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
1.181 @@ -555,7 +551,7 @@
1.182    using polymul_properties(3) by blast
1.183  lemma polymul_norm:
1.184    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.185 -  shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul (p,q))"
1.186 +  shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul p q)"
1.187    using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
1.188
1.189  lemma headconst_zero: "isnpolyh p n0 \<Longrightarrow> headconst p = 0\<^sub>N \<longleftrightarrow> p = 0\<^sub>p"
1.190 @@ -623,12 +619,12 @@
1.191  next
1.192    case (2 n)
1.193    let ?q = "polypow ((Suc n) div 2) p"
1.194 -  let ?d = "polymul(?q,?q)"
1.195 +  let ?d = "polymul ?q ?q"
1.196    have "odd (Suc n) \<or> even (Suc n)" by simp
1.197    moreover
1.198    {assume odd: "odd (Suc n)"
1.199      have th: "(Suc (Suc (Suc (0\<Colon>nat)) * (Suc n div Suc (Suc (0\<Colon>nat))))) = Suc n div 2 + Suc n div 2 + 1" by arith
1.200 -    from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul(p, ?d))" by (simp add: Let_def)
1.201 +    from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)" by (simp add: Let_def)
1.202      also have "\<dots> = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2)*(Ipoly bs p)^(Suc n div 2)"
1.203        using "2.hyps" by simp
1.204      also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)"
1.205 @@ -653,10 +649,10 @@
1.206  proof (induct k arbitrary: n rule: polypow.induct)
1.207    case (2 k n)
1.208    let ?q = "polypow (Suc k div 2) p"
1.209 -  let ?d = "polymul (?q,?q)"
1.210 +  let ?d = "polymul ?q ?q"
1.211    from prems have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+
1.212    from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp
1.213 -  from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul(p,?d)) n" by simp
1.214 +  from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n" by simp
1.215    from dn on show ?case by (simp add: Let_def)
1.216  qed auto
1.217
1.218 @@ -1181,12 +1177,12 @@
1.219     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.220    shows "\<lbrakk>isnpolyh p n0; isnpolyh q n1 ; p \<noteq> 0\<^sub>p ; q \<noteq> 0\<^sub>p \<rbrakk> \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q"
1.221  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
1.222 -  case (2 a b c' n' p' n0 n1)
1.223 -  hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum (a,b)"  by (simp_all add: head_isnpolyh)
1.224 +  case (2 c c' n' p' n0 n1)
1.225 +  hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum c"  by (simp_all add: head_isnpolyh)
1.226    thus ?case using prems by (cases n', auto)
1.227  next
1.228 -  case (3 c n p a' b' n0 n1)
1.229 -  hence "isnpolyh (head (CN c n p)) n0" "isnormNum (a',b')"  by (simp_all add: head_isnpolyh)
1.230 +  case (3 c n p c' n0 n1)
1.231 +  hence "isnpolyh (head (CN c n p)) n0" "isnormNum c'"  by (simp_all add: head_isnpolyh)
1.232    thus ?case using prems by (cases n, auto)
1.233  next
1.234    case (4 c n p c' n' p' n0 n1)
1.235 @@ -1197,11 +1193,11 @@
1.236    moreover
1.237    {assume nn': "n < n'" hence ?case
1.238        using norm
1.239 -    "4.hyps"(5)[OF norm(1,6)]
1.240 -    "4.hyps"(6)[OF norm(2,6)] by (simp, cases n, simp,cases n', simp_all)}
1.241 +    "4.hyps"(2)[OF norm(1,6)]
1.242 +    "4.hyps"(1)[OF norm(2,6)] by (simp, cases n, simp,cases n', simp_all)}
1.243    moreover {assume nn': "n'< n"
1.244 -    hence ?case using norm "4.hyps"(1) [OF norm(5,3)]
1.245 -      "4.hyps"(2)[OF norm(5,4)]
1.246 +    hence ?case using norm "4.hyps"(6) [OF norm(5,3)]
1.247 +      "4.hyps"(5)[OF norm(5,4)]
1.248        by (simp,cases n',simp,cases n,auto)}
1.249    moreover {assume nn': "n' = n"
1.250      from nn' polymul_normh[OF norm(5,4)]
1.251 @@ -1225,8 +1221,8 @@
1.252      have dth:"degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp
1.253      hence dth':"degree (CN c 0 p *\<^sub>p c') \<noteq> degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp
1.254      from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth
1.255 -    have ?case   using norm "4.hyps"(1)[OF norm(5,3)]
1.256 -        "4.hyps"(2)[OF norm(5,4)] nn' nz by simp }
1.257 +    have ?case   using norm "4.hyps"(6)[OF norm(5,3)]
1.258 +        "4.hyps"(5)[OF norm(5,4)] nn' nz by simp }
1.259      ultimately have ?case by (cases n) auto}
1.260    ultimately show ?case by blast
1.261  qed simp_all
```