Software Foundations is always a great place to start! (https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/) It uses Coq not I

Software Foundations is always a great place to start! (https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/) It uses Coq not Isabelle, but it's a great starting point and contains a ton of useful information. The book is one large literate program, so it's easy to follow along and do the exercises.