author immler Mon Jun 11 14:49:34 2018 +0200 (11 months ago) changeset 68412 07f8c09e3f79 parent 68411 d8363de26567 child 68414 b001bef9aa39
default value for parametricity of dim
```     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)
```