# HG changeset patch
# User nipkow
# Date 1528727378 -7200
# Node ID b001bef9aa39981e85655abe790af8c53d534295
# Parent  07f8c09e3f79c36592b76f483461c85b8be581d0# Parent  b56ed5010e6970b77688d0d033457e12a3ca849c
merged

diff -r b56ed5010e69 -r b001bef9aa39 src/HOL/Vector_Spaces.thy
--- a/src/HOL/Vector_Spaces.thy	Mon Jun 11 16:29:27 2018 +0200
+++ b/src/HOL/Vector_Spaces.thy	Mon Jun 11 16:29:38 2018 +0200
@@ -524,7 +524,8 @@
 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"
@@ -538,7 +539,8 @@
   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"
@@ -552,7 +554,7 @@
   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)