tuned proofs;
authorwenzelm
Wed Aug 28 23:41:21 2013 +0200 (2013-08-28)
changeset 53253220f306f5c4e
parent 53252 4766fbe322b5
child 53254 082d0972096b
tuned proofs;
src/HOL/Multivariate_Analysis/Determinants.thy
src/HOL/Multivariate_Analysis/Operator_Norm.thy
     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.18  lemma setprod_add_split:
    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.34 -apply (simp add: add_commute)
    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.40 +  apply (simp add: add_commute)
    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.421  lemma det_row_add:
   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.426 -unfolding det_def vec_lambda_beta setsum_addf[symmetric]
   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.474      by (simp add: field_simps)
   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.532      by (simp add: field_simps)
   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.678 +    by (simp add: det_row_add cong del: if_weak_cong)
   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.781  proof (simp add: det_def setsum_right_distrib cong add: setprod_cong, rule setsum_cong2)
   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.1053    apply (simp add: norm_eq_sqrt_inner)
  1.1054 -  by (simp add: dot_norm  linear_add[symmetric])
  1.1055 +  apply (simp add: dot_norm  linear_add[symmetric])
  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.1194      by (simp add: inner_add fc field_simps)
  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.1240 +      by (simp add: norm_eq norm_eq_1 inner_add inner_diff)
  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.1279          apply (simp add: dist_norm)
  1.1280          apply (rule f1[rule_format])
  1.1281 -        by(simp add: field_simps)}
  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.1290          apply (simp add: dist_norm)
  1.1291          apply (rule f1[rule_format])
  1.1292 -        by(simp add: field_simps)}
  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.136    by (simp add: SOME_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