src/HOL/Library/Formal_Power_Series.thy

 
 instantiation fps :: (field) euclidean_ring
 begin
 
 definition fps_euclidean_size_def:
-  "euclidean_size f = (if f = 0 then 0 else Suc (subdegree f))"
+  "euclidean_size f = (if f = 0 then 0 else 2 ^ subdegree f)"
 
 instance proof
   fix f g :: "'a fps" assume [simp]: "g \<noteq> 0"
   show "euclidean_size f \<le> euclidean_size (f * g)"
     by (cases "f = 0") (auto simp: fps_euclidean_size_def)
   show "euclidean_size (f mod g) < euclidean_size g"
     apply (cases "f = 0", simp add: fps_euclidean_size_def)
     apply (rule disjE[OF le_less_linear[of "subdegree g" "subdegree f"]])
     apply (simp_all add: fps_mod_eq_zero fps_euclidean_size_def subdegree_mod)
     done
-qed
+qed (simp_all add: fps_euclidean_size_def)
 
 end
 
 instantiation fps :: (field) euclidean_ring_gcd
 begin
 definition fps_gcd_def: "(gcd :: 'a fps \<Rightarrow> _) = gcd_eucl"
 definition fps_lcm_def: "(lcm :: 'a fps \<Rightarrow> _) = lcm_eucl"
 definition fps_Gcd_def: "(Gcd :: 'a fps set \<Rightarrow> _) = Gcd_eucl"
 definition fps_Lcm_def: "(Lcm :: 'a fps set \<Rightarrow> _) = Lcm_eucl"
-instance by intro_classes (simp_all add: fps_gcd_def fps_lcm_def fps_Gcd_def fps_Lcm_def)
+instance by standard (simp_all add: fps_gcd_def fps_lcm_def fps_Gcd_def fps_Lcm_def)
 end
 
 lemma fps_gcd:
   assumes [simp]: "f \<noteq> 0" "g \<noteq> 0"
   shows   "gcd f g = X ^ min (subdegree f) (subdegree g)"

   proof (rule ccontr)
     assume "Lcm A \<noteq> 0"
     from unbounded obtain f where f: "f \<in> A" "subdegree (Lcm A) < subdegree f"
       unfolding bdd_above_def by (auto simp: not_le)
     moreover from this and \<open>Lcm A \<noteq> 0\<close> have "subdegree f \<le> subdegree (Lcm A)"
-      by (intro dvd_imp_subdegree_le) simp_all
+      by (intro dvd_imp_subdegree_le dvd_Lcm) simp_all
     ultimately show False by simp
   qed
   with unbounded show ?thesis by simp
-qed (simp_all add: fps_Lcm)
+qed (simp_all add: fps_Lcm Lcm_eq_0_I)
+
 
 
 subsection \<open>Formal Derivatives, and the MacLaurin theorem around 0\<close>
 
 definition "fps_deriv f = Abs_fps (\<lambda>n. of_nat (n + 1) * f $ (n + 1))"

   by (simp add: ac_simps)
 
 
 subsection \<open>Hypergeometric series\<close>
 
+(* TODO: Rename this *)
 definition "F as bs (c::'a::{field_char_0,field}) =
   Abs_fps (\<lambda>n. (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
     (foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
 
 lemma F_nth[simp]: "F as bs c $ n =