src/HOL/Analysis/Linear_Algebra.thy
changeset 68058 69715dfdc286
parent 67982 7643b005b29a
child 68062 ee88c0fccbae
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sun Apr 29 21:26:57 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Apr 30 22:13:04 2018 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4  lemma hull_unique: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> S t' \<Longrightarrow> t \<subseteq> t') \<Longrightarrow> (S hull s = t)"
     1.5    unfolding hull_def by auto
     1.6  
     1.7 -lemma hull_induct: "(\<And>x. x\<in> S \<Longrightarrow> P x) \<Longrightarrow> Q {x. P x} \<Longrightarrow> \<forall>x\<in> Q hull S. P x"
     1.8 +lemma hull_induct: "\<lbrakk>a \<in> Q hull S; \<And>x. x\<in> S \<Longrightarrow> P x; Q {x. P x}\<rbrakk> \<Longrightarrow> P a"
     1.9    using hull_minimal[of S "{x. P x}" Q]
    1.10    by (auto simp add: subset_eq)
    1.11  
    1.12 @@ -339,20 +339,12 @@
    1.13    unfolding dependent_def by auto
    1.14  
    1.15  lemma (in real_vector) independent_mono: "independent A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> independent B"
    1.16 -  apply (clarsimp simp add: dependent_def span_mono)
    1.17 -  apply (subgoal_tac "span (B - {a}) \<le> span (A - {a})")
    1.18 -  apply force
    1.19 -  apply (rule span_mono)
    1.20 -  apply auto
    1.21 -  done
    1.22 +  unfolding dependent_def span_mono
    1.23 +  by (metis insert_Diff local.span_mono subsetCE subset_insert_iff) 
    1.24  
    1.25  lemma (in real_vector) span_subspace: "A \<subseteq> B \<Longrightarrow> B \<le> span A \<Longrightarrow>  subspace B \<Longrightarrow> span A = B"
    1.26    by (metis order_antisym span_def hull_minimal)
    1.27  
    1.28 -lemma (in real_vector) span_induct':
    1.29 -  "\<forall>x \<in> S. P x \<Longrightarrow> subspace {x. P x} \<Longrightarrow> \<forall>x \<in> span S. P x"
    1.30 -  unfolding span_def by (rule hull_induct) auto
    1.31 -
    1.32  inductive_set (in real_vector) span_induct_alt_help for S :: "'a set"
    1.33  where
    1.34    span_induct_alt_help_0: "0 \<in> span_induct_alt_help S"
    1.35 @@ -1063,19 +1055,19 @@
    1.36    done
    1.37  
    1.38  lemma linear_eq_0_span:
    1.39 -  assumes lf: "linear f" and f0: "\<forall>x\<in>B. f x = 0"
    1.40 -  shows "\<forall>x \<in> span B. f x = 0"
    1.41 -  using f0 subspace_kernel[OF lf]
    1.42 -  by (rule span_induct')
    1.43 -
    1.44 -lemma linear_eq_0: "linear f \<Longrightarrow> S \<subseteq> span B \<Longrightarrow> \<forall>x\<in>B. f x = 0 \<Longrightarrow> \<forall>x\<in>S. f x = 0"
    1.45 -  using linear_eq_0_span[of f B] by auto
    1.46 -
    1.47 -lemma linear_eq_span:  "linear f \<Longrightarrow> linear g \<Longrightarrow> \<forall>x\<in>B. f x = g x \<Longrightarrow> \<forall>x \<in> span B. f x = g x"
    1.48 -  using linear_eq_0_span[of "\<lambda>x. f x - g x" B] by (auto simp: linear_compose_sub)
    1.49 -
    1.50 -lemma linear_eq: "linear f \<Longrightarrow> linear g \<Longrightarrow> S \<subseteq> span B \<Longrightarrow> \<forall>x\<in>B. f x = g x \<Longrightarrow> \<forall>x\<in>S. f x = g x"
    1.51 -  using linear_eq_span[of f g B] by auto
    1.52 +  assumes x: "x \<in> span B" and lf: "linear f" and f0: "\<And>x. x\<in>B \<Longrightarrow> f x = 0"
    1.53 +  shows "f x = 0"
    1.54 +  using x f0 subspace_kernel[OF lf] span_induct
    1.55 +  by blast
    1.56 +
    1.57 +lemma linear_eq_0: "\<lbrakk>x \<in> S; linear f; S \<subseteq> span B; \<And>x. x\<in>B \<Longrightarrow> f x = 0\<rbrakk> \<Longrightarrow> f x = 0"
    1.58 +  using linear_eq_0_span[of x B f] by auto
    1.59 +
    1.60 +lemma linear_eq_span: "\<lbrakk>x \<in> span B; linear f; linear g; \<And>x. x\<in>B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> f x = g x"
    1.61 +  using linear_eq_0_span[of x B "\<lambda>x. f x - g x"]  by (auto simp: linear_compose_sub)
    1.62 +
    1.63 +lemma linear_eq: "\<lbrakk>x \<in> S; linear f; linear g; S \<subseteq> span B; \<And>x. x\<in>B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> f x = g x"
    1.64 +  using linear_eq_span[of _ B f g] by auto
    1.65  
    1.66  text \<open>The degenerate case of the Exchange Lemma.\<close>
    1.67  
    1.68 @@ -1174,13 +1166,13 @@
    1.69    have fB: "inj_on f B"
    1.70      using fi by (auto simp: \<open>span S = span B\<close> intro: subset_inj_on span_superset)
    1.71  
    1.72 -  have "\<forall>x\<in>span B. g (f x) = x"
    1.73 -  proof (intro linear_eq_span)
    1.74 +  have "g (f x) = x" if "x \<in> span B" for x
    1.75 +  proof (rule linear_eq_span)
    1.76      show "linear (\<lambda>x. x)" "linear (\<lambda>x. g (f x))"
    1.77        using linear_id linear_compose[OF \<open>linear f\<close> \<open>linear g\<close>] by (auto simp: id_def comp_def)
    1.78 -    show "\<forall>x \<in> B. g (f x) = x"
    1.79 -      using g fi \<open>span S = span B\<close> by (auto simp: fB)
    1.80 -  qed
    1.81 +    show "g (f x) = x" if "x \<in> B" for x
    1.82 +      using g fi \<open>span S = span B\<close>   by (simp add: fB that)
    1.83 +  qed (rule that)
    1.84    moreover
    1.85    have "inv_into B f ` f ` B \<subseteq> B"
    1.86      by (auto simp: fB)
    1.87 @@ -1210,8 +1202,7 @@
    1.88    ultimately have "\<forall>x\<in>B. f (g x) = x"
    1.89      by auto
    1.90    then have "\<forall>x\<in>span B. f (g x) = x"
    1.91 -    using linear_id linear_compose[OF \<open>linear g\<close> \<open>linear f\<close>]
    1.92 -    by (intro linear_eq_span) (auto simp: id_def comp_def)
    1.93 +    using linear_id linear_compose[OF \<open>linear g\<close> \<open>linear f\<close>] linear_eq_span by fastforce
    1.94    moreover have "inv_into (span S) f ` B \<subseteq> span S"
    1.95      using \<open>B \<subseteq> T\<close> \<open>span T \<subseteq> f`span S\<close> by (auto intro: inv_into_into span_superset)
    1.96    then have "range g \<subseteq> span S"
    1.97 @@ -2457,8 +2448,8 @@
    1.98      done
    1.99    with a have a0:"?a  \<noteq> 0"
   1.100      by auto
   1.101 -  have "\<forall>x\<in>span B. ?a \<bullet> x = 0"
   1.102 -  proof (rule span_induct')
   1.103 +  have "?a \<bullet> x = 0" if "x\<in>span B" for x
   1.104 +  proof (rule span_induct [OF that])
   1.105      show "subspace {x. ?a \<bullet> x = 0}"
   1.106        by (auto simp add: subspace_def inner_add)
   1.107    next
   1.108 @@ -2481,9 +2472,9 @@
   1.109            intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])
   1.110          done
   1.111      }
   1.112 -    then show "\<forall>x \<in> B. ?a \<bullet> x = 0"
   1.113 -      by blast
   1.114 -  qed
   1.115 +    then show "?a \<bullet> x = 0" if "x \<in> B" for x
   1.116 +      using that by blast
   1.117 +    qed
   1.118    with a0 show ?thesis
   1.119      unfolding sSB by (auto intro: exI[where x="?a"])
   1.120  qed
   1.121 @@ -2635,9 +2626,9 @@
   1.122    fixes f :: "'a::euclidean_space \<Rightarrow> _"
   1.123    assumes lf: "linear f"
   1.124      and lg: "linear g"
   1.125 -    and fg: "\<forall>b\<in>Basis. f b = g b"
   1.126 +    and fg: "\<And>b. b \<in> Basis \<Longrightarrow> f b = g b"
   1.127    shows "f = g"
   1.128 -  using linear_eq[OF lf lg, of _ Basis] fg by auto
   1.129 +  using linear_eq[OF _ lf lg, of _ _ Basis] fg by auto
   1.130  
   1.131  text \<open>Similar results for bilinear functions.\<close>
   1.132  
   1.133 @@ -2646,8 +2637,9 @@
   1.134      and bg: "bilinear g"
   1.135      and SB: "S \<subseteq> span B"
   1.136      and TC: "T \<subseteq> span C"
   1.137 -    and fg: "\<forall>x\<in> B. \<forall>y\<in> C. f x y = g x y"
   1.138 -  shows "\<forall>x\<in>S. \<forall>y\<in>T. f x y = g x y "
   1.139 +    and "x\<in>S" "y\<in>T"
   1.140 +    and fg: "\<And>x y. \<lbrakk>x \<in> B; y\<in> C\<rbrakk> \<Longrightarrow> f x y = g x y"
   1.141 +  shows "f x y = g x y"
   1.142  proof -
   1.143    let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
   1.144    from bf bg have sp: "subspace ?P"
   1.145 @@ -2655,27 +2647,30 @@
   1.146      by (auto simp add: span_0 bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def
   1.147        intro: bilinear_ladd[OF bf])
   1.148  
   1.149 -  have "\<forall>x \<in> span B. \<forall>y\<in> span C. f x y = g x y"
   1.150 -    apply (rule span_induct' [OF _ sp])
   1.151 -    apply (rule ballI)
   1.152 -    apply (rule span_induct')
   1.153 -    apply (simp add: fg)
   1.154 +  have sfg: "\<And>x. x \<in> B \<Longrightarrow> subspace {a. f x a = g x a}"
   1.155      apply (auto simp add: subspace_def)
   1.156      using bf bg unfolding bilinear_def linear_iff
   1.157 -    apply (auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def
   1.158 +    apply (auto simp add: bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add 
   1.159        intro: bilinear_ladd[OF bf])
   1.160      done
   1.161 +  have "\<forall>y\<in> span C. f x y = g x y" if "x \<in> span B" for x
   1.162 +    apply (rule span_induct [OF that sp])
   1.163 +    apply (rule ballI)
   1.164 +    apply (erule span_induct)
   1.165 +    apply (simp_all add: sfg fg)
   1.166 +    done
   1.167    then show ?thesis
   1.168 -    using SB TC by auto
   1.169 +    using SB TC assms by auto
   1.170  qed
   1.171  
   1.172  lemma bilinear_eq_stdbasis:
   1.173    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> _"
   1.174    assumes bf: "bilinear f"
   1.175      and bg: "bilinear g"
   1.176 -    and fg: "\<forall>i\<in>Basis. \<forall>j\<in>Basis. f i j = g i j"
   1.177 +    and fg: "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> f i j = g i j"
   1.178    shows "f = g"
   1.179 -  using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis] fg] by blast
   1.180 +  using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg
   1.181 +  by blast
   1.182  
   1.183  text \<open>An injective map @{typ "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"} is also surjective.\<close>
   1.184  
   1.185 @@ -2695,13 +2690,7 @@
   1.186      apply (rule card_ge_dim_independent)
   1.187      apply blast
   1.188      apply (rule independent_injective_image[OF B(2) lf fi])
   1.189 -    apply (rule order_eq_refl)
   1.190 -    apply (rule sym)
   1.191 -    unfolding d
   1.192 -    apply (rule card_image)
   1.193 -    apply (rule subset_inj_on[OF fi])
   1.194 -    apply blast
   1.195 -    done
   1.196 +    by (metis card_image d fi inj_on_subset order_refl top_greatest)
   1.197    from th show ?thesis
   1.198      unfolding span_linear_image[OF lf] surj_def
   1.199      using B(3) by blast