src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 41763 8ce56536fda7
parent 41413 64cd30d6b0b8
child 41807 ab5d2d81f9fb
child 41808 9f436d00248f
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 14 12:25:26 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 14 15:27:23 2011 +0100
     1.3 @@ -131,19 +131,7 @@
     1.4                 pp' = polyadd (p,p')
     1.5             in (if pp' = 0\<^sub>p then cc' else CN cc' n pp')))"
     1.6    "polyadd (a, b) = Add a b"
     1.7 -(hints recdef_simp add: Let_def measure_def split_def inv_image_def)
     1.8 -
     1.9 -(*
    1.10 -declare stupid [simp del, code del]
    1.11 -
    1.12 -lemma [simp,code]: "polyadd (CN c n p, CN c' n' p') = 
    1.13 -    (if n < n' then CN (polyadd(c,CN c' n' p')) n p
    1.14 -     else if n'<n then CN (polyadd(CN c n p, c')) n' p'
    1.15 -     else (let cc' = polyadd (c,c') ; 
    1.16 -               pp' = polyadd (p,p')
    1.17 -           in (if pp' = 0\<^sub>p then cc' else CN cc' n pp')))"
    1.18 -  by (simp add: Let_def stupid)
    1.19 -*)
    1.20 +(hints recdef_simp add: Let_def measure_def split_def inv_image_def recdef_cong del: if_cong)
    1.21  
    1.22  recdef polyneg "measure size"
    1.23    "polyneg (C c) = C (~\<^sub>N c)"
    1.24 @@ -286,12 +274,12 @@
    1.25    from prems have ngen0: "n \<ge> n0" by simp
    1.26    from prems have n'gen1: "n' \<ge> n1" by simp 
    1.27    have "n < n' \<or> n' < n \<or> n = n'" by auto
    1.28 -  moreover {assume eq: "n = n'" hence eq': "\<not> n' < n \<and> \<not> n < n'" by simp
    1.29 -    with prems(2)[rule_format, OF eq' nc nc'] 
    1.30 +  moreover {assume eq: "n = n'"
    1.31 +    with prems(2)[OF nc nc'] 
    1.32      have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto
    1.33      hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)"
    1.34        using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto
    1.35 -    from eq prems(1)[rule_format, OF eq' np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
    1.36 +    from eq prems(1)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
    1.37      have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp
    1.38      from minle npp' ncc'n01 prems ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}
    1.39    moreover {assume lt: "n < n'"
    1.40 @@ -300,7 +288,7 @@
    1.41      from prems have th21: "isnpolyh c (Suc n)" by simp
    1.42      from prems have th22: "isnpolyh (CN c' n' p') n'" by simp
    1.43      from lt have th23: "min (Suc n) n' = Suc n" by arith
    1.44 -    from prems(4)[rule_format, OF lt th21 th22]
    1.45 +    from prems(4)[OF th21 th22]
    1.46      have "isnpolyh (polyadd (c, CN c' n' p')) (Suc n)" using th23 by simp
    1.47      with prems th1 have ?case by simp } 
    1.48    moreover {assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp
    1.49 @@ -309,7 +297,7 @@
    1.50      from prems have th21: "isnpolyh c' (Suc n')" by simp_all
    1.51      from prems have th22: "isnpolyh (CN c n p) n" by simp
    1.52      from gt have th23: "min n (Suc n') = Suc n'" by arith
    1.53 -    from prems(3)[rule_format, OF  gt' th22 th21]
    1.54 +    from prems(3)[OF th22 th21]
    1.55      have "isnpolyh (polyadd (CN c n p,c')) (Suc n')" using th23 by simp
    1.56      with prems th1 have ?case by simp}
    1.57        ultimately show ?case by blast
    1.58 @@ -328,14 +316,20 @@
    1.59    degreen (polyadd(p,q)) m = max (degreen p m) (degreen q m)"
    1.60  proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct)
    1.61    case (4 c n p c' n' p' m n0 n1)
    1.62 -  thus ?case 
    1.63 -    apply (cases "n' < n", simp_all add: Let_def)
    1.64 -    apply (cases "n = n'", simp_all)
    1.65 -    apply (cases "n' = m", simp_all add: Let_def)
    1.66 -    by (erule allE[where x="m"], erule allE[where x="Suc m"], 
    1.67 -           erule allE[where x="m"], erule allE[where x="Suc m"], 
    1.68 -           clarsimp,erule allE[where x="m"],erule allE[where x="Suc m"], simp)
    1.69 -qed simp_all 
    1.70 +  have "n' = n \<or> n < n' \<or> n' < n" by arith
    1.71 +  thus ?case
    1.72 +  proof (elim disjE)
    1.73 +    assume [simp]: "n' = n"
    1.74 +    from 4(1)[of n n m] 4(2)[of "Suc n" "Suc n" m] 4(5-7)
    1.75 +    show ?thesis by (auto simp: Let_def)
    1.76 +  next
    1.77 +    assume "n < n'"
    1.78 +    with 4 show ?thesis by auto
    1.79 +  next
    1.80 +    assume "n' < n"
    1.81 +    with 4 show ?thesis by auto
    1.82 +  qed
    1.83 +qed auto
    1.84  
    1.85  lemma headnz[simp]: "\<lbrakk>isnpolyh p n ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> headn p m \<noteq> 0\<^sub>p"
    1.86    by (induct p arbitrary: n rule: headn.induct, auto)
    1.87 @@ -363,26 +357,28 @@
    1.88    case (3 c n p c' n0 n1) thus ?case by (cases n, auto)
    1.89  next
    1.90    case (4 c n p c' n' p' n0 n1 m) 
    1.91 -  thus ?case 
    1.92 -    apply (cases "n < n'", simp_all add: Let_def)
    1.93 -    apply (cases "n' < n", simp_all)
    1.94 -    apply (erule allE[where x="n"],erule allE[where x="Suc n"],clarify)
    1.95 -    apply (erule allE[where x="n'"],erule allE[where x="Suc n'"],clarify)
    1.96 -    by (erule allE[where x="m"],erule allE[where x="m"], auto)
    1.97 +  have "n' = n \<or> n < n' \<or> n' < n" by arith
    1.98 +  thus ?case
    1.99 +  proof (elim disjE)
   1.100 +    assume [simp]: "n' = n"
   1.101 +    from 4(1)[of n n m] 4(2)[of "Suc n" "Suc n" m] 4(5-7)
   1.102 +    show ?thesis by (auto simp: Let_def)
   1.103 +  qed simp_all
   1.104  qed auto
   1.105  
   1.106 -
   1.107  lemma polyadd_eq_const_degreen: "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\<rbrakk> 
   1.108    \<Longrightarrow> degreen p m = degreen q m"
   1.109  proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
   1.110    case (4 c n p c' n' p' m n0 n1 x) 
   1.111 -  hence z: "CN c n p +\<^sub>p CN c' n' p' = C x" by simp
   1.112    {assume nn': "n' < n" hence ?case using prems by simp}
   1.113    moreover 
   1.114    {assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith
   1.115      moreover {assume "n < n'" with prems have ?case by simp }
   1.116      moreover {assume eq: "n = n'" hence ?case using prems 
   1.117 -        by (cases "p +\<^sub>p p' = 0\<^sub>p", auto simp add: Let_def) }
   1.118 +        apply (cases "p +\<^sub>p p' = 0\<^sub>p")
   1.119 +        apply (auto simp add: Let_def)
   1.120 +        by blast
   1.121 +      }
   1.122      ultimately have ?case by blast}
   1.123    ultimately show ?case by blast
   1.124  qed simp_all
   1.125 @@ -632,23 +628,8 @@
   1.126    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.127    shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p -\<^sub>p q = 0\<^sub>p) = (p = q)"
   1.128    unfolding polysub_def split_def fst_conv snd_conv
   1.129 -  apply (induct p q arbitrary: n0 n1 rule:polyadd.induct, simp_all add: Nsub0[simplified Nsub_def])
   1.130 -  apply (clarsimp simp add: Let_def)
   1.131 -  apply (case_tac "n < n'", simp_all)
   1.132 -  apply (case_tac "n' < n", simp_all)
   1.133 -  apply (erule impE)+
   1.134 -  apply (rule_tac x="Suc n" in exI, simp)
   1.135 -  apply (rule_tac x="n" in exI, simp)
   1.136 -  apply (erule impE)+
   1.137 -  apply (rule_tac x="n" in exI, simp)
   1.138 -  apply (rule_tac x="Suc n" in exI, simp)
   1.139 -  apply (erule impE)+
   1.140 -  apply (rule_tac x="Suc n" in exI, simp)
   1.141 -  apply (rule_tac x="n" in exI, simp)
   1.142 -  apply (erule impE)+
   1.143 -  apply (rule_tac x="Suc n" in exI, simp)
   1.144 -  apply clarsimp
   1.145 -  done
   1.146 +  by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
   1.147 +  (auto simp: Nsub0[simplified Nsub_def] Let_def)
   1.148  
   1.149  text{* polypow is a power function and preserves normal forms *}
   1.150  
   1.151 @@ -1209,14 +1190,11 @@
   1.152  apply (case_tac n, simp, simp)
   1.153  apply (case_tac n, case_tac n', simp add: Let_def)
   1.154  apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p")
   1.155 -apply (clarsimp simp add: polyadd_eq_const_degree)
   1.156 -apply clarsimp
   1.157 -apply (erule_tac impE,blast)
   1.158 -apply (erule_tac impE,blast)
   1.159 -apply clarsimp
   1.160 -apply simp
   1.161 -apply (case_tac n', simp_all)
   1.162 -done
   1.163 +apply (auto simp add: polyadd_eq_const_degree)
   1.164 +apply (metis head_nz)
   1.165 +apply (metis head_nz)
   1.166 +apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq)
   1.167 +by (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
   1.168  
   1.169  lemma polymul_head_polyeq: 
   1.170     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"