Interpretation of Locales in Isabelle: Theories and Proof Contexts

摘要

The generic proof assistant Isabelle provides a landscape of specification contexts that is considerably richer than that of most other provers. Theories are the level of specification where object-logics are axiomatised. Isabelle's proof language Isar enables local exploration in contexts generated in the course of natural deduction proofs. Finally, locales, which may be seen as detached proof contexts, offer an intermediate level of specification geared towards reuse. All three kinds of contexts are structured, to different extents. We analyse the "topology" of Isabelle's landscape of specification contexts, by means of development graphs, in order to establish what kinds of reuse are possible.