Isabelle/Isar でルール導入を行いたい。見つけた
proof (rule_tac P="λn. f n ≥ n ∧ f n ≥ 1" in f.induct)
また
proof (rule f.induct[of "λn. f n ≥ n ∧ f n ≥ 1"])
私がやりたいことを正確に行います。しかし、「新しいスタイル」の Isar を使用してその行を書くにはどうすればよいでしょうか? ご覧のとおりP、関数の誘導規則で変数をインスタンス化する方法を Isabelle に伝えようとしているだけですf。