'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'?
Sources
This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.
Source: Stack Overflow
| Solution | Source |
|---|