summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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})"