CODEWITHSUNDEEP
isabelleisar
cxandru
cxandru

Reputation: 158

Induction on second argument Isar

inductive T :: "alpha list ⇒ bool" where
 Tε : "T []" |
 TaTb : "T l ⟹ T r ⟹ T (l @ a#(r @ [b]))"

lemma Tapp: "⟦T l;  T r⟧ ⟹ T (l@r)"
proof (induction r rule: T.induct)

I get 'Failed to apply initial proof method⌂'

In Isabelle one could use rotate_tac I guess to get induction to work on the desired argument, what's the Isar equivalent? Would it help to reformulate the lemma with 'assumes' & 'shows'?

Upvotes: 1

Views: 138

Answers (1)

Javier Díaz
Javier Díaz

Reputation: 1101

Rule induction is always on the leftmost premise of the goal. Therefore, the Isabelle/Isar solution consists on inverting the order of the premises:

lemma Tapp: "⟦T r;  T l⟧ ⟹ T (l@r)"
proof (induction r rule: T.induct)
...

Or, using assumes and shows:

lemma Tapp: assumes "T r" and "T l" shows "T (l@r)"
using assms proof (induction r rule: T.induct)
...

Upvotes: 3

Related Questions