Isabelleちょっとやってます、という近況報告？

ここ最近Isabelleを触っている。 Coqと比べると日本語の資料が少ないのでつらい。

とりあえずいろいろわからないことが出てきたので並べてみる。

2以上の自然数を扱うと簡約できない

例としてmap関数を定義する。

fun map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
  "map _ [] = []"
| "map f (x # xs) = (f x) # (map f xs)"

value "map (plus 3) (1 # 2 # [])"

そのまま自然数の3や5を命題に含めると解くことができない。

lemma test_map1: "map (\<lambda> x. plus 3 x) ((Suc 1) # 0 # (Suc 1) # []) = (5 # 3 # 5 # [])"
  sorry

(Suc (Suc 1)) みたいにすると解ける。

lemma test_map2: "map oddb (Suc 1 # 1 # Suc 1 # (Suc (Suc (Suc (Suc 1)))) # []) = (False # True # False # True # [])"
  apply (simp)
  done

もちろんこれを続けるのは限界があるので、なんか方法を見つけないといけない。

命題にforallの有無がどう影響を与えるかわかっていない

別の命題を解いてしまっているのではないかという懸念がある。 goalだけみると同じにみえるけどよくわかってない。

forallがないとうまくいかない場合

以下は Failed to apply proof method と怒られる。

lemma mult_eq_0: "n * m = 0 \<longrightarrow> n = 0 \<or> m = 0"
  apply (simp)
  done

\<forall> n m::nat. を命題に足すと No subgoals までできる。

lemma mult_eq_0: "\<forall> n m::nat. n * m = 0 \<longrightarrow> n = 0 \<or> m = 0"
  apply (simp)
  done

forallがあるとうまくいかない場合

以下は Cannot determine type b. と怒られる。

theorem not_true_is_false: "\<forall> b::bool. b \<noteq> True \<longrightarrow> b = False"
  apply (case_tac b)
   apply (simp_all)
  done

\<forall> b::bool. を命題から消すと No subgoals! までできる。

theorem not_true_is_false: "b \<noteq> True \<longrightarrow> b = False"
  apply (case_tac b)
   apply (simp_all)
  done