言語ごとに問題の解き方について解説します。
Isabelleでは通常、次のようなファイルが用意された状態でジャッジが行われます。
ROOT: このtheoryをビルドするために必要なファイル
Goal.thy: 示すべき定理が書かれたファイル
Submitted.thy: 提出されるファイル
Definitions.thy等: その他、問題で指定する定義が書かれたファイル(存在する場合)
提出されたファイルはSubmitted.thyという名前で保存されます。Goal.thyは通常、by (rule goal)の形で与えられるので、次を満たすようなtheoryファイルを提出することで正解となります。
theoryはSubmittedとすること
必要があれば指定されたファイル(Definitions.thyなど)をimportすること。特に指定がなければMainをimportしてよい。
goalという名前をもつ定理を1つ含む証明を提出すること。その際goalの命題は問題で要求されているものと同じものとすること。(命題そのものは問題ごとに与えられるGoal.thyを確認してください。)
証明は完全なものであること(sorryやoopsを含まないこと)。