merged

--- a/src/Doc/Prog_Prove/Types_and_funs.thy	Tue Jan 10 17:13:01 2017 +0100
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Tue Jan 10 17:24:15 2017 +0100
@@ -218,9 +218,10 @@
 a function @{text "contents ::"} @{typ "'a tree \<Rightarrow> 'a list"}
 that collects all values in a tree in a list, in any order,
 without removing duplicates.
-Then define a function @{text "treesum ::"} @{typ "nat tree \<Rightarrow> nat"}
+Then define a function @{text "sum_tree ::"} @{typ "nat tree \<Rightarrow> nat"}
 that sums up all values in a tree of natural numbers
-and prove @{prop "treesum t = listsum(contents t)"}.
+and prove @{prop "sum_tree t = sum_list(contents t)"}
+(where @{const sum_list} is predefined).
 \end{exercise}
 
 \begin{exercise}

--- a/src/HOL/Library/Polynomial.thy	Tue Jan 10 17:13:01 2017 +0100
+++ b/src/HOL/Library/Polynomial.thy	Tue Jan 10 17:24:15 2017 +0100
@@ -3650,29 +3650,36 @@
 
 lemmas eucl_rel_poly_unique_mod = eucl_rel_poly_unique [THEN conjunct2]
 
-instantiation poly :: (field) ring_div
+instantiation poly :: (field) semidom_modulo
 begin
-
-definition modulo_poly where
-  mod_poly_def: "f mod g \<equiv>
-    if g = 0 then f
-    else pseudo_mod (smult ((1/coeff g (degree g)) ^ (Suc (degree f) - degree g)) f) g"
-
-lemma eucl_rel_poly: "eucl_rel_poly (x::'a::field poly) y (x div y, x mod y)"
-  unfolding eucl_rel_poly_iff
-proof (intro conjI)
-  show "x = x div y * y + x mod y"
-  proof(cases "y = 0")
-    case True show ?thesis by(simp add: True divide_poly_def divide_poly_0 mod_poly_def)
+ 
+definition modulo_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
+  where mod_poly_def: "f mod g = (if g = 0 then f
+    else pseudo_mod (smult ((1 / lead_coeff g) ^ (Suc (degree f) - degree g)) f) g)"
+
+instance proof
+  fix x y :: "'a poly"
+  show "x div y * y + x mod y = x"
+  proof (cases "y = 0")
+    case True then show ?thesis
+      by (simp add: divide_poly_0 mod_poly_def)
   next
     case False
-    then have "pseudo_divmod (smult ((1 / coeff y (degree y)) ^ (Suc (degree x) - degree y)) x) y =
-          (x div y, x mod y)"
-      unfolding divide_poly_field mod_poly_def pseudo_mod_def by simp
-    from pseudo_divmod[OF False this]
+    then have "pseudo_divmod (smult ((1 / lead_coeff y) ^ (Suc (degree x) - degree y)) x) y =
+      (x div y, x mod y)"
+      by (simp add: divide_poly_field mod_poly_def pseudo_mod_def)
+    from pseudo_divmod [OF False this]
     show ?thesis using False
-      by (simp add: power_mult_distrib[symmetric] mult.commute)
+      by (simp add: power_mult_distrib [symmetric] ac_simps)
   qed
+qed
+  
+end
+    
+lemma eucl_rel_poly: "eucl_rel_poly x y (x div y, x mod y)"
+unfolding eucl_rel_poly_iff proof
+  show "x = x div y * y + x mod y"
+    by (simp add: div_mult_mod_eq)
   show "if y = 0 then x div y = 0 else x mod y = 0 \<or> degree (x mod y) < degree y"
   proof (cases "y = 0")
     case True then show ?thesis by auto
@@ -3684,18 +3691,14 @@
 
 lemma div_poly_eq:
   "eucl_rel_poly (x::'a::field poly) y (q, r) \<Longrightarrow> x div y = q"
-  by(rule eucl_rel_poly_unique_div[OF eucl_rel_poly])
+  by(rule eucl_rel_poly_unique_div [OF eucl_rel_poly])
 
 lemma mod_poly_eq:
   "eucl_rel_poly (x::'a::field poly) y (q, r) \<Longrightarrow> x mod y = r"
-  by (rule eucl_rel_poly_unique_mod[OF eucl_rel_poly])
-
-instance
+  by (rule eucl_rel_poly_unique_mod [OF eucl_rel_poly])
+
+instance poly :: (field) ring_div
 proof
-  fix x y :: "'a poly"
-  from eucl_rel_poly[of x y,unfolded eucl_rel_poly_iff]
-  show "x div y * y + x mod y = x" by auto
-next
   fix x y z :: "'a poly"
   assume "y \<noteq> 0"
   hence "eucl_rel_poly (x + z * y) y (z + x div y, x mod y)"
@@ -3729,8 +3732,6 @@
   qed
 qed
 
-end
-
 lemma div_pCons_eq:
   "pCons a p div q = (if q = 0 then 0
      else pCons (coeff (pCons a (p mod q)) (degree q) / lead_coeff q)