# HG changeset patch
# User immler
# Date 1528721374 -7200
# Node ID 07f8c09e3f79c36592b76f483461c85b8be581d0
# Parent  d8363de2656744998f9f18ae35c1af1c90fcdd5a
default value for parametricity of dim

diff -r d8363de26567 -r 07f8c09e3f79 src/HOL/Vector_Spaces.thy
--- a/src/HOL/Vector_Spaces.thy	Mon Jun 11 08:15:43 2018 +0200
+++ b/src/HOL/Vector_Spaces.thy	Mon Jun 11 14:49:34 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)