### Abstract

Tail-recursive function definitions are sometimes more straightforward than alternatives, but proving theorems on them may be roundabout because of the peculiar form of the resulting recursion induction rules.

This paper describes a proof method that provides a general solution to this problem by means of suitable invariants over inductive sets, and illustrates the application of such method by examining two case studies.

### License

BSD License

### Topics

- Computer science/Functional programming

### Session Tail_Recursive_Functions

- Method
- CaseStudy1
- CaseStudy2

## Cite

×

Tail_Recursive_Functions-AFP

    @article{Tail_Recursive_Functions-AFP,
      author  = {Pasquale Noce},
      title   = {A General Method for the Proof of Theorems on Tail-recursive Functions},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/Tail_Recursive_Functions.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 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- Jun 13, 2015 : Isabelle2015
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Dec 2, 2013 : Isabelle2013-1