Scoped Metatheorems
David Basin, Seán Matthews · Electronic Notes in Theoretical Computer Science · 1998
Proof development systems traditionally structure theories hierarchically: Theorems established in a subtheory hold in all supertheories. While often effective, this is sometimes too restrictive as there are certain facts that are true of some but not all extensions. We present a solution where instead of first formalizing a theory and then establishing facts, we parameterize each statement with its scope of application. We present this idea abstractly and consider concrete implementations based on parameterized inductive definitions.