### Abstract

In this entry we formalize Isabelle's metalogic in Isabelle/HOL. Furthermore, we define a language of proof terms and an executable proof checker and prove its soundness wrt. the metalogic. The formalization is intentionally kept close to the Isabelle implementation(for example using de Brujin indices) to enable easy integration of generated code with the Isabelle system without a complicated translation layer. The formalization is described in our CADE 28 paper.

### License

BSD License

### Topics

- Logic/General logic

### Related publications

- Nipkow, T., & Roßkopf, S. (2021). Isabelle’s Metalogic: Formalization and Proof Checker. Lecture Notes in Computer Science, 93–110. https://doi.org/10.1007/978-3-030-79876-5_6
- Roßkopf, S., & Nipkow, T. (2022). A Formalization and Proof Checker for Isabelle’s Metalogic. Journal of Automated Reasoning, 67(1). https://doi.org/10.1007/s10817-022-09648-w

### Session Metalogic_ProofChecker

- Core
- Preliminaries
- Term
- Sorts
- SortConstants
- Theory
- Term_Subst
- Name
- BetaNorm
- BetaNormProof
- EtaNorm
- EtaNormProof
- Logic
- EqualityProof
- ProofTerm
- SortsExe
- Instances
- TheoryExe
- CheckerExe
- CodeGen

### Depends on

- List Index

## Cite

×

Metalogic_ProofChecker-AFP

    @article{Metalogic_ProofChecker-AFP,
      author  = {Tobias Nipkow and Simon Roßkopf},
      title   = {Isabelle's Metalogic: Formalization and Proof Checker},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Metalogic_ProofChecker.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Apr 28, 2021 : Isabelle2021