← ファイル一覧
（保存にはログインが要ります）
1_basis/2_class.book
ヘッダ
行番号
title クラス author admin import 1_logic
section クラスの導入 txt このシステムではクラスというものも扱えます。gramにcが入ったwordが登場します。 txt クラスは素朴に「ものの集まり」と捉えるのが良いです。「属する」が基本になります。 word ∈_ txt クラスを走る変数がv_-Formです。gramが(,c)で `X_` などがあります。 txt `x ∈_ X_` はp-Formです。「`x`というものがクラス`X_`に入っている」と読むと良いでしょう。 txt `X_ ∈_ X_` はp-Formではありません(s-Formとc-Formは区別されます)。 br txt クラスを扱うときには、「クラスの等号」が出てきます。 word =_ txt これは次の「定義」を持ちます。一般に 〇. は 〇の定義 という位置づけになります。 prop =_. br txt cvtという規則が重要です。 txt 〇. は自然にcvt規則を生成します。=_. は次のようなcvtを生成します。 txt cvt …`$X =_ $Y` ≃ `∀ x \, (x ∈_ $X ⇔ x ∈_ $Y)` br txt 「単ソート翻訳」では cvt規則 によって \(\mathbb{W}_+\) が処理されます。 txt 次のthmはgoalが `∀ x \, (x ∈_ X_ ⇔ x ∈_ X_)` となり、自明です。 !let goal := `X_ =_ X_` thm goal -| O prf goal p-| O ; section 内包記法 txt 内包記法はクラスを生成する標準的な道具です。`\{ cls x | P^ \}` という自然な形で使用できるようにしておきます。 word \cls abbr cls !txt なお内包記法で `P^` に制限はありません。 br txt 次のcvtが重要です。 txt cvt …`$X ∈_ \{ cls x | $P \}`≃ substitution(`$P`, `x` ↦ `$X`) txt 次の翻訳は内側からやる方が楽です。<br> `x ∈_ \{ cls y | z ∈_ \{ cls x | x = y \} \}` ≅ `z = x` txt 外側からだと \(\int f(x)dx = \int f(y)dy\) みたいな「束縛変数の名前替え」が必要になります。
表示（保存しません）
保存にはMatheliaへのログインが要ります。