src/HOL/Types_To_Sets/Examples/Finite.thy
changeset 64551 79e9587dbcca
child 67399 eab6ce8368fa
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Types_To_Sets/Examples/Finite.thy	Mon Dec 12 11:33:14 2016 +0100
     1.3 @@ -0,0 +1,90 @@
     1.4 +(*  Title:      HOL/Types_To_Sets/Examples/Finite.thy
     1.5 +    Author:     Ondřej Kunčar, TU München
     1.6 +*)
     1.7 +
     1.8 +theory Finite
     1.9 +  imports "../Types_To_Sets" Prerequisites
    1.10 +begin
    1.11 +
    1.12 +section \<open>The Type-Based Theorem\<close>
    1.13 +
    1.14 +text\<open>This example file shows how we perform the relativization in presence of axiomatic
    1.15 +  type classes: we internalize them.\<close>
    1.16 +
    1.17 +definition injective :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
    1.18 +  where "injective f \<equiv> (\<forall>x y. f x = f y \<longrightarrow> x = y)"
    1.19 +
    1.20 +text\<open>We want to relativize the following type-based theorem using the type class finite.\<close>
    1.21 +
    1.22 +lemma type_based: "\<exists>f :: 'a::finite \<Rightarrow> nat. injective f"
    1.23 +  unfolding injective_def
    1.24 +  using finite_imp_inj_to_nat_seg[of "UNIV::'a set", unfolded inj_on_def] by auto
    1.25 +
    1.26 +section \<open>Definitions and Setup for The Relativization\<close>
    1.27 +
    1.28 +text\<open>We have to define what being injective on a set means.\<close>
    1.29 +
    1.30 +definition injective_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
    1.31 +  where "injective_on A f \<equiv> \<forall>x \<in> A. \<forall>y \<in> A. f x = f y \<longrightarrow> x = y"
    1.32 +
    1.33 +text\<open>The predicate injective_on is the relativization of the predicate injective.\<close>
    1.34 +
    1.35 +lemma injective_transfer[transfer_rule]:
    1.36 +  includes lifting_syntax
    1.37 +  assumes [transfer_rule]: "right_total T"
    1.38 +  assumes [transfer_rule]: "bi_unique T"
    1.39 +  shows "((T ===> op =) ===> op=) (injective_on (Collect(Domainp T))) injective"
    1.40 +  unfolding injective_on_def[abs_def] injective_def[abs_def] by transfer_prover
    1.41 +
    1.42 +text\<open>Similarly, we define the relativization of the internalization
    1.43 +     of the type class finite, class.finite\<close>
    1.44 +
    1.45 +definition finite_on :: "'a set => bool" where "finite_on A = finite A"
    1.46 +
    1.47 +lemma class_finite_transfer[transfer_rule]:
    1.48 +  assumes [transfer_rule]: "right_total (T::'a\<Rightarrow>'b\<Rightarrow>bool)"
    1.49 +  assumes [transfer_rule]: "bi_unique T"
    1.50 +  shows "op= (finite_on (Collect(Domainp T))) (class.finite TYPE('b))"
    1.51 +  unfolding finite_on_def class.finite_def by transfer_prover
    1.52 +
    1.53 +text\<open>The aforementioned development can be automated. The main part is already automated
    1.54 +     by the transfer_prover.\<close>
    1.55 +
    1.56 +section \<open>The Relativization to The Set-Based Theorem\<close>
    1.57 +
    1.58 +lemmas internalized = type_based[internalize_sort "'a::finite"]
    1.59 +text\<open>We internalized the type class finite and thus reduced the task to the
    1.60 +  original relativization algorithm.\<close>
    1.61 +thm internalized
    1.62 +
    1.63 +text\<open>This is the set-based variant.\<close>
    1.64 +
    1.65 +lemma set_based:
    1.66 +  assumes "(A::'a set) \<noteq> {}"
    1.67 +  shows "finite_on A \<longrightarrow> (\<exists>f :: 'a \<Rightarrow> nat. injective_on A f)"
    1.68 +proof -
    1.69 +  {
    1.70 +    text\<open>We define the type 'b to be isomorphic to A.\<close>
    1.71 +    assume T: "\<exists>(Rep :: 'b \<Rightarrow> 'a) Abs. type_definition Rep Abs A"
    1.72 +    from T obtain rep :: "'b \<Rightarrow> 'a" and abs :: "'a \<Rightarrow> 'b" where t: "type_definition rep abs A"
    1.73 +      by auto
    1.74 +
    1.75 +    text\<open>Setup for the Transfer tool.\<close>
    1.76 +    define cr_b where "cr_b == \<lambda>r a. r = rep a"
    1.77 +    note type_definition_Domainp[OF t cr_b_def, transfer_domain_rule]
    1.78 +    note typedef_right_total[OF t cr_b_def, transfer_rule]
    1.79 +    note typedef_bi_unique[OF t cr_b_def, transfer_rule]
    1.80 +
    1.81 +    have ?thesis
    1.82 +      text\<open>Relativization by the Transfer tool.\<close>
    1.83 +      using internalized[where 'a = 'b, untransferred, simplified]
    1.84 +      by blast
    1.85 +  } note * = this[cancel_type_definition, OF assms] text\<open>We removed the definition of 'b.\<close>
    1.86 +
    1.87 +  show ?thesis by (rule *)
    1.88 +qed
    1.89 +
    1.90 +text\<open>The Final Result. We can compare the type-based and the set-based statement.\<close>
    1.91 +thm type_based set_based
    1.92 +
    1.93 +end