src/HOL/Multivariate_Analysis/Linear_Algebra.thy

--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 25 15:35:54 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 25 16:06:50 2011 -0700
@@ -1766,8 +1766,15 @@
 lemma vector_sub_project_orthogonal: "(b::'a::euclidean_space) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *\<^sub>R b) = 0"
   unfolding inner_simps by auto
 
+lemma pairwise_orthogonal_insert:
+  assumes "pairwise orthogonal S"
+  assumes "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
+  shows "pairwise orthogonal (insert x S)"
+  using assms unfolding pairwise_def
+  by (auto simp add: orthogonal_commute)
+
 lemma basis_orthogonal:
-  fixes B :: "('a::euclidean_space) set"
+  fixes B :: "('a::real_inner) set"
   assumes fB: "finite B"
   shows "\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C"
   (is " \<exists>C. ?P B C")
@@ -1795,48 +1802,20 @@
       by (rule span_superset)}
   then have SC: "span ?C = span (insert a B)"
     unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto
-  thm pairwise_def
-  {fix x y assume xC: "x \<in> ?C" and yC: "y \<in> ?C" and xy: "x \<noteq> y"
-    {assume xa: "x = ?a" and ya: "y = ?a"
-      have "orthogonal x y" using xa ya xy by blast}
-    moreover
-    {assume xa: "x = ?a" and ya: "y \<noteq> ?a" "y \<in> C"
-      from ya have Cy: "C = insert y (C - {y})" by blast
-      have fth: "finite (C - {y})" using C by simp
-      have "orthogonal x y"
-        using xa ya
-        unfolding orthogonal_def xa inner_simps diff_eq_0_iff_eq
-        apply simp
-        apply (subst Cy)
-        using C(1) fth
-        apply (simp only: setsum_clauses)
-        apply (auto simp add: inner_add inner_commute[of y a] inner_setsum_left)
-        apply (rule setsum_0')
-        apply clarsimp
-        apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
-        by auto}
-    moreover
-    {assume xa: "x \<noteq> ?a" "x \<in> C" and ya: "y = ?a"
-      from xa have Cx: "C = insert x (C - {x})" by blast
-      have fth: "finite (C - {x})" using C by simp
-      have "orthogonal x y"
-        using xa ya
-        unfolding orthogonal_def ya inner_simps diff_eq_0_iff_eq
-        apply simp
-        apply (subst Cx)
-        using C(1) fth
-        apply (simp only: setsum_clauses)
-        apply (subst inner_commute[of x])
-        apply (auto simp add: inner_add inner_commute[of x a] inner_setsum_right)
-        apply (rule setsum_0')
-        apply clarsimp
-        apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
-        by auto}
-    moreover
-    {assume xa: "x \<in> C" and ya: "y \<in> C"
-      have "orthogonal x y" using xa ya xy C(4) unfolding pairwise_def by blast}
-    ultimately have "orthogonal x y" using xC yC by blast}
-  then have CPO: "pairwise orthogonal ?C" unfolding pairwise_def by blast
+  { fix y assume yC: "y \<in> C"
+    hence Cy: "C = insert y (C - {y})" by blast
+    have fth: "finite (C - {y})" using C by simp
+    have "orthogonal ?a y"
+      unfolding orthogonal_def
+      unfolding inner_diff inner_setsum_left diff_eq_0_iff_eq
+      unfolding setsum_diff1' [OF `finite C` `y \<in> C`]
+      apply (clarsimp simp add: inner_commute[of y a])
+      apply (rule setsum_0')
+      apply clarsimp
+      apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
+      using `y \<in> C` by auto }
+  with `pairwise orthogonal C` have CPO: "pairwise orthogonal ?C"
+    by (rule pairwise_orthogonal_insert)
   from fC cC SC CPO have "?P (insert a B) ?C" by blast
   then show ?case by blast
 qed