src/HOL/Library/Formal_Power_Series.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 41959 b460124855b8
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  notation fps_nth (infixl "$" 75)
     1.5  
     1.6  lemma expand_fps_eq: "p = q \<longleftrightarrow> (\<forall>n. p $ n = q $ n)"
     1.7 -  by (simp add: fps_nth_inject [symmetric] ext_iff)
     1.8 +  by (simp add: fps_nth_inject [symmetric] fun_eq_iff)
     1.9  
    1.10  lemma fps_ext: "(\<And>n. p $ n = q $ n) \<Longrightarrow> p = q"
    1.11    by (simp add: expand_fps_eq)
    1.12 @@ -791,14 +791,14 @@
    1.13        apply (rule setsum_reindex_cong[where f="\<lambda>i. n + 1 - i"])
    1.14        apply (simp add: inj_on_def Ball_def)
    1.15        apply presburger
    1.16 -      apply (rule set_ext)
    1.17 +      apply (rule set_eqI)
    1.18        apply (presburger add: image_iff)
    1.19        by simp
    1.20      have s1: "setsum (\<lambda>i. f $ i * g $ (n + 1 - i)) ?Zn1 = setsum (\<lambda>i. f $ (n + 1 - i) * g $ i) ?Zn1"
    1.21        apply (rule setsum_reindex_cong[where f="\<lambda>i. n + 1 - i"])
    1.22        apply (simp add: inj_on_def Ball_def)
    1.23        apply presburger
    1.24 -      apply (rule set_ext)
    1.25 +      apply (rule set_eqI)
    1.26        apply (presburger add: image_iff)
    1.27        by simp
    1.28      have "(f * ?D g + ?D f * g)$n = (?D g * f + ?D f * g)$n" by (simp only: mult_commute)
    1.29 @@ -1244,7 +1244,7 @@
    1.30      {assume n0: "n \<noteq> 0"
    1.31        then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1}\<union>{2..n} = {1..n}"
    1.32          "{0..n - 1}\<union>{n} = {0..n}"
    1.33 -        by (auto simp: set_ext_iff)
    1.34 +        by (auto simp: set_eq_iff)
    1.35        have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}"
    1.36          "{0..n - 1}\<inter>{n} ={}" using n0 by simp_all
    1.37        have f: "finite {0}" "finite {1}" "finite {2 .. n}"
    1.38 @@ -1455,7 +1455,7 @@
    1.39    moreover
    1.40    {fix k assume k: "m = Suc k"
    1.41      have km: "k < m" using k by arith
    1.42 -    have u0: "{0 .. k} \<union> {m} = {0..m}" using k apply (simp add: set_ext_iff) by presburger
    1.43 +    have u0: "{0 .. k} \<union> {m} = {0..m}" using k apply (simp add: set_eq_iff) by presburger
    1.44      have f0: "finite {0 .. k}" "finite {m}" by auto
    1.45      have d0: "{0 .. k} \<inter> {m} = {}" using k by auto
    1.46      have "(setprod a {0 .. m}) $ n = (setprod a {0 .. k} * a m) $ n"
    1.47 @@ -1472,7 +1472,7 @@
    1.48        apply clarsimp
    1.49        apply (rule finite_imageI)
    1.50        apply (rule natpermute_finite)
    1.51 -      apply (clarsimp simp add: set_ext_iff)
    1.52 +      apply (clarsimp simp add: set_eq_iff)
    1.53        apply auto
    1.54        apply (rule setsum_cong2)
    1.55        unfolding setsum_left_distrib
    1.56 @@ -2153,7 +2153,7 @@
    1.57  qed
    1.58  
    1.59  lemma fps_inv_ginv: "fps_inv = fps_ginv X"
    1.60 -  apply (auto simp add: ext_iff fps_eq_iff fps_inv_def fps_ginv_def)
    1.61 +  apply (auto simp add: fun_eq_iff fps_eq_iff fps_inv_def fps_ginv_def)
    1.62    apply (induct_tac n rule: nat_less_induct, auto)
    1.63    apply (case_tac na)
    1.64    apply simp
    1.65 @@ -2192,7 +2192,7 @@
    1.66    "setsum (%i. a (i :: nat) * b (n - i)) {0 .. n} = setsum (%(i,j). a i * b j) {(i,j). i <= n \<and> j \<le> n \<and> i + j = n}"
    1.67    apply (rule setsum_reindex_cong[where f=fst])
    1.68    apply (clarsimp simp add: inj_on_def)
    1.69 -  apply (auto simp add: set_ext_iff image_iff)
    1.70 +  apply (auto simp add: set_eq_iff image_iff)
    1.71    apply (rule_tac x= "x" in exI)
    1.72    apply clarsimp
    1.73    apply (rule_tac x="n - x" in exI)
    1.74 @@ -2264,7 +2264,7 @@
    1.75    let ?KM=  "{(k,m). k + m \<le> n}"
    1.76    let ?f = "%s. UNION {(0::nat)..s} (%i. {(i,s - i)})"
    1.77    have th0: "?KM = UNION {0..n} ?f"
    1.78 -    apply (simp add: set_ext_iff)
    1.79 +    apply (simp add: set_eq_iff)
    1.80      apply arith (* FIXME: VERY slow! *)
    1.81      done
    1.82    show "?l = ?r "
    1.83 @@ -3312,10 +3312,10 @@
    1.84  
    1.85  lemma XDp_commute:
    1.86    shows "XDp b o XDp (c::'a::comm_ring_1) = XDp c o XDp b"
    1.87 -  by (auto simp add: XDp_def ext_iff fps_eq_iff algebra_simps)
    1.88 +  by (auto simp add: XDp_def fun_eq_iff fps_eq_iff algebra_simps)
    1.89  
    1.90  lemma XDp0[simp]: "XDp 0 = XD"
    1.91 -  by (simp add: ext_iff fps_eq_iff)
    1.92 +  by (simp add: fun_eq_iff fps_eq_iff)
    1.93  
    1.94  lemma XDp_fps_integral[simp]:"XDp 0 (fps_integral a c) = X * a"
    1.95    by (simp add: fps_eq_iff fps_integral_def)