summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | eberlm <eberlm@in.tum.de> |

Sat, 15 Jul 2017 21:40:24 +0100 | |

changeset 66281 | 6ad54b84ca5d |

parent 66280 | 0c5eb47e2696 |

child 66282 | e5ba49a72ab9 |

facts about cardinality of vector type

--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Sat Jul 15 16:27:10 2017 +0100 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Sat Jul 15 21:40:24 2017 +0100 @@ -9,6 +9,8 @@ Euclidean_Space L2_Norm "~~/src/HOL/Library/Numeral_Type" + "~~/src/HOL/Library/Countable_Set" + "~~/src/HOL/Library/FuncSet" begin subsection \<open>Finite Cartesian products, with indexing and lambdas.\<close> @@ -55,6 +57,80 @@ lemma vec_lambda_eta: "(\<chi> i. (g$i)) = g" by (simp add: vec_eq_iff) +subsection \<open>Cardinality of vectors\<close> + +instance vec :: (finite, finite) finite +proof + show "finite (UNIV :: ('a, 'b) vec set)" + proof (subst bij_betw_finite) + show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" + by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff) + have "finite (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" + by (intro finite_PiE) auto + also have "(PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set)) = Pi UNIV (\<lambda>_. UNIV)" + by auto + finally show "finite \<dots>" . + qed +qed + +lemma countable_PiE: + "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)" + by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) + +instance vec :: (countable, finite) countable +proof + have "countable (UNIV :: ('a, 'b) vec set)" + proof (rule countableI_bij2) + show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" + by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff) + have "countable (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" + by (intro countable_PiE) auto + also have "(PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set)) = Pi UNIV (\<lambda>_. UNIV)" + by auto + finally show "countable \<dots>" . + qed + thus "\<exists>t::('a, 'b) vec \<Rightarrow> nat. inj t" + by (auto elim!: countableE) +qed + +lemma infinite_UNIV_vec: + assumes "infinite (UNIV :: 'a set)" + shows "infinite (UNIV :: ('a, 'b :: finite) vec set)" +proof (subst bij_betw_finite) + show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" + by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff) + have "infinite (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" (is "infinite ?A") + proof + assume "finite ?A" + hence "finite ((\<lambda>f. f undefined) ` ?A)" + by (rule finite_imageI) + also have "(\<lambda>f. f undefined) ` ?A = UNIV" + by auto + finally show False + using \<open>infinite (UNIV :: 'a set)\<close> by contradiction + qed + also have "?A = Pi UNIV (\<lambda>_. UNIV)" + by auto + finally show "infinite (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" . +qed + +lemma CARD_vec [simp]: + "CARD(('a,'b::finite) vec) = CARD('a) ^ CARD('b)" +proof (cases "finite (UNIV :: 'a set)") + case True + show ?thesis + proof (subst bij_betw_same_card) + show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" + by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff) + have "CARD('a) ^ CARD('b) = card (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" + (is "_ = card ?A") + by (subst card_PiE) (auto simp: prod_constant) + + also have "?A = Pi UNIV (\<lambda>_. UNIV)" + by auto + finally show "card \<dots> = CARD('a) ^ CARD('b)" .. + qed +qed (simp_all add: infinite_UNIV_vec) subsection \<open>Group operations and class instances\<close>