Traditionally, formal languages are defined as sets of words. More

recently, the alternative coalgebraic or coinductive representation as

infinite tries, i.e., prefix trees branching over the alphabet, has

been used to obtain compact and elegant proofs of classic results in

language theory. In this paper, we study this representation in the

Isabelle proof assistant. We define regular operations on infinite

tries and prove the axioms of Kleene algebra for those

operations. Thereby, we exercise corecursion and coinduction and

confirm the coinductive view being profitable in formalizations, as it

improves over the set-of-words view with respect to proof automation.