限量子の使いようが、いまひとつ理解しきれていない。 Isabelle の集合の条件部に EX を書くと、 EX の条件を満たすものが列挙される。 lemma "{0, 1, 2, 3, 4} = {u::nat. EX j k. j <= k & k < 3 & u = j + k}" apply auto apply (rule_tac x=0 in exI) ap…

PuTTY を使っていて、外部サーバーへの接続方法が ext-server (のような) 名前で保存されているとする。 > pscp -load "ext-server" <localfile name> <ext-server-account>@<ext-server name>:.</ext-server></ext-server-account></localfile>

正月休みにも継続できるよう、 Sourceforge のシェルアカウント内に Isabelle 環境を構築。公式のインストール手順に書かれている tarball を四つ落としてくる。 $ wget http://isabelle.in.tum.de/dist/Isabelle2008.tar.gz $ wget http://isabelle.in.tum.…