tuned proofs;
authorwenzelm
Fri Oct 05 13:57:48 2012 +0200 (2012-10-05)
changeset 49711e5aaae7eadc9
parent 49710 21d88a631fcc
child 49712 a1bd8fe5131b
tuned proofs;
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Oct 05 13:48:22 2012 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Oct 05 13:57:48 2012 +0200
     1.3 @@ -708,8 +708,10 @@
     1.4  lemma (in real_vector) span_subspace: "A \<subseteq> B \<Longrightarrow> B \<le> span A \<Longrightarrow>  subspace B \<Longrightarrow> span A = B"
     1.5    by (metis order_antisym span_def hull_minimal)
     1.6  
     1.7 -lemma (in real_vector) span_induct': assumes SP: "\<forall>x \<in> S. P x"
     1.8 -  and P: "subspace {x. P x}" shows "\<forall>x \<in> span S. P x"
     1.9 +lemma (in real_vector) span_induct':
    1.10 +  assumes SP: "\<forall>x \<in> S. P x"
    1.11 +    and P: "subspace {x. P x}"
    1.12 +  shows "\<forall>x \<in> span S. P x"
    1.13    using span_induct SP P by blast
    1.14  
    1.15  inductive_set (in real_vector) span_induct_alt_help for S:: "'a set"
    1.16 @@ -842,7 +844,8 @@
    1.17    ultimately show "subspace ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
    1.18      by (rule subspace_linear_image)
    1.19  next
    1.20 -  fix T assume "A \<union> B \<subseteq> T" and "subspace T"
    1.21 +  fix T
    1.22 +  assume "A \<union> B \<subseteq> T" and "subspace T"
    1.23    then show "(\<lambda>(a, b). a + b) ` (span A \<times> span B) \<subseteq> T"
    1.24      by (auto intro!: subspace_add elim: span_induct)
    1.25  qed
    1.26 @@ -885,7 +888,8 @@
    1.27  text {* Hence some "reversal" results. *}
    1.28  
    1.29  lemma in_span_insert:
    1.30 -  assumes a: "a \<in> span (insert b S)" and na: "a \<notin> span S"
    1.31 +  assumes a: "a \<in> span (insert b S)"
    1.32 +    and na: "a \<notin> span S"
    1.33    shows "b \<in> span (insert a S)"
    1.34  proof -
    1.35    from span_breakdown[of b "insert b S" a, OF insertI1 a]
    1.36 @@ -1073,7 +1077,8 @@
    1.37    shows "span S = {y. \<exists>u. setsum (\<lambda>v. u v *\<^sub>R v) S = y}"
    1.38    (is "_ = ?rhs")
    1.39  proof -
    1.40 -  { fix y assume y: "y \<in> span S"
    1.41 +  { fix y
    1.42 +    assume y: "y \<in> span S"
    1.43      from y obtain S' u where fS': "finite S'" and SS': "S' \<subseteq> S" and
    1.44        u: "setsum (\<lambda>v. u v *\<^sub>R v) S' = y" unfolding span_explicit by blast
    1.45      let ?u = "\<lambda>x. if x \<in> S' then u x else 0"
    1.46 @@ -1135,7 +1140,8 @@
    1.47    by blast
    1.48  
    1.49  lemma spanning_subset_independent:
    1.50 -  assumes BA: "B \<subseteq> A" and iA: "independent A"
    1.51 +  assumes BA: "B \<subseteq> A"
    1.52 +    and iA: "independent A"
    1.53      and AsB: "A \<subseteq> span B"
    1.54    shows "A = B"
    1.55  proof
    1.56 @@ -1162,8 +1168,9 @@
    1.57  text {* The general case of the Exchange Lemma, the key to what follows. *}
    1.58  
    1.59  lemma exchange_lemma:
    1.60 -  assumes f:"finite t" and i: "independent s"
    1.61 -    and sp:"s \<subseteq> span t"
    1.62 +  assumes f:"finite t"
    1.63 +    and i: "independent s"
    1.64 +    and sp: "s \<subseteq> span t"
    1.65    shows "\<exists>t'. (card t' = card t) \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
    1.66    using f i sp
    1.67  proof (induct "card (t - s)" arbitrary: s t rule: less_induct)
    1.68 @@ -1177,11 +1184,12 @@
    1.69        done }
    1.70    moreover
    1.71    { assume st: "t \<subseteq> s"
    1.72 -
    1.73      from spanning_subset_independent[OF st s sp]
    1.74 -      st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t])
    1.75 -      apply (auto intro: span_superset)
    1.76 -      done }
    1.77 +      st ft span_mono[OF st] have ?ths
    1.78 +        apply -
    1.79 +        apply (rule exI[where x=t])
    1.80 +        apply (auto intro: span_superset)
    1.81 +        done }
    1.82    moreover
    1.83    { assume st: "\<not> s \<subseteq> t" "\<not> t \<subseteq> s"
    1.84      from st(2) obtain b where b: "b \<in> t" "b \<notin> s" by blast
    1.85 @@ -1276,8 +1284,7 @@
    1.86    apply (simp add: inner_setsum_right dot_basis)
    1.87    done
    1.88  
    1.89 -lemma (in euclidean_space) range_basis:
    1.90 -  "range basis = insert 0 (basis ` {..<DIM('a)})"
    1.91 +lemma (in euclidean_space) range_basis: "range basis = insert 0 (basis ` {..<DIM('a)})"
    1.92  proof -
    1.93    have *: "UNIV = {..<DIM('a)} \<union> {DIM('a)..}" by auto
    1.94    show ?thesis unfolding * image_Un basis_finite by auto
    1.95 @@ -1508,7 +1515,8 @@
    1.96        apply (rule setsum_norm_le)
    1.97        using fN fM
    1.98        apply simp
    1.99 -      apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] field_simps simp del: scaleR_scaleR)
   1.100 +      apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
   1.101 +        field_simps simp del: scaleR_scaleR)
   1.102        apply (rule mult_mono)
   1.103        apply (auto simp add: zero_le_mult_iff component_le_norm)
   1.104        apply (rule mult_mono)
   1.105 @@ -1930,7 +1938,8 @@
   1.106          apply (clarsimp simp add: inner_add inner_setsum_left)
   1.107          apply (rule setsum_0', rule ballI)
   1.108          unfolding inner_commute
   1.109 -        apply (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])
   1.110 +        apply (auto simp add: x field_simps
   1.111 +          intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])
   1.112          done }
   1.113      then show "\<forall>x \<in> B. ?a \<bullet> x = 0" by blast
   1.114    qed
     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Oct 05 13:48:22 2012 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Oct 05 13:57:48 2012 +0200
     2.3 @@ -28,12 +28,14 @@
     2.4  
     2.5  lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)"
     2.6  proof-
     2.7 -  {assume "T1=T2" hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp}
     2.8 +  { assume "T1=T2"
     2.9 +    hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp }
    2.10    moreover
    2.11 -  {assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
    2.12 +  { assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
    2.13      hence "openin T1 = openin T2" by (simp add: fun_eq_iff)
    2.14      hence "topology (openin T1) = topology (openin T2)" by simp
    2.15 -    hence "T1 = T2" unfolding openin_inverse .}
    2.16 +    hence "T1 = T2" unfolding openin_inverse .
    2.17 +  }
    2.18    ultimately show ?thesis by blast
    2.19  qed
    2.20  
    2.21 @@ -66,9 +68,11 @@
    2.22  
    2.23  lemma openin_topspace[intro, simp]: "openin U (topspace U)" by (simp add: openin_Union topspace_def)
    2.24  
    2.25 -lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)" (is "?lhs \<longleftrightarrow> ?rhs")
    2.26 +lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)"
    2.27 +  (is "?lhs \<longleftrightarrow> ?rhs")
    2.28  proof
    2.29 -  assume ?lhs then show ?rhs by auto
    2.30 +  assume ?lhs
    2.31 +  then show ?rhs by auto
    2.32  next
    2.33    assume H: ?rhs
    2.34    let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}"
    2.35 @@ -77,6 +81,7 @@
    2.36    finally show "openin U S" .
    2.37  qed
    2.38  
    2.39 +
    2.40  subsubsection {* Closed sets *}
    2.41  
    2.42  definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
    2.43 @@ -167,9 +172,11 @@
    2.44    apply (rule iffI, clarify)
    2.45    apply (frule openin_subset[of U])  apply blast
    2.46    apply (rule exI[where x="topspace U"])
    2.47 -  by auto
    2.48 -
    2.49 -lemma subtopology_superset: assumes UV: "topspace U \<subseteq> V"
    2.50 +  apply auto
    2.51 +  done
    2.52 +
    2.53 +lemma subtopology_superset:
    2.54 +  assumes UV: "topspace U \<subseteq> V"
    2.55    shows "subtopology U V = U"
    2.56  proof-
    2.57    {fix S