CODEWITHSUNDEEP
isabelleinduction
Wolfgang Jeltsch
Wolfgang Jeltsch

Reputation: 801

How can I combine rule induction with variable generalization in Isabelle?

In Isabelle, I can generalize variables in induction proofs using the arbitrary keyword. This definitely works for ordinary induction, like in apply (induction n arbitrary: m). I can also have rule induction, like in apply (induction rule: R.induct). But how can I generalize variables when using rule induction?

In my particular use case, I need to prove a theorem of the form R x ⟹ S y ⟹ ⟨…⟩. The predicate R is inductively defined, and I want to use rule induction for it. The variable y cannot be fixed in the proof, but must be arbitrary. As a workaround, I have proved the theorem R x ⟹ (∀ y . S y ⟶ ⟨…⟩) instead, but I was not able to prove it without resorting to the sledgehammer, and I also guess that using ∀ and ⟶ here is not canonical.

Upvotes: 0

Views: 416

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8248

You can combine arbitrary and rule without a problem. However, the arbitrary has to appear before the rule.

Upvotes: 2

Related Questions