単純な帰納的に定義された集合について補題があるとしましょう:
inductive_set foo :: "'a ⇒ 'a list set" for x :: 'a where
"[] ∈ foo x" | "[x] ∈ foo x"
lemma "⋀x y. y ∈ foo x ⟹ qux x y ⟹ baz x y"
(「⋀x y」ビットが残ることは私にとって重要です。補題は、長い適用チェーンの途中で私の証明の状態を実際に述べているからです。)
この補題の証明を開始するのに問題があります。ルール誘導で進めたいと思います。
最初の試み
書いてみた
apply (induct rule: foo.induct)
しかし、それはうまくいきません:inductメソッドは失敗します。x次のように、y明示的に修正してからメソッドを呼び出すことで、これを回避できることがわかりましinductた。
proof -
fix x :: 'a
fix y :: "'a list"
assume "y ∈ foo x" and "qux x y"
thus "baz x y"
apply (induct rule: foo.induct)
oops
ただし、実際には適用チェーンの途中なので、構造化された証明ブロックには入りたくありません。
2 回目の試行
代わりにメソッドを使用してみましinduct_tacたが、残念ながら、ルールを希望どおりにinduct_tac適用できません。foo.induct入力すると
apply (induct_tac rule: foo.induct, assumption)
最初のサブゴールは
⋀x y. y ∈ foo x ⟹ qux x y ⟹ baz x []
qux x []これは私が望むものではありません:の代わりに欲しかったのですqux x y。このinduct方法はこれを正しく行いましたが、上記で説明した他の問題がありました。