src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
changeset 44170 510ac30f44c0
parent 44167 e81d676d598e
child 44211 bd7c586b902e
     1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Aug 12 07:18:28 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Aug 12 09:17:24 2011 -0700
     1.3 @@ -762,7 +762,7 @@
     1.4  apply auto
     1.5  apply (rule span_mul)
     1.6  apply (rule span_superset)
     1.7 -apply (auto simp add: Collect_def mem_def)
     1.8 +apply auto
     1.9  done
    1.10  
    1.11  lemma finite_stdbasis: "finite {cart_basis i ::real^'n |i. i\<in> (UNIV:: 'n set)}" (is "finite ?S")
    1.12 @@ -785,12 +785,12 @@
    1.13  proof-
    1.14    let ?U = "UNIV :: 'n set"
    1.15    let ?B = "cart_basis ` S"
    1.16 -  let ?P = "\<lambda>(x::real^_). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x$i =0"
    1.17 +  let ?P = "{(x::real^_). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x$i =0}"
    1.18   {fix x::"real^_" assume xS: "x\<in> ?B"
    1.19 -   from xS have "?P x" by auto}
    1.20 +   from xS have "x \<in> ?P" by auto}
    1.21   moreover
    1.22   have "subspace ?P"
    1.23 -   by (auto simp add: subspace_def Collect_def mem_def)
    1.24 +   by (auto simp add: subspace_def)
    1.25   ultimately show ?thesis
    1.26     using x span_induct[of ?B ?P x] iS by blast
    1.27  qed
    1.28 @@ -830,7 +830,7 @@
    1.29      from equalityD2[OF span_stdbasis]
    1.30      have IU: " (UNIV :: (real^'m) set) \<subseteq> span ?I" by blast
    1.31      from linear_eq[OF lf lg IU] fg x
    1.32 -    have "f x = g x" unfolding Collect_def  Ball_def mem_def by metis}
    1.33 +    have "f x = g x" unfolding Ball_def mem_Collect_eq by metis}
    1.34    then show ?thesis by (auto intro: ext)
    1.35  qed
    1.36