author krauss Mon Feb 21 23:14:36 2011 +0100 (2011-02-21) changeset 41812 d46c2908a838 parent 41811 7e338ccabff0 child 41813 4eb43410d2fa
recdef -> fun; curried
```     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 @@ -105,30 +105,33 @@
1.4  | "headconst (C n) = n"
1.5
1.6  subsection{* Operations for normalization *}
1.7 +
1.8 +
1.9  consts
1.10 -  polyadd :: "poly\<times>poly \<Rightarrow> poly"
1.11    polysub :: "poly\<times>poly \<Rightarrow> poly"
1.12    polymul :: "poly\<times>poly \<Rightarrow> poly"
1.13
1.14 -abbreviation poly_add :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
1.15 -  where "a +\<^sub>p b \<equiv> polyadd (a,b)"
1.16  abbreviation poly_mul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
1.17    where "a *\<^sub>p b \<equiv> polymul (a,b)"
1.18  abbreviation poly_sub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
1.19    where "a -\<^sub>p b \<equiv> polysub (a,b)"
1.20
1.21 -recdef polyadd "measure (\<lambda> (a,b). polysize a + polysize b)"
1.22 -  "polyadd (C c, C c') = C (c+\<^sub>Nc')"
1.23 -  "polyadd (C c, CN c' n' p') = CN (polyadd (C c, c')) n' p'"
1.24 -  "polyadd (CN c n p, C c') = CN (polyadd (c, C c')) n p"
1.25 -  "polyadd (CN c n p, CN c' n' p') =
1.26 -    (if n < n' then CN (polyadd(c,CN c' n' p')) n p
1.27 -     else if n'<n then CN (polyadd(CN c n p, c')) n' p'
1.28 -     else (let cc' = polyadd (c,c') ;
1.29 -               pp' = polyadd (p,p')
1.30 +declare if_cong[fundef_cong del]
1.31 +declare let_cong[fundef_cong del]
1.32 +
1.33 +fun polyadd :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
1.34 +where
1.35 +  "polyadd (C c) (C c') = C (c+\<^sub>Nc')"
1.36 +|  "polyadd (C c) (CN c' n' p') = CN (polyadd (C c) c') n' p'"
1.37 +| "polyadd (CN c n p) (C c') = CN (polyadd c (C c')) n p"
1.38 +| "polyadd (CN c n p) (CN c' n' p') =
1.39 +    (if n < n' then CN (polyadd c (CN c' n' p')) n p
1.40 +     else if n'<n then CN (polyadd (CN c n p) c') n' p'
1.41 +     else (let cc' = polyadd c c' ;
1.42 +               pp' = polyadd p p'
1.43             in (if pp' = 0\<^sub>p then cc' else CN cc' n pp')))"
1.45 -(hints recdef_simp add: Let_def measure_def split_def inv_image_def recdef_cong del: if_cong)
1.47 +
1.48
1.49  fun polyneg :: "poly \<Rightarrow> poly" ("~\<^sub>p")
1.50  where
1.51 @@ -136,7 +139,7 @@
1.52  | "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)"
1.53  | "polyneg a = Neg a"
1.54
1.55 -defs polysub_def[code]: "polysub \<equiv> \<lambda> (p,q). polyadd (p,polyneg q)"
1.56 +defs polysub_def[code]: "polysub \<equiv> \<lambda> (p,q). polyadd p (polyneg q)"
1.57
1.58  recdef polymul "measure (\<lambda>(a,b). size a + size b)"
1.59    "polymul(C c, C c') = C (c*\<^sub>Nc')"
1.60 @@ -148,10 +151,13 @@
1.61    (if n<n' then CN (polymul(c,CN c' n' p')) n (polymul(p,CN c' n' p'))
1.62    else if n' < n
1.63    then CN (polymul(CN c n p,c')) n' (polymul(CN c n p,p'))
1.64 -  else polyadd(polymul(CN c n p, c'),CN 0\<^sub>p n' (polymul(CN c n p, p'))))"
1.65 +  else polyadd (polymul(CN c n p, c')) (CN 0\<^sub>p n' (polymul(CN c n p, p'))))"
1.66    "polymul (a,b) = Mul a b"
1.67  (hints recdef_cong del: if_cong)
1.68
1.69 +declare if_cong[fundef_cong]
1.70 +declare let_cong[fundef_cong]
1.71 +
1.72  fun polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
1.73  where
1.74    "polypow 0 = (\<lambda>p. 1\<^sub>p)"
1.75 @@ -256,21 +262,21 @@
1.76  text{* polyadd preserves normal forms *}
1.77
1.78  lemma polyadd_normh: "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk>
1.79 -      \<Longrightarrow> isnpolyh (polyadd(p,q)) (min n0 n1)"
1.80 +      \<Longrightarrow> isnpolyh (polyadd p q) (min n0 n1)"
1.81  proof(induct p q arbitrary: n0 n1 rule: polyadd.induct)
1.82 -  case (2 a b c' n' p' n0 n1)
1.83 -  from prems have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp
1.84 +  case (2 ab c' n' p' n0 n1)
1.85 +  from prems have  th1: "isnpolyh (C ab) (Suc n')" by simp
1.86    from prems(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
1.87    with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
1.88 -  with prems(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp
1.89 +  with prems(1)[OF th1 th2] have th3:"isnpolyh (C ab +\<^sub>p c') (Suc n')" by simp
1.90    from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp
1.91    thus ?case using prems th3 by simp
1.92  next
1.93 -  case (3 c' n' p' a b n1 n0)
1.94 -  from prems have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp
1.95 +  case (3 c' n' p' ab n1 n0)
1.96 +  from prems have  th1: "isnpolyh (C ab) (Suc n')" by simp
1.97    from prems(2) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
1.98    with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
1.99 -  with prems(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp
1.100 +  with prems(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C ab) (Suc n')" by simp
1.101    from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp
1.102    thus ?case using prems th3 by simp
1.103  next
1.104 @@ -281,11 +287,11 @@
1.105    from prems have n'gen1: "n' \<ge> n1" by simp
1.106    have "n < n' \<or> n' < n \<or> n = n'" by auto
1.107    moreover {assume eq: "n = n'"
1.108 -    with prems(2)[OF nc nc']
1.109 +    with "4.hyps"(3)[OF nc nc']
1.110      have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto
1.111      hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)"
1.112        using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto
1.113 -    from eq prems(1)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
1.114 +    from eq "4.hyps"(4)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
1.115      have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp
1.116      from minle npp' ncc'n01 prems ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}
1.117    moreover {assume lt: "n < n'"
1.118 @@ -294,8 +300,8 @@
1.119      from prems have th21: "isnpolyh c (Suc n)" by simp
1.120      from prems have th22: "isnpolyh (CN c' n' p') n'" by simp
1.121      from lt have th23: "min (Suc n) n' = Suc n" by arith
1.122 -    from prems(4)[OF th21 th22]
1.123 -    have "isnpolyh (polyadd (c, CN c' n' p')) (Suc n)" using th23 by simp
1.124 +    from "4.hyps"(1)[OF th21 th22]
1.125 +    have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)" using th23 by simp
1.126      with prems th1 have ?case by simp }
1.127    moreover {assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp
1.128      have "min n0 n1 \<le> n1"  by simp
1.129 @@ -303,30 +309,30 @@
1.130      from prems have th21: "isnpolyh c' (Suc n')" by simp_all
1.131      from prems have th22: "isnpolyh (CN c n p) n" by simp
1.132      from gt have th23: "min n (Suc n') = Suc n'" by arith
1.133 -    from prems(3)[OF th22 th21]
1.134 -    have "isnpolyh (polyadd (CN c n p,c')) (Suc n')" using th23 by simp
1.135 +    from "4.hyps"(2)[OF th22 th21]
1.136 +    have "isnpolyh (polyadd (CN c n p) c') (Suc n')" using th23 by simp
1.137      with prems th1 have ?case by simp}
1.138        ultimately show ?case by blast
1.139  qed auto
1.140
1.141 -lemma polyadd[simp]: "Ipoly bs (polyadd (p,q)) = (Ipoly bs p) + (Ipoly bs q)"
1.142 +lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
1.143  by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib)
1.144
1.145 -lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd(p,q))"
1.146 +lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd p q)"
1.147    using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
1.148
1.149  text{* The degree of addition and other general lemmas needed for the normal form of polymul *}
1.150
1.152    "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degreen p m \<noteq> degreen q m ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow>
1.153 -  degreen (polyadd(p,q)) m = max (degreen p m) (degreen q m)"
1.154 +  degreen (polyadd p q) m = max (degreen p m) (degreen q m)"
1.155  proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct)
1.156    case (4 c n p c' n' p' m n0 n1)
1.157    have "n' = n \<or> n < n' \<or> n' < n" by arith
1.158    thus ?case
1.159    proof (elim disjE)
1.160      assume [simp]: "n' = n"
1.161 -    from 4(1)[of n n m] 4(2)[of "Suc n" "Suc n" m] 4(5-7)
1.162 +    from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
1.163      show ?thesis by (auto simp: Let_def)
1.164    next
1.165      assume "n < n'"
1.166 @@ -367,12 +373,12 @@
1.167    thus ?case
1.168    proof (elim disjE)
1.169      assume [simp]: "n' = n"
1.170 -    from 4(1)[of n n m] 4(2)[of "Suc n" "Suc n" m] 4(5-7)
1.171 +    from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
1.172      show ?thesis by (auto simp: Let_def)
1.173    qed simp_all
1.174  qed auto
1.175
1.176 -lemma polyadd_eq_const_degreen: "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\<rbrakk>
1.177 +lemma polyadd_eq_const_degreen: "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd p q = C c\<rbrakk>
1.178    \<Longrightarrow> degreen p m = degreen q m"
1.179  proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
1.180    case (4 c n p c' n' p' m n0 n1 x)
1.181 @@ -1074,18 +1080,16 @@
1.182  unfolding polysub_def split_def fst_conv snd_conv
1.183  using np nq h d
1.185 -  case (1 a b a' b') thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def])
1.186 +  case (1 c c') thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def])
1.187  next
1.188 -  case (2 a b c' n' p')
1.189 -  let ?c = "(a,b)"
1.190 -  from prems have "degree (C ?c) = degree (CN c' n' p')" by simp
1.191 +  case (2 c c' n' p')
1.192 +  from prems have "degree (C c) = degree (CN c' n' p')" by simp
1.193    hence nz:"n' > 0" by (cases n', auto)
1.194    hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
1.195    with prems show ?case by simp
1.196  next
1.197 -  case (3 c n p a' b')
1.198 -  let ?c' = "(a',b')"
1.199 -  from prems have "degree (C ?c') = degree (CN c n p)" by simp
1.200 +  case (3 c n p c')
1.201 +  from prems have "degree (C c') = degree (CN c n p)" by simp
1.202    hence nz:"n > 0" by (cases n, auto)
1.203    hence "head (CN c n p) = CN c n p" by (cases n, auto)
1.204    with prems show ?case by simp
1.205 @@ -1124,7 +1128,7 @@
1.206      hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
1.208    ultimately show ?case  by blast
1.209 -qed auto
1.210 +qed auto
1.211
1.214 @@ -1155,7 +1159,7 @@
1.215    by (induct p rule: head.induct, auto)
1.216
1.218 -  "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\<rbrakk> \<Longrightarrow> degree p = degree q"
1.219 +  "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd p q = C c\<rbrakk> \<Longrightarrow> degree p = degree q"
1.220    using polyadd_eq_const_degreen degree_eq_degreen0 by simp
1.221
1.222  lemma polyadd_head: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
1.223 @@ -1233,12 +1237,12 @@
1.225    by (induct p rule: head.induct, auto)
1.226
1.227 -lemma degree_CN: "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<le> 1+ degree p"
1.228 +lemma degree_CN: "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<le> 1 + degree p"
1.229    by (cases n, simp_all)
1.230  lemma degree_CN': "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<ge>  degree p"
1.231    by (cases n, simp_all)
1.232
1.233 -lemma polyadd_different_degree: "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degree p \<noteq> degree q\<rbrakk> \<Longrightarrow> degree (polyadd(p,q)) = max (degree p) (degree q)"
1.234 +lemma polyadd_different_degree: "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degree p \<noteq> degree q\<rbrakk> \<Longrightarrow> degree (polyadd p q) = max (degree p) (degree q)"
1.235    using polyadd_different_degreen degree_eq_degreen0 by simp
1.236
1.237  lemma degreen_polyneg: "isnpolyh p n0 \<Longrightarrow> degreen (~\<^sub>p p) m = degreen p m"
```