Theory Finite

(*  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