src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 41815 9a0cacbcd825
parent 41814 3848eb635eab
child 41816 7a55699805dc
     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 @@ -258,26 +258,26 @@
     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 ab c' n' p' n0 n1)
     1.7 -  from prems have  th1: "isnpolyh (C ab) (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 ab) (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 ab +\<^sub>p c') (Suc n')" by simp
    1.13 +  with 2(1)[OF th1 th2] have th3:"isnpolyh (C ab +\<^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' ab n1 n0)
    1.19 -  from prems have  th1: "isnpolyh (C ab) (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 ab) (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 ab) (Suc n')" by simp
    1.25 +  with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C ab) (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 "4.hyps"(3)[OF nc nc'] 
    1.41 @@ -286,25 +286,25 @@
    1.42        using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto
    1.43      from eq "4.hyps"(4)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
    1.44      have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp
    1.45 -    from minle npp' ncc'n01 prems ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}
    1.46 +    from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}
    1.47    moreover {assume lt: "n < n'"
    1.48      have "min n0 n1 \<le> n0" by simp
    1.49 -    with prems have th1:"min n0 n1 \<le> n" by auto 
    1.50 -    from prems have th21: "isnpolyh c (Suc n)" by simp
    1.51 -    from prems have th22: "isnpolyh (CN c' n' p') n'" by simp
    1.52 +    with 4 lt have th1:"min n0 n1 \<le> n" by auto 
    1.53 +    from 4 have th21: "isnpolyh c (Suc n)" by simp
    1.54 +    from 4 have th22: "isnpolyh (CN c' n' p') n'" by simp
    1.55      from lt have th23: "min (Suc n) n' = Suc n" by arith
    1.56      from "4.hyps"(1)[OF th21 th22]
    1.57      have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)" using th23 by simp
    1.58 -    with prems th1 have ?case by simp } 
    1.59 +    with 4 lt th1 have ?case by simp } 
    1.60    moreover {assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp
    1.61      have "min n0 n1 \<le> n1"  by simp
    1.62 -    with prems have th1:"min n0 n1 \<le> n'" by auto
    1.63 -    from prems have th21: "isnpolyh c' (Suc n')" by simp_all
    1.64 -    from prems have th22: "isnpolyh (CN c n p) n" by simp
    1.65 +    with 4 gt have th1:"min n0 n1 \<le> n'" by auto
    1.66 +    from 4 have th21: "isnpolyh c' (Suc n')" by simp_all
    1.67 +    from 4 have th22: "isnpolyh (CN c n p) n" by simp
    1.68      from gt have th23: "min n (Suc n') = Suc n'" by arith
    1.69      from "4.hyps"(2)[OF th22 th21]
    1.70      have "isnpolyh (polyadd (CN c n p) c') (Suc n')" using th23 by simp
    1.71 -    with prems th1 have ?case by simp}
    1.72 +    with 4 gt th1 have ?case by simp}
    1.73        ultimately show ?case by blast
    1.74  qed auto
    1.75  
    1.76 @@ -375,11 +375,11 @@
    1.77    \<Longrightarrow> degreen p m = degreen q m"
    1.78  proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
    1.79    case (4 c n p c' n' p' m n0 n1 x) 
    1.80 -  {assume nn': "n' < n" hence ?case using prems by simp}
    1.81 +  {assume nn': "n' < n" hence ?case using 4 by simp}
    1.82    moreover 
    1.83    {assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith
    1.84 -    moreover {assume "n < n'" with prems have ?case by simp }
    1.85 -    moreover {assume eq: "n = n'" hence ?case using prems 
    1.86 +    moreover {assume "n < n'" with 4 have ?case by simp }
    1.87 +    moreover {assume eq: "n = n'" hence ?case using 4 
    1.88          apply (cases "p +\<^sub>p p' = 0\<^sub>p")
    1.89          apply (auto simp add: Let_def)
    1.90          by blast
    1.91 @@ -645,7 +645,7 @@
    1.92    case (2 k n)
    1.93    let ?q = "polypow (Suc k div 2) p"
    1.94    let ?d = "polymul ?q ?q"
    1.95 -  from prems have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+
    1.96 +  from 2 have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+
    1.97    from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp
    1.98    from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n" by simp
    1.99    from dn on show ?case by (simp add: Let_def)
   1.100 @@ -706,7 +706,7 @@
   1.101    using np
   1.102  proof (induct p arbitrary: n rule: behead.induct)
   1.103    case (1 c p n) hence pn: "isnpolyh p n" by simp
   1.104 -  from prems(2)[OF pn] 
   1.105 +  from 1(1)[OF pn] 
   1.106    have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . 
   1.107    then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
   1.108      by (simp_all add: th[symmetric] field_simps power_Suc)
   1.109 @@ -722,7 +722,7 @@
   1.110    case (goal1 c n p n')
   1.111    hence "n = Suc (n - 1)" by simp
   1.112    hence "isnpolyh p (Suc (n - 1))"  using `isnpolyh p n` by simp
   1.113 -  with prems(2) show ?case by simp
   1.114 +  with goal1(2) show ?case by simp
   1.115  qed
   1.116  
   1.117  lemma isconstant_polybound0: "isnpolyh p n0 \<Longrightarrow> isconstant p \<longleftrightarrow> polybound0 p"
   1.118 @@ -1074,16 +1074,16 @@
   1.119    case (1 c c') thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def]) 
   1.120  next
   1.121    case (2 c c' n' p') 
   1.122 -  from prems have "degree (C c) = degree (CN c' n' p')" by simp
   1.123 +  from 2 have "degree (C c) = degree (CN c' n' p')" by simp
   1.124    hence nz:"n' > 0" by (cases n', auto)
   1.125    hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
   1.126 -  with prems show ?case by simp
   1.127 +  with 2 show ?case by simp
   1.128  next
   1.129    case (3 c n p c') 
   1.130 -  from prems have "degree (C c') = degree (CN c n p)" by simp
   1.131 +  hence "degree (C c') = degree (CN c n p)" by simp
   1.132    hence nz:"n > 0" by (cases n, auto)
   1.133    hence "head (CN c n p) = CN c n p" by (cases n, auto)
   1.134 -  with prems show ?case by simp
   1.135 +  with 3 show ?case by simp
   1.136  next
   1.137    case (4 c n p c' n' p')
   1.138    hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1" 
   1.139 @@ -1098,22 +1098,22 @@
   1.140    moreover
   1.141    {assume nn': "n = n'"
   1.142      have "n = 0 \<or> n >0" by arith
   1.143 -    moreover {assume nz: "n = 0" hence ?case using prems by (auto simp add: Let_def degcmc')}
   1.144 +    moreover {assume nz: "n = 0" hence ?case using 4 nn' by (auto simp add: Let_def degcmc')}
   1.145      moreover {assume nz: "n > 0"
   1.146        with nn' H(3) have  cc':"c = c'" and pp': "p = p'" by (cases n, auto)+
   1.147 -      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.148 +      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] using nn' 4 by (simp add: Let_def)}
   1.149      ultimately have ?case by blast}
   1.150    moreover
   1.151    {assume nn': "n < n'" hence n'p: "n' > 0" by simp 
   1.152      hence headcnp':"head (CN c' n' p') = CN c' n' p'"  by (cases n', simp_all)
   1.153 -    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.154 +    have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" using 4 nn' by (cases n', simp_all)
   1.155      hence "n > 0" by (cases n, simp_all)
   1.156      hence headcnp: "head (CN c n p) = CN c n p" by (cases n, auto)
   1.157      from H(3) headcnp headcnp' nn' have ?case by auto}
   1.158    moreover
   1.159    {assume nn': "n > n'"  hence np: "n > 0" by simp 
   1.160      hence headcnp:"head (CN c n p) = CN c n p"  by (cases n, simp_all)
   1.161 -    from prems have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp
   1.162 +    from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp
   1.163      from np have degcnp: "degree (CN c n p) = 0" by (cases n, simp_all)
   1.164      with degcnpeq have "n' > 0" by (cases n', simp_all)
   1.165      hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
   1.166 @@ -1127,7 +1127,7 @@
   1.167  lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p"
   1.168  proof(induct k arbitrary: n0 p)
   1.169    case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
   1.170 -  with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
   1.171 +  with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
   1.172      and "head (shift1 p) = head p" by (simp_all add: shift1_head) 
   1.173    thus ?case by (simp add: funpow_swap1)
   1.174  qed auto  
   1.175 @@ -1174,11 +1174,11 @@
   1.176  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
   1.177    case (2 c c' n' p' n0 n1)
   1.178    hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum c"  by (simp_all add: head_isnpolyh)
   1.179 -  thus ?case using prems by (cases n', auto) 
   1.180 +  thus ?case using 2 by (cases n', auto) 
   1.181  next 
   1.182    case (3 c n p c' n0 n1) 
   1.183    hence "isnpolyh (head (CN c n p)) n0" "isnormNum c'"  by (simp_all add: head_isnpolyh)
   1.184 -  thus ?case using prems by (cases n, auto)
   1.185 +  thus ?case using 3 by (cases n, auto)
   1.186  next
   1.187    case (4 c n p c' n' p' n0 n1)
   1.188    hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"
   1.189 @@ -1574,7 +1574,7 @@
   1.190  
   1.191  lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs"
   1.192    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.193 -  using swap[OF prems] swapnorm_def by simp
   1.194 +  using swap[OF assms] swapnorm_def by simp
   1.195  
   1.196  lemma swapnorm_isnpoly[simp]: 
   1.197      assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"