Rule induction in Isar

Question

I want to do a rule induction in Isabelle/Isar. I find that

proof (rule_tac P="λn. f n ≥ n ∧ f n ≥ 1" in f.induct)

or

proof (rule f.induct[of "λn. f n ≥ n ∧ f n ≥ 1"])

do exactly what I want. But how can I write that line using "new style" Isar? As you can see, I'm simply trying to tell Isabelle how to instantiate the P variable in the induction rule for my function f.

Answer 1

I would say that you are already using Isar style as there is no apply.

You can also use the syntax f.induct[where P="λn. f n ≥ n ∧ f n ≥ 1"].

Also, often it is not necessary to instantiate P manually since unification will give you P. Maybe you have to reformulate your goal to achieve this. In Isar style unification also happens after proof when you start a show, so that is another option to avoid giving it explicitly.