Since multi-way trees can be defined as a recursive type:
data RoseTree a = Node {leaf :: a, subTrees :: [RoseTree a]}
is there a corresponding principle for performing structural induction on this type?
To state that property P holds for all (*) rose trees, you have to prove that
l :: [RoseTree] is a list of rose trees whose elements satisfy P, and x :: a is arbitrary, then Note x l satisfies PThe part about P holding on the elements of l is the induction hypothesis, which you can use to prove P(Node x l).
There is no explicit base case here: this is because there's no explicit base case constructor. Yet, Node x [] acts as an implicit base case for the trees,
and indeed when l is empty we get a base case for induction implicitly. Concretely, the hypothesis "all the elements of l satisfy P" becomes vacuously true when l is empty, so we get P(Node x []) from the induction principle above.
(*) More precisely, this principle proves P for every finite-depth rose tree. If you really have to consider infinite-depth ones (e.g. circular trees), you need coinduction.