|
This is the theory of transitive and well founded relations as sets (using ProofPower's SET type constructor).
|
|
Most ProofPower relations are properties not sets, so the theory of this kind of well-foundedness is developed here.
|
|
|
This is a proof of the recursion theorem for well-founded recursive definitions.
It is modelled on Tobias Nipkow's proof for Isabelle HOL and uses relations modelled with ProofPower HOL's SET type constructor.
|
|
This document contains the proof of a recursion theorem asserting the existence of a fixed point for any functional which
"respects" some well-founded relation.
|
|
|
Introduction
A new "wf_rel" theory is created as a child of "bin_rel".
Probably
|
|
Transitive Relations
Elementary results about transitive relations and transitive closure.
|
|
Well-Founded Relations
Definition of well-founded and transitive-well-founded and proof that the transitive closure of a well-founded relation is
transitive-well-founded.
|
|
|
Proof Context
In this section I will create a decent proof context for recursive definitions, eventually.
|
|
|
|
|
Introduction
A new "wf_relp" theory is created as a child of "wf_rel".
The purpose of this theory is entirely cosmetic.
I want to use the results in developing set theory but I want to avoid use of the membership sign in a context in which it
is likely to cause confusion.
|
|
Transitive Relations
Elementary results about transitive relations and transitive closure.
|
|
Well-Founded Relations
Definition of well-founded and transitive-well-founded and proof that the transitive closure of a well-founded relation is
transitive-well-founded.
|
|
|
Proof Context
In this section I will create a decent proof context for recursive definitions, eventually.
|
|
|
|
|
Introduction
A new "wf_rec" theory is created as a child of "wf_rel".
Probably
|
|
Well-Founded Recursion
In this section is proved the theorem which justifies well-founded recursive definitions.
|
|
Recursive Definition
|
|
|
Proof Context
In this section I will create a decent proof context for recursive definitions, eventually.
|
|
|
|
|
Introduction
A new "wf_recp" theory is created as a child of "wf_relp".
|
|
Defining the Fixed Point Operator
The main part of this is the proof that functionals which are well-founded with respect to some well-founded relation have
fixed points.
This done, the operator "fix" is defined, which yields such a fixed point.
|
|
|
Proof Context
In this section I will create a decent proof context for recursive definitions, eventually.
|
|
|
|
© 