更新 140107_2040
ここで短い答えを出すのは難しいです。すべてが非常に複雑になるため、私はベクトルに対してのみすべてを処理します。ベクトルの長さの関数をできるだけ早く提供しようとしています。次に、ベクター型を適切に理解するために何をしたかについての大きな説明に入りますが、必要がない場合は、必ずしもそうではありません。
Finite_Cartesian_Product.thy という名前に反映されている Amine Chaieb は、一般化された有限デカルト積を定義しています。したがって、もちろん、ベクトルと n-タプルの定義も取得します。それが一般化されたデカルト積であることは、膨大な説明を必要とするものであり、認識して作業するのに長い時間がかかったものです. そうは言っても、彼は type という名前を付けたので、これを vector と呼びますvec。
この定義によって定義されるベクトルとは何かを参照して、すべてを理解する必要があります。
typedef ('a, 'b) vec = "UNIV :: (('b::finite) => 'a) set"
これは、ベクトルが関数であることを示していますf::('b::finite) => 'a。関数の定義域は でありUNIV::'b set、これは有限であり、インデックス セットと呼ばれます。たとえば、インデックス セットをtypedefasで定義するとし{1,2,3}ます。
関数のコドメインは任意の型にすることができますが{a,b}、 で定義された定数のセットにしtypedefます。HOL 関数は合計であるため、 の各要素を{1,2,3}の要素にマップする必要があります{a,b}。
ここで、要素を から にマップするすべての関数のセットを考えてみましょ{1,2,3}う{a,b}。そのよう2^3 = 8な機能があります。私は今、nタプル表記とともにZFC関数表記に頼っています。
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_i3 になります。
あなたの関数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メソッドは簡単に goalCARD(t123) = (3::nat)を生成しました。ここで、t123は 3 つの要素で定義した型です。私はそれを乗り越えることができませんでした。
詳細を理解したい人は、を使用して type を作成するときに作成されるRep_tおよびAbs_t関数の使用法を理解する必要があります。の場合、関数は とでしたが、とに名前が変更されています。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に知らせたということです。繰り返しになりますが、記述的な識別子により、私の型が class型である場合、そのカーディナリティを で計算できるように見えます。これは、 typeをインデックス セットとして使用する任意のベクトルの長さになります。valuecard_UNIVcard_UNIVfinite_UNIVt123finite_UNIVcardt123
何が関係しているかを示すいくつかの用語をここに示します。私の例の理論が読み込まれている場合は、いつものように、さまざまな識別子を 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、一般に必要とされない型クラスの要件があります。
型 class に対してインデックス セットをインスタンス化する必要はありませんfinite_UNIV。使用できるようにするために必要なロジックがcard (UNIV::('b::finite set))整っていなければならないというだけです。
Multivariate_Analysis私が行ったすべてのことに対して、ロジックはすでにそこにあるはずです。私が言ったことはすべて誤りの対象です。
(更新終了。)
vecここでの Multivariate_Analysisでの私の経験についての結論
一般化されたインデックス セットを使用することは、少なくとも私にとっては非常に複雑に思えます。リストとしてのベクトルは、Matrix.thy のように、私が望むもののように思えますが、時には複雑にする必要があるかもしれません。
最大の問題typedefは、有限のユニバーサル セットを持つ型を作成するために使用することです。有限集合を簡単に作成する方法がわかりません。近づかないほうがいいというコメントを過去に見ましたtypedef。セットに基づいて型を作成するというのは一見良さそうに思えますが、処理が面倒です。
[ここで、 で使用されている有限の一般化されたインデックス セットについてさらにコメントしvecます。型理論で一般数学を形式化する教科書がどこにあるのかわからないため、ZFC の定義に頼らなければなりません。この wiki 記事は、一般化されたデカルト積を示しています。
Wiki: 有限または無限のインデックス セットを使用した無限の製品定義
定義の鍵は、実数などの無限集合をインデックス セットとして使用できることです。
インデックス セットとして有限セットを使用する限り、カーディナリティの有限セットはn自然数と 1 対 1 で配置でき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
私の答えの最初の部分
(ソースのインポートが表示されていないため、オペレーターがどこから来ているのかは明らかではありませんでした。物事を混乱させるマトリックス AFP エントリもあります。さらに、HOL のアトミック定数と変数を除いて、ほとんどすべてがしたがって、何かを関数として分類しても、文脈がなければ何も明確にはなりません. エラーを生成しないソースを提供すると役立ちます. 通常のエントリポイントはComplex_Mainです. これは、私がここで述べたことのほとんどを要約しています.
関連する質問へのリンク
[13-05-27] Isabelle: 行列の扱い方
[13-05-30] Isabelle: 定数因子を含む行列を転置します
[13-06-25]イザベル行列演算: ライブラリ内の det_linear_row_setsum 表記が異なる
[13-08-12] Isabelle: ベクトルの最大値
[13-09-12]数値より小さい多項式の次数
[13-11-21] Isabelle: 定数を乗じた多項式の次数
[13-11-26] Isabelle: 行列 (A^n) の累乗?
[13-12-01] Isabelle: A*1 と A**mat 1 の違い
[14-01-17] Isabelle: setprod の問題
