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.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.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.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
```