如何在Isabelle中恢复或查看证明对应的纯Lambda表达式？

Great questions—you’re spot on about Isabelle/HOL representing proofs as typed λ-terms that match the theorem’s type. Let’s walk through exactly how to access and inspect these raw expressions:

Extracting the Proof Term for a Proven Theorem #

If you already have a fully proven theorem (say, named my_theorem), use Isabelle’s ML interface to pull out its underlying λ-term. Run this in the Isabelle console:

val proof_term = Thm.proof_of @{thm my_theorem};
Pretty.writeln (Term.pretty_global @{context} proof_term);

Here’s what each part does:

• Thm.proof_of @{thm my_theorem} grabs the raw proof term (your λ-expression) directly from the theorem object.
• Term.pretty_global @{context} proof_term makes the term human-readable—raw terms are often unmanageably messy otherwise!
• Pretty.writeln prints the formatted result to your console for inspection.

Cleaning Up Verbose Output #

Raw proof terms can get extremely long, especially for non-trivial proofs. If you want a more streamlined view of the core λ-structure, simplify the term first with:

val simplified_proof = Simplifier.simplify @{context} proof_term;
Pretty.writeln (Term.pretty_global @{context} simplified_proof);

This cuts down on redundant steps and noise, making it easier to follow the actual λ-calculus logic.

Checking Partial Proofs Mid-Construction #

If you’re still building a proof interactively (using apply or proof blocks), you can peek at the partial λ-term being assembled as you work:

val current_proof = Proof_Context.get_proof @{context};
Pretty.writeln (Proof.pretty @{context} current_proof);

This shows you the skeleton of the proof term as you add each step, which is a great way to connect your interactive proof commands to the underlying λ-calculus.

内容的提问来源于stack exchange，提问作者Tom