1(*  Title:      HOL/Types_To_Sets/Examples/Finite.thy
2    Author:     Ond��ej Kun��ar, TU M��nchen
3*)
4
5theory Finite
6  imports "../Types_To_Sets" Prerequisites
7begin
8
9section \<open>The Type-Based Theorem\<close>
10
11text\<open>This example file shows how we perform the relativization in presence of axiomatic
12  type classes: we internalize them.\<close>
13
14definition injective :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
15  where "injective f \<equiv> (\<forall>x y. f x = f y \<longrightarrow> x = y)"
16
17text\<open>We want to relativize the following type-based theorem using the type class finite.\<close>
18
19lemma type_based: "\<exists>f :: 'a::finite \<Rightarrow> nat. injective f"
20  unfolding injective_def
21  using finite_imp_inj_to_nat_seg[of "UNIV::'a set", unfolded inj_on_def] by auto
22
23section \<open>Definitions and Setup for The Relativization\<close>
24
25text\<open>We have to define what being injective on a set means.\<close>
26
27definition injective_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
28  where "injective_on A f \<equiv> \<forall>x \<in> A. \<forall>y \<in> A. f x = f y \<longrightarrow> x = y"
29
30text\<open>The predicate injective_on is the relativization of the predicate injective.\<close>
31
32lemma injective_transfer[transfer_rule]:
33  includes lifting_syntax
34  assumes [transfer_rule]: "right_total T"
35  assumes [transfer_rule]: "bi_unique T"
36  shows "((T ===> (=)) ===> (=)) (injective_on (Collect(Domainp T))) injective"
37  unfolding injective_on_def[abs_def] injective_def[abs_def] by transfer_prover
38
39text\<open>Similarly, we define the relativization of the internalization
40     of the type class finite, class.finite\<close>
41
42definition finite_on :: "'a set => bool" where "finite_on A = finite A"
43
44lemma class_finite_transfer[transfer_rule]:
45  assumes [transfer_rule]: "right_total (T::'a\<Rightarrow>'b\<Rightarrow>bool)"
46  assumes [transfer_rule]: "bi_unique T"
47  shows "(=) (finite_on (Collect(Domainp T))) (class.finite TYPE('b))"
48  unfolding finite_on_def class.finite_def by transfer_prover
49
50text\<open>The aforementioned development can be automated. The main part is already automated
51     by the transfer_prover.\<close>
52
53section \<open>The Relativization to The Set-Based Theorem\<close>
54
55lemmas internalized = type_based[internalize_sort "'a::finite"]
56text\<open>We internalized the type class finite and thus reduced the task to the
57  original relativization algorithm.\<close>
58thm internalized
59
60text\<open>This is the set-based variant.\<close>
61
62lemma set_based:
63  assumes "(A::'a set) \<noteq> {}"
64  shows "finite_on A \<longrightarrow> (\<exists>f :: 'a \<Rightarrow> nat. injective_on A f)"
65proof -
66  {
67    text\<open>We define the type 'b to be isomorphic to A.\<close>
68    assume T: "\<exists>(Rep :: 'b \<Rightarrow> 'a) Abs. type_definition Rep Abs A"
69    from T obtain rep :: "'b \<Rightarrow> 'a" and abs :: "'a \<Rightarrow> 'b" where t: "type_definition rep abs A"
70      by auto
71
72    text\<open>Setup for the Transfer tool.\<close>
73    define cr_b where "cr_b == \<lambda>r a. r = rep a"
74    note type_definition_Domainp[OF t cr_b_def, transfer_domain_rule]
75    note typedef_right_total[OF t cr_b_def, transfer_rule]
76    note typedef_bi_unique[OF t cr_b_def, transfer_rule]
77
78    have ?thesis
79      text\<open>Relativization by the Transfer tool.\<close>
80      using internalized[where 'a = 'b, untransferred, simplified]
81      by blast
82  } note * = this[cancel_type_definition, OF assms] text\<open>We removed the definition of 'b.\<close>
83
84  show ?thesis by (rule *)
85qed
86
87text\<open>The Final Result. We can compare the type-based and the set-based statement.\<close>
88thm type_based set_based
89
90end
91