equal
deleted
inserted
replaced
31 |
31 |
32 lemma dimindex_unique: " (UNIV :: 'a set) hassize n ==> DIM('a) = n" |
32 lemma dimindex_unique: " (UNIV :: 'a set) hassize n ==> DIM('a) = n" |
33 by (simp add: dimindex_def hassize_def) |
33 by (simp add: dimindex_def hassize_def) |
34 |
34 |
35 |
35 |
36 section{* An indexing type parametrized by base type. *} |
36 subsection{* An indexing type parametrized by base type. *} |
37 |
37 |
38 typedef 'a finite_image = "{1 .. DIM('a)}" |
38 typedef 'a finite_image = "{1 .. DIM('a)}" |
39 using dimindex_ge_1 by auto |
39 using dimindex_ge_1 by auto |
40 |
40 |
41 lemma finite_image_image: "(UNIV :: 'a finite_image set) = Abs_finite_image ` {1 .. DIM('a)}" |
41 lemma finite_image_image: "(UNIV :: 'a finite_image set) = Abs_finite_image ` {1 .. DIM('a)}" |