Я хочу провести индукцию правил в Изабель / Изар. Я нахожу это
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"])
делаю именно то, что хочу. Но как я могу написать эту строчку, используя «новый стиль» Isar? Как видите, я просто пытаюсь сказать Изабель, как создать экземпляр переменной P в правиле индукции для моей функции f.
Я бы сказал, что вы уже используете стиль Isar, поскольку apply отсутствует.
Вы также можете использовать синтаксис f.induct[where P="λn. f n ≥ n ∧ f n ≥ 1"].
Кроме того, часто нет необходимости создавать экземпляр P вручную, так как объединение даст вам P. Возможно, вам придется переформулировать свою цель, чтобы достичь этого. В стиле Isar унификация также происходит после proof, когда вы запускаете show, так что это еще один вариант, чтобы избежать его явного указания.
