更新 140107_2040
在这里很难做出简短的回答。我只为向量工作，因为这一切都非常复杂。我尝试尽可能快地为您提供向量长度的函数。然后，我将详细解释我做了什么来对向量类型有一个体面的理解，但如果你不需要它，不一定适合你。
由名称 Finite_Cartesian_Product.thy 反映，Amine Chaieb 定义了一个广义的有限笛卡尔积。所以，当然，我们也得到了向量和 n 元组的定义。它是一个广义的笛卡尔积需要大量的解释，也是我花了很长时间才认识到和解决的问题。话虽如此，我将其称为向量，因为他将类型命名为vec。
一切都需要参考什么是向量来理解，向量是由这个定义定义的：
typedef ('a, 'b) vec = "UNIV :: (('b::finite) => 'a) set"
这告诉我们向量是一个函数f::('b::finite) => 'a。函数的域是UNIV::'b set，它是有限的，称为索引集。例如，让索引集用typedef 定义为{1,2,3}。
函数的codomain可以是任何类型，但让它是一组常量{a,b}，用typedef定义。因为 HOL 函数是总的，所以 {1,2,3} 的每个元素都必须映射到 {a,b} 的一个元素。
现在，考虑将元素从{1,2,3} 映射到{a,b} 的所有此类函数的集合。会有2^3 = 8这样的功能。我现在求助于 ZFC 函数表示法以及 n 元组表示法：
f_1: {1,2,3} --> {a,b} == {(1,a),(2,a),(3,a)} == (a,a,a)
f_2 == {(1,a),(2,a),(3,b)} == (a,a,b)
f_3 == {(1,a),(2,b),(3,a)} == (a,b,a)
f_4 == {(1,a),(2,b),(3,b)} == (a,b,b)
f_5 to f_8 == (b,a,a), (b,a,b), (b,b,a), (b,b,b)
那么对于任何向量f_i，它又是一个函数，向量的长度将是f_i的域的基数，即3。
我很确定你的函数card_diagonal 是函数范围的基数，我在更远的地方测试了它的矢量版本，但它基本上向我展示了如何获得域的基数。
这是向量长度的函数：
definition vec_length :: "('a, 'b::finite) vec => nat" where
"vec_length v = card {i. ? c. c = (vec_nth v) i}"
declare
vec_length_def [simp add]
您可能想用v $ i 替换(vec_nth v) i。 ? 是 \<exists>。
在下面的示例中，simp 方法很容易生成目标CARD(t123) = (3::nat)，其中t123 是我定义的类型，其中包含 3 个元素。我过不去。
任何想了解细节的人都需要了解Rep_t和Abs_t函数的使用，它们是在typedef用于创建类型t时创建的。在vec 的情况下，函数本来是Rep_vec 和Abs_vec，但它们用morphisms 重命名为vec_nth 和vec_lambda。
非向量特定向量长度请上一步
更新 140111
这应该是我的最后一次更新，因为要完全让我满意，我需要了解更多关于一般实例化类型类的知识，以及如何具体实例化类型类，以便我的具体示例UNIV::t123 set，是有限的。
我非常欢迎在我可能错的地方得到纠正。我宁愿在教科书中阅读有关Multivariate_Analysis 的内容，也不愿像这样学习如何使用 Isar 和 Isabelle/HOL。
从表面上看，('a, 'b) vec 类型向量的长度概念非常简单。它是'b::finite 类型的全集的基数。
直观地说，这是有道理的，所以我过早地承诺了这个想法，但我不会永久承诺，因为我无法完成我的示例。
我在下面的“调查”理论的末尾添加了更新。
我之前没有做的是实例化我的示例类型t123，这是一个使用集合{c1,c2,c3} 定义的类型，作为类型类top。
更短的故事是，在追求top 时，value 提示我涉及类型类card_UNIV，其中card_UNIV 是基于finite_UNIV。再一次，描述性标识符看起来如果我的类型 t123 是类型类 finite_UNIV，那么我可以使用 card 计算它的基数，这将是使用类型 t123 的任何向量的长度索引集。
我在这里展示了一些术语来表明所涉及的内容，通常，如果您加载了我的示例理论，可以通过 cntl 单击各种标识符来研究这些术语。更多细节在我下面的调查来源中。
term "UNIV::t123 set"
term "top::t123 set"
term "card (UNIV::t123 set)" (*OUTPUT PANEL: CARD(t123)::nat.*)
term "card (top::t123 set)" (*OUTPUT PANEL: CARD(t123)::nat.*)
value "card (top::t123 set)" (*ERROR: Type t123 not of sort card_UNIV.*)
term "card_UNIV"
term "finite_UNIV"
（更新结束。）
140112最终更新到最后更新
不永久承诺是值得的，虽然回答问题是一种很好的学习方式，但在这种情况下也有不利之处。
对于向量类型，定义中唯一的类型类是finite，但是，上面，我正在做的涉及类型类finite_UNIV，它在src/HOL/Library/Cardinality.thy中。
尝试使用card，就像使用card (UNIV::t123 set) 一样，对于vec 类型不起作用，因为您不能假定类型类finite_UNIV 已为索引集类型实例化。如果我对现在似乎很明显的事情有误，我想知道。
好吧，尽管我定义的函数vector_length 并没有尝试直接采用UNIV::'b set 的基数，但在我的示例中，简化器产生了目标CARD(t123) = (3::nat)。
我推测这对自己意味着什么，但我还没有找到CARD，所以我把我的推测留给自己。
（更新结束。）
140117决赛决赛决赛
试图使用value来了解card的使用让我误入歧途。 value 命令基于代码生成器，value 将具有一般不需要的类型类要求。
没有要求为类型类finite_UNIV 实例化索引集。只是需要能够使用card (UNIV::('b::finite set)) 的逻辑必须到位。
对于我所做的任何事情，似乎Multivariate_Analysis 中应该已经存在逻辑。我所说的任何内容都会有错误。
（更新结束。）
关于我在 Multivariate_Analysis 中使用 vec 的经验的结论
至少对我而言，使用广义索引集似乎过于复杂。向量作为列表似乎是我想要的，就像 Matrix.thy 一样，但有时事情可能需要很复杂。
最大的痛苦是使用typedef 创建一个具有有限全集的类型。我不知道如何轻松创建有限集。以前看到有评论说最好远离typedef。起初听起来不错，它基于集合创建类型，但最终处理起来很麻烦。
[我在此进一步评论vec 中使用的有限广义索引集。我不得不求助于 ZFC 定义，因为我不知道用类型论将一般数学形式化的教科书在哪里。这篇 wiki 文章展示了一个广义的笛卡尔积：
Wiki: Infinite product definition using a finite or infinite index set
定义的关键是无限集可以作为索引集，比如实数。
就使用有限集作为索引集而言，任何基数有限集n 都可以与自然数1...n 一对一放置，而有限的自然数排序通常是我们的方式将使用向量。
并不是说我不相信某个地方的某个人需要具有有限索引集的向量，它不是自然数，而是我所看到的向量和矩阵的所有数学运算都是长度为 n::nat 或 @ 987654409@ 矩阵。
就我自己而言，我认为最好的向量和矩阵将基于list，因为列表的组件位置基于自然数。使用 Isabelle/HOL list 会带来很多计算魔法。]
我通过什么来获得以上成就
我花了很多功夫来解决这个问题。我对如何使用 Isabelle 的了解要少得多。
(*It's much faster to start jEdit with Multivariate_Analysis as the logic.*)
theory i140107a__Multvariate_Ana_vec_length
imports Complex_Main Multivariate_Analysis (*"../../../iHelp/i"*)
begin
declare[[show_sorts=true]] (*Set false if you don't want typing shown.*)
declare[[show_brackets=true]]
(*---FINITE UNIVERSAL SET, NOT FINITE SET
*)
(*
First, we need to understand what `x::('a::finite)` means. It means that
`x` is a type for which the universal set of it's type is finite, where
the universal set is `UNIV::('a set)`. It does not mean that terms of type
`'a::finite` are finite sets.
The use of `typedef` below will hopefully make this clear. The following are
related to all of this, cntl-click on them to investigate them.
*)
term "x::('a::finite)"
term "finite::('a set => bool)" (*the finite predicate*)
term "UNIV::('a set) == top" (*UNIV is designated universal set in Set.thy.*)
term "finite (UNIV :: 'a set)"
term "finite (top :: 'a set)"
(*
It happens to be that the `finite` predicate is used in the definition of
type class `finite`. Here are some pertinent snippets, after which I comment
on them:
class top =
fixes top :: 'a ("⊤")
abbreviation UNIV :: "'a set" where
"UNIV == top"
class finite =
assumes finite_UNIV: "finite (UNIV :: 'a set)"
The `assumes` in the `finite` type-class specifies that constant `top::'a set`
is finite, where `top` can be seen as defined in type-class `top`. Thus, any
type of type-class `top` must have a `top` constant.
The constant `top` is in Orderings.thy, and the Orderings theory comes next
after HOL.thy, which is fundamental. As to why this use of the constant `top`
by type-class `finite` can make the universe of a type finite, I don't know.
*)
(*---DISCOVERING LOWER LEVEL SYNTAX TO WORK WITH
*)
(*
From the output panel, I copied the type shown for `term "v::('a ^ 'b)"`. I
then cntl-clicked on `vec` to take me to the `vec` definition.
*)
term "v::('a ^ 'b)"
term "v::('a,'b::finite) vec"
(*
The `typedef` command defines the `('a, 'b) vec` type as an element of a
particular set, in particular, as an element in the set of all functions of
type `('b::finite) => 'a`. I rename `vec` to `vec2` so I can experiment with
`vec2`.
*)
typedef ('a, 'b) vec2 = "UNIV :: (('b::finite) => 'a) set"
by(auto)
notation
Rep_vec2 (infixl "$$" 90)
(*
The `morphisms` command renamed `Rep_vec` and `Abs_vec` to `vec_nth` and
`vec_lambda`, but I don't rename them for `vec2`. To create the `vec_length`
function, I'll be using the `Rep` function, which is `vec_nth` for `vec`.
However, the `Abs` function comes into play further down with the concrete
examples. It's used to coerce a function into a type that uses the type
construcor `vec`.
*)
term "Rep_vec2::(('a, 'b::finite) vec2 => ('b::finite => 'a))"
term "Abs_vec2::(('a::finite => 'b) => ('b, 'a::finite) vec2)"
(*---FIGURING OUT HOW THE REP FUNCTION WORKS WITH 0, 1, OR 2 ARGS
*)
(*
To figure it all out, I need to study these Rep_t function types. The type
of terms without explicit typing have the type shown below them, with the
appropriate `vec` or `vec2`.
*)
term "op $"
term "vec_nth"
term "op $$"
term "Rep_vec2::(('a, 'b::finite) vec2 => ('b::finite => 'a))"
term "op $ x"
term "vec_nth x"
term "op $$ x"
term "(Rep_vec2 x)::('b::finite => 'a)"
term "x $ i"
term "op $ x i"
term "vec_nth x i"
term "x $$ i"
term "op $$ x i"
term "(Rep_vec2 (x::('a, 'b::finite) vec2) (i::('b::finite))) :: 'a"
(*
No brackets shows more clearly that `x $$ i` is the curried function
`Rep_vec2` taking the arguments `x::(('a, 'b::finite) vec2)` and
`i::('b::finite)`.
*)
term "Rep_vec2::('a, 'b::finite) vec2 => 'b::finite => 'a"
(*---THE FUNCTION FOR THE LENGTH OF A VECTOR*)
(*
This is based on your `card_diagonal`, but it's `card` of the range of
`vec_nth v`. You want `card` of the domain.
*)
theorem "{ (v $ i) | i. True } = {c. ? i. c = (v $ i)}"
by(simp)
definition range_size :: "('a, 'b::finite) vec => nat" where
"range_size v = card {c. ? i. c = (v $ i)}"
declare
range_size_def [simp add]
(*
This is the card of the domain of `(vec_nth v)::('b::finite => 'a)`. I use
`vec_nth v` just to emphasize that what we want is `card` of the domain.
*)
theorem "(vec_nth v) i = (v $ i)"
by(simp)
definition vec_length :: "('a, 'b::finite) vec => nat" where
"vec_length v = card {i. ? c. c = (vec_nth v) i}"
declare
vec_length_def [simp add]
theorem
"∀x y. vec_length (x::('a, 'b) vec) = vec_length (y::('a, 'b::finite) vec)"
by(simp)
(*---EXAMPLES TO TEST THINGS OUT
*)
(*
Creating some constants.
*)
typedecl cT
consts
c1::cT
c2::cT
c3::cT
(*
Creating a type using the set {c1,c2,c3}.
*)
typedef t123 = "{c1,c2,c3}"
by(auto)
(*
The functions Abs_t123 and Rep_t123 are created. I have to use Abs_t123 below
to coerce the type of `cT` to `t123`. Here, I show the type of `Abs_t123`.
*)
term "Abs_t123 :: (cT => t123)"
term "Abs_t123 c1 :: t123"
(*
Use these `declare` commands to do automatic `Abs` coercion. I comment
them out to show how I do coercions explicitly.
*)
(*declare [[coercion_enabled]]*)
(*declare [[coercion Abs_t123]]*)
(*
I have to instantiate type `t123` as type-class `finite`. It seems it should
be simple to prove, but I can't prove it, so I use `sorry`.
*)
instantiation t123 :: finite
begin
instance sorry
end
term "UNIV::t123 set"
term "card (UNIV::t123 set)"
theorem "card (UNIV::t123 set) = 3"
try0
oops
(*
Generalized vectors use an index set, in this case `{c1,c2,c3}`. A vector is
an element from the set `(('b::finite) => 'a) set`. Concretely, my vectors are
going to be from the set `(t123 => nat) set`. I define a vector by defining a
function `t123_to_0`. Using normal vector notation, it is the vector
`<0,0,0>`. Using ZFC ordered pair function notation, it is the set
{(c1,0),(c2,0),(c3,0)}.
*)
definition t123_to_0 :: "t123 => nat" where
"t123_to_0 x = 0"
declare
t123_to_0_def [simp add]
(*
I'm going to have to use `vec_lambda`, `vec_nth`, and `Abs_t123`, so I create
some `term` variations to look at types in the output panel, to try to figure
out how to mix and match functions and arguments.
*)
term "vec_lambda (f::('a::finite => 'b)) :: ('b, 'a::finite) vec"
term "vec_lambda t123_to_0 :: (nat, t123) vec"
term "vec_nth (vec_lambda t123_to_0)"
term "vec_nth (vec_lambda t123_to_0) (Abs_t123 c1)"
(*
The function `vec_length` seems to work. You'd think that `CARD(t123) = 3`
would be true. I try to cntl-click on `CARD`, but it doesn't work.
*)
theorem "vec_length (vec_lambda t123_to_0) = (3::nat)"
apply(simp)
(*GOAL: (CARD(t123) = (3::nat))*)
oops
theorem "(vec_nth (vec_lambda t123_to_0) (Abs_t123 c1)) = (0::nat)"
by(auto)
theorem "range_size (vec_lambda t123_to_0) = (1::nat)"
by(auto)
definition t123_to_x :: "t123 => t123" where
"t123_to_x x = x"
declare
t123_to_x_def [simp add]
theorem "(vec_nth (vec_lambda t123_to_x) (Abs_t123 c1)) = (Abs_t123 c1)"
by(auto)
theorem "(vec_nth (vec_lambda t123_to_x) (Abs_t123 c2)) = (Abs_t123 c2)"
by(auto)
(*THE LENGTH BASED SOLELY ON THE TYPE, NOT ON A PARTICULAR VECTOR
*)
(*Update 140111: The length of a vector is going to be the cardinality of the
universal set of the type, `UNIV::('a::finite set)`. For `t123`, the following
terms are involved.
*)
term "UNIV::t123 set"
term "top::t123 set"
term "card (UNIV::t123 set)" (*OUTPUT PANEL: CARD(t123)::nat.*)
term "card (top::t123 set)" (*OUTPUT PANEL: CARD(t123)::nat.*)
(*
It can be seen that `card (top::t123 set)` is the same as the theorem above
with the goal `CARD(t123) = (3::nat)`. What I didn't do above is instantiate
type `t123` for type-class `top`. I try to define `top_t123`, but it gives me
an error.
*)
instantiation t123 :: top
begin
definition top_t123 :: "t123 set" where
"top_t123 = {Abs_t123 c1, Abs_t123 c2, Abs_t123 c3}"
(*ERROR
Clash of specifications
"i140107a__Multvariate_Ana_vec_length.top_set_inst.top_set_def" and
"Set.top_set_inst.top_set_def" for constant "Orderings.top_class.top"
*)
instance sorry
end
(*To define the cardinality of type `t123` appears to be an involved process,
but maybe there's one easy type-class that can be instantiated that gives me
everything I need. The use of `value` shows that type `t123` needs to be
type-class `card_UNIV`, but `card_UNIV` is based on class `finite_UNIV`.
Understanding it all is involved enough to give job security to a person who
does understand it.
*)
value "card (top::t123 set)" (*ERROR: Type t123 not of sort card_UNIV.*)
term "card_UNIV"
term "finite_UNIV"
(******************************************************************************)
end
我的答案的第一部分
（因为没有显示源的导入，所以不清楚任何运算符的来源。还有Matrix AFP entry 混淆事物。此外，除了 HOL 中的原子常量和变量之外，大多数东西都是一个函数，因此将某些东西分类为函数并不能在没有上下文的情况下澄清任何事情。提供不会产生错误的源代码会有所帮助。正常的入口点是Complex_Main。这总结了我在这里所说的大部分内容.)
相关问题的链接
[13-05-27]Isabelle: how to work with matrices
[13-05-30]Isabelle: transpose a matrix that includes a constant factor
[13-06-25]Isabelle matrix arithmetic: det_linear_row_setsum in library with different notation
[13-08-12]Isabelle: maximum value in a vector
[13-09-12]Degree of polynomial smaller than a number
[13-11-21]Isabelle: degree of polynomial multiplied with constant
[13-11-26]Isabelle: Power of a matrix (A^n)?
[13-12-01]Isabelle: difference between A * 1 and A ** mat 1
[14-01-17]Isabelle: Issue with setprod