default value for parametricity of dim
authorimmler
Mon Jun 11 14:49:34 2018 +0200 (11 months ago)
changeset 6841207f8c09e3f79
parent 68411 d8363de26567
child 68414 b001bef9aa39
default value for parametricity of dim
src/HOL/Vector_Spaces.thy
     1.1 --- a/src/HOL/Vector_Spaces.thy	Mon Jun 11 08:15:43 2018 +0200
     1.2 +++ b/src/HOL/Vector_Spaces.thy	Mon Jun 11 14:49:34 2018 +0200
     1.3 @@ -524,7 +524,8 @@
     1.4  qed
     1.5  
     1.6  definition dim :: "'b set \<Rightarrow> nat"
     1.7 -  where "dim V = card (SOME b. independent b \<and> span b = span V)"
     1.8 +  where "dim V = (if \<exists>b. independent b \<and> span b = span V then
     1.9 +    card (SOME b. independent b \<and> span b = span V) else 0)"
    1.10  
    1.11  lemma dim_eq_card:
    1.12    assumes BV: "span B = span V" and B: "independent B"
    1.13 @@ -538,7 +539,8 @@
    1.14    then have "card B = card (SOME B. p B)"
    1.15      by (auto intro: bij_betw_same_card)
    1.16    then show ?thesis
    1.17 -    by (simp add: dim_def p_def)
    1.18 +    using BV B
    1.19 +    by (auto simp add: dim_def p_def)
    1.20  qed
    1.21  
    1.22  lemma basis_card_eq_dim: "B \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> card B = dim V"
    1.23 @@ -552,7 +554,7 @@
    1.24    by (rule dim_eq_card[OF refl])
    1.25  
    1.26  lemma dim_span[simp]: "dim (span S) = dim S"
    1.27 -  by (simp add: dim_def span_span)
    1.28 +  by (auto simp add: dim_def span_span)
    1.29  
    1.30  lemma dim_span_eq_card_independent: "independent B \<Longrightarrow> dim (span B) = card B"
    1.31    by (simp add: dim_eq_card)