Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem with induction_schema

view this post on Zulip Email Gateway (Aug 22 2022 at 12:22):

From: Manuel Eberl <eberlm@in.tum.de>
Hallo,

Simon and I just came across the following problem with induction_schema
which is present both in Isabelle2015 and 45eee631ea4f:

This works as intended:
lemma "P 0 ⟹ (⋀n. P n ⟹ P (Suc n)) ⟹ P x"
apply (induction_schema)

But this leads to looping:

lemma "P 0 ⟹ (⋀x. P x ⟹ P (Suc x)) ⟹ P x"
apply (induction_schema)

Apparently, there is some strange issue with the variable names here.

Manuel

Last updated: Apr 24 2024 at 20:16 UTC