Are you aware of the Archive of Formal Proof for Isabelle? It's a collection of formalized mathematics (and some program verification). Reading the papers there, and browsing the Isabelle theory file sources is a good way to learn.
The Isar tutorial is also a good place to look, if you want to write proofs that look like informal mathematics (as opposed to tactic style). It's quite hard to get the hang of at first (mostly due to lack of documentation), but once you get it, it's a lot easier to work with than plain lists of tactics.
If you're wanting to formalise anything with name binders (lambda-calculus, FOL, programming languages, pi-calculus, etc.) you should also check out the Nominal package for Isabelle which again helps with abstracting the proofs.
No comments:
Post a Comment