What is the correct way in Isabelle/HOL (2021) to define a function f from a specific set A to another set B?
From mathematics, a function f: A -> B is often defined as a map from its domain A to its co-domain B. And a function f is defined as a special kind of relation in A × B with only one y ∈ B that satisfies x f y for each x ∈ A.
But in Isabelle/HOL, functions seems to be defined in terms of computation, e.g. f x = Suc x. It seems that there is no place to define domain and co-domains explicitly.
I was just wondering if there is a conventional way to define functions in Isabelle to be with domain and co-domains and be compatible with the definition of relations above.
Background
As you have noted, in Isabelle/HOL, conventionally, a function is a term of the type 'a⇒'b, where 'a and 'b can be arbitrary types. As such, all functions in Isabelle are total. There is a blog post by Joachim Breitner that explains this very well: link. I will not restate any elements of the content of the blog post: instead, I will concentrate on the issue that you have raised in your question.
Conventional definitions of a function
I am aware of two methodologies for the definition of a function in traditional mathematics (here I use the term "traditional mathematics" to mean mathematics exposed in some set-theoretic foundation):
You can find some further discussion here. If the function is a binary relation, then the domain and the range are normally identified with the domain and the range of the relation that the function represents. However, it makes little sense to speak about the codomain of such an entity. If the function is defined as a triple (A,B,r), then the codomain is the assigned set B.
Isabelle/HOL I: functions as relations
Isabelle/HOL already provides a definition of the concept of a single-valued relation in the theory Relation.thy. The definition is implicit in the definition of the predicate single_valued:
definition single_valued :: "('a × 'b) set ⇒ bool"
where "single_valued r ⟷ (∀x y. (x, y) ∈ r ⟶ (∀z. (x, z) ∈ r ⟶ y = z))"
Thus, effectively, a single-valued relation is a term of the type ('a × 'b) set such that it satisfies the predicate single_valued. Some elementary results about this definition are also provided.
Of course, this predicate can be used to create a new type constructor of "functions-as-relations" from 'a to 'b. See the official documentation of Isabelle [3, section 11.7] and the article Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL [4, section 3] for further information about defining new type constructors in Isabelle/HOL. It is not unlikely that such a type is already available somewhere, but I could not find it (or anything similar) after a quick search of the sources.
Of course, there is little that can prevent one from providing a type that captures either of the set-theoretic definitions of a function presented in the previous subsection of the answer. I guess, something like the following definition could work, but I have not tested it:
typedef ('a, 'b) relfun =
‹
{
(A::'a set, B::'b set, f::('a × 'b) set).
single_valued f ∧ Domain f = A ∧ Range f ⊆ B
}
›
proof-
let ?r = ‹({}, {}, {})›
show ?thesis unfolding single_valued_def by (intro exI[of _ ?r]) simp
qed
Isabelle/HOL II: FuncSet and other restrictions
While the functions in Isabelle/HOL are total, one can still mimick the restriction of a function to a certain pre-defined domain (i.e. a proper subset of UNIV::'a set) using a variety of methodologies. One common methodology (exposed in the theory HOL-Library.FuncSet) is to force the function to be undefined on parts of the domain. My answer in the following thread explains this in more detail.
Isabelle/HOL III: HOL/ZF, ZFC in HOL and HOTG
This might be marginally off-topic. However, there exist extensions of Isabelle/HOL with the axioms of set-theory of different strengths [5,6,7]. For example, ZFC in HOL [6] provides a certain type V that represents the von Neumann universe. One can now define all relevant set-theoretic concepts internalized in this type, including, of course, either one of the conventional definitions of a function. In ZFC in HOL one can internalize functions defined in HOL using the so-called operator VLambda like so: (F::V) = VLambda (A::V) (f::V⇒V). Now, F is a single-valued binary relation internalized in the type V with the domain A and the values of the form ⟨x, f x⟩.
As a side note, I have exposed both definitions of a function as predicates on V explicitly while working on my own formalization of category theory: Category Theory for ZFC in HOL.
Summary
What is the correct way in Isabelle/HOL (2021) to define a function f from a specific set A to another set B?
To answer your question directly, my opinion is that there is no single "correct way" to define a function from a specific set A to another set B. However, you have many options that you can explore: each of these options will have advantages and disadvantages that are specific to it.
References