# HG changeset patch
# User krauss
# Date 1298326476 -3600
# Node ID d46c2908a838a8b1ebd91a0ed59045e3a6139616
# Parent  7e338ccabff073d649ba3f1a48ad712dca02d38c
recdef -> fun; curried

diff -r 7e338ccabff0 -r d46c2908a838 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 21 23:14:36 2011 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 21 23:14:36 2011 +0100
@@ -105,30 +105,33 @@
 | "headconst (C n) = n"
 
 subsection{* Operations for normalization *}
+
+
 consts 
-  polyadd :: "poly\<times>poly \<Rightarrow> poly"
   polysub :: "poly\<times>poly \<Rightarrow> poly"
   polymul :: "poly\<times>poly \<Rightarrow> poly"
 
-abbreviation poly_add :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
-  where "a +\<^sub>p b \<equiv> polyadd (a,b)"
 abbreviation poly_mul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
   where "a *\<^sub>p b \<equiv> polymul (a,b)"
 abbreviation poly_sub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
   where "a -\<^sub>p b \<equiv> polysub (a,b)"
 
-recdef polyadd "measure (\<lambda> (a,b). polysize a + polysize b)"
-  "polyadd (C c, C c') = C (c+\<^sub>Nc')"
-  "polyadd (C c, CN c' n' p') = CN (polyadd (C c, c')) n' p'"
-  "polyadd (CN c n p, C c') = CN (polyadd (c, C c')) n p"
-  "polyadd (CN c n p, CN c' n' p') =
-    (if n < n' then CN (polyadd(c,CN c' n' p')) n p
-     else if n'<n then CN (polyadd(CN c n p, c')) n' p'
-     else (let cc' = polyadd (c,c') ; 
-               pp' = polyadd (p,p')
+declare if_cong[fundef_cong del]
+declare let_cong[fundef_cong del]
+
+fun polyadd :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
+where
+  "polyadd (C c) (C c') = C (c+\<^sub>Nc')"
+|  "polyadd (C c) (CN c' n' p') = CN (polyadd (C c) c') n' p'"
+| "polyadd (CN c n p) (C c') = CN (polyadd c (C c')) n p"
+| "polyadd (CN c n p) (CN c' n' p') =
+    (if n < n' then CN (polyadd c (CN c' n' p')) n p
+     else if n'<n then CN (polyadd (CN c n p) c') n' p'
+     else (let cc' = polyadd c c' ; 
+               pp' = polyadd p p'
            in (if pp' = 0\<^sub>p then cc' else CN cc' n pp')))"
-  "polyadd (a, b) = Add a b"
-(hints recdef_simp add: Let_def measure_def split_def inv_image_def recdef_cong del: if_cong)
+| "polyadd a b = Add a b"
+
 
 fun polyneg :: "poly \<Rightarrow> poly" ("~\<^sub>p")
 where
@@ -136,7 +139,7 @@
 | "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)"
 | "polyneg a = Neg a"
 
-defs polysub_def[code]: "polysub \<equiv> \<lambda> (p,q). polyadd (p,polyneg q)"
+defs polysub_def[code]: "polysub \<equiv> \<lambda> (p,q). polyadd p (polyneg q)"
 
 recdef polymul "measure (\<lambda>(a,b). size a + size b)"
   "polymul(C c, C c') = C (c*\<^sub>Nc')"
@@ -148,10 +151,13 @@
   (if n<n' then CN (polymul(c,CN c' n' p')) n (polymul(p,CN c' n' p'))
   else if n' < n 
   then CN (polymul(CN c n p,c')) n' (polymul(CN c n p,p'))
-  else polyadd(polymul(CN c n p, c'),CN 0\<^sub>p n' (polymul(CN c n p, p'))))"
+  else polyadd (polymul(CN c n p, c')) (CN 0\<^sub>p n' (polymul(CN c n p, p'))))"
   "polymul (a,b) = Mul a b"
 (hints recdef_cong del: if_cong)
 
+declare if_cong[fundef_cong]
+declare let_cong[fundef_cong]
+
 fun polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
 where
   "polypow 0 = (\<lambda>p. 1\<^sub>p)"
@@ -256,21 +262,21 @@
 text{* polyadd preserves normal forms *}
 
 lemma polyadd_normh: "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> 
-      \<Longrightarrow> isnpolyh (polyadd(p,q)) (min n0 n1)"
+      \<Longrightarrow> isnpolyh (polyadd p q) (min n0 n1)"
 proof(induct p q arbitrary: n0 n1 rule: polyadd.induct)
-  case (2 a b c' n' p' n0 n1)
-  from prems have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp 
+  case (2 ab c' n' p' n0 n1)
+  from prems have  th1: "isnpolyh (C ab) (Suc n')" by simp 
   from prems(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
   with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
-  with prems(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp
+  with prems(1)[OF th1 th2] have th3:"isnpolyh (C ab +\<^sub>p c') (Suc n')" by simp
   from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 
   thus ?case using prems th3 by simp
 next
-  case (3 c' n' p' a b n1 n0)
-  from prems have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp 
+  case (3 c' n' p' ab n1 n0)
+  from prems have  th1: "isnpolyh (C ab) (Suc n')" by simp 
   from prems(2) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
   with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
-  with prems(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp
+  with prems(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C ab) (Suc n')" by simp
   from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 
   thus ?case using prems th3 by simp
 next
@@ -281,11 +287,11 @@
   from prems have n'gen1: "n' \<ge> n1" by simp 
   have "n < n' \<or> n' < n \<or> n = n'" by auto
   moreover {assume eq: "n = n'"
-    with prems(2)[OF nc nc'] 
+    with "4.hyps"(3)[OF nc nc'] 
     have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto
     hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)"
       using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto
-    from eq prems(1)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
+    from eq "4.hyps"(4)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
     have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp
     from minle npp' ncc'n01 prems ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}
   moreover {assume lt: "n < n'"
@@ -294,8 +300,8 @@
     from prems have th21: "isnpolyh c (Suc n)" by simp
     from prems have th22: "isnpolyh (CN c' n' p') n'" by simp
     from lt have th23: "min (Suc n) n' = Suc n" by arith
-    from prems(4)[OF th21 th22]
-    have "isnpolyh (polyadd (c, CN c' n' p')) (Suc n)" using th23 by simp
+    from "4.hyps"(1)[OF th21 th22]
+    have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)" using th23 by simp
     with prems th1 have ?case by simp } 
   moreover {assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp
     have "min n0 n1 \<le> n1"  by simp
@@ -303,30 +309,30 @@
     from prems have th21: "isnpolyh c' (Suc n')" by simp_all
     from prems have th22: "isnpolyh (CN c n p) n" by simp
     from gt have th23: "min n (Suc n') = Suc n'" by arith
-    from prems(3)[OF th22 th21]
-    have "isnpolyh (polyadd (CN c n p,c')) (Suc n')" using th23 by simp
+    from "4.hyps"(2)[OF th22 th21]
+    have "isnpolyh (polyadd (CN c n p) c') (Suc n')" using th23 by simp
     with prems th1 have ?case by simp}
       ultimately show ?case by blast
 qed auto
 
-lemma polyadd[simp]: "Ipoly bs (polyadd (p,q)) = (Ipoly bs p) + (Ipoly bs q)"
+lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
 by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib)
 
-lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd(p,q))"
+lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd p q)"
   using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
 
 text{* The degree of addition and other general lemmas needed for the normal form of polymul *}
 
 lemma polyadd_different_degreen: 
   "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degreen p m \<noteq> degreen q m ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow> 
-  degreen (polyadd(p,q)) m = max (degreen p m) (degreen q m)"
+  degreen (polyadd p q) m = max (degreen p m) (degreen q m)"
 proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct)
   case (4 c n p c' n' p' m n0 n1)
   have "n' = n \<or> n < n' \<or> n' < n" by arith
   thus ?case
   proof (elim disjE)
     assume [simp]: "n' = n"
-    from 4(1)[of n n m] 4(2)[of "Suc n" "Suc n" m] 4(5-7)
+    from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
     show ?thesis by (auto simp: Let_def)
   next
     assume "n < n'"
@@ -367,12 +373,12 @@
   thus ?case
   proof (elim disjE)
     assume [simp]: "n' = n"
-    from 4(1)[of n n m] 4(2)[of "Suc n" "Suc n" m] 4(5-7)
+    from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
     show ?thesis by (auto simp: Let_def)
   qed simp_all
 qed auto
 
-lemma polyadd_eq_const_degreen: "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\<rbrakk> 
+lemma polyadd_eq_const_degreen: "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd p q = C c\<rbrakk> 
   \<Longrightarrow> degreen p m = degreen q m"
 proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
   case (4 c n p c' n' p' m n0 n1 x) 
@@ -1074,18 +1080,16 @@
 unfolding polysub_def split_def fst_conv snd_conv
 using np nq h d
 proof(induct p q rule:polyadd.induct)
-  case (1 a b a' b') thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def]) 
+  case (1 c c') thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def]) 
 next
-  case (2 a b c' n' p') 
-  let ?c = "(a,b)"
-  from prems have "degree (C ?c) = degree (CN c' n' p')" by simp
+  case (2 c c' n' p') 
+  from prems have "degree (C c) = degree (CN c' n' p')" by simp
   hence nz:"n' > 0" by (cases n', auto)
   hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
   with prems show ?case by simp
 next
-  case (3 c n p a' b') 
-  let ?c' = "(a',b')"
-  from prems have "degree (C ?c') = degree (CN c n p)" by simp
+  case (3 c n p c') 
+  from prems have "degree (C c') = degree (CN c n p)" by simp
   hence nz:"n > 0" by (cases n, auto)
   hence "head (CN c n p) = CN c n p" by (cases n, auto)
   with prems show ?case by simp
@@ -1124,7 +1128,7 @@
     hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
     from H(3) headcnp headcnp' nn' have ?case by auto}
   ultimately show ?case  by blast
-qed auto 
+qed auto
  
 lemma shift1_head : "isnpolyh p n0 \<Longrightarrow> head (shift1 p) = head p"
 by (induct p arbitrary: n0 rule: head.induct, simp_all add: shift1_def)
@@ -1155,7 +1159,7 @@
   by (induct p rule: head.induct, auto)
 
 lemma polyadd_eq_const_degree: 
-  "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\<rbrakk> \<Longrightarrow> degree p = degree q" 
+  "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd p q = C c\<rbrakk> \<Longrightarrow> degree p = degree q" 
   using polyadd_eq_const_degreen degree_eq_degreen0 by simp
 
 lemma polyadd_head: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
@@ -1233,12 +1237,12 @@
 lemma degree_head[simp]: "degree (head p) = 0"
   by (induct p rule: head.induct, auto)
 
-lemma degree_CN: "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<le> 1+ degree p"
+lemma degree_CN: "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<le> 1 + degree p"
   by (cases n, simp_all)
 lemma degree_CN': "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<ge>  degree p"
   by (cases n, simp_all)
 
-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)"
+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)"
   using polyadd_different_degreen degree_eq_degreen0 by simp
 
 lemma degreen_polyneg: "isnpolyh p n0 \<Longrightarrow> degreen (~\<^sub>p p) m = degreen p m"