author krauss Mon Feb 14 15:27:23 2011 +0100 (2011-02-14) changeset 41763 8ce56536fda7 parent 41762 00060198de12 child 41764 5268aef2fe83
strengthened induction rule;
clarified some proofs
```     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})"
```