src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 changeset 41807 ab5d2d81f9fb parent 41763 8ce56536fda7 child 41816 7a55699805dc
```     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 21 18:29:47 2011 +0100
1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 21 23:47:19 2011 +0100
1.3 @@ -253,53 +253,53 @@
1.4        \<Longrightarrow> isnpolyh (polyadd(p,q)) (min n0 n1)"
1.5  proof(induct p q arbitrary: n0 n1 rule: polyadd.induct)
1.6    case (2 a b c' n' p' n0 n1)
1.7 -  from prems have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp
1.8 -  from prems(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
1.9 +  from 2 have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp
1.10 +  from 2(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
1.11    with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
1.12 -  with prems(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp
1.13 +  with 2(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp
1.14    from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp
1.15 -  thus ?case using prems th3 by simp
1.16 +  thus ?case using 2 th3 by simp
1.17  next
1.18    case (3 c' n' p' a b n1 n0)
1.19 -  from prems have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp
1.20 -  from prems(2) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
1.21 +  from 3 have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp
1.22 +  from 3(2) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
1.23    with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
1.24 -  with prems(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp
1.25 +  with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp
1.26    from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp
1.27 -  thus ?case using prems th3 by simp
1.28 +  thus ?case using 3 th3 by simp
1.29  next
1.30    case (4 c n p c' n' p' n0 n1)
1.31    hence nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" by simp_all
1.32 -  from prems have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all
1.33 -  from prems have ngen0: "n \<ge> n0" by simp
1.34 -  from prems have n'gen1: "n' \<ge> n1" by simp
1.35 +  from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all
1.36 +  from 4 have ngen0: "n \<ge> n0" by simp
1.37 +  from 4 have n'gen1: "n' \<ge> n1" by simp
1.38    have "n < n' \<or> n' < n \<or> n = n'" by auto
1.39    moreover {assume eq: "n = n'"
1.40 -    with prems(2)[OF nc nc']
1.41 +    with 4(2)[OF nc nc']
1.42      have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto
1.43      hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)"
1.44        using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto
1.45 -    from eq prems(1)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
1.46 +    from eq 4(1)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
1.47      have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp
1.48 -    from minle npp' ncc'n01 prems ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}
1.49 +    from minle npp' ncc'n01 eq ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}
1.50    moreover {assume lt: "n < n'"
1.51      have "min n0 n1 \<le> n0" by simp
1.52 -    with prems have th1:"min n0 n1 \<le> n" by auto
1.53 -    from prems have th21: "isnpolyh c (Suc n)" by simp
1.54 -    from prems have th22: "isnpolyh (CN c' n' p') n'" by simp
1.55 +    with 4 have th1:"min n0 n1 \<le> n" by auto
1.56 +    from 4 have th21: "isnpolyh c (Suc n)" by simp
1.57 +    from 4 have th22: "isnpolyh (CN c' n' p') n'" by simp
1.58      from lt have th23: "min (Suc n) n' = Suc n" by arith
1.59 -    from prems(4)[OF th21 th22]
1.60 +    from 4(4)[OF th21 th22]
1.61      have "isnpolyh (polyadd (c, CN c' n' p')) (Suc n)" using th23 by simp
1.62 -    with prems th1 have ?case by simp }
1.63 +    with 4 lt th1 have ?case by simp }
1.64    moreover {assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp
1.65      have "min n0 n1 \<le> n1"  by simp
1.66 -    with prems have th1:"min n0 n1 \<le> n'" by auto
1.67 -    from prems have th21: "isnpolyh c' (Suc n')" by simp_all
1.68 -    from prems have th22: "isnpolyh (CN c n p) n" by simp
1.69 +    with 4 have th1:"min n0 n1 \<le> n'" by auto
1.70 +    from 4 have th21: "isnpolyh c' (Suc n')" by simp_all
1.71 +    from 4 have th22: "isnpolyh (CN c n p) n" by simp
1.72      from gt have th23: "min n (Suc n') = Suc n'" by arith
1.73 -    from prems(3)[OF th22 th21]
1.74 +    from 4(3)[OF th22 th21]
1.75      have "isnpolyh (polyadd (CN c n p,c')) (Suc n')" using th23 by simp
1.76 -    with prems th1 have ?case by simp}
1.77 +    with 4 gt th1 have ?case by simp}
1.78        ultimately show ?case by blast
1.79  qed auto
1.80
1.81 @@ -370,14 +370,15 @@
1.82    \<Longrightarrow> degreen p m = degreen q m"
1.83  proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
1.84    case (4 c n p c' n' p' m n0 n1 x)
1.85 -  {assume nn': "n' < n" hence ?case using prems by simp}
1.86 +  {assume nn': "n' < n" hence ?case using 4 by simp}
1.87    moreover
1.88    {assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith
1.89 -    moreover {assume "n < n'" with prems have ?case by simp }
1.90 -    moreover {assume eq: "n = n'" hence ?case using prems
1.91 +    moreover {assume "n < n'" with 4 have ?case by simp }
1.92 +    moreover {assume eq: "n = n'" hence ?case using 4
1.93          apply (cases "p +\<^sub>p p' = 0\<^sub>p")
1.94          apply (auto simp add: Let_def)
1.95 -        by blast
1.96 +        apply blast
1.97 +        done
1.98        }
1.99      ultimately have ?case by blast}
1.100    ultimately show ?case by blast
1.101 @@ -664,13 +665,13 @@
1.102  qed
1.103
1.104  lemma polypow_normh:
1.105 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.106 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.107    shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
1.108  proof (induct k arbitrary: n rule: polypow.induct)
1.109    case (2 k n)
1.110    let ?q = "polypow (Suc k div 2) p"
1.111    let ?d = "polymul (?q,?q)"
1.112 -  from prems have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+
1.113 +  from 2 have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+
1.114    from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp
1.115    from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul(p,?d)) n" by simp
1.116    from dn on show ?case by (simp add: Let_def)
1.117 @@ -695,7 +696,7 @@
1.118
1.119
1.120  lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"
1.121 -by (simp add: shift1_def polymul)
1.122 +  by (simp add: shift1_def)
1.123
1.124  lemma shift1_isnpoly:
1.125    assumes pn: "isnpoly p" and pnz: "p \<noteq> 0\<^sub>p" shows "isnpoly (shift1 p) "
1.126 @@ -713,7 +714,7 @@
1.127    using f np by (induct k arbitrary: p, auto)
1.128
1.129  lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (Mul (Pw (Bound 0) n) p)"
1.130 -  by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc )
1.131 +  by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
1.132
1.133  lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
1.134    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
1.135 @@ -731,10 +732,10 @@
1.136    using np
1.137  proof (induct p arbitrary: n rule: behead.induct)
1.138    case (1 c p n) hence pn: "isnpolyh p n" by simp
1.139 -  from prems(2)[OF pn]
1.140 +  from 1(1)[OF pn]
1.141    have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" .
1.142    then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
1.143 -    by (simp_all add: th[symmetric] field_simps power_Suc)
1.144 +    by (simp_all add: th[symmetric] field_simps)
1.145  qed (auto simp add: Let_def)
1.146
1.148 @@ -747,7 +748,7 @@
1.149    case (goal1 c n p n')
1.150    hence "n = Suc (n - 1)" by simp
1.151    hence "isnpolyh p (Suc (n - 1))"  using `isnpolyh p n` by simp
1.152 -  with prems(2) show ?case by simp
1.153 +  with goal1(2) show ?case by simp
1.154  qed
1.155
1.156  lemma isconstant_polybound0: "isnpolyh p n0 \<Longrightarrow> isconstant p \<longleftrightarrow> polybound0 p"
1.157 @@ -838,7 +839,7 @@
1.158  qed
1.159
1.160  lemma decr_maxindex: "polybound0 p \<Longrightarrow> maxindex (decrpoly p) = maxindex p - 1"
1.161 -  by (induct p, auto)
1.162 +  by (induct p) auto
1.163
1.164  lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p"
1.165    unfolding wf_bs_def by simp
1.166 @@ -1033,7 +1034,7 @@
1.167      isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
1.168
1.169  lemma polymul_1[simp]:
1.170 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.171 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.172    and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p"
1.173    using isnpolyh_unique[OF polymul_normh[OF np one_normh] np]
1.174      isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
1.175 @@ -1101,17 +1102,17 @@
1.176  next
1.177    case (2 a b c' n' p')
1.178    let ?c = "(a,b)"
1.179 -  from prems have "degree (C ?c) = degree (CN c' n' p')" by simp
1.180 +  from 2 have "degree (C ?c) = degree (CN c' n' p')" by simp
1.181    hence nz:"n' > 0" by (cases n', auto)
1.182    hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
1.183 -  with prems show ?case by simp
1.184 +  with 2 show ?case by simp
1.185  next
1.186    case (3 c n p a' b')
1.187    let ?c' = "(a',b')"
1.188 -  from prems have "degree (C ?c') = degree (CN c n p)" by simp
1.189 +  from 3 have "degree (C ?c') = degree (CN c n p)" by simp
1.190    hence nz:"n > 0" by (cases n, auto)
1.191    hence "head (CN c n p) = CN c n p" by (cases n, auto)
1.192 -  with prems show ?case by simp
1.193 +  with 3 show ?case by simp
1.194  next
1.195    case (4 c n p c' n' p')
1.196    hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1"
1.197 @@ -1126,36 +1127,40 @@
1.198    moreover
1.199    {assume nn': "n = n'"
1.200      have "n = 0 \<or> n >0" by arith
1.201 -    moreover {assume nz: "n = 0" hence ?case using prems by (auto simp add: Let_def degcmc')}
1.202 +    moreover {assume nz: "n = 0" hence ?case using 4 nn' by (auto simp add: Let_def degcmc')}
1.203      moreover {assume nz: "n > 0"
1.204 -      with nn' H(3) have  cc':"c = c'" and pp': "p = p'" by (cases n, auto)+
1.205 -      hence ?case using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] polysub_same_0[OF c'nh, simplified polysub_def split_def fst_conv snd_conv] using nn' prems by (simp add: Let_def)}
1.206 +      with nn' H(3) have  cc': "c = c'" and pp': "p = p'" by (cases n, auto)+
1.207 +      hence ?case
1.208 +        using polysub_same_0 [OF p'nh, simplified polysub_def split_def fst_conv snd_conv]
1.209 +          polysub_same_0 [OF c'nh, simplified polysub_def split_def fst_conv snd_conv]
1.210 +        using 4 nn' by (simp add: Let_def) }
1.211      ultimately have ?case by blast}
1.212    moreover
1.213    {assume nn': "n < n'" hence n'p: "n' > 0" by simp
1.214      hence headcnp':"head (CN c' n' p') = CN c' n' p'"  by (cases n', simp_all)
1.215 -    have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" using prems by (cases n', simp_all)
1.216 -    hence "n > 0" by (cases n, simp_all)
1.217 -    hence headcnp: "head (CN c n p) = CN c n p" by (cases n, auto)
1.219 +    have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')"
1.220 +      using 4 nn' by (cases n', simp_all)
1.221 +    hence "n > 0" by (cases n) simp_all
1.222 +    hence headcnp: "head (CN c n p) = CN c n p" by (cases n) auto
1.223 +    from H(3) headcnp headcnp' nn' have ?case by auto }
1.224    moreover
1.225    {assume nn': "n > n'"  hence np: "n > 0" by simp
1.226 -    hence headcnp:"head (CN c n p) = CN c n p"  by (cases n, simp_all)
1.227 -    from prems have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp
1.228 -    from np have degcnp: "degree (CN c n p) = 0" by (cases n, simp_all)
1.229 +    hence headcnp: "head (CN c n p) = CN c n p" by (cases n) simp_all
1.230 +    from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp
1.231 +    from np have degcnp: "degree (CN c n p) = 0" by (cases n) simp_all
1.232      with degcnpeq have "n' > 0" by (cases n', simp_all)
1.233 -    hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
1.235 +    hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n') auto
1.236 +    from H(3) headcnp headcnp' nn' have ?case by auto }
1.237    ultimately show ?case  by blast
1.238  qed auto
1.239
1.242 +  by (induct p arbitrary: n0 rule: head.induct) (simp_all add: shift1_def)
1.243
1.244  lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p"
1.245  proof(induct k arbitrary: n0 p)
1.246    case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
1.247 -  with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
1.248 +  with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
1.250    thus ?case by (simp add: funpow_swap1)
1.251  qed auto
1.252 @@ -1194,19 +1199,20 @@
1.255  apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq)
1.256 -by (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
1.257 +apply (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
1.258 +done
1.259
1.261 -   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.262 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.263    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.264  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
1.265    case (2 a b c' n' p' n0 n1)
1.267 -  thus ?case using prems by (cases n', auto)
1.268 +  thus ?case using 2 by (cases n') auto
1.269  next
1.270    case (3 c n p a' b' n0 n1)
1.272 -  thus ?case using prems by (cases n, auto)
1.273 +  thus ?case using 3 by (cases n) auto
1.274  next
1.275    case (4 c n p c' n' p' n0 n1)
1.276    hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"
1.277 @@ -1215,15 +1221,14 @@
1.278    have "n < n' \<or> n' < n \<or> n = n'" by arith
1.279    moreover
1.280    {assume nn': "n < n'" hence ?case
1.281 -      thm prems
1.282 -      using norm
1.283 -    prems(6)[rule_format, OF nn' norm(1,6)]
1.284 -    prems(7)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all)}
1.285 +    using norm
1.286 +    4(5)[rule_format, OF nn' norm(1,6)]
1.287 +    4(6)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all) }
1.288    moreover {assume nn': "n'< n"
1.289      hence stupid: "n' < n \<and> \<not> n < n'" by simp
1.290 -    hence ?case using norm prems(4) [rule_format, OF stupid norm(5,3)]
1.291 -      prems(5)[rule_format, OF stupid norm(5,4)]
1.292 -      by (simp,cases n',simp,cases n,auto)}
1.293 +    hence ?case using norm 4(3) [rule_format, OF stupid norm(5,3)]
1.294 +      4(4)[rule_format, OF stupid norm(5,4)]
1.295 +      by (simp,cases n',simp,cases n,auto) }
1.296    moreover {assume nn': "n' = n"
1.297      hence stupid: "\<not> n' < n \<and> \<not> n < n'" by simp
1.298      from nn' polymul_normh[OF norm(5,4)]
1.299 @@ -1247,8 +1252,8 @@
1.300      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.301      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.303 -    have ?case   using norm prems(2)[rule_format, OF stupid norm(5,3)]
1.304 -        prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
1.305 +    have ?case using norm 4(1)[rule_format, OF stupid norm(5,3)]
1.306 +        4(2)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
1.307      ultimately have ?case by (cases n) auto}
1.308    ultimately show ?case by blast
1.309  qed simp_all
1.310 @@ -1603,12 +1608,13 @@
1.311
1.312  definition "swapnorm n m t = polynate (swap n m t)"
1.313
1.314 -lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs"
1.315 +lemma swapnorm:
1.316 +  assumes nbs: "n < length bs" and mbs: "m < length bs"
1.317    shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field_char_0, field_inverse_zero})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
1.318 -  using swap[OF prems] swapnorm_def by simp
1.319 +  using swap[OF assms] swapnorm_def by simp
1.320
1.321  lemma swapnorm_isnpoly[simp]:
1.322 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.323 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.324    shows "isnpoly (swapnorm n m p)"
1.325    unfolding swapnorm_def by simp
1.326
1.327 @@ -1625,9 +1631,9 @@
1.328    "isweaknpoly p = False"
1.329
1.330  lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p"
1.331 -  by (induct p arbitrary: n0, auto)
1.332 +  by (induct p arbitrary: n0) auto
1.333
1.334  lemma swap_isweanpoly: "isweaknpoly p \<Longrightarrow> isweaknpoly (swap n m p)"
1.335 -  by (induct p, auto)
1.336 +  by (induct p) auto
1.337
1.338  end
1.339 \ No newline at end of file
```