src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 changeset 41811 7e338ccabff0 parent 41810 588c95c4b53e child 41812 d46c2908a838
```     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
```