### Abstract

FinFuns are total functions that are constant except for a finite set of points, i.e. a generalisation of finite maps. They are formalised as a new type in Isabelle/HOL such that the code generator can handle equality tests and quantification on FinFuns. On the code output level, FinFuns are explicitly represented by constant functions and pointwise updates, similarly to associative lists. Inside the logic, they behave like ordinary functions with extensionality. Via the update/constant pattern, a recursion combinator and an induction rule for FinFuns allow for defining and reasoning about operators on FinFun that are also executable.

### License

BSD License

### History

March 7, 2012
  replace sets as FinFuns by predicates as FinFuns because the set type constructor has been reintroduced (revision b7aa87989f3a)
November 4, 2010
  new conversion function from FinFun to list of elements in the domain (revision 0c167102e6ed)
August 13, 2010
  new concept domain of a FinFun as a FinFun (revision 34b3517cbc09)

### Topics

- Computer science/Data structures

### Session FinFun

- FinFun
- FinFunPred

### Used by

- A Formal Model of Extended Finite State Machines
- Nominal 2
- The Correctness of Launchbury’s Natural Semantics for Lazy Evaluation
- Jinja with Threads

## Cite

×

FinFun-AFP

    @article{FinFun-AFP,
      author  = {Andreas Lochbihler},
      title   = {Code Generation for Functions as Data},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2009},
      note    = {\url{https://isa-afp.org/entries/FinFun.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
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Mar 2, 2013 : Isabelle2013
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jun 30, 2010 : Isabelle2009-2
- Dec 12, 2009 : Isabelle2009-1
- May 25, 2009 : Isabelle2009