src/HOL/Vector_Spaces.thy

   from this[of B C] this[of C B] B C eq \<open>infinite C\<close> \<open>infinite B\<close>
   show ?thesis by (auto simp add: ordIso_iff_ordLeq card_of_ordIso)
 qed
 
 definition dim :: "'b set \<Rightarrow> nat"
-  where "dim V = card (SOME b. independent b \<and> span b = span V)"
+  where "dim V = (if \<exists>b. independent b \<and> span b = span V then
+    card (SOME b. independent b \<and> span b = span V) else 0)"
 
 lemma dim_eq_card:
   assumes BV: "span B = span V" and B: "independent B"
   shows "dim V = card B"
 proof -

   then have "\<exists>f. bij_betw f B (SOME B. p B)"
     by (subst (asm) p_def, intro bij_if_span_eq_span_bases[OF B]) (simp_all add: BV)
   then have "card B = card (SOME B. p B)"
     by (auto intro: bij_betw_same_card)
   then show ?thesis
-    by (simp add: dim_def p_def)
+    using BV B
+    by (auto simp add: dim_def p_def)
 qed
 
 lemma basis_card_eq_dim: "B \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> card B = dim V"
   using dim_eq_card[of B V] span_mono[of B V] span_minimal[OF _ subspace_span, of V B] by auto
 

 
 lemma dim_eq_card_independent: "independent B \<Longrightarrow> dim B = card B"
   by (rule dim_eq_card[OF refl])
 
 lemma dim_span[simp]: "dim (span S) = dim S"
-  by (simp add: dim_def span_span)
+  by (auto simp add: dim_def span_span)
 
 lemma dim_span_eq_card_independent: "independent B \<Longrightarrow> dim (span B) = card B"
   by (simp add: dim_eq_card)
 
 lemma dim_le_card: assumes "V \<subseteq> span W" "finite W" shows "dim V \<le> card W"