We next explain how to obtain benefits of proof generation in systems based on theorems as ADT.

To obtain (low-level) proofs: store proofs and ancestores with each formula in the 'theorem' ADT.

To use proofs and avoid overhead of checking on-the-fly:

• first construct a proof (it can be arbitrarily domain-specific, high-level proof)
• then write a checker that traverses the domain-specfic proof, applying proof commands and evaluating proof into a 'theorem' value

Modern LCF-based provers such as Isabelle contain 'reflection' capabilities as an additional feature.

If we prove, within the system, that certain executable function preserves the truth value of a formula, we can

• generate the code for this function
• use the generated code as a built-in formula transformation

This was used within Isabelle in recent work “Linear quantifier elimination”.