更新 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，它是有限的，称为索引集。例如，让索引集定义为typedefas {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方法很容易生成一个 goal CARD(t123) = (3::nat)，其中t123是我定义的类型，其中包含 3 个元素。我无法克服这一点。
任何想了解细节的人都需要了解用于创建类型时创建的Rep_t和Abs_t函数的使用。在 的情况下，函数本来是and ，但它们被重命名为to and 。typedeftvecRep_vecAbs_vecmorphismsvec_nthvec_lambda
请问非向量特定向量长度请上一步
更新 140111
这应该是我的最后一次更新，因为要完全让我满意，我需要了解更多关于一般实例化类型类的知识，以及如何具体实例化类型类，以便我的具体示例UNIV::t123 set, 是有限的。
我非常欢迎在我可能错的地方得到纠正。我宁愿阅读Multivariate_Analysis教科书，也不愿像这样学习如何使用 Isar 和 Isabelle/HOL。
从表面上看，类型向量长度的概念('a, 'b) vec非常简单。它是类型的全集的基数'b::finite。
直观地说，这是有道理的，所以我过早地承诺了这个想法，但我不会永久承诺，因为我无法完成我的示例。
我在下面的“调查”理论的末尾添加了更新。
我之前没有做的是将我的示例类型，t123用 set 定义的类型实例{c1,c2,c3}化为类型 class top。
更短的故事是，在追求中top，value提示我涉及类型类card_UNIV，card_UNIV基于finite_UNIV. 同样，描述性标识符看起来如果我t123的类型是 class 类型finite_UNIV，那么我可以用 计算它的基数card，这将是使用 typet123作为索引集的任何向量的长度。
我在这里展示了一些术语，它们表明所涉及的内容，像往常一样，如果您加载了我的示例理论，可以通过 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，如 with card (UNIV::t123 set)，对 type 不起作用，vec因为您不能假设 type 类finite_UNIV已为索引集类型实例化。如果我对现在似乎很明显的事情有误，我想知道。
好吧，即使我定义的函数vector_length, 并没有尝试UNIV::'b set直接采用 的基数，但在我的示例中，简化器会产生目标CARD(t123) = (3::nat)。
我推测这对自己意味着什么，但我还没有追查到CARD，所以我把我的推测留给自己。
（更新结束。）
140117决赛决赛决赛
尝试使用value来学习使用card导致我误入歧途。该value命令基于代码生成器，并且value具有通常不需要的类型类要求。
不需要为类型 class 实例化索引集finite_UNIV。只是需要能够使用的逻辑必须card (UNIV::('b::finite set))到位。
似乎逻辑应该已经存在于Multivariate_Analysis我所做的任何事情中。我所说的任何事情都会有错误。
（更新结束。）
关于我vec在 Multivariate_Analysis 中的经验的结论
至少对我来说，使用广义索引集似乎过于复杂。向量作为列表似乎是我想要的，就像 Matrix.thy 一样，但有时事情可能需要很复杂。
最大的痛苦是使用typedef创建具有有限通用集的类型。我不知道如何轻松创建有限集。以前看到有评论说最好远离typedef。起初听起来不错，它基于集合创建了一个类型，但最终处理起来很麻烦。
[我在这里进一步评论vec. 我不得不求助于 ZFC 定义，因为我不知道用类型论将一般数学形式化的教科书在哪里。这篇 wiki 文章展示了一个广义的笛卡尔积：
Wiki：使用有限或无限索引集的无限产品定义
定义的关键是无限集可以用作索引集，例如实数。
就使用有限集作为索引集而言，任何有限的基数集n都可以与自然数 一对一地放置1...n，并且有限的自然数排序通常是我们使用向量的方式。
并不是说我不相信某个地方的某个人需要具有不是自然数的有限索引集的向量，而是我所看到的向量和矩阵的所有数学都是长度向量n::nat或n::nat x m::nat矩阵。
就我自己而言，我认为最好的向量和矩阵将基于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 条目来混淆事物。此外，除了 HOL 中的原子常量和变量之外，大多数东西都是一个函数，因此在没有上下文的情况下将某些东西分类为函数并不能澄清任何事情。提供不会产生错误的源代码会有所帮助。正常的入口点是Complex_Main。这总结了我在这里所说的大部分内容。）
相关问题的链接
[13-05-27] Isabelle：如何使用矩阵
[13-05-30] Isabelle：转置包含常数因子的矩阵
[13-06-25] Isabelle 矩阵算术：库中具有不同符号的 det_linear_row_setsum
[13-08-12] Isabelle：向量中的最大值
[13-09-12]多项式的次数小于一个数
[13-11-21] Isabelle：多项式的次数乘以常数
[13-11-26]伊莎贝尔：矩阵的幂（A^n）？
[13-12-01]伊莎贝尔：A * 1 和 A ** mat 1 的区别
[14-01-17]伊莎贝尔：setprod 的问题
