# Theory Finite

theory Finite
imports Types_To_Sets Prerequisites
```(*  Title:      HOL/Types_To_Sets/Examples/Finite.thy
Author:     Ondřej Kunčar, TU München
*)

theory Finite
imports "../Types_To_Sets" Prerequisites
begin

section ‹The Type-Based Theorem›

text‹This example file shows how we perform the relativization in presence of axiomatic
type classes: we internalize them.›

definition injective :: "('a ⇒ 'b) ⇒ bool"
where "injective f ≡ (∀x y. f x = f y ⟶ x = y)"

text‹We want to relativize the following type-based theorem using the type class finite.›

lemma type_based: "∃f :: 'a::finite ⇒ nat. injective f"
unfolding injective_def
using finite_imp_inj_to_nat_seg[of "UNIV::'a set", unfolded inj_on_def] by auto

section ‹Definitions and Setup for The Relativization›

text‹We have to define what being injective on a set means.›

definition injective_on :: "'a set ⇒ ('a ⇒ 'b) ⇒ bool"
where "injective_on A f ≡ ∀x ∈ A. ∀y ∈ A. f x = f y ⟶ x = y"

text‹The predicate injective_on is the relativization of the predicate injective.›

lemma injective_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total T"
assumes [transfer_rule]: "bi_unique T"
shows "((T ===> (=)) ===> (=)) (injective_on (Collect(Domainp T))) injective"
unfolding injective_on_def[abs_def] injective_def[abs_def] by transfer_prover

text‹Similarly, we define the relativization of the internalization
of the type class finite, class.finite›

definition finite_on :: "'a set => bool" where "finite_on A = finite A"

lemma class_finite_transfer[transfer_rule]:
assumes [transfer_rule]: "right_total (T::'a⇒'b⇒bool)"
assumes [transfer_rule]: "bi_unique T"
shows "(=) (finite_on (Collect(Domainp T))) (class.finite TYPE('b))"
unfolding finite_on_def class.finite_def by transfer_prover

text‹The aforementioned development can be automated. The main part is already automated
by the transfer_prover.›

section ‹The Relativization to The Set-Based Theorem›

lemmas internalized = type_based[internalize_sort "'a::finite"]
text‹We internalized the type class finite and thus reduced the task to the
original relativization algorithm.›
thm internalized

text‹This is the set-based variant.›

lemma set_based:
assumes "(A::'a set) ≠ {}"
shows "finite_on A ⟶ (∃f :: 'a ⇒ nat. injective_on A f)"
proof -
{
text‹We define the type 'b to be isomorphic to A.›
assume T: "∃(Rep :: 'b ⇒ 'a) Abs. type_definition Rep Abs A"
from T obtain rep :: "'b ⇒ 'a" and abs :: "'a ⇒ 'b" where t: "type_definition rep abs A"
by auto

text‹Setup for the Transfer tool.›
define cr_b where "cr_b == λr a. r = rep a"
note type_definition_Domainp[OF t cr_b_def, transfer_domain_rule]
note typedef_right_total[OF t cr_b_def, transfer_rule]
note typedef_bi_unique[OF t cr_b_def, transfer_rule]

have ?thesis
text‹Relativization by the Transfer tool.›
using internalized[where 'a = 'b, untransferred, simplified]
by blast
} note * = this[cancel_type_definition, OF assms] text‹We removed the definition of 'b.›

show ?thesis by (rule *)
qed

text‹The Final Result. We can compare the type-based and the set-based statement.›
thm type_based set_based

end
```