tuned proofs;
authorwenzelm
Tue Mar 18 10:00:23 2014 +0100 (2014-03-18)
changeset 5619821dd034523e5
parent 56197 416f7a00e4cb
child 56199 8e8d28ed7529
tuned proofs;
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Mar 17 23:16:26 2014 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Mar 18 10:00:23 2014 +0100
     1.3 @@ -1481,7 +1481,8 @@
     1.4  lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p"
     1.5  proof (induct k arbitrary: n0 p)
     1.6    case 0
     1.7 -  then show ?case by auto
     1.8 +  then show ?case
     1.9 +    by auto
    1.10  next
    1.11    case (Suc k n0 p)
    1.12    then have "isnpolyh (shift1 p) 0"
    1.13 @@ -1522,7 +1523,6 @@
    1.14    shows "head (p +\<^sub>p q) = (if degree p < degree q then head q else head p)"
    1.15    using np nq deg
    1.16    apply (induct p q arbitrary: n0 n1 rule: polyadd.induct)
    1.17 -  using np
    1.18    apply simp_all
    1.19    apply (case_tac n', simp, simp)
    1.20    apply (case_tac n, simp, simp)
    1.21 @@ -1657,8 +1657,9 @@
    1.22      and np: "isnpolyh p n0"
    1.23      and ns: "isnpolyh s n1"
    1.24      and ap: "head p = a"
    1.25 -    and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
    1.26 -  shows "polydivide_aux a n p k s = (k',r) \<longrightarrow> k' \<ge> k \<and> (degree r = 0 \<or> degree r < degree p) \<and>
    1.27 +    and ndp: "degree p = n"
    1.28 +    and pnz: "p \<noteq> 0\<^sub>p"
    1.29 +  shows "polydivide_aux a n p k s = (k', r) \<longrightarrow> k' \<ge> k \<and> (degree r = 0 \<or> degree r < degree p) \<and>
    1.30      (\<exists>nr. isnpolyh r nr) \<and> (\<exists>q n1. isnpolyh q n1 \<and> (polypow (k' - k) a) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
    1.31    using ns
    1.32  proof (induct "degree s" arbitrary: s k k' r n1 rule: less_induct)
    1.33 @@ -1979,13 +1980,13 @@
    1.34  definition "isnonconstant p \<longleftrightarrow> \<not> isconstant p"
    1.35  
    1.36  lemma isnonconstant_pnormal_iff:
    1.37 -  assumes nc: "isnonconstant p"
    1.38 +  assumes "isnonconstant p"
    1.39    shows "pnormal (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0"
    1.40  proof
    1.41    let ?p = "polypoly bs p"
    1.42    assume H: "pnormal ?p"
    1.43    have csz: "coefficients p \<noteq> []"
    1.44 -    using nc by (cases p) auto
    1.45 +    using assms by (cases p) auto
    1.46    from coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] pnormal_last_nonzero[OF H]
    1.47    show "Ipoly bs (head p) \<noteq> 0"
    1.48      by (simp add: polypoly_def)
    1.49 @@ -1993,7 +1994,7 @@
    1.50    assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
    1.51    let ?p = "polypoly bs p"
    1.52    have csz: "coefficients p \<noteq> []"
    1.53 -    using nc by (cases p) auto
    1.54 +    using assms by (cases p) auto
    1.55    then have pz: "?p \<noteq> []"
    1.56      by (simp add: polypoly_def)
    1.57    then have lg: "length ?p > 0"
    1.58 @@ -2013,18 +2014,18 @@
    1.59    done
    1.60  
    1.61  lemma isnonconstant_nonconstant:
    1.62 -  assumes inc: "isnonconstant p"
    1.63 +  assumes "isnonconstant p"
    1.64    shows "nonconstant (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0"
    1.65  proof
    1.66    let ?p = "polypoly bs p"
    1.67    assume nc: "nonconstant ?p"
    1.68 -  from isnonconstant_pnormal_iff[OF inc, of bs] nc
    1.69 +  from isnonconstant_pnormal_iff[OF assms, of bs] nc
    1.70    show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
    1.71      unfolding nonconstant_def by blast
    1.72  next
    1.73    let ?p = "polypoly bs p"
    1.74    assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
    1.75 -  from isnonconstant_pnormal_iff[OF inc, of bs] h
    1.76 +  from isnonconstant_pnormal_iff[OF assms, of bs] h
    1.77    have pn: "pnormal ?p"
    1.78      by blast
    1.79    {
    1.80 @@ -2032,8 +2033,8 @@
    1.81      assume H: "?p = [x]"
    1.82      from H have "length (coefficients p) = 1"
    1.83        unfolding polypoly_def by auto
    1.84 -    with isnonconstant_coefficients_length[OF inc]
    1.85 -      have False by arith
    1.86 +    with isnonconstant_coefficients_length[OF assms]
    1.87 +    have False by arith
    1.88    }
    1.89    then show "nonconstant ?p"
    1.90      using pn unfolding nonconstant_def by blast
    1.91 @@ -2077,7 +2078,7 @@
    1.92  primrec swap :: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly"
    1.93  where
    1.94    "swap n m (C x) = C x"
    1.95 -| "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
    1.96 +| "swap n m (Bound k) = Bound (if k = n then m else if k = m then n else k)"
    1.97  | "swap n m (Neg t) = Neg (swap n m t)"
    1.98  | "swap n m (Add s t) = Add (swap n m s) (swap n m t)"
    1.99  | "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"