recdef -> fun; curried
authorkrauss
Mon Feb 21 23:14:36 2011 +0100 (2011-02-21)
changeset 41812d46c2908a838
parent 41811 7e338ccabff0
child 41813 4eb43410d2fa
recdef -> fun; curried
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 @@ -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.44 -  "polyadd (a, b) = Add a b"
    1.45 -(hints recdef_simp add: Let_def measure_def split_def inv_image_def recdef_cong del: if_cong)
    1.46 +| "polyadd a b = Add a b"
    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.151  lemma polyadd_different_degreen: 
   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.184  proof(induct p q rule:polyadd.induct)
   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.207      from H(3) headcnp headcnp' nn' have ?case by auto}
   1.208    ultimately show ?case  by blast
   1.209 -qed auto 
   1.210 +qed auto
   1.211   
   1.212  lemma shift1_head : "isnpolyh p n0 \<Longrightarrow> head (shift1 p) = head p"
   1.213  by (induct p arbitrary: n0 rule: head.induct, simp_all add: shift1_def)
   1.214 @@ -1155,7 +1159,7 @@
   1.215    by (induct p rule: head.induct, auto)
   1.216  
   1.217  lemma polyadd_eq_const_degree: 
   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.224  lemma degree_head[simp]: "degree (head p) = 0"
   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"