strengthened polymul.induct
authorkrauss
Mon Feb 21 23:14:36 2011 +0100 (2011-02-21)
changeset 418117e338ccabff0
parent 41810 588c95c4b53e
child 41812 d46c2908a838
strengthened polymul.induct
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
     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 @@ -150,6 +150,7 @@
     1.4    then CN (polymul(CN c n p,c')) n' (polymul(CN c n p,p'))
     1.5    else polyadd(polymul(CN c n p, c'),CN 0\<^sub>p n' (polymul(CN c n p, p'))))"
     1.6    "polymul (a,b) = Mul a b"
     1.7 +(hints recdef_cong del: if_cong)
     1.8  
     1.9  fun polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
    1.10  where
    1.11 @@ -400,73 +401,56 @@
    1.12    case (2 a b c' n' p') 
    1.13    let ?c = "(a,b)"
    1.14    { case (1 n0 n1) 
    1.15 -    hence n: "isnpolyh (C ?c) n'" "isnpolyh c' (Suc n')" "isnpolyh p' n'" "isnormNum ?c" 
    1.16 -      "isnpolyh (CN c' n' p') n1"
    1.17 -      by simp_all
    1.18 -    {assume "?c = 0\<^sub>N" hence ?case by auto}
    1.19 -      moreover {assume cnz: "?c \<noteq> 0\<^sub>N" 
    1.20 -        from "2.hyps"(1)[rule_format,where xb="n'",  OF cnz n(1) n(3)] 
    1.21 -          "2.hyps"(2)[rule_format, where x="Suc n'" 
    1.22 -          and xa="Suc n'" and xb = "n'", OF cnz ] cnz n have ?case
    1.23 -          by (auto simp add: min_def)}
    1.24 -      ultimately show ?case by blast
    1.25 +    with "2.hyps"(1-3)[of n' n' n']
    1.26 +      and "2.hyps"(4-6)[of "Suc n'" "Suc n'" n']
    1.27 +    show ?case by (auto simp add: min_def)
    1.28    next
    1.29      case (2 n0 n1) thus ?case by auto 
    1.30    next
    1.31      case (3 n0 n1) thus ?case  using "2.hyps" by auto } 
    1.32  next
    1.33 -  case (3 c n p a b){
    1.34 -    let ?c' = "(a,b)"
    1.35 -    case (1 n0 n1) 
    1.36 -    hence n: "isnpolyh (C ?c') n" "isnpolyh c (Suc n)" "isnpolyh p n" "isnormNum ?c'" 
    1.37 -      "isnpolyh (CN c n p) n0"
    1.38 -      by simp_all
    1.39 -    {assume "?c' = 0\<^sub>N" hence ?case by auto}
    1.40 -      moreover {assume cnz: "?c' \<noteq> 0\<^sub>N"
    1.41 -        from "3.hyps"(1)[rule_format,where xb="n",  OF cnz n(3) n(1)] 
    1.42 -          "3.hyps"(2)[rule_format, where x="Suc n" 
    1.43 -          and xa="Suc n" and xb = "n", OF cnz ] cnz n have ?case
    1.44 -          by (auto simp add: min_def)}
    1.45 -      ultimately show ?case by blast
    1.46 +  case (3 c n p a b)
    1.47 +  let ?c' = "(a,b)"
    1.48 +  { case (1 n0 n1) 
    1.49 +    with "3.hyps"(1-3)[of n n n]
    1.50 +      "3.hyps"(4-6)[of "Suc n" "Suc n" n]
    1.51 +    show ?case by (auto simp add: min_def)
    1.52    next
    1.53 -    case (2 n0 n1) thus ?case apply auto done
    1.54 +    case (2 n0 n1) thus ?case by auto
    1.55    next
    1.56      case (3 n0 n1) thus ?case  using "3.hyps" by auto } 
    1.57  next
    1.58    case (4 c n p c' n' p')
    1.59    let ?cnp = "CN c n p" let ?cnp' = "CN c' n' p'"
    1.60 -    {fix n0 n1
    1.61 -      assume "isnpolyh ?cnp n0" and "isnpolyh ?cnp' n1"
    1.62 +    {
    1.63 +      case (1 n0 n1)
    1.64        hence cnp: "isnpolyh ?cnp n" and cnp': "isnpolyh ?cnp' n'"
    1.65          and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)" 
    1.66          and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')"
    1.67          and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1"
    1.68          by simp_all
    1.69 -      have "n < n' \<or> n' < n \<or> n' = n" by auto
    1.70 -      moreover
    1.71 -      {assume nn': "n < n'"
    1.72 -        with "4.hyps"(5)[rule_format, OF nn' np cnp', where xb ="n"] 
    1.73 -          "4.hyps"(6)[rule_format, OF nn' nc cnp', where xb="n"] nn' nn0 nn1 cnp
    1.74 -        have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
    1.75 -          by (simp add: min_def) }
    1.76 -      moreover
    1.77 -
    1.78 -      {assume nn': "n > n'" hence stupid: "n' < n \<and> \<not> n < n'" by arith
    1.79 -        with "4.hyps"(3)[rule_format, OF stupid cnp np', where xb="n'"]
    1.80 -          "4.hyps"(4)[rule_format, OF stupid cnp nc', where xb="Suc n'"] 
    1.81 -          nn' nn0 nn1 cnp'
    1.82 -        have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
    1.83 -          by (cases "Suc n' = n", simp_all add: min_def)}
    1.84 -      moreover
    1.85 -      {assume nn': "n' = n" hence stupid: "\<not> n' < n \<and> \<not> n < n'" by arith
    1.86 -        from "4.hyps"(1)[rule_format, OF stupid cnp np', where xb="n"]
    1.87 -          "4.hyps"(2)[rule_format, OF stupid cnp nc', where xb="n"] nn' cnp cnp' nn1
    1.88 -        
    1.89 -        have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
    1.90 -          by simp (rule polyadd_normh,simp_all add: min_def isnpolyh_mono[OF nn0]) }
    1.91 -      ultimately show "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)" by blast }
    1.92 -    note th = this
    1.93 -    {fix n0 n1 m
    1.94 +      { assume "n < n'"
    1.95 +        with "4.hyps"(13-14)[OF np cnp', of n]
    1.96 +          "4.hyps"(16)[OF nc cnp', of n] nn0 cnp
    1.97 +        have ?case by (simp add: min_def)
    1.98 +      } moreover {
    1.99 +        assume "n' < n"
   1.100 +        with "4.hyps"(1-2)[OF cnp np', of "n'"]
   1.101 +          "4.hyps"(4)[OF cnp nc', of "Suc n'"] nn1 cnp'
   1.102 +        have ?case
   1.103 +          by (cases "Suc n' = n", simp_all add: min_def)
   1.104 +      } moreover {
   1.105 +        assume "n' = n"
   1.106 +        with "4.hyps"(1-2)[OF cnp np', of n]
   1.107 +          "4.hyps"(4)[OF cnp nc', of n] cnp cnp' nn1 nn0
   1.108 +        have ?case
   1.109 +          apply (auto intro!: polyadd_normh)
   1.110 +          apply (simp_all add: min_def isnpolyh_mono[OF nn0])
   1.111 +          done
   1.112 +      }
   1.113 +      ultimately show ?case by arith
   1.114 +    next
   1.115 +      fix n0 n1 m
   1.116        assume np: "isnpolyh ?cnp n0" and np':"isnpolyh ?cnp' n1"
   1.117        and m: "m \<le> min n0 n1"
   1.118        let ?d = "degreen (?cnp *\<^sub>p ?cnp') m"
   1.119 @@ -476,22 +460,20 @@
   1.120        have "n'<n \<or> n < n' \<or> n' = n" by auto
   1.121        moreover 
   1.122        {assume "n' < n \<or> n < n'"
   1.123 -        with "4.hyps" np np' m 
   1.124 -        have ?eq apply (cases "n' < n", simp_all)
   1.125 -        apply (erule allE[where x="n"],erule allE[where x="n"],auto) 
   1.126 -        done }
   1.127 +        with "4.hyps"(3,15,18) np np' m 
   1.128 +        have ?eq by auto }
   1.129        moreover
   1.130 -      {assume nn': "n' = n"  hence nn:"\<not> n' < n \<and> \<not> n < n'" by arith
   1.131 -        from "4.hyps"(1)[rule_format, OF nn, where x="n" and xa ="n'" and xb="n"]
   1.132 -          "4.hyps"(2)[rule_format, OF nn, where x="n" and xa ="Suc n'" and xb="n"] 
   1.133 +      {assume nn': "n' = n" hence nn:"\<not> n' < n \<and> \<not> n < n'" by arith
   1.134 +        from "4.hyps"(1,3)[of n n' n]
   1.135 +          "4.hyps"(4,5)[of n "Suc n'" n]
   1.136            np np' nn'
   1.137          have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
   1.138            "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   1.139            "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
   1.140            "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
   1.141          {assume mn: "m = n" 
   1.142 -          from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
   1.143 -            "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] norm nn' mn
   1.144 +          from "4.hyps"(2,3)[OF norm(1,4), of n]
   1.145 +            "4.hyps"(4,6)[OF norm(1,2), of n] norm nn' mn
   1.146            have degs:  "degreen (?cnp *\<^sub>p c') n = 
   1.147              (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"
   1.148              "degreen (?cnp *\<^sub>p p') n = ?d1  + degreen p' n" by (simp_all add: min_def)
   1.149 @@ -502,8 +484,8 @@
   1.150            have nmin: "n \<le> min n n" by (simp add: min_def)
   1.151            from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
   1.152            have deg: "degreen (CN c n p *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n = degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp 
   1.153 -          from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
   1.154 -            "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"]
   1.155 +          from "4.hyps"(1-3)[OF norm(1,4), of n]
   1.156 +            "4.hyps"(4-6)[OF norm(1,2), of n]
   1.157              mn norm m nn' deg
   1.158            have ?eq by simp}
   1.159          moreover
   1.160 @@ -511,28 +493,19 @@
   1.161            from nn' m np have max1: "m \<le> max n n"  by simp 
   1.162            hence min1: "m \<le> min n n" by simp     
   1.163            hence min2: "m \<le> min n (Suc n)" by simp
   1.164 -          {assume "c' = 0\<^sub>p"
   1.165 -            from `c' = 0\<^sub>p` have ?eq
   1.166 -              using "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
   1.167 -            "4.hyps"(2)[rule_format, OF nn norm(1,2) min2] mn nn'
   1.168 -              apply simp
   1.169 -              done}
   1.170 -          moreover
   1.171 -          {assume cnz: "c' \<noteq> 0\<^sub>p"
   1.172 -            from "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
   1.173 -              "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
   1.174 -              degreen_polyadd[OF norm(3,6) max1]
   1.175 +          from "4.hyps"(1-3)[OF norm(1,4) min1]
   1.176 +            "4.hyps"(4-6)[OF norm(1,2) min2]
   1.177 +            degreen_polyadd[OF norm(3,6) max1]
   1.178  
   1.179 -            have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m 
   1.180 -              \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
   1.181 -              using mn nn' cnz np np' by simp
   1.182 -            with "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
   1.183 -              "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
   1.184 -              degreen_0[OF norm(3) mn'] have ?eq using nn' mn cnz np np' by clarsimp}
   1.185 -          ultimately have ?eq by blast }
   1.186 +          have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m 
   1.187 +            \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
   1.188 +            using mn nn' np np' by simp
   1.189 +          with "4.hyps"(1-3)[OF norm(1,4) min1]
   1.190 +            "4.hyps"(4-6)[OF norm(1,2) min2]
   1.191 +            degreen_0[OF norm(3) mn']
   1.192 +          have ?eq using nn' mn np np' by clarsimp}
   1.193          ultimately have ?eq by blast}
   1.194        ultimately show ?eq by blast}
   1.195 -    note degth = this
   1.196      { case (2 n0 n1)
   1.197        hence np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1" 
   1.198          and m: "m \<le> min n0 n1" by simp_all
   1.199 @@ -540,8 +513,8 @@
   1.200        let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
   1.201        {assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
   1.202          hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp
   1.203 -        from "4.hyps"(1) [rule_format, OF nn, where x="n" and xa = "n" and xb="n"] 
   1.204 -          "4.hyps"(2) [rule_format, OF nn, where x="n" and xa = "Suc n" and xb="n"] 
   1.205 +        from "4.hyps"(1-3) [of n n n]
   1.206 +          "4.hyps"(4-6)[of n "Suc n" n]
   1.207            np np' C(2) mn
   1.208          have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
   1.209            "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   1.210 @@ -878,8 +851,7 @@
   1.211    done
   1.212  
   1.213  lemma wf_bs_polyul: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p *\<^sub>p q)"
   1.214 -
   1.215 - unfolding wf_bs_def 
   1.216 +  unfolding wf_bs_def 
   1.217    apply (induct p q arbitrary: bs rule: polymul.induct) 
   1.218    apply (simp_all add: wf_bs_polyadd)
   1.219    apply clarsimp
   1.220 @@ -1220,17 +1192,14 @@
   1.221    have "n < n' \<or> n' < n \<or> n = n'" by arith
   1.222    moreover 
   1.223    {assume nn': "n < n'" hence ?case 
   1.224 -      thm prems
   1.225        using norm 
   1.226 -    prems(6)[rule_format, OF nn' norm(1,6)]
   1.227 -    prems(7)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all)}
   1.228 +    "4.hyps"(5)[OF norm(1,6)]
   1.229 +    "4.hyps"(6)[OF norm(2,6)] by (simp, cases n, simp,cases n', simp_all)}
   1.230    moreover {assume nn': "n'< n"
   1.231 -    hence stupid: "n' < n \<and> \<not> n < n'" by simp
   1.232 -    hence ?case using norm prems(4) [rule_format, OF stupid norm(5,3)]
   1.233 -      prems(5)[rule_format, OF stupid norm(5,4)] 
   1.234 +    hence ?case using norm "4.hyps"(1) [OF norm(5,3)]
   1.235 +      "4.hyps"(2)[OF norm(5,4)] 
   1.236        by (simp,cases n',simp,cases n,auto)}
   1.237    moreover {assume nn': "n' = n"
   1.238 -    hence stupid: "\<not> n' < n \<and> \<not> n < n'" by simp
   1.239      from nn' polymul_normh[OF norm(5,4)] 
   1.240      have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def)
   1.241      from nn' polymul_normh[OF norm(5,3)] norm 
   1.242 @@ -1252,8 +1221,8 @@
   1.243      have dth:"degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp
   1.244      hence dth':"degree (CN c 0 p *\<^sub>p c') \<noteq> degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp
   1.245      from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth
   1.246 -    have ?case   using norm prems(2)[rule_format, OF stupid norm(5,3)]
   1.247 -        prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
   1.248 +    have ?case   using norm "4.hyps"(1)[OF norm(5,3)]
   1.249 +        "4.hyps"(2)[OF norm(5,4)] nn' nz by simp }
   1.250      ultimately have ?case by (cases n) auto} 
   1.251    ultimately show ?case by blast
   1.252  qed simp_all