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