miz3

miz3
http://arxiv.org/abs/1201.3601
はメモリー（Unixのみ）に常駐して mizar のような natural language declarative style の証明を書く為の自動入力ツールで，インストールは

cp miz3/exrc ~/.exrc
export PATH = $PATH:~/CAS/hol_light/miz3/bin

として，HOL Light から

#use "miz3/make.ml";;

とすれば，vi 上で Ctrl+c Return により，次のアクションをプロンプトしてくれます（便利かも知れませんが，私には．．．）．

また，既存の HOL Light の証明からのコンバート機能も備えいます（こちらはそれなりに楽しめそうです）．使い方は簡単で，上に続けて

#use "miz3/miz3_of_hol.ml";;

とし，例えば，test.ml というファイルに

let thm20130322 = prove
 (`!m. ODD (3 EXP m)`,
  INDUCT_TAC THENL
  [ARITH_TAC;
   ASM_MESON_TAC [ARITH_RULE `ODD 3`; EXP; ODD_MULT]]);;

と書かれていれば

# miz3_of_hol "test.ml" "thm20130322";;
0..0..1..4..13..38..103..256..617..1449..solved at 3337
val it : step =
  !m. ODD (3 EXP m) [1]
  proof
    ODD (3 EXP 0) [2] by ARITH_TAC;
    !m. ODD (3 EXP m) ==> ODD (3 EXP SUC m) [3]
    proof
      let m be num;
      assume ODD (3 EXP m) [4];
    qed
      by ASM_MESON_TAC [ARITH_RULE (parse_term "ODD 3"); EXP; ODD_MULT],4;
  qed by INDUCT_TAC from 1,2;

のようになります．

おまけ

# let tm = `!m. ODD (3 EXP m)` ;;
val tm : term = `!m. ODD (3 EXP m)`
# PV9 [MK_num_INDUCTION tm; ARITH_RULE `ODD 1 /\ ODD 3`; EXP; ODD_MULT] tm;;
-------- Proof 1 --------

THEOREM PROVED

------ process 3952 exit (max_proofs) ------
val it : thm = |- !m. ODD (3 EXP m)