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