Abstract
Dealing with binders, renaming of bound variables, capture-avoiding substitution, etc., is very often a major problem in formal proofs, especially in proofs by structural and rule induction. Nominal Isabelle is designed to make such proofs easy to formalise: it provides an infrastructure for declaring nominal datatypes (that is alpha-equivalence classes) and for defining functions over them by structural recursion. It also provides induction principles that have Barendregt’s variable convention already built in.
This entry can be used as a more advanced replacement for HOL/Nominal in the Isabelle distribution.
Depends On
Used by
- MiniSail
- Goedel_HFSet_Semanticless
- Robinson_Arithmetic
- LambdaAuth
- Modal_Logics_for_NTS
- Rewriting_Z
- Incompleteness
- Launchbury
Topics
Theories
- Nominal2_Base
- files/nominal_basics.ML
- files/nominal_thmdecls.ML
- files/nominal_permeq.ML
- files/nominal_library.ML
- files/nominal_atoms.ML
- files/nominal_eqvt.ML
- Nominal2_Abs
- Nominal2_FCB
- Nominal2
- files/nominal_dt_data.ML
- files/nominal_dt_rawfuns.ML
- files/nominal_dt_alpha.ML
- files/nominal_dt_quot.ML
- files/nominal_induct.ML
- files/nominal_inductive.ML
- files/nominal_function_common.ML
- files/nominal_function_core.ML
- files/nominal_mutual.ML
- files/nominal_function.ML
- files/nominal_termination.ML
- Atoms
- Eqvt