定理記述

こんな感じかな。

theorem 定理の名前
 require モジュール1, モジュール2
 using 定義, 定理1, 定理2, 規則
 for 宣言1, 宣言2
 given 命題1, 命題2
 holds 命題
 proof
   証明
 end
end

考慮点は

• カンマの代わりにandか？
• for given の繰り返しを許すか
• holdsの前にforを許すか

proofの代わりに as axiom と as conjecture が許される。theorem as axiom と theorem as conjecture は別記法で書ける。

axiom 公理の名前
 require モジュール
 using 定義1, 定義2
 for 宣言1, 宣言2
 given 命題1, 命題2
 holds 命題
end

公理の記述のなかで定義を使うならば、requireとusingは書く。

色々と略記できる。

requireの共通化

module モジュール名
require モジュール1, モジュール2

theorem 定理の名前
 using 定義, 定理1, 定理2, 規則
 for 宣言1, 宣言2
 given 命題1, 命題2
 holds 命題
 proof
   証明
 end
end

宣言（型宣言）の共通化

module モジュール名
require モジュール1, モジュール2

for 宣言1, 宣言2

theorem 定理の名前
 using 定義, 定理1, 定理2, 規則

 given 命題1, 命題2
 holds 命題
 proof
   証明
 end
end

仮定の共通化

module モジュール名
require モジュール1, モジュール2

for 宣言1, 宣言2
given 命題1, 命題2

theorem 定理の名前
 using 定義, 定理1, 定理2, 規則
 holds 命題
 proof
   証明
 end
end

usingの省略

module モジュール名
require モジュール1, モジュール2

for 宣言1, 宣言2
given 命題1, 命題2

theorem 定理の名前
 holds 命題
 proof
   証明
 end
end

holdsの省略

module モジュール名
require モジュール1, モジュール2

for 宣言1, 宣言2
given 命題1, 命題2

theorem 定理の名前
 命題
 proof
   証明
 end
end