author wenzelm Wed Aug 28 23:41:21 2013 +0200 (2013-08-28) changeset 53253 220f306f5c4e parent 53252 4766fbe322b5 child 53254 082d0972096b
tuned proofs;
```     1.1 --- a/src/HOL/Multivariate_Analysis/Determinants.thy	Wed Aug 28 22:50:23 2013 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Wed Aug 28 23:41:21 2013 +0200
1.3 @@ -11,14 +11,18 @@
1.4  begin
1.5
1.6  subsection{* First some facts about products*}
1.7 -lemma setprod_insert_eq: "finite A \<Longrightarrow> setprod f (insert a A) = (if a \<in> A then setprod f A else f a * setprod f A)"
1.8 -apply clarsimp
1.9 -by(subgoal_tac "insert a A = A", auto)
1.10 +
1.11 +lemma setprod_insert_eq:
1.12 +  "finite A \<Longrightarrow> setprod f (insert a A) = (if a \<in> A then setprod f A else f a * setprod f A)"
1.13 +  apply clarsimp
1.14 +  apply (subgoal_tac "insert a A = A")
1.15 +  apply auto
1.16 +  done
1.17
1.19    assumes mn: "(m::nat) <= n + 1"
1.20    shows "setprod f {m.. n+p} = setprod f {m .. n} * setprod f {n+1..n+p}"
1.21 -proof-
1.22 +proof -
1.23    let ?A = "{m .. n+p}"
1.24    let ?B = "{m .. n}"
1.25    let ?C = "{n+1..n+p}"
1.26 @@ -30,47 +34,56 @@
1.27
1.28
1.29  lemma setprod_offset: "setprod f {(m::nat) + p .. n + p} = setprod (\<lambda>i. f (i + p)) {m..n}"
1.30 -apply (rule setprod_reindex_cong[where f="op + p"])
1.31 -apply (auto simp add: image_iff Bex_def inj_on_def)
1.32 -apply arith
1.33 -apply (rule ext)
1.35 -done
1.36 +  apply (rule setprod_reindex_cong[where f="op + p"])
1.37 +  apply (auto simp add: image_iff Bex_def inj_on_def)
1.38 +  apply presburger
1.39 +  apply (rule ext)
1.41 +  done
1.42
1.43 -lemma setprod_singleton: "setprod f {x} = f x" by simp
1.44 -
1.45 -lemma setprod_singleton_nat_seg: "setprod f {n..n} = f (n::'a::order)" by simp
1.46 +lemma setprod_singleton: "setprod f {x} = f x"
1.47 +  by simp
1.48
1.49 -lemma setprod_numseg: "setprod f {m..0} = (if m=0 then f 0 else 1)"
1.50 -  "setprod f {m .. Suc n} = (if m \<le> Suc n then f (Suc n) * setprod f {m..n}
1.51 -                             else setprod f {m..n})"
1.52 +lemma setprod_singleton_nat_seg: "setprod f {n..n} = f (n::'a::order)"
1.53 +  by simp
1.54 +
1.55 +lemma setprod_numseg:
1.56 +  "setprod f {m..0} = (if m = 0 then f 0 else 1)"
1.57 +  "setprod f {m .. Suc n} =
1.58 +    (if m \<le> Suc n then f (Suc n) * setprod f {m..n} else setprod f {m..n})"
1.59    by (auto simp add: atLeastAtMostSuc_conv)
1.60
1.61 -lemma setprod_le: assumes fS: "finite S" and fg: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> (g x :: 'a::linordered_idom)"
1.62 +lemma setprod_le:
1.63 +  assumes fS: "finite S"
1.64 +    and fg: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> (g x :: 'a::linordered_idom)"
1.65    shows "setprod f S \<le> setprod g S"
1.66 -using fS fg
1.67 -apply(induct S)
1.68 -apply simp
1.69 -apply auto
1.70 -apply (rule mult_mono)
1.71 -apply (auto intro: setprod_nonneg)
1.72 -done
1.73 +  using fS fg
1.74 +  apply (induct S)
1.75 +  apply simp
1.76 +  apply auto
1.77 +  apply (rule mult_mono)
1.78 +  apply (auto intro: setprod_nonneg)
1.79 +  done
1.80
1.81    (* FIXME: In Finite_Set there is a useless further assumption *)
1.82 -lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: field_inverse_zero)"
1.83 +lemma setprod_inversef:
1.84 +  "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: field_inverse_zero)"
1.85    apply (erule finite_induct)
1.86    apply (simp)
1.87    apply simp
1.88    done
1.89
1.90 -lemma setprod_le_1: assumes fS: "finite S" and f: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> (1::'a::linordered_idom)"
1.91 +lemma setprod_le_1:
1.92 +  assumes fS: "finite S"
1.93 +    and f: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> (1::'a::linordered_idom)"
1.94    shows "setprod f S \<le> 1"
1.95 -using setprod_le[OF fS f] unfolding setprod_1 .
1.96 +  using setprod_le[OF fS f] unfolding setprod_1 .
1.97
1.98 -subsection{* Trace *}
1.99 +
1.100 +subsection {* Trace *}
1.101
1.102 -definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a" where
1.103 -  "trace A = setsum (\<lambda>i. ((A\$i)\$i)) (UNIV::'n set)"
1.104 +definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a"
1.105 +  where "trace A = setsum (\<lambda>i. ((A\$i)\$i)) (UNIV::'n set)"
1.106
1.107  lemma trace_0: "trace(mat 0) = 0"
1.108    by (simp add: trace_def mat_def)
1.109 @@ -87,14 +100,17 @@
1.110  lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)"
1.111    apply (simp add: trace_def matrix_matrix_mult_def)
1.112    apply (subst setsum_commute)
1.113 -  by (simp add: mult_commute)
1.114 +  apply (simp add: mult_commute)
1.115 +  done
1.116
1.117  (* ------------------------------------------------------------------------- *)
1.118  (* Definition of determinant.                                                *)
1.119  (* ------------------------------------------------------------------------- *)
1.120
1.121  definition det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where
1.122 -  "det A = setsum (\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A\$i\$p i) (UNIV :: 'n set)) {p. p permutes (UNIV :: 'n set)}"
1.123 +  "det A =
1.124 +    setsum (\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A\$i\$p i) (UNIV :: 'n set))
1.125 +      {p. p permutes (UNIV :: 'n set)}"
1.126
1.127  (* ------------------------------------------------------------------------- *)
1.128  (* A few general lemmas we need below.                                       *)
1.129 @@ -105,7 +121,8 @@
1.130    shows "setprod f S = setprod (f o p) S"
1.131    using assms by (fact setprod.permute)
1.132
1.133 -lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}"
1.134 +lemma setproduct_permute_nat_interval:
1.135 +  "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}"
1.136    by (blast intro!: setprod_permute)
1.137
1.138  (* ------------------------------------------------------------------------- *)
1.139 @@ -113,52 +130,71 @@
1.140  (* ------------------------------------------------------------------------- *)
1.141
1.142  lemma det_transpose: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)"
1.143 -proof-
1.144 +proof -
1.145    let ?di = "\<lambda>A i j. A\$i\$j"
1.146    let ?U = "(UNIV :: 'n set)"
1.147    have fU: "finite ?U" by simp
1.148 -  {fix p assume p: "p \<in> {p. p permutes ?U}"
1.149 +  {
1.150 +    fix p
1.151 +    assume p: "p \<in> {p. p permutes ?U}"
1.152      from p have pU: "p permutes ?U" by blast
1.153      have sth: "sign (inv p) = sign p"
1.154        by (metis sign_inverse fU p mem_Collect_eq permutation_permutes)
1.155      from permutes_inj[OF pU]
1.156      have pi: "inj_on p ?U" by (blast intro: subset_inj_on)
1.157      from permutes_image[OF pU]
1.158 -    have "setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U = setprod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)" by simp
1.159 +    have "setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U =
1.160 +      setprod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)" by simp
1.161      also have "\<dots> = setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) o p) ?U"
1.162        unfolding setprod_reindex[OF pi] ..
1.163      also have "\<dots> = setprod (\<lambda>i. ?di A i (p i)) ?U"
1.164 -    proof-
1.165 -      {fix i assume i: "i \<in> ?U"
1.166 +    proof -
1.167 +      {
1.168 +        fix i
1.169 +        assume i: "i \<in> ?U"
1.170          from i permutes_inv_o[OF pU] permutes_in_image[OF pU]
1.171          have "((\<lambda>i. ?di (transpose A) i (inv p i)) o p) i = ?di A i (p i)"
1.172 -          unfolding transpose_def by (simp add: fun_eq_iff)}
1.173 -      then show "setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) o p) ?U = setprod (\<lambda>i. ?di A i (p i)) ?U" by (auto intro: setprod_cong)
1.174 +          unfolding transpose_def by (simp add: fun_eq_iff)
1.175 +      }
1.176 +      then show "setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) o p) ?U =
1.177 +        setprod (\<lambda>i. ?di A i (p i)) ?U" by (auto intro: setprod_cong)
1.178      qed
1.179 -    finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)" using sth
1.180 -      by simp}
1.181 -  then show ?thesis unfolding det_def apply (subst setsum_permutations_inverse)
1.182 -  apply (rule setsum_cong2) by blast
1.183 +    finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) =
1.184 +      of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)" using sth by simp
1.185 +  }
1.186 +  then show ?thesis
1.187 +    unfolding det_def
1.188 +    apply (subst setsum_permutations_inverse)
1.189 +    apply (rule setsum_cong2)
1.190 +    apply blast
1.191 +    done
1.192  qed
1.193
1.194  lemma det_lowerdiagonal:
1.195    fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})"
1.196    assumes ld: "\<And>i j. i < j \<Longrightarrow> A\$i\$j = 0"
1.197    shows "det A = setprod (\<lambda>i. A\$i\$i) (UNIV:: 'n set)"
1.198 -proof-
1.199 +proof -
1.200    let ?U = "UNIV:: 'n set"
1.201    let ?PU = "{p. p permutes ?U}"
1.202    let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A\$i\$p i) (UNIV :: 'n set)"
1.203    have fU: "finite ?U" by simp
1.204    from finite_permutations[OF fU] have fPU: "finite ?PU" .
1.205    have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id)
1.206 -  {fix p assume p: "p \<in> ?PU -{id}"
1.207 -    from p have pU: "p permutes ?U" and pid: "p \<noteq> id" by blast+
1.208 -    from permutes_natset_le[OF pU] pid obtain i where
1.209 -      i: "p i > i" by (metis not_le)
1.210 -    from ld[OF i] have ex:"\<exists>i \<in> ?U. A\$i\$p i = 0" by blast
1.211 -    from setprod_zero[OF fU ex] have "?pp p = 0" by simp}
1.212 -  then have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0"  by blast
1.213 +  {
1.214 +    fix p
1.215 +    assume p: "p \<in> ?PU -{id}"
1.216 +    from p have pU: "p permutes ?U" and pid: "p \<noteq> id"
1.217 +      by blast+
1.218 +    from permutes_natset_le[OF pU] pid obtain i where i: "p i > i"
1.219 +      by (metis not_le)
1.220 +    from ld[OF i] have ex:"\<exists>i \<in> ?U. A\$i\$p i = 0"
1.221 +      by blast
1.222 +    from setprod_zero[OF fU ex] have "?pp p = 0"
1.223 +      by simp
1.224 +  }
1.225 +  then have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0"
1.226 +    by blast
1.227    from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis
1.228      unfolding det_def by (simp add: sign_id)
1.229  qed
1.230 @@ -167,21 +203,26 @@
1.231    fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}"
1.232    assumes ld: "\<And>i j. i > j \<Longrightarrow> A\$i\$j = 0"
1.233    shows "det A = setprod (\<lambda>i. A\$i\$i) (UNIV:: 'n set)"
1.234 -proof-
1.235 +proof -
1.236    let ?U = "UNIV:: 'n set"
1.237    let ?PU = "{p. p permutes ?U}"
1.238    let ?pp = "(\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A\$i\$p i) (UNIV :: 'n set))"
1.239    have fU: "finite ?U" by simp
1.240    from finite_permutations[OF fU] have fPU: "finite ?PU" .
1.241    have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id)
1.242 -  {fix p assume p: "p \<in> ?PU -{id}"
1.243 -    from p have pU: "p permutes ?U" and pid: "p \<noteq> id" by blast+
1.244 -    from permutes_natset_ge[OF pU] pid obtain i where
1.245 -      i: "p i < i" by (metis not_le)
1.246 +  {
1.247 +    fix p
1.248 +    assume p: "p \<in> ?PU -{id}"
1.249 +    from p have pU: "p permutes ?U" and pid: "p \<noteq> id"
1.250 +      by blast+
1.251 +    from permutes_natset_ge[OF pU] pid obtain i where i: "p i < i"
1.252 +      by (metis not_le)
1.253      from ld[OF i] have ex:"\<exists>i \<in> ?U. A\$i\$p i = 0" by blast
1.254 -    from setprod_zero[OF fU ex] have "?pp p = 0" by simp}
1.255 -  then have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0"  by blast
1.256 -  from   setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis
1.257 +    from setprod_zero[OF fU ex] have "?pp p = 0" by simp
1.258 +  }
1.259 +  then have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0"
1.260 +    by blast
1.261 +  from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis
1.262      unfolding det_def by (simp add: sign_id)
1.263  qed
1.264
1.265 @@ -189,14 +230,16 @@
1.266    fixes A :: "'a::comm_ring_1^'n^'n"
1.267    assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A\$i\$j = 0"
1.268    shows "det A = setprod (\<lambda>i. A\$i\$i) (UNIV::'n set)"
1.269 -proof-
1.270 +proof -
1.271    let ?U = "UNIV:: 'n set"
1.272    let ?PU = "{p. p permutes ?U}"
1.273    let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A\$i\$p i) (UNIV :: 'n set)"
1.274    have fU: "finite ?U" by simp
1.275    from finite_permutations[OF fU] have fPU: "finite ?PU" .
1.276    have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id)
1.277 -  {fix p assume p: "p \<in> ?PU - {id}"
1.278 +  {
1.279 +    fix p
1.280 +    assume p: "p \<in> ?PU - {id}"
1.281      then have "p \<noteq> id" by simp
1.282      then obtain i where i: "p i \<noteq> i" unfolding fun_eq_iff by auto
1.283      from ld [OF i [symmetric]] have ex:"\<exists>i \<in> ?U. A\$i\$p i = 0" by blast
1.284 @@ -207,16 +250,22 @@
1.285  qed
1.286
1.287  lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1"
1.288 -proof-
1.289 +proof -
1.290    let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n"
1.291    let ?U = "UNIV :: 'n set"
1.292    let ?f = "\<lambda>i j. ?A\$i\$j"
1.293 -  {fix i assume i: "i \<in> ?U"
1.294 -    have "?f i i = 1" using i by (vector mat_def)}
1.295 -  hence th: "setprod (\<lambda>i. ?f i i) ?U = setprod (\<lambda>x. 1) ?U"
1.296 +  {
1.297 +    fix i
1.298 +    assume i: "i \<in> ?U"
1.299 +    have "?f i i = 1" using i by (vector mat_def)
1.300 +  }
1.301 +  then have th: "setprod (\<lambda>i. ?f i i) ?U = setprod (\<lambda>x. 1) ?U"
1.302      by (auto intro: setprod_cong)
1.303 -  {fix i j assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i \<noteq> j"
1.304 -    have "?f i j = 0" using i j ij by (vector mat_def) }
1.305 +  {
1.306 +    fix i j
1.307 +    assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i \<noteq> j"
1.308 +    have "?f i j = 0" using i j ij by (vector mat_def)
1.309 +  }
1.310    then have "det ?A = setprod (\<lambda>i. ?f i i) ?U" using det_diagonal
1.311      by blast
1.312    also have "\<dots> = 1" unfolding th setprod_1 ..
1.313 @@ -232,23 +281,27 @@
1.314    shows "det(\<chi> i. A\$p i :: 'a^'n^'n) = of_int (sign p) * det A"
1.315    apply (simp add: det_def setsum_right_distrib mult_assoc[symmetric])
1.316    apply (subst sum_permutations_compose_right[OF p])
1.317 -proof(rule setsum_cong2)
1.318 +proof (rule setsum_cong2)
1.319    let ?U = "UNIV :: 'n set"
1.320    let ?PU = "{p. p permutes ?U}"
1.321 -  fix q assume qPU: "q \<in> ?PU"
1.322 +  fix q
1.323 +  assume qPU: "q \<in> ?PU"
1.324    have fU: "finite ?U" by simp
1.325 -  from qPU have q: "q permutes ?U" by blast
1.326 +  from qPU have q: "q permutes ?U"
1.327 +    by blast
1.328    from p q have pp: "permutation p" and qp: "permutation q"
1.329      by (metis fU permutation_permutes)+
1.330    from permutes_inv[OF p] have ip: "inv p permutes ?U" .
1.331 -    have "setprod (\<lambda>i. A\$p i\$ (q o p) i) ?U = setprod ((\<lambda>i. A\$p i\$(q o p) i) o inv p) ?U"
1.332 -      by (simp only: setprod_permute[OF ip, symmetric])
1.333 -    also have "\<dots> = setprod (\<lambda>i. A \$ (p o inv p) i \$ (q o (p o inv p)) i) ?U"
1.334 -      by (simp only: o_def)
1.335 -    also have "\<dots> = setprod (\<lambda>i. A\$i\$q i) ?U" by (simp only: o_def permutes_inverses[OF p])
1.336 -    finally   have thp: "setprod (\<lambda>i. A\$p i\$ (q o p) i) ?U = setprod (\<lambda>i. A\$i\$q i) ?U"
1.337 -      by blast
1.338 -  show "of_int (sign (q o p)) * setprod (\<lambda>i. A\$ p i\$ (q o p) i) ?U = of_int (sign p) * of_int (sign q) * setprod (\<lambda>i. A\$i\$q i) ?U"
1.339 +  have "setprod (\<lambda>i. A\$p i\$ (q o p) i) ?U = setprod ((\<lambda>i. A\$p i\$(q o p) i) o inv p) ?U"
1.340 +    by (simp only: setprod_permute[OF ip, symmetric])
1.341 +  also have "\<dots> = setprod (\<lambda>i. A \$ (p o inv p) i \$ (q o (p o inv p)) i) ?U"
1.342 +    by (simp only: o_def)
1.343 +  also have "\<dots> = setprod (\<lambda>i. A\$i\$q i) ?U"
1.344 +    by (simp only: o_def permutes_inverses[OF p])
1.345 +  finally have thp: "setprod (\<lambda>i. A\$p i\$ (q o p) i) ?U = setprod (\<lambda>i. A\$i\$q i) ?U"
1.346 +    by blast
1.347 +  show "of_int (sign (q o p)) * setprod (\<lambda>i. A\$ p i\$ (q o p) i) ?U =
1.348 +    of_int (sign p) * of_int (sign q) * setprod (\<lambda>i. A\$i\$q i) ?U"
1.349      by (simp only: thp sign_compose[OF qp pp] mult_commute of_int_mult)
1.350  qed
1.351
1.352 @@ -256,7 +309,7 @@
1.353    fixes A :: "'a::comm_ring_1^'n^'n"
1.354    assumes p: "p permutes (UNIV :: 'n set)"
1.355    shows "det(\<chi> i j. A\$i\$ p j :: 'a^'n^'n) = of_int (sign p) * det A"
1.356 -proof-
1.357 +proof -
1.358    let ?Ap = "\<chi> i j. A\$i\$ p j :: 'a^'n^'n"
1.359    let ?At = "transpose A"
1.360    have "of_int (sign p) * det A = det (transpose (\<chi> i. transpose A \$ p i))"
1.361 @@ -270,16 +323,16 @@
1.362  lemma det_identical_rows:
1.363    fixes A :: "'a::linordered_idom^'n^'n"
1.364    assumes ij: "i \<noteq> j"
1.365 -  and r: "row i A = row j A"
1.366 +    and r: "row i A = row j A"
1.367    shows "det A = 0"
1.368  proof-
1.369 -  have tha: "\<And>(a::'a) b. a = b ==> b = - a ==> a = 0"
1.370 +  have tha: "\<And>(a::'a) b. a = b \<Longrightarrow> b = - a \<Longrightarrow> a = 0"
1.371      by simp
1.372    have th1: "of_int (-1) = - 1" by simp
1.373    let ?p = "Fun.swap i j id"
1.374    let ?A = "\<chi> i. A \$ ?p i"
1.375    from r have "A = ?A" by (simp add: vec_eq_iff row_def swap_def)
1.376 -  hence "det A = det ?A" by simp
1.377 +  then have "det A = det ?A" by simp
1.378    moreover have "det A = - det ?A"
1.379      by (simp add: det_permute_rows[OF permutes_swap_id] sign_swap_id ij th1)
1.380    ultimately show "det A = 0" by (metis tha)
1.381 @@ -288,21 +341,22 @@
1.382  lemma det_identical_columns:
1.383    fixes A :: "'a::linordered_idom^'n^'n"
1.384    assumes ij: "i \<noteq> j"
1.385 -  and r: "column i A = column j A"
1.386 +    and r: "column i A = column j A"
1.387    shows "det A = 0"
1.388 -apply (subst det_transpose[symmetric])
1.389 -apply (rule det_identical_rows[OF ij])
1.390 -by (metis row_transpose r)
1.391 +  apply (subst det_transpose[symmetric])
1.392 +  apply (rule det_identical_rows[OF ij])
1.393 +  apply (metis row_transpose r)
1.394 +  done
1.395
1.396  lemma det_zero_row:
1.397    fixes A :: "'a::{idom, ring_char_0}^'n^'n"
1.398    assumes r: "row i A = 0"
1.399    shows "det A = 0"
1.400 -using r
1.401 -apply (simp add: row_def det_def vec_eq_iff)
1.402 -apply (rule setsum_0')
1.403 -apply (auto simp: sign_nz)
1.404 -done
1.405 +  using r
1.406 +  apply (simp add: row_def det_def vec_eq_iff)
1.407 +  apply (rule setsum_0')
1.408 +  apply (auto simp: sign_nz)
1.409 +  done
1.410
1.411  lemma det_zero_column:
1.412    fixes A :: "'a::{idom,ring_char_0}^'n^'n"
1.413 @@ -310,27 +364,32 @@
1.414    shows "det A = 0"
1.415    apply (subst det_transpose[symmetric])
1.416    apply (rule det_zero_row [of i])
1.417 -  by (metis row_transpose r)
1.418 +  apply (metis row_transpose r)
1.419 +  done
1.420
1.422    fixes a b c :: "'n::finite \<Rightarrow> _ ^ 'n"
1.423    shows "det((\<chi> i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) =
1.424 -             det((\<chi> i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) +
1.425 -             det((\<chi> i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)"
1.427 +    det((\<chi> i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) +
1.428 +    det((\<chi> i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)"
1.429 +    unfolding det_def vec_lambda_beta setsum_addf[symmetric]
1.430  proof (rule setsum_cong2)
1.431    let ?U = "UNIV :: 'n set"
1.432    let ?pU = "{p. p permutes ?U}"
1.433    let ?f = "(\<lambda>i. if i = k then a i + b i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n"
1.434    let ?g = "(\<lambda> i. if i = k then a i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n"
1.435    let ?h = "(\<lambda> i. if i = k then b i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n"
1.436 -  fix p assume p: "p \<in> ?pU"
1.437 +  fix p
1.438 +  assume p: "p \<in> ?pU"
1.439    let ?Uk = "?U - {k}"
1.440    from p have pU: "p permutes ?U" by blast
1.441    have kU: "?U = insert k ?Uk" by blast
1.442 -  {fix j assume j: "j \<in> ?Uk"
1.443 +  {
1.444 +    fix j
1.445 +    assume j: "j \<in> ?Uk"
1.446      from j have "?f j \$ p j = ?g j \$ p j" and "?f j \$ p j= ?h j \$ p j"
1.447 -      by simp_all}
1.448 +      by simp_all
1.449 +  }
1.450    then have th1: "setprod (\<lambda>i. ?f i \$ p i) ?Uk = setprod (\<lambda>i. ?g i \$ p i) ?Uk"
1.451      and th2: "setprod (\<lambda>i. ?f i \$ p i) ?Uk = setprod (\<lambda>i. ?h i \$ p i) ?Uk"
1.452      apply -
1.453 @@ -342,36 +401,45 @@
1.454    also have "\<dots> = ?f k \$ p k  * setprod (\<lambda>i. ?f i \$ p i) ?Uk"
1.455      apply (rule setprod_insert)
1.456      apply simp
1.457 -    by blast
1.458 -  also have "\<dots> = (a k \$ p k * setprod (\<lambda>i. ?f i \$ p i) ?Uk) + (b k\$ p k * setprod (\<lambda>i. ?f i \$ p i) ?Uk)" by (simp add: field_simps)
1.459 -  also have "\<dots> = (a k \$ p k * setprod (\<lambda>i. ?g i \$ p i) ?Uk) + (b k\$ p k * setprod (\<lambda>i. ?h i \$ p i) ?Uk)" by (metis th1 th2)
1.460 +    apply blast
1.461 +    done
1.462 +  also have "\<dots> = (a k \$ p k * setprod (\<lambda>i. ?f i \$ p i) ?Uk) + (b k\$ p k * setprod (\<lambda>i. ?f i \$ p i) ?Uk)"
1.463 +    by (simp add: field_simps)
1.464 +  also have "\<dots> = (a k \$ p k * setprod (\<lambda>i. ?g i \$ p i) ?Uk) + (b k\$ p k * setprod (\<lambda>i. ?h i \$ p i) ?Uk)"
1.465 +    by (metis th1 th2)
1.466    also have "\<dots> = setprod (\<lambda>i. ?g i \$ p i) (insert k ?Uk) + setprod (\<lambda>i. ?h i \$ p i) (insert k ?Uk)"
1.467      unfolding  setprod_insert[OF th3] by simp
1.468 -  finally have "setprod (\<lambda>i. ?f i \$ p i) ?U = setprod (\<lambda>i. ?g i \$ p i) ?U + setprod (\<lambda>i. ?h i \$ p i) ?U" unfolding kU[symmetric] .
1.469 -  then show "of_int (sign p) * setprod (\<lambda>i. ?f i \$ p i) ?U = of_int (sign p) * setprod (\<lambda>i. ?g i \$ p i) ?U + of_int (sign p) * setprod (\<lambda>i. ?h i \$ p i) ?U"
1.470 +  finally have "setprod (\<lambda>i. ?f i \$ p i) ?U =
1.471 +    setprod (\<lambda>i. ?g i \$ p i) ?U + setprod (\<lambda>i. ?h i \$ p i) ?U" unfolding kU[symmetric] .
1.472 +  then show "of_int (sign p) * setprod (\<lambda>i. ?f i \$ p i) ?U =
1.473 +    of_int (sign p) * setprod (\<lambda>i. ?g i \$ p i) ?U + of_int (sign p) * setprod (\<lambda>i. ?h i \$ p i) ?U"
1.475  qed
1.476
1.477  lemma det_row_mul:
1.478    fixes a b :: "'n::finite \<Rightarrow> _ ^ 'n"
1.479    shows "det((\<chi> i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) =
1.480 -             c* det((\<chi> i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)"
1.481 -
1.482 -unfolding det_def vec_lambda_beta setsum_right_distrib
1.483 +    c * det((\<chi> i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)"
1.484 +  unfolding det_def vec_lambda_beta setsum_right_distrib
1.485  proof (rule setsum_cong2)
1.486    let ?U = "UNIV :: 'n set"
1.487    let ?pU = "{p. p permutes ?U}"
1.488    let ?f = "(\<lambda>i. if i = k then c*s a i else b i)::'n \<Rightarrow> 'a::comm_ring_1^'n"
1.489    let ?g = "(\<lambda> i. if i = k then a i else b i)::'n \<Rightarrow> 'a::comm_ring_1^'n"
1.490 -  fix p assume p: "p \<in> ?pU"
1.491 +  fix p
1.492 +  assume p: "p \<in> ?pU"
1.493    let ?Uk = "?U - {k}"
1.494    from p have pU: "p permutes ?U" by blast
1.495    have kU: "?U = insert k ?Uk" by blast
1.496 -  {fix j assume j: "j \<in> ?Uk"
1.497 -    from j have "?f j \$ p j = ?g j \$ p j" by simp}
1.498 +  {
1.499 +    fix j
1.500 +    assume j: "j \<in> ?Uk"
1.501 +    from j have "?f j \$ p j = ?g j \$ p j" by simp
1.502 +  }
1.503    then have th1: "setprod (\<lambda>i. ?f i \$ p i) ?Uk = setprod (\<lambda>i. ?g i \$ p i) ?Uk"
1.504      apply -
1.505 -    apply (rule setprod_cong, simp_all)
1.506 +    apply (rule setprod_cong)
1.507 +    apply simp_all
1.508      done
1.509    have th3: "finite ?Uk" "k \<notin> ?Uk" by auto
1.510    have "setprod (\<lambda>i. ?f i \$ p i) ?U = setprod (\<lambda>i. ?f i \$ p i) (insert k ?Uk)"
1.511 @@ -379,29 +447,34 @@
1.512    also have "\<dots> = ?f k \$ p k  * setprod (\<lambda>i. ?f i \$ p i) ?Uk"
1.513      apply (rule setprod_insert)
1.514      apply simp
1.515 -    by blast
1.516 -  also have "\<dots> = (c*s a k) \$ p k * setprod (\<lambda>i. ?f i \$ p i) ?Uk" by (simp add: field_simps)
1.517 +    apply blast
1.518 +    done
1.519 +  also have "\<dots> = (c*s a k) \$ p k * setprod (\<lambda>i. ?f i \$ p i) ?Uk"
1.520 +    by (simp add: field_simps)
1.521    also have "\<dots> = c* (a k \$ p k * setprod (\<lambda>i. ?g i \$ p i) ?Uk)"
1.522      unfolding th1 by (simp add: mult_ac)
1.523    also have "\<dots> = c* (setprod (\<lambda>i. ?g i \$ p i) (insert k ?Uk))"
1.524 -    unfolding  setprod_insert[OF th3] by simp
1.525 -  finally have "setprod (\<lambda>i. ?f i \$ p i) ?U = c* (setprod (\<lambda>i. ?g i \$ p i) ?U)" unfolding kU[symmetric] .
1.526 -  then show "of_int (sign p) * setprod (\<lambda>i. ?f i \$ p i) ?U = c * (of_int (sign p) * setprod (\<lambda>i. ?g i \$ p i) ?U)"
1.527 +    unfolding setprod_insert[OF th3] by simp
1.528 +  finally have "setprod (\<lambda>i. ?f i \$ p i) ?U = c* (setprod (\<lambda>i. ?g i \$ p i) ?U)"
1.529 +    unfolding kU[symmetric] .
1.530 +  then show "of_int (sign p) * setprod (\<lambda>i. ?f i \$ p i) ?U =
1.531 +    c * (of_int (sign p) * setprod (\<lambda>i. ?g i \$ p i) ?U)"
1.533  qed
1.534
1.535  lemma det_row_0:
1.536    fixes b :: "'n::finite \<Rightarrow> _ ^ 'n"
1.537    shows "det((\<chi> i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0"
1.538 -using det_row_mul[of k 0 "\<lambda>i. 1" b]
1.539 -apply (simp)
1.540 -  unfolding vector_smult_lzero .
1.541 +  using det_row_mul[of k 0 "\<lambda>i. 1" b]
1.542 +  apply simp
1.543 +  apply (simp only: vector_smult_lzero)
1.544 +  done
1.545
1.546  lemma det_row_operation:
1.547    fixes A :: "'a::linordered_idom^'n^'n"
1.548    assumes ij: "i \<noteq> j"
1.549    shows "det (\<chi> k. if k = i then row i A + c *s row j A else row k A) = det A"
1.550 -proof-
1.551 +proof -
1.552    let ?Z = "(\<chi> k. if k = i then row j A else row k A) :: 'a ^'n^'n"
1.553    have th: "row i ?Z = row j ?Z" by (vector row_def)
1.554    have th2: "((\<chi> k. if k = i then row i A else row k A) :: 'a^'n^'n) = A"
1.555 @@ -415,30 +488,38 @@
1.556    fixes A :: "real^'n^'n"
1.557    assumes x: "x \<in> span {row j A |j. j \<noteq> i}"
1.558    shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A"
1.559 -proof-
1.560 +proof -
1.561    let ?U = "UNIV :: 'n set"
1.562    let ?S = "{row j A |j. j \<noteq> i}"
1.563    let ?d = "\<lambda>x. det (\<chi> k. if k = i then x else row k A)"
1.564    let ?P = "\<lambda>x. ?d (row i A + x) = det A"
1.565 -  {fix k
1.566 -
1.567 -    have "(if k = i then row i A + 0 else row k A) = row k A" by simp}
1.568 +  {
1.569 +    fix k
1.570 +    have "(if k = i then row i A + 0 else row k A) = row k A" by simp
1.571 +  }
1.572    then have P0: "?P 0"
1.573      apply -
1.574      apply (rule cong[of det, OF refl])
1.575 -    by (vector row_def)
1.576 +    apply (vector row_def)
1.577 +    done
1.578    moreover
1.579 -  {fix c z y assume zS: "z \<in> ?S" and Py: "?P y"
1.580 +  {
1.581 +    fix c z y
1.582 +    assume zS: "z \<in> ?S" and Py: "?P y"
1.583      from zS obtain j where j: "z = row j A" "i \<noteq> j" by blast
1.584      let ?w = "row i A + y"
1.585      have th0: "row i A + (c*s z + y) = ?w + c*s z" by vector
1.586      have thz: "?d z = 0"
1.587        apply (rule det_identical_rows[OF j(2)])
1.588 -      using j by (vector row_def)
1.589 -    have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" unfolding th0 ..
1.590 -    then have "?P (c*s z + y)" unfolding thz Py det_row_mul[of i] det_row_add[of i]
1.591 -      by simp }
1.592 -
1.593 +      using j
1.594 +      apply (vector row_def)
1.595 +      done
1.596 +    have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)"
1.597 +      unfolding th0 ..
1.598 +    then have "?P (c*s z + y)"
1.599 +      unfolding thz Py det_row_mul[of i] det_row_add[of i]
1.600 +      by simp
1.601 +  }
1.602    ultimately show ?thesis
1.603      apply -
1.604      apply (rule span_induct_alt[of ?P ?S, OF P0, folded scalar_mult_eq_scaleR])
1.605 @@ -456,53 +537,68 @@
1.606    fixes A:: "real^'n^'n"
1.607    assumes d: "dependent (rows A)"
1.608    shows "det A = 0"
1.609 -proof-
1.610 +proof -
1.611    let ?U = "UNIV :: 'n set"
1.612    from d obtain i where i: "row i A \<in> span (rows A - {row i A})"
1.613      unfolding dependent_def rows_def by blast
1.614 -  {fix j k assume jk: "j \<noteq> k"
1.615 -    and c: "row j A = row k A"
1.616 -    from det_identical_rows[OF jk c] have ?thesis .}
1.617 +  {
1.618 +    fix j k
1.619 +    assume jk: "j \<noteq> k" and c: "row j A = row k A"
1.620 +    from det_identical_rows[OF jk c] have ?thesis .
1.621 +  }
1.622    moreover
1.623 -  {assume H: "\<And> i j. i \<noteq> j \<Longrightarrow> row i A \<noteq> row j A"
1.624 +  {
1.625 +    assume H: "\<And> i j. i \<noteq> j \<Longrightarrow> row i A \<noteq> row j A"
1.626      have th0: "- row i A \<in> span {row j A|j. j \<noteq> i}"
1.627        apply (rule span_neg)
1.628        apply (rule set_rev_mp)
1.629        apply (rule i)
1.630        apply (rule span_mono)
1.631 -      using H i by (auto simp add: rows_def)
1.632 +      using H i
1.633 +      apply (auto simp add: rows_def)
1.634 +      done
1.635      from det_row_span[OF th0]
1.636      have "det A = det (\<chi> k. if k = i then 0 *s 1 else row k A)"
1.637        unfolding right_minus vector_smult_lzero ..
1.638      with det_row_mul[of i "0::real" "\<lambda>i. 1"]
1.639 -    have "det A = 0" by simp}
1.640 +    have "det A = 0" by simp
1.641 +  }
1.642    ultimately show ?thesis by blast
1.643  qed
1.644
1.645 -lemma det_dependent_columns: assumes d: "dependent(columns (A::real^'n^'n))" shows "det A = 0"
1.646 -by (metis d det_dependent_rows rows_transpose det_transpose)
1.647 +lemma det_dependent_columns:
1.648 +  assumes d: "dependent (columns (A::real^'n^'n))"
1.649 +  shows "det A = 0"
1.650 +  by (metis d det_dependent_rows rows_transpose det_transpose)
1.651
1.652  (* ------------------------------------------------------------------------- *)
1.653  (* Multilinearity and the multiplication formula.                            *)
1.654  (* ------------------------------------------------------------------------- *)
1.655
1.656  lemma Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)"
1.657 -  apply (rule iffD1[OF vec_lambda_unique]) by vector
1.658 +  by (rule iffD1[OF vec_lambda_unique]) vector
1.659
1.660  lemma det_linear_row_setsum:
1.661    assumes fS: "finite S"
1.662 -  shows "det ((\<chi> i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n) = setsum (\<lambda>j. det ((\<chi> i. if i = k then a  i j else c i)::'a^'n^'n)) S"
1.663 -proof(induct rule: finite_induct[OF fS])
1.664 -  case 1 thus ?case apply simp  unfolding setsum_empty det_row_0[of k] ..
1.665 +  shows "det ((\<chi> i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n) =
1.666 +    setsum (\<lambda>j. det ((\<chi> i. if i = k then a  i j else c i)::'a^'n^'n)) S"
1.667 +proof (induct rule: finite_induct[OF fS])
1.668 +  case 1
1.669 +  then show ?case
1.670 +    apply simp
1.671 +    unfolding setsum_empty det_row_0[of k]
1.672 +    apply rule
1.673 +    done
1.674  next
1.675    case (2 x F)
1.676 -  then  show ?case by (simp add: det_row_add cong del: if_weak_cong)
1.677 +  then show ?case
1.679  qed
1.680
1.681  lemma finite_bounded_functions:
1.682    assumes fS: "finite S"
1.683    shows "finite {f. (\<forall>i \<in> {1.. (k::nat)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1 .. k} \<longrightarrow> f i = i)}"
1.684 -proof(induct k)
1.685 +proof (induct k)
1.686    case 0
1.687    have th: "{f. \<forall>i. f i = i} = {id}" by auto
1.688    show ?case by (auto simp add: th)
1.689 @@ -526,13 +622,14 @@
1.690  lemma det_linear_rows_setsum_lemma:
1.691    assumes fS: "finite S" and fT: "finite T"
1.692    shows "det((\<chi> i. if i \<in> T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n) =
1.693 -             setsum (\<lambda>f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n))
1.694 -                 {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}"
1.695 -using fT
1.696 -proof(induct T arbitrary: a c set: finite)
1.697 +    setsum (\<lambda>f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n))
1.698 +      {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}"
1.699 +  using fT
1.700 +proof (induct T arbitrary: a c set: finite)
1.701    case empty
1.702 -  have th0: "\<And>x y. (\<chi> i. if i \<in> {} then x i else y i) = (\<chi> i. y i)" by vector
1.703 -  from "empty.prems"  show ?case unfolding th0 by simp
1.704 +  have th0: "\<And>x y. (\<chi> i. if i \<in> {} then x i else y i) = (\<chi> i. y i)"
1.705 +    by vector
1.706 +  from empty.prems show ?case unfolding th0 by simp
1.707  next
1.708    case (insert z T a c)
1.709    let ?F = "\<lambda>T. {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}"
1.710 @@ -540,42 +637,48 @@
1.711    let ?k = "\<lambda>h. (h(z),(\<lambda>i. if i = z then i else h i))"
1.712    let ?s = "\<lambda> k a c f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n)"
1.713    let ?c = "\<lambda>i. if i = z then a i j else c i"
1.714 -  have thif: "\<And>a b c d. (if a \<or> b then c else d) = (if a then c else if b then c else d)" by simp
1.715 +  have thif: "\<And>a b c d. (if a \<or> b then c else d) = (if a then c else if b then c else d)"
1.716 +    by simp
1.717    have thif2: "\<And>a b c d e. (if a then b else if c then d else e) =
1.718 -     (if c then (if a then b else d) else (if a then b else e))" by simp
1.719 -  from `z \<notin> T` have nz: "\<And>i. i \<in> T \<Longrightarrow> i = z \<longleftrightarrow> False" by auto
1.720 +     (if c then (if a then b else d) else (if a then b else e))"
1.721 +    by simp
1.722 +  from `z \<notin> T` have nz: "\<And>i. i \<in> T \<Longrightarrow> i = z \<longleftrightarrow> False"
1.723 +    by auto
1.724    have "det (\<chi> i. if i \<in> insert z T then setsum (a i) S else c i) =
1.725 -        det (\<chi> i. if i = z then setsum (a i) S
1.726 -                 else if i \<in> T then setsum (a i) S else c i)"
1.727 +    det (\<chi> i. if i = z then setsum (a i) S else if i \<in> T then setsum (a i) S else c i)"
1.728      unfolding insert_iff thif ..
1.729 -  also have "\<dots> = (\<Sum>j\<in>S. det (\<chi> i. if i \<in> T then setsum (a i) S
1.730 -                    else if i = z then a i j else c i))"
1.731 +  also have "\<dots> = (\<Sum>j\<in>S. det (\<chi> i. if i \<in> T then setsum (a i) S else if i = z then a i j else c i))"
1.732      unfolding det_linear_row_setsum[OF fS]
1.733      apply (subst thif2)
1.734 -    using nz by (simp cong del: if_weak_cong cong add: if_cong)
1.735 +    using nz
1.736 +    apply (simp cong del: if_weak_cong cong add: if_cong)
1.737 +    done
1.738    finally have tha:
1.739      "det (\<chi> i. if i \<in> insert z T then setsum (a i) S else c i) =
1.740       (\<Sum>(j, f)\<in>S \<times> ?F T. det (\<chi> i. if i \<in> T then a i (f i)
1.741                                  else if i = z then a i j
1.742                                  else c i))"
1.743 -    unfolding  insert.hyps unfolding setsum_cartesian_product by blast
1.744 +    unfolding insert.hyps unfolding setsum_cartesian_product by blast
1.745    show ?case unfolding tha
1.746 -    apply(rule setsum_eq_general_reverses[where h= "?h" and k= "?k"],
1.747 +    apply (rule setsum_eq_general_reverses[where h= "?h" and k= "?k"],
1.748        blast intro: finite_cartesian_product fS finite,
1.749        blast intro: finite_cartesian_product fS finite)
1.750      using `z \<notin> T`
1.751      apply auto
1.752      apply (rule cong[OF refl[of det]])
1.753 -    by vector
1.754 +    apply vector
1.755 +    done
1.756  qed
1.757
1.758  lemma det_linear_rows_setsum:
1.759    assumes fS: "finite (S::'n::finite set)"
1.760 -  shows "det (\<chi> i. setsum (a i) S) = setsum (\<lambda>f. det (\<chi> i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. \<forall>i. f i \<in> S}"
1.761 -proof-
1.762 -  have th0: "\<And>x y. ((\<chi> i. if i \<in> (UNIV:: 'n set) then x i else y i) :: 'a^'n^'n) = (\<chi> i. x i)" by vector
1.763 -
1.764 -  from det_linear_rows_setsum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite] show ?thesis by simp
1.765 +  shows "det (\<chi> i. setsum (a i) S) =
1.766 +    setsum (\<lambda>f. det (\<chi> i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. \<forall>i. f i \<in> S}"
1.767 +proof -
1.768 +  have th0: "\<And>x y. ((\<chi> i. if i \<in> (UNIV:: 'n set) then x i else y i) :: 'a^'n^'n) = (\<chi> i. x i)"
1.769 +    by vector
1.770 +  from det_linear_rows_setsum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite]
1.771 +  show ?thesis by simp
1.772  qed
1.773
1.774  lemma matrix_mul_setsum_alt:
1.775 @@ -585,75 +688,93 @@
1.776
1.777  lemma det_rows_mul:
1.778    "det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n) =
1.779 -  setprod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)"
1.780 +    setprod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)"
1.782    let ?U = "UNIV :: 'n set"
1.783    let ?PU = "{p. p permutes ?U}"
1.784 -  fix p assume pU: "p \<in> ?PU"
1.785 +  fix p
1.786 +  assume pU: "p \<in> ?PU"
1.787    let ?s = "of_int (sign p)"
1.788 -  from pU have p: "p permutes ?U" by blast
1.789 +  from pU have p: "p permutes ?U"
1.790 +    by blast
1.791    have "setprod (\<lambda>i. c i * a i \$ p i) ?U = setprod c ?U * setprod (\<lambda>i. a i \$ p i) ?U"
1.792      unfolding setprod_timesf ..
1.793    then show "?s * (\<Prod>xa\<in>?U. c xa * a xa \$ p xa) =
1.794 -        setprod c ?U * (?s* (\<Prod>xa\<in>?U. a xa \$ p xa))" by (simp add: field_simps)
1.795 +    setprod c ?U * (?s* (\<Prod>xa\<in>?U. a xa \$ p xa))" by (simp add: field_simps)
1.796  qed
1.797
1.798  lemma det_mul:
1.799    fixes A B :: "'a::linordered_idom^'n^'n"
1.800    shows "det (A ** B) = det A * det B"
1.801 -proof-
1.802 +proof -
1.803    let ?U = "UNIV :: 'n set"
1.804    let ?F = "{f. (\<forall>i\<in> ?U. f i \<in> ?U) \<and> (\<forall>i. i \<notin> ?U \<longrightarrow> f i = i)}"
1.805    let ?PU = "{p. p permutes ?U}"
1.806    have fU: "finite ?U" by simp
1.807    have fF: "finite ?F" by (rule finite)
1.808 -  {fix p assume p: "p permutes ?U"
1.809 -
1.810 +  {
1.811 +    fix p
1.812 +    assume p: "p permutes ?U"
1.813      have "p \<in> ?F" unfolding mem_Collect_eq permutes_in_image[OF p]
1.814 -      using p[unfolded permutes_def] by simp}
1.815 +      using p[unfolded permutes_def] by simp
1.816 +  }
1.817    then have PUF: "?PU \<subseteq> ?F"  by blast
1.818 -  {fix f assume fPU: "f \<in> ?F - ?PU"
1.819 +  {
1.820 +    fix f
1.821 +    assume fPU: "f \<in> ?F - ?PU"
1.822      have fUU: "f ` ?U \<subseteq> ?U" using fPU by auto
1.823 -    from fPU have f: "\<forall>i \<in> ?U. f i \<in> ?U"
1.824 -      "\<forall>i. i \<notin> ?U \<longrightarrow> f i = i" "\<not>(\<forall>y. \<exists>!x. f x = y)" unfolding permutes_def
1.825 -      by auto
1.826 +    from fPU have f: "\<forall>i \<in> ?U. f i \<in> ?U" "\<forall>i. i \<notin> ?U \<longrightarrow> f i = i" "\<not>(\<forall>y. \<exists>!x. f x = y)"
1.827 +      unfolding permutes_def by auto
1.828
1.829      let ?A = "(\<chi> i. A\$i\$f i *s B\$f i) :: 'a^'n^'n"
1.830      let ?B = "(\<chi> i. B\$f i) :: 'a^'n^'n"
1.831 -    {assume fni: "\<not> inj_on f ?U"
1.832 +    {
1.833 +      assume fni: "\<not> inj_on f ?U"
1.834        then obtain i j where ij: "f i = f j" "i \<noteq> j"
1.835          unfolding inj_on_def by blast
1.836        from ij
1.837        have rth: "row i ?B = row j ?B" by (vector row_def)
1.838        from det_identical_rows[OF ij(2) rth]
1.839        have "det (\<chi> i. A\$i\$f i *s B\$f i) = 0"
1.840 -        unfolding det_rows_mul by simp}
1.841 +        unfolding det_rows_mul by simp
1.842 +    }
1.843      moreover
1.844 -    {assume fi: "inj_on f ?U"
1.845 +    {
1.846 +      assume fi: "inj_on f ?U"
1.847        from f fi have fith: "\<And>i j. f i = f j \<Longrightarrow> i = j"
1.848          unfolding inj_on_def by metis
1.849        note fs = fi[unfolded surjective_iff_injective_gen[OF fU fU refl fUU, symmetric]]
1.850
1.851 -      {fix y
1.852 +      {
1.853 +        fix y
1.854          from fs f have "\<exists>x. f x = y" by blast
1.855          then obtain x where x: "f x = y" by blast
1.856 -        {fix z assume z: "f z = y" from fith x z have "z = x" by metis}
1.857 -        with x have "\<exists>!x. f x = y" by blast}
1.858 -      with f(3) have "det (\<chi> i. A\$i\$f i *s B\$f i) = 0" by blast}
1.859 -    ultimately have "det (\<chi> i. A\$i\$f i *s B\$f i) = 0" by blast}
1.860 -  hence zth: "\<forall> f\<in> ?F - ?PU. det (\<chi> i. A\$i\$f i *s B\$f i) = 0" by simp
1.861 -  {fix p assume pU: "p \<in> ?PU"
1.862 +        {
1.863 +          fix z
1.864 +          assume z: "f z = y"
1.865 +          from fith x z have "z = x" by metis
1.866 +        }
1.867 +        with x have "\<exists>!x. f x = y" by blast
1.868 +      }
1.869 +      with f(3) have "det (\<chi> i. A\$i\$f i *s B\$f i) = 0" by blast
1.870 +    }
1.871 +    ultimately have "det (\<chi> i. A\$i\$f i *s B\$f i) = 0" by blast
1.872 +  }
1.873 +  hence zth: "\<forall> f\<in> ?F - ?PU. det (\<chi> i. A\$i\$f i *s B\$f i) = 0"
1.874 +    by simp
1.875 +  {
1.876 +    fix p
1.877 +    assume pU: "p \<in> ?PU"
1.878      from pU have p: "p permutes ?U" by blast
1.879      let ?s = "\<lambda>p. of_int (sign p)"
1.880 -    let ?f = "\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A \$ i \$ p i) *
1.881 -               (?s q * (\<Prod>i\<in> ?U. B \$ i \$ q i))"
1.882 +    let ?f = "\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A \$ i \$ p i) * (?s q * (\<Prod>i\<in> ?U. B \$ i \$ q i))"
1.883      have "(setsum (\<lambda>q. ?s q *
1.884 -            (\<Prod>i\<in> ?U. (\<chi> i. A \$ i \$ p i *s B \$ p i :: 'a^'n^'n) \$ i \$ q i)) ?PU) =
1.885 -        (setsum (\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A \$ i \$ p i) *
1.886 -               (?s q * (\<Prod>i\<in> ?U. B \$ i \$ q i))) ?PU)"
1.887 +        (\<Prod>i\<in> ?U. (\<chi> i. A \$ i \$ p i *s B \$ p i :: 'a^'n^'n) \$ i \$ q i)) ?PU) =
1.888 +      (setsum (\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A \$ i \$ p i) * (?s q * (\<Prod>i\<in> ?U. B \$ i \$ q i))) ?PU)"
1.889        unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f]
1.890      proof(rule setsum_cong2)
1.891 -      fix q assume qU: "q \<in> ?PU"
1.892 +      fix q
1.893 +      assume qU: "q \<in> ?PU"
1.894        hence q: "q permutes ?U" by blast
1.895        from p q have pp: "permutation p" and pq: "permutation q"
1.896          unfolding permutation_permutes by auto
1.897 @@ -666,11 +787,15 @@
1.898          by (simp add:  th00 mult_ac sign_idempotent sign_compose)
1.899        have th001: "setprod (\<lambda>i. B\$i\$ q (inv p i)) ?U = setprod ((\<lambda>i. B\$i\$ q (inv p i)) o p) ?U"
1.900          by (rule setprod_permute[OF p])
1.901 -      have thp: "setprod (\<lambda>i. (\<chi> i. A\$i\$p i *s B\$p i :: 'a^'n^'n) \$i \$ q i) ?U = setprod (\<lambda>i. A\$i\$p i) ?U * setprod (\<lambda>i. B\$i\$ q (inv p i)) ?U"
1.902 +      have thp: "setprod (\<lambda>i. (\<chi> i. A\$i\$p i *s B\$p i :: 'a^'n^'n) \$i \$ q i) ?U =
1.903 +        setprod (\<lambda>i. A\$i\$p i) ?U * setprod (\<lambda>i. B\$i\$ q (inv p i)) ?U"
1.904          unfolding th001 setprod_timesf[symmetric] o_def permutes_inverses[OF p]
1.905          apply (rule setprod_cong[OF refl])
1.906 -        using permutes_in_image[OF q] by vector
1.907 -      show "?s q * setprod (\<lambda>i. (((\<chi> i. A\$i\$p i *s B\$p i) :: 'a^'n^'n)\$i\$q i)) ?U = ?s p * (setprod (\<lambda>i. A\$i\$p i) ?U) * (?s (q o inv p) * setprod (\<lambda>i. B\$i\$(q o inv p) i) ?U)"
1.908 +        using permutes_in_image[OF q]
1.909 +        apply vector
1.910 +        done
1.911 +      show "?s q * setprod (\<lambda>i. (((\<chi> i. A\$i\$p i *s B\$p i) :: 'a^'n^'n)\$i\$q i)) ?U =
1.912 +        ?s p * (setprod (\<lambda>i. A\$i\$p i) ?U) * (?s (q o inv p) * setprod (\<lambda>i. B\$i\$(q o inv p) i) ?U)"
1.913          using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp]
1.914          by (simp add: sign_nz th00 field_simps sign_idempotent sign_compose)
1.915      qed
1.916 @@ -703,22 +828,24 @@
1.917  lemma invertible_det_nz:
1.918    fixes A::"real ^'n^'n"
1.919    shows "invertible A \<longleftrightarrow> det A \<noteq> 0"
1.920 -proof-
1.921 -  {assume "invertible A"
1.922 +proof -
1.923 +  {
1.924 +    assume "invertible A"
1.925      then obtain B :: "real ^'n^'n" where B: "A ** B = mat 1"
1.926        unfolding invertible_righ_inverse by blast
1.927      hence "det (A ** B) = det (mat 1 :: real ^'n^'n)" by simp
1.928 -    hence "det A \<noteq> 0"
1.929 -      apply (simp add: det_mul det_I) by algebra }
1.930 +    hence "det A \<noteq> 0" by (simp add: det_mul det_I) algebra
1.931 +  }
1.932    moreover
1.933 -  {assume H: "\<not> invertible A"
1.934 +  {
1.935 +    assume H: "\<not> invertible A"
1.936      let ?U = "UNIV :: 'n set"
1.937      have fU: "finite ?U" by simp
1.938      from H obtain c i where c: "setsum (\<lambda>i. c i *s row i A) ?U = 0"
1.939        and iU: "i \<in> ?U" and ci: "c i \<noteq> 0"
1.940        unfolding invertible_righ_inverse
1.941        unfolding matrix_right_invertible_independent_rows by blast
1.942 -    have stupid: "\<And>(a::real^'n) b. a + b = 0 \<Longrightarrow> -a = b"
1.943 +    have *: "\<And>(a::real^'n) b. a + b = 0 \<Longrightarrow> -a = b"
1.944        apply (drule_tac f="op + (- a)" in cong[OF refl])
1.945        apply (simp only: ab_left_minus add_assoc[symmetric])
1.946        apply simp
1.947 @@ -729,7 +856,7 @@
1.948        apply -
1.949        apply (rule vector_mul_lcancel_imp[OF ci])
1.950        apply (auto simp add: field_simps)
1.951 -      unfolding stupid ..
1.952 +      unfolding * ..
1.953      have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}"
1.954        unfolding thr0
1.955        apply (rule span_setsum)
1.956 @@ -743,7 +870,8 @@
1.957      have thrb: "row i ?B = 0" using iU by (vector row_def)
1.958      have "det A = 0"
1.959        unfolding det_row_span[OF thr, symmetric] right_minus
1.960 -      unfolding  det_zero_row[OF thrb]  ..}
1.961 +      unfolding det_zero_row[OF thrb] ..
1.962 +  }
1.963    ultimately show ?thesis by blast
1.964  qed
1.965
1.966 @@ -756,7 +884,7 @@
1.967    shows "det ((\<chi> i. if i = k then setsum (\<lambda>i. x\$i *s row i A) (UNIV::'n set)
1.968                             else row i A)::real^'n^'n) = x\$k * det A"
1.969    (is "?lhs = ?rhs")
1.970 -proof-
1.971 +proof -
1.972    let ?U = "UNIV :: 'n set"
1.973    let ?Uk = "?U - {k}"
1.974    have U: "?U = insert k ?Uk" by blast
1.975 @@ -766,7 +894,8 @@
1.976      by (vector field_simps)
1.977    have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" by auto
1.978    have "(\<chi> i. row i A) = A" by (vector row_def)
1.979 -  then have thd1: "det (\<chi> i. row i A) = det A"  by simp
1.980 +  then have thd1: "det (\<chi> i. row i A) = det A"
1.981 +    by simp
1.982    have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x \$ i *s row i A) else row i A) = det A"
1.983      apply (rule det_row_span)
1.984      apply (rule span_setsum[OF fUk])
1.985 @@ -784,37 +913,44 @@
1.986      unfolding thd0
1.987      unfolding det_row_mul
1.988      unfolding th001[of k "\<lambda>i. row i A"]
1.989 -    unfolding thd1  by (simp add: field_simps)
1.990 +    unfolding thd1
1.991 +    apply (simp add: field_simps)
1.992 +    done
1.993  qed
1.994
1.995  lemma cramer_lemma:
1.996    fixes A :: "real^'n^'n"
1.997    shows "det((\<chi> i j. if j = k then (A *v x)\$i else A\$i\$j):: real^'n^'n) = x\$k * det A"
1.998 -proof-
1.999 +proof -
1.1000    let ?U = "UNIV :: 'n set"
1.1001 -  have stupid: "\<And>c. setsum (\<lambda>i. c i *s row i (transpose A)) ?U = setsum (\<lambda>i. c i *s column i A) ?U"
1.1002 +  have *: "\<And>c. setsum (\<lambda>i. c i *s row i (transpose A)) ?U = setsum (\<lambda>i. c i *s column i A) ?U"
1.1003      by (auto simp add: row_transpose intro: setsum_cong2)
1.1004    show ?thesis  unfolding matrix_mult_vsum
1.1005 -  unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric]
1.1006 -  unfolding stupid[of "\<lambda>i. x\$i"]
1.1007 -  apply (subst det_transpose[symmetric])
1.1008 -  apply (rule cong[OF refl[of det]]) by (vector transpose_def column_def row_def)
1.1009 +    unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric]
1.1010 +    unfolding *[of "\<lambda>i. x\$i"]
1.1011 +    apply (subst det_transpose[symmetric])
1.1012 +    apply (rule cong[OF refl[of det]])
1.1013 +    apply (vector transpose_def column_def row_def)
1.1014 +    done
1.1015  qed
1.1016
1.1017  lemma cramer:
1.1018    fixes A ::"real^'n^'n"
1.1019    assumes d0: "det A \<noteq> 0"
1.1020    shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b\$i else A\$i\$j) / det A)"
1.1021 -proof-
1.1022 +proof -
1.1023    from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1"
1.1024      unfolding invertible_det_nz[symmetric] invertible_def by blast
1.1025    have "(A ** B) *v b = b" by (simp add: B matrix_vector_mul_lid)
1.1026 -  hence "A *v (B *v b) = b" by (simp add: matrix_vector_mul_assoc)
1.1027 +  then have "A *v (B *v b) = b" by (simp add: matrix_vector_mul_assoc)
1.1028    then have xe: "\<exists>x. A*v x = b" by blast
1.1029 -  {fix x assume x: "A *v x = b"
1.1030 -  have "x = (\<chi> k. det(\<chi> i j. if j=k then b\$i else A\$i\$j) / det A)"
1.1031 -    unfolding x[symmetric]
1.1032 -    using d0 by (simp add: vec_eq_iff cramer_lemma field_simps)}
1.1033 +  {
1.1034 +    fix x
1.1035 +    assume x: "A *v x = b"
1.1036 +    have "x = (\<chi> k. det(\<chi> i j. if j=k then b\$i else A\$i\$j) / det A)"
1.1037 +      unfolding x[symmetric]
1.1038 +      using d0 by (simp add: vec_eq_iff cramer_lemma field_simps)
1.1039 +  }
1.1040    with xe show ?thesis by auto
1.1041  qed
1.1042
1.1043 @@ -824,16 +960,19 @@
1.1044
1.1045  definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
1.1046
1.1047 -lemma orthogonal_transformation: "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>(v::real ^_). norm (f v) = norm v)"
1.1048 +lemma orthogonal_transformation:
1.1049 +  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>(v::real ^_). norm (f v) = norm v)"
1.1050    unfolding orthogonal_transformation_def
1.1051    apply auto
1.1052    apply (erule_tac x=v in allE)+
1.1056 +  done
1.1057
1.1058 -definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
1.1059 +definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
1.1060 +  transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
1.1061
1.1062 -lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n)  \<longleftrightarrow> transpose Q ** Q = mat 1"
1.1063 +lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1"
1.1064    by (metis matrix_left_right_inverse orthogonal_matrix_def)
1.1065
1.1066  lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)"
1.1067 @@ -842,28 +981,31 @@
1.1068  lemma orthogonal_matrix_mul:
1.1069    fixes A :: "real ^'n^'n"
1.1070    assumes oA : "orthogonal_matrix A"
1.1071 -  and oB: "orthogonal_matrix B"
1.1072 +    and oB: "orthogonal_matrix B"
1.1073    shows "orthogonal_matrix(A ** B)"
1.1074    using oA oB
1.1075    unfolding orthogonal_matrix matrix_transpose_mul
1.1076    apply (subst matrix_mul_assoc)
1.1077    apply (subst matrix_mul_assoc[symmetric])
1.1078 -  by (simp add: matrix_mul_rid)
1.1079 +  apply (simp add: matrix_mul_rid)
1.1080 +  done
1.1081
1.1082  lemma orthogonal_transformation_matrix:
1.1083    fixes f:: "real^'n \<Rightarrow> real^'n"
1.1084    shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)"
1.1085    (is "?lhs \<longleftrightarrow> ?rhs")
1.1086 -proof-
1.1087 +proof -
1.1088    let ?mf = "matrix f"
1.1089    let ?ot = "orthogonal_transformation f"
1.1090    let ?U = "UNIV :: 'n set"
1.1091    have fU: "finite ?U" by simp
1.1092    let ?m1 = "mat 1 :: real ^'n^'n"
1.1093 -  {assume ot: ?ot
1.1094 +  {
1.1095 +    assume ot: ?ot
1.1096      from ot have lf: "linear f" and fd: "\<forall>v w. f v \<bullet> f w = v \<bullet> w"
1.1097        unfolding  orthogonal_transformation_def orthogonal_matrix by blast+
1.1098 -    {fix i j
1.1099 +    {
1.1100 +      fix i j
1.1101        let ?A = "transpose ?mf ** ?mf"
1.1102        have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)"
1.1103          "\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)"
1.1104 @@ -871,16 +1013,22 @@
1.1105        from fd[rule_format, of "axis i 1" "axis j 1", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul]
1.1106        have "?A\$i\$j = ?m1 \$ i \$ j"
1.1107          by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def
1.1108 -            th0 setsum_delta[OF fU] mat_def axis_def) }
1.1109 -    hence "orthogonal_matrix ?mf" unfolding orthogonal_matrix by vector
1.1110 -    with lf have ?rhs by blast}
1.1111 +            th0 setsum_delta[OF fU] mat_def axis_def)
1.1112 +    }
1.1113 +    then have "orthogonal_matrix ?mf" unfolding orthogonal_matrix
1.1114 +      by vector
1.1115 +    with lf have ?rhs by blast
1.1116 +  }
1.1117    moreover
1.1118 -  {assume lf: "linear f" and om: "orthogonal_matrix ?mf"
1.1119 +  {
1.1120 +    assume lf: "linear f" and om: "orthogonal_matrix ?mf"
1.1121      from lf om have ?lhs
1.1122        unfolding orthogonal_matrix_def norm_eq orthogonal_transformation
1.1123        unfolding matrix_works[OF lf, symmetric]
1.1124        apply (subst dot_matrix_vector_mul)
1.1125 -      by (simp add: dot_matrix_product matrix_mul_lid)}
1.1126 +      apply (simp add: dot_matrix_product matrix_mul_lid)
1.1127 +      done
1.1128 +  }
1.1129    ultimately show ?thesis by blast
1.1130  qed
1.1131
1.1132 @@ -888,21 +1036,26 @@
1.1133    fixes Q:: "'a::linordered_idom^'n^'n"
1.1134    assumes oQ: "orthogonal_matrix Q"
1.1135    shows "det Q = 1 \<or> det Q = - 1"
1.1136 -proof-
1.1137 -
1.1138 +proof -
1.1139    have th: "\<And>x::'a. x = 1 \<or> x = - 1 \<longleftrightarrow> x*x = 1" (is "\<And>x::'a. ?ths x")
1.1140 -  proof-
1.1141 +  proof -
1.1142      fix x:: 'a
1.1143 -    have th0: "x*x - 1 = (x - 1)*(x + 1)" by (simp add: field_simps)
1.1144 +    have th0: "x*x - 1 = (x - 1)*(x + 1)"
1.1145 +      by (simp add: field_simps)
1.1146      have th1: "\<And>(x::'a) y. x = - y \<longleftrightarrow> x + y = 0"
1.1147 -      apply (subst eq_iff_diff_eq_0) by simp
1.1148 -    have "x*x = 1 \<longleftrightarrow> x*x - 1 = 0" by simp
1.1149 +      apply (subst eq_iff_diff_eq_0)
1.1150 +      apply simp
1.1151 +      done
1.1152 +    have "x * x = 1 \<longleftrightarrow> x*x - 1 = 0" by simp
1.1153      also have "\<dots> \<longleftrightarrow> x = 1 \<or> x = - 1" unfolding th0 th1 by simp
1.1154      finally show "?ths x" ..
1.1155    qed
1.1156 -  from oQ have "Q ** transpose Q = mat 1" by (metis orthogonal_matrix_def)
1.1157 -  hence "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)" by simp
1.1158 -  hence "det Q * det Q = 1" by (simp add: det_mul det_I det_transpose)
1.1159 +  from oQ have "Q ** transpose Q = mat 1"
1.1160 +    by (metis orthogonal_matrix_def)
1.1161 +  then have "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)"
1.1162 +    by simp
1.1163 +  then have "det Q * det Q = 1"
1.1164 +    by (simp add: det_mul det_I det_transpose)
1.1165    then show ?thesis unfolding th .
1.1166  qed
1.1167
1.1168 @@ -911,25 +1064,29 @@
1.1169  (* ------------------------------------------------------------------------- *)
1.1170  lemma scaling_linear:
1.1171    fixes f :: "real ^'n \<Rightarrow> real ^'n"
1.1172 -  assumes f0: "f 0 = 0" and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y"
1.1173 +  assumes f0: "f 0 = 0"
1.1174 +    and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y"
1.1175    shows "linear f"
1.1176 -proof-
1.1177 -  {fix v w
1.1178 -    {fix x note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right] }
1.1179 +proof -
1.1180 +  {
1.1181 +    fix v w
1.1182 +    {
1.1183 +      fix x
1.1184 +      note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right]
1.1185 +    }
1.1186      note th0 = this
1.1187      have "f v \<bullet> f w = c\<^sup>2 * (v \<bullet> w)"
1.1188        unfolding dot_norm_neg dist_norm[symmetric]
1.1189        unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
1.1190    note fc = this
1.1191    show ?thesis
1.1192 -    unfolding linear_def vector_eq[where 'a="real^'n"] scalar_mult_eq_scaleR
1.1193 +    unfolding linear_def vector_eq[where 'a="real^'n"] scalar_mult_eq_scaleR
1.1195  qed
1.1196
1.1197  lemma isometry_linear:
1.1198 -  "f (0:: real^'n) = (0:: real^'n) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y
1.1199 -        \<Longrightarrow> linear f"
1.1200 -by (rule scaling_linear[where c=1]) simp_all
1.1201 +  "f (0:: real^'n) = (0:: real^'n) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y \<Longrightarrow> linear f"
1.1202 +  by (rule scaling_linear[where c=1]) simp_all
1.1203
1.1204  (* ------------------------------------------------------------------------- *)
1.1205  (* Hence another formulation of orthogonal transformation.                   *)
1.1206 @@ -948,7 +1105,8 @@
1.1207    apply clarify
1.1208    apply (erule_tac x=v in allE)
1.1209    apply (erule_tac x=0 in allE)
1.1210 -  by (simp add: dist_norm)
1.1211 +  apply (simp add: dist_norm)
1.1212 +  done
1.1213
1.1214  (* ------------------------------------------------------------------------- *)
1.1215  (* Can extend an isometry from unit sphere.                                  *)
1.1216 @@ -957,15 +1115,19 @@
1.1217  lemma isometry_sphere_extend:
1.1218    fixes f:: "real ^'n \<Rightarrow> real ^'n"
1.1219    assumes f1: "\<forall>x. norm x = 1 \<longrightarrow> norm (f x) = 1"
1.1220 -  and fd1: "\<forall> x y. norm x = 1 \<longrightarrow> norm y = 1 \<longrightarrow> dist (f x) (f y) = dist x y"
1.1221 +    and fd1: "\<forall> x y. norm x = 1 \<longrightarrow> norm y = 1 \<longrightarrow> dist (f x) (f y) = dist x y"
1.1222    shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)"
1.1223 -proof-
1.1224 -  {fix x y x' y' x0 y0 x0' y0' :: "real ^'n"
1.1225 -    assume H: "x = norm x *\<^sub>R x0" "y = norm y *\<^sub>R y0"
1.1226 -    "x' = norm x *\<^sub>R x0'" "y' = norm y *\<^sub>R y0'"
1.1227 -    "norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1"
1.1228 -    "norm(x0' - y0') = norm(x0 - y0)"
1.1229 -    hence *:"x0 \<bullet> y0 = x0' \<bullet> y0' + y0' \<bullet> x0' - y0 \<bullet> x0 " by(simp add: norm_eq norm_eq_1 inner_add inner_diff)
1.1230 +proof -
1.1231 +  {
1.1232 +    fix x y x' y' x0 y0 x0' y0' :: "real ^'n"
1.1233 +    assume H:
1.1234 +      "x = norm x *\<^sub>R x0"
1.1235 +      "y = norm y *\<^sub>R y0"
1.1236 +      "x' = norm x *\<^sub>R x0'" "y' = norm y *\<^sub>R y0'"
1.1237 +      "norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1"
1.1238 +      "norm(x0' - y0') = norm(x0 - y0)"
1.1239 +    hence *: "x0 \<bullet> y0 = x0' \<bullet> y0' + y0' \<bullet> x0' - y0 \<bullet> x0 "
1.1241      have "norm(x' - y') = norm(x - y)"
1.1242        apply (subst H(1))
1.1243        apply (subst H(2))
1.1244 @@ -974,48 +1136,71 @@
1.1245        using H(5-9)
1.1246        apply (simp add: norm_eq norm_eq_1)
1.1247        apply (simp add: inner_diff scalar_mult_eq_scaleR) unfolding *
1.1248 -      by (simp add: field_simps) }
1.1249 +      apply (simp add: field_simps)
1.1250 +      done
1.1251 +  }
1.1252    note th0 = this
1.1253    let ?g = "\<lambda>x. if x = 0 then 0 else norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)"
1.1254 -  {fix x:: "real ^'n" assume nx: "norm x = 1"
1.1255 -    have "?g x = f x" using nx by auto}
1.1256 -  hence thfg: "\<forall>x. norm x = 1 \<longrightarrow> ?g x = f x" by blast
1.1257 +  {
1.1258 +    fix x:: "real ^'n"
1.1259 +    assume nx: "norm x = 1"
1.1260 +    have "?g x = f x" using nx by auto
1.1261 +  }
1.1262 +  then have thfg: "\<forall>x. norm x = 1 \<longrightarrow> ?g x = f x"
1.1263 +    by blast
1.1264    have g0: "?g 0 = 0" by simp
1.1265 -  {fix x y :: "real ^'n"
1.1266 -    {assume "x = 0" "y = 0"
1.1267 -      then have "dist (?g x) (?g y) = dist x y" by simp }
1.1268 +  {
1.1269 +    fix x y :: "real ^'n"
1.1270 +    {
1.1271 +      assume "x = 0" "y = 0"
1.1272 +      then have "dist (?g x) (?g y) = dist x y" by simp
1.1273 +    }
1.1274      moreover
1.1275 -    {assume "x = 0" "y \<noteq> 0"
1.1276 +    {
1.1277 +      assume "x = 0" "y \<noteq> 0"
1.1278        then have "dist (?g x) (?g y) = dist x y"
1.1280          apply (rule f1[rule_format])
1.1282 +        apply (simp add: field_simps)
1.1283 +        done
1.1284 +    }
1.1285      moreover
1.1286 -    {assume "x \<noteq> 0" "y = 0"
1.1287 +    {
1.1288 +      assume "x \<noteq> 0" "y = 0"
1.1289        then have "dist (?g x) (?g y) = dist x y"
1.1291          apply (rule f1[rule_format])
1.1293 +        apply (simp add: field_simps)
1.1294 +        done
1.1295 +    }
1.1296      moreover
1.1297 -    {assume z: "x \<noteq> 0" "y \<noteq> 0"
1.1298 -      have th00: "x = norm x *\<^sub>R (inverse (norm x) *\<^sub>R x)" "y = norm y *\<^sub>R (inverse (norm y) *\<^sub>R y)" "norm x *\<^sub>R f ((inverse (norm x) *\<^sub>R x)) = norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)"
1.1299 +    {
1.1300 +      assume z: "x \<noteq> 0" "y \<noteq> 0"
1.1301 +      have th00:
1.1302 +        "x = norm x *\<^sub>R (inverse (norm x) *\<^sub>R x)"
1.1303 +        "y = norm y *\<^sub>R (inverse (norm y) *\<^sub>R y)"
1.1304 +        "norm x *\<^sub>R f ((inverse (norm x) *\<^sub>R x)) = norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)"
1.1305          "norm y *\<^sub>R f (inverse (norm y) *\<^sub>R y) = norm y *\<^sub>R f (inverse (norm y) *\<^sub>R y)"
1.1306          "norm (inverse (norm x) *\<^sub>R x) = 1"
1.1307          "norm (f (inverse (norm x) *\<^sub>R x)) = 1"
1.1308          "norm (inverse (norm y) *\<^sub>R y) = 1"
1.1309          "norm (f (inverse (norm y) *\<^sub>R y)) = 1"
1.1310          "norm (f (inverse (norm x) *\<^sub>R x) - f (inverse (norm y) *\<^sub>R y)) =
1.1311 -        norm (inverse (norm x) *\<^sub>R x - inverse (norm y) *\<^sub>R y)"
1.1312 +          norm (inverse (norm x) *\<^sub>R x - inverse (norm y) *\<^sub>R y)"
1.1313          using z
1.1314          by (auto simp add: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
1.1315        from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
1.1316 -        by (simp add: dist_norm)}
1.1317 -    ultimately have "dist (?g x) (?g y) = dist x y" by blast}
1.1318 +        by (simp add: dist_norm)
1.1319 +    }
1.1320 +    ultimately have "dist (?g x) (?g y) = dist x y" by blast
1.1321 +  }
1.1322    note thd = this
1.1323      show ?thesis
1.1324      apply (rule exI[where x= ?g])
1.1325      unfolding orthogonal_transformation_isometry
1.1326 -      using  g0 thfg thd by metis
1.1327 +    using g0 thfg thd
1.1328 +    apply metis
1.1329 +    done
1.1330  qed
1.1331
1.1332  (* ------------------------------------------------------------------------- *)
1.1333 @@ -1029,14 +1214,17 @@
1.1334    fixes Q :: "'a::linordered_idom^'n^'n"
1.1335    shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q"
1.1336    by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix)
1.1337 +
1.1338  (* ------------------------------------------------------------------------- *)
1.1339  (* Explicit formulas for low dimensions.                                     *)
1.1340  (* ------------------------------------------------------------------------- *)
1.1341
1.1342 -lemma setprod_1: "setprod f {(1::nat)..1} = f 1" by simp
1.1343 +lemma setprod_1: "setprod f {(1::nat)..1} = f 1"
1.1344 +  by simp
1.1345
1.1346  lemma setprod_2: "setprod f {(1::nat)..2} = f 1 * f 2"
1.1347    by (simp add: eval_nat_numeral setprod_numseg mult_commute)
1.1348 +
1.1349  lemma setprod_3: "setprod f {(1::nat)..3} = f 1 * f 2 * f 3"
1.1350    by (simp add: eval_nat_numeral setprod_numseg mult_commute)
1.1351
1.1352 @@ -1044,33 +1232,33 @@
1.1353    by (simp add: det_def sign_id)
1.1354
1.1355  lemma det_2: "det (A::'a::comm_ring_1^2^2) = A\$1\$1 * A\$2\$2 - A\$1\$2 * A\$2\$1"
1.1356 -proof-
1.1357 +proof -
1.1358    have f12: "finite {2::2}" "1 \<notin> {2::2}" by auto
1.1359    show ?thesis
1.1360 -  unfolding det_def UNIV_2
1.1361 -  unfolding setsum_over_permutations_insert[OF f12]
1.1362 -  unfolding permutes_sing
1.1363 -  by (simp add: sign_swap_id sign_id swap_id_eq)
1.1364 +    unfolding det_def UNIV_2
1.1365 +    unfolding setsum_over_permutations_insert[OF f12]
1.1366 +    unfolding permutes_sing
1.1367 +    by (simp add: sign_swap_id sign_id swap_id_eq)
1.1368  qed
1.1369
1.1370 -lemma det_3: "det (A::'a::comm_ring_1^3^3) =
1.1371 -  A\$1\$1 * A\$2\$2 * A\$3\$3 +
1.1372 -  A\$1\$2 * A\$2\$3 * A\$3\$1 +
1.1373 -  A\$1\$3 * A\$2\$1 * A\$3\$2 -
1.1374 -  A\$1\$1 * A\$2\$3 * A\$3\$2 -
1.1375 -  A\$1\$2 * A\$2\$1 * A\$3\$3 -
1.1376 -  A\$1\$3 * A\$2\$2 * A\$3\$1"
1.1377 -proof-
1.1378 +lemma det_3:
1.1379 +  "det (A::'a::comm_ring_1^3^3) =
1.1380 +    A\$1\$1 * A\$2\$2 * A\$3\$3 +
1.1381 +    A\$1\$2 * A\$2\$3 * A\$3\$1 +
1.1382 +    A\$1\$3 * A\$2\$1 * A\$3\$2 -
1.1383 +    A\$1\$1 * A\$2\$3 * A\$3\$2 -
1.1384 +    A\$1\$2 * A\$2\$1 * A\$3\$3 -
1.1385 +    A\$1\$3 * A\$2\$2 * A\$3\$1"
1.1386 +proof -
1.1387    have f123: "finite {2::3, 3}" "1 \<notin> {2::3, 3}" by auto
1.1388    have f23: "finite {3::3}" "2 \<notin> {3::3}" by auto
1.1389
1.1390    show ?thesis
1.1391 -  unfolding det_def UNIV_3
1.1392 -  unfolding setsum_over_permutations_insert[OF f123]
1.1393 -  unfolding setsum_over_permutations_insert[OF f23]
1.1394 -
1.1395 -  unfolding permutes_sing
1.1396 -  by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)
1.1397 +    unfolding det_def UNIV_3
1.1398 +    unfolding setsum_over_permutations_insert[OF f123]
1.1399 +    unfolding setsum_over_permutations_insert[OF f23]
1.1400 +    unfolding permutes_sing
1.1401 +    by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)
1.1402  qed
1.1403
1.1404  end
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Wed Aug 28 22:50:23 2013 +0200
2.2 +++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Wed Aug 28 23:41:21 2013 +0200
2.3 @@ -11,72 +11,83 @@
2.4  definition "onorm f = Sup {norm (f x)| x. norm x = 1}"
2.5
2.6  lemma norm_bound_generalize:
2.7 -  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
2.8 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
2.9    assumes lf: "linear f"
2.10 -  shows "(\<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> b) \<longleftrightarrow> (\<forall>x. norm (f x) \<le> b * norm x)" (is "?lhs \<longleftrightarrow> ?rhs")
2.11 -proof-
2.12 -  {assume H: ?rhs
2.13 -    {fix x :: "'a" assume x: "norm x = 1"
2.14 -      from H[rule_format, of x] x have "norm (f x) \<le> b" by simp}
2.15 -    then have ?lhs by blast }
2.16 +  shows "(\<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> b) \<longleftrightarrow> (\<forall>x. norm (f x) \<le> b * norm x)"
2.17 +  (is "?lhs \<longleftrightarrow> ?rhs")
2.18 +proof
2.19 +  assume H: ?rhs
2.20 +  {
2.21 +    fix x :: "'a"
2.22 +    assume x: "norm x = 1"
2.23 +    from H[rule_format, of x] x have "norm (f x) \<le> b" by simp
2.24 +  }
2.25 +  then show ?lhs by blast
2.26 +next
2.27 +  assume H: ?lhs
2.28 +  have bp: "b \<ge> 0"
2.29 +    apply -
2.30 +    apply (rule order_trans [OF norm_ge_zero])
2.31 +    apply (rule H[rule_format, of "SOME x::'a. x \<in> Basis"])
2.32 +    apply (auto intro: SOME_Basis norm_Basis)
2.33 +    done
2.34 +  {
2.35 +    fix x :: "'a"
2.36 +    {
2.37 +      assume "x = 0"
2.38 +      then have "norm (f x) \<le> b * norm x"
2.39 +        by (simp add: linear_0[OF lf] bp)
2.40 +    }
2.41 +    moreover
2.42 +    {
2.43 +      assume x0: "x \<noteq> 0"
2.44 +      then have n0: "norm x \<noteq> 0" by (metis norm_eq_zero)
2.45 +      let ?c = "1/ norm x"
2.46 +      have "norm (?c *\<^sub>R x) = 1" using x0 by (simp add: n0)
2.47 +      with H have "norm (f (?c *\<^sub>R x)) \<le> b" by blast
2.48 +      then have "?c * norm (f x) \<le> b"
2.49 +        by (simp add: linear_cmul[OF lf])
2.50 +      then have "norm (f x) \<le> b * norm x"
2.51 +        using n0 norm_ge_zero[of x] by (auto simp add: field_simps)
2.52 +    }
2.53 +    ultimately have "norm (f x) \<le> b * norm x" by blast
2.54 +  }
2.55 +  then show ?rhs by blast
2.56 +qed
2.57
2.58 -  moreover
2.59 -  {assume H: ?lhs
2.60 -    have bp: "b \<ge> 0"
2.61 -      apply -
2.62 -      apply(rule order_trans [OF norm_ge_zero])
2.63 -      apply(rule H[rule_format, of "SOME x::'a. x \<in> Basis"])
2.64 -      by (auto intro: SOME_Basis norm_Basis)
2.65 -    {fix x :: "'a"
2.66 -      {assume "x = 0"
2.67 -        then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] bp)}
2.68 -      moreover
2.69 -      {assume x0: "x \<noteq> 0"
2.70 -        hence n0: "norm x \<noteq> 0" by (metis norm_eq_zero)
2.71 -        let ?c = "1/ norm x"
2.72 -        have "norm (?c *\<^sub>R x) = 1" using x0 by (simp add: n0)
2.73 -        with H have "norm (f (?c *\<^sub>R x)) \<le> b" by blast
2.74 -        hence "?c * norm (f x) \<le> b"
2.75 -          by (simp add: linear_cmul[OF lf])
2.76 -        hence "norm (f x) \<le> b * norm x"
2.77 -          using n0 norm_ge_zero[of x] by (auto simp add: field_simps)}
2.78 -      ultimately have "norm (f x) \<le> b * norm x" by blast}
2.79 -    then have ?rhs by blast}
2.80 -  ultimately show ?thesis by blast
2.81 -qed
2.82 -
2.83  lemma onorm:
2.84    fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
2.85    assumes lf: "linear f"
2.86 -  shows "norm (f x) <= onorm f * norm x"
2.87 -  and "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
2.88 -proof-
2.89 -  {
2.90 -    let ?S = "{norm (f x) |x. norm x = 1}"
2.91 -    have "norm (f (SOME i. i \<in> Basis)) \<in> ?S"
2.92 -      by (auto intro!: exI[of _ "SOME i. i \<in> Basis"] norm_Basis SOME_Basis)
2.93 -    hence Se: "?S \<noteq> {}" by auto
2.94 -    from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
2.95 -      unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def)
2.96 -    { from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
2.97 -      show "norm (f x) <= onorm f * norm x"
2.98 -        apply -
2.99 -        apply (rule spec[where x = x])
2.100 -        unfolding norm_bound_generalize[OF lf, symmetric]
2.101 -        by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
2.102 -    {
2.103 -      show "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
2.104 -        using isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
2.105 -        unfolding norm_bound_generalize[OF lf, symmetric]
2.106 -        by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
2.107 -  }
2.108 +  shows "norm (f x) \<le> onorm f * norm x"
2.109 +    and "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
2.110 +proof -
2.111 +  let ?S = "{norm (f x) |x. norm x = 1}"
2.112 +  have "norm (f (SOME i. i \<in> Basis)) \<in> ?S"
2.113 +    by (auto intro!: exI[of _ "SOME i. i \<in> Basis"] norm_Basis SOME_Basis)
2.114 +  then have Se: "?S \<noteq> {}" by auto
2.115 +  from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
2.116 +    unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def)
2.117 +  from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
2.118 +  show "norm (f x) <= onorm f * norm x"
2.119 +    apply -
2.120 +    apply (rule spec[where x = x])
2.121 +    unfolding norm_bound_generalize[OF lf, symmetric]
2.122 +    apply (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
2.123 +    done
2.124 +  show "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
2.125 +    using isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
2.126 +    unfolding norm_bound_generalize[OF lf, symmetric]
2.127 +    by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
2.128  qed
2.129
2.130 -lemma onorm_pos_le: assumes lf: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space)" shows "0 <= onorm f"
2.131 -  using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "SOME i. i \<in> Basis"]]
2.132 +lemma onorm_pos_le:
2.133 +  assumes lf: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space)"
2.134 +  shows "0 \<le> onorm f"
2.135 +  using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "SOME i. i \<in> Basis"]]
2.137
2.138 -lemma onorm_eq_0: assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
2.139 +lemma onorm_eq_0:
2.140 +  assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
2.141    shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
2.142    using onorm[OF lf]
2.143    apply (auto simp add: onorm_pos_le)
2.144 @@ -87,47 +98,53 @@
2.145    done
2.146
2.147  lemma onorm_const: "onorm(\<lambda>x::'a::euclidean_space. (y::'b::euclidean_space)) = norm y"
2.148 -proof-
2.149 +proof -
2.150    let ?f = "\<lambda>x::'a. (y::'b)"
2.151    have th: "{norm (?f x)| x. norm x = 1} = {norm y}"
2.152      by (auto simp: SOME_Basis intro!: exI[of _ "SOME i. i \<in> Basis"])
2.153    show ?thesis
2.154      unfolding onorm_def th
2.155 -    apply (rule cSup_unique) by (simp_all  add: setle_def)
2.156 +    apply (rule cSup_unique)
2.157 +    apply (simp_all  add: setle_def)
2.158 +    done
2.159  qed
2.160
2.161 -lemma onorm_pos_lt: assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
2.162 +lemma onorm_pos_lt:
2.163 +  assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
2.164    shows "0 < onorm f \<longleftrightarrow> ~(\<forall>x. f x = 0)"
2.165    unfolding onorm_eq_0[OF lf, symmetric]
2.166    using onorm_pos_le[OF lf] by arith
2.167
2.168  lemma onorm_compose:
2.169    assumes lf: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space)"
2.170 -  and lg: "linear (g::'k::euclidean_space \<Rightarrow> 'n::euclidean_space)"
2.171 -  shows "onorm (f o g) <= onorm f * onorm g"
2.172 -  apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format])
2.173 -  unfolding o_def
2.174 -  apply (subst mult_assoc)
2.175 -  apply (rule order_trans)
2.176 -  apply (rule onorm(1)[OF lf])
2.177 -  apply (rule mult_left_mono)
2.178 -  apply (rule onorm(1)[OF lg])
2.179 -  apply (rule onorm_pos_le[OF lf])
2.180 -  done
2.181 +    and lg: "linear (g::'k::euclidean_space \<Rightarrow> 'n::euclidean_space)"
2.182 +  shows "onorm (f o g) \<le> onorm f * onorm g"
2.183 +    apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format])
2.184 +    unfolding o_def
2.185 +    apply (subst mult_assoc)
2.186 +    apply (rule order_trans)
2.187 +    apply (rule onorm(1)[OF lf])
2.188 +    apply (rule mult_left_mono)
2.189 +    apply (rule onorm(1)[OF lg])
2.190 +    apply (rule onorm_pos_le[OF lf])
2.191 +    done
2.192
2.193 -lemma onorm_neg_lemma: assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
2.194 +lemma onorm_neg_lemma:
2.195 +  assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
2.196    shows "onorm (\<lambda>x. - f x) \<le> onorm f"
2.197    using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]
2.198    unfolding norm_minus_cancel by metis
2.199
2.200 -lemma onorm_neg: assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
2.201 +lemma onorm_neg:
2.202 +  assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
2.203    shows "onorm (\<lambda>x. - f x) = onorm f"
2.204    using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]]
2.205    by simp
2.206
2.207  lemma onorm_triangle:
2.208 -  assumes lf: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space)" and lg: "linear g"
2.209 -  shows "onorm (\<lambda>x. f x + g x) <= onorm f + onorm g"
2.210 +  assumes lf: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space)"
2.211 +    and lg: "linear g"
2.212 +  shows "onorm (\<lambda>x. f x + g x) \<le> onorm f + onorm g"
2.213    apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format])
2.214    apply (rule order_trans)
2.215    apply (rule norm_triangle_ineq)
2.216 @@ -137,17 +154,20 @@
2.217    apply (rule onorm(1)[OF lg])
2.218    done
2.219
2.220 -lemma onorm_triangle_le: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) <= e
2.221 -  \<Longrightarrow> onorm(\<lambda>x. f x + g x) <= e"
2.222 +lemma onorm_triangle_le:
2.223 +  "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space) \<Longrightarrow>
2.224 +    linear g \<Longrightarrow> onorm f + onorm g \<le> e \<Longrightarrow> onorm (\<lambda>x. f x + g x) \<le> e"
2.225    apply (rule order_trans)
2.226    apply (rule onorm_triangle)
2.227    apply assumption+
2.228    done
2.229
2.230 -lemma onorm_triangle_lt: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) < e
2.231 -  ==> onorm(\<lambda>x. f x + g x) < e"
2.232 +lemma onorm_triangle_lt:
2.233 +  "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space) \<Longrightarrow> linear g \<Longrightarrow>
2.234 +    onorm f + onorm g < e \<Longrightarrow> onorm(\<lambda>x. f x + g x) < e"
2.235    apply (rule order_le_less_trans)
2.236    apply (rule onorm_triangle)
2.237 -  by assumption+
2.238 +  apply assumption+
2.239 +  done
2.240
2.241  end
```