generalized proofs
authorimmler
Mon Jan 11 15:20:17 2016 +0100 (2016-01-11)
changeset 62127d8e7738bd2e9
parent 62126 2d187ace2827
child 62128 3201ddb00097
generalized proofs
src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Mon Jan 11 13:15:15 2016 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Mon Jan 11 15:20:17 2016 +0100
     1.3 @@ -467,74 +467,15 @@
     1.4    "(if P then (1::'a::comm_semiring_1) else 0) * q = (if P then q else 0)"
     1.5    by auto
     1.6  
     1.7 -text \<open>TODO: generalize this and @{thm compact_lemma}?!\<close>
     1.8  lemma compact_blinfun_lemma:
     1.9    fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
    1.10    assumes "bounded (range f)"
    1.11    shows "\<forall>d\<subseteq>Basis. \<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists> r.
    1.12      subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
    1.13 -proof safe
    1.14 -  fix d :: "'a set"
    1.15 -  assume d: "d \<subseteq> Basis"
    1.16 -  with finite_Basis have "finite d"
    1.17 -    by (blast intro: finite_subset)
    1.18 -  from this d show "\<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists>r. subseq r \<and>
    1.19 -    (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
    1.20 -  proof (induct d)
    1.21 -    case empty
    1.22 -    then show ?case
    1.23 -      unfolding subseq_def by auto
    1.24 -  next
    1.25 -    case (insert k d)
    1.26 -    have k[intro]: "k \<in> Basis"
    1.27 -      using insert by auto
    1.28 -    have s': "bounded ((\<lambda>x. blinfun_apply x k) ` range f)"
    1.29 -      using \<open>bounded (range f)\<close>
    1.30 -      by (auto intro!: bounded_linear_image bounded_linear_intros)
    1.31 -    obtain l1::"'a \<Rightarrow>\<^sub>L 'b" and r1 where r1: "subseq r1"
    1.32 -      and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) i) (l1 i) < e) sequentially"
    1.33 -      using insert(3) using insert(4) by auto
    1.34 -    have f': "\<forall>n. f (r1 n) k \<in> (\<lambda>x. blinfun_apply x k) ` range f"
    1.35 -      by simp
    1.36 -    have "bounded (range (\<lambda>i. f (r1 i) k))"
    1.37 -      by (metis (lifting) bounded_subset f' image_subsetI s')
    1.38 -    then obtain l2 r2
    1.39 -      where r2: "subseq r2"
    1.40 -      and lr2: "((\<lambda>i. f (r1 (r2 i)) k) \<longlongrightarrow> l2) sequentially"
    1.41 -      using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) k"]
    1.42 -      by (auto simp: o_def)
    1.43 -    def r \<equiv> "r1 \<circ> r2"
    1.44 -    have r:"subseq r"
    1.45 -      using r1 and r2 unfolding r_def o_def subseq_def by auto
    1.46 -    moreover
    1.47 -    def l \<equiv> "blinfun_of_matrix (\<lambda>i j. if j = k then l2 \<bullet> i else l1 j \<bullet> i)::'a \<Rightarrow>\<^sub>L 'b"
    1.48 -    {
    1.49 -      fix e::real
    1.50 -      assume "e > 0"
    1.51 -      from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n)  i) (l1  i) < e) sequentially"
    1.52 -        by blast
    1.53 -      from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n))  k) l2 < e) sequentially"
    1.54 -        by (rule tendstoD)
    1.55 -      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n))  i) (l1  i) < e) sequentially"
    1.56 -        by (rule eventually_subseq)
    1.57 -      have l2: "l k = l2"
    1.58 -        using insert.prems
    1.59 -        by (auto simp: blinfun_of_matrix.rep_eq inner_Basis l_def mult_if_delta
    1.60 -          scaleR_setsum_left[symmetric] setsum.delta' intro!: euclidean_eqI[where 'a='b])
    1.61 -      {
    1.62 -        fix i assume "i \<in> d"
    1.63 -        with insert have "i \<in> Basis" "i \<noteq> k" by auto
    1.64 -        hence l1: "l i = (l1 i)"
    1.65 -          by (auto simp: blinfun_of_matrix.rep_eq inner_Basis l_def mult_if_delta
    1.66 -            scaleR_setsum_left[symmetric] setsum.delta' intro!: euclidean_eqI[where 'a='b])
    1.67 -      } note l1 = this
    1.68 -      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n)  i) (l  i) < e) sequentially"
    1.69 -        using N1' N2
    1.70 -        by eventually_elim (insert insert.prems, auto simp: r_def o_def l1 l2)
    1.71 -    }
    1.72 -    ultimately show ?case by auto
    1.73 -  qed
    1.74 -qed
    1.75 +  by (rule compact_lemma_general[where unproj = "\<lambda>e. blinfun_of_matrix (\<lambda>i j. e j \<bullet> i)"])
    1.76 +   (auto intro!: euclidean_eqI[where 'a='b] bounded_linear_image assms
    1.77 +    simp: blinfun_of_matrix_works blinfun_of_matrix_apply inner_Basis mult_if_delta setsum.delta'
    1.78 +      scaleR_setsum_left[symmetric])
    1.79  
    1.80  lemma blinfun_euclidean_eqI: "(\<And>i. i \<in> Basis \<Longrightarrow> blinfun_apply x i = blinfun_apply y i) \<Longrightarrow> x = y"
    1.81    apply (auto intro!: blinfun_eqI)
     2.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Jan 11 13:15:15 2016 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Jan 11 15:20:17 2016 +0100
     2.3 @@ -820,47 +820,14 @@
     2.4  lemma compact_lemma_cart:
     2.5    fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n"
     2.6    assumes f: "bounded (range f)"
     2.7 -  shows "\<forall>d.
     2.8 -        \<exists>l r. subseq r \<and>
     2.9 +  shows "\<exists>l r. subseq r \<and>
    2.10          (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
    2.11 -proof
    2.12 -  fix d :: "'n set"
    2.13 -  have "finite d" by simp
    2.14 -  thus "\<exists>l::'a ^ 'n. \<exists>r. subseq r \<and>
    2.15 -      (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
    2.16 -  proof (induct d)
    2.17 -    case empty
    2.18 -    thus ?case unfolding subseq_def by auto
    2.19 -  next
    2.20 -    case (insert k d)
    2.21 -    obtain l1::"'a^'n" and r1 where r1:"subseq r1"
    2.22 -      and lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially"
    2.23 -      using insert(3) by auto
    2.24 -    have s': "bounded ((\<lambda>x. x $ k) ` range f)" using \<open>bounded (range f)\<close>
    2.25 -      by (auto intro!: bounded_component_cart)
    2.26 -    have f': "\<forall>n. f (r1 n) $ k \<in> (\<lambda>x. x $ k) ` range f" by simp
    2.27 -    have "bounded (range (\<lambda>i. f (r1 i) $ k))"
    2.28 -      by (metis (lifting) bounded_subset image_subsetI f' s')
    2.29 -    then obtain l2 r2 where r2: "subseq r2"
    2.30 -      and lr2: "((\<lambda>i. f (r1 (r2 i)) $ k) \<longlongrightarrow> l2) sequentially"
    2.31 -      using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) $ k"] by (auto simp: o_def)
    2.32 -    def r \<equiv> "r1 \<circ> r2"
    2.33 -    have r: "subseq r"
    2.34 -      using r1 and r2 unfolding r_def o_def subseq_def by auto
    2.35 -    moreover
    2.36 -    def l \<equiv> "(\<chi> i. if i = k then l2 else l1$i)::'a^'n"
    2.37 -    { fix e :: real assume "e > 0"
    2.38 -      from lr1 \<open>e>0\<close> have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially"
    2.39 -        by blast
    2.40 -      from lr2 \<open>e>0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) $ k) l2 < e) sequentially"
    2.41 -        by (rule tendstoD)
    2.42 -      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) $ i) (l1 $ i) < e) sequentially"
    2.43 -        by (rule eventually_subseq)
    2.44 -      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) $ i) (l $ i) < e) sequentially"
    2.45 -        using N1' N2 by (rule eventually_elim2, simp add: l_def r_def)
    2.46 -    }
    2.47 -    ultimately show ?case by auto
    2.48 -  qed
    2.49 +    (is "?th d")
    2.50 +proof -
    2.51 +  have "\<forall>d' \<subseteq> d. ?th d'"
    2.52 +    by (rule compact_lemma_general[where unproj=vec_lambda])
    2.53 +      (auto intro!: f bounded_component_cart simp: vec_lambda_eta)
    2.54 +  then show "?th d" by simp
    2.55  qed
    2.56  
    2.57  instance vec :: (heine_borel, finite) heine_borel
     3.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 11 13:15:15 2016 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 11 15:20:17 2016 +0100
     3.3 @@ -4443,61 +4443,75 @@
     3.4      using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
     3.5  qed
     3.6  
     3.7 -lemma compact_lemma:
     3.8 -  fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
     3.9 -  assumes "bounded (range f)"
    3.10 -  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
    3.11 -    subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
    3.12 +lemma compact_lemma_general:
    3.13 +  fixes f :: "nat \<Rightarrow> 'a"
    3.14 +  fixes proj::"'a \<Rightarrow> 'b \<Rightarrow> 'c::heine_borel" (infixl "proj" 60)
    3.15 +  fixes unproj:: "('b \<Rightarrow> 'c) \<Rightarrow> 'a"
    3.16 +  assumes finite_basis: "finite basis"
    3.17 +  assumes bounded_proj: "\<And>k. k \<in> basis \<Longrightarrow> bounded ((\<lambda>x. x proj k) ` range f)"
    3.18 +  assumes proj_unproj: "\<And>e k. k \<in> basis \<Longrightarrow> (unproj e) proj k = e k"
    3.19 +  assumes unproj_proj: "\<And>x. unproj (\<lambda>k. x proj k) = x"
    3.20 +  shows "\<forall>d\<subseteq>basis. \<exists>l::'a. \<exists> r.
    3.21 +    subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
    3.22  proof safe
    3.23 -  fix d :: "'a set"
    3.24 -  assume d: "d \<subseteq> Basis"
    3.25 -  with finite_Basis have "finite d"
    3.26 +  fix d :: "'b set"
    3.27 +  assume d: "d \<subseteq> basis"
    3.28 +  with finite_basis have "finite d"
    3.29      by (blast intro: finite_subset)
    3.30    from this d show "\<exists>l::'a. \<exists>r. subseq r \<and>
    3.31 -    (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
    3.32 +    (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
    3.33    proof (induct d)
    3.34      case empty
    3.35      then show ?case
    3.36        unfolding subseq_def by auto
    3.37    next
    3.38      case (insert k d)
    3.39 -    have k[intro]: "k \<in> Basis"
    3.40 +    have k[intro]: "k \<in> basis"
    3.41        using insert by auto
    3.42 -    have s': "bounded ((\<lambda>x. x \<bullet> k) ` range f)"
    3.43 -      using \<open>bounded (range f)\<close>
    3.44 -      by (auto intro!: bounded_linear_image bounded_linear_inner_left)
    3.45 +    have s': "bounded ((\<lambda>x. x proj k) ` range f)"
    3.46 +      using k
    3.47 +      by (rule bounded_proj)
    3.48      obtain l1::"'a" and r1 where r1: "subseq r1"
    3.49 -      and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \<bullet> i) (l1 \<bullet> i) < e) sequentially"
    3.50 +      and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"
    3.51        using insert(3) using insert(4) by auto
    3.52 -    have f': "\<forall>n. f (r1 n) \<bullet> k \<in> (\<lambda>x. x \<bullet> k) ` range f"
    3.53 +    have f': "\<forall>n. f (r1 n) proj k \<in> (\<lambda>x. x proj k) ` range f"
    3.54        by simp
    3.55 -    have "bounded (range (\<lambda>i. f (r1 i) \<bullet> k))"
    3.56 +    have "bounded (range (\<lambda>i. f (r1 i) proj k))"
    3.57        by (metis (lifting) bounded_subset f' image_subsetI s')
    3.58 -    then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \<bullet> k) \<longlongrightarrow> l2) sequentially"
    3.59 -      using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) \<bullet> k"]
    3.60 +    then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) proj k) \<longlongrightarrow> l2) sequentially"
    3.61 +      using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) proj k"]
    3.62        by (auto simp: o_def)
    3.63      def r \<equiv> "r1 \<circ> r2"
    3.64      have r:"subseq r"
    3.65        using r1 and r2 unfolding r_def o_def subseq_def by auto
    3.66      moreover
    3.67 -    def l \<equiv> "(\<Sum>i\<in>Basis. (if i = k then l2 else l1\<bullet>i) *\<^sub>R i)::'a"
    3.68 +    def l \<equiv> "unproj (\<lambda>i. if i = k then l2 else l1 proj i)::'a"
    3.69      {
    3.70        fix e::real
    3.71        assume "e > 0"
    3.72 -      from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \<bullet> i) (l1 \<bullet> i) < e) sequentially"
    3.73 +      from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"
    3.74          by blast
    3.75 -      from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) \<bullet> k) l2 < e) sequentially"
    3.76 +      from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) proj k) l2 < e) sequentially"
    3.77          by (rule tendstoD)
    3.78 -      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) \<bullet> i) (l1 \<bullet> i) < e) sequentially"
    3.79 +      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e) sequentially"
    3.80          by (rule eventually_subseq)
    3.81 -      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
    3.82 +      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) proj i) (l proj i) < e) sequentially"
    3.83          using N1' N2
    3.84 -        by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def)
    3.85 +        by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def proj_unproj)
    3.86      }
    3.87      ultimately show ?case by auto
    3.88    qed
    3.89  qed
    3.90  
    3.91 +lemma compact_lemma:
    3.92 +  fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
    3.93 +  assumes "bounded (range f)"
    3.94 +  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
    3.95 +    subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
    3.96 +  by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"])
    3.97 +     (auto intro!: assms bounded_linear_inner_left bounded_linear_image
    3.98 +       simp: euclidean_representation)
    3.99 +
   3.100  instance euclidean_space \<subseteq> heine_borel
   3.101  proof
   3.102    fix f :: "nat \<Rightarrow> 'a"