31 |
31 |
32 lemma injective_transfer[transfer_rule]: |
32 lemma injective_transfer[transfer_rule]: |
33 includes lifting_syntax |
33 includes lifting_syntax |
34 assumes [transfer_rule]: "right_total T" |
34 assumes [transfer_rule]: "right_total T" |
35 assumes [transfer_rule]: "bi_unique T" |
35 assumes [transfer_rule]: "bi_unique T" |
36 shows "((T ===> op =) ===> op=) (injective_on (Collect(Domainp T))) injective" |
36 shows "((T ===> (=)) ===> (=)) (injective_on (Collect(Domainp T))) injective" |
37 unfolding injective_on_def[abs_def] injective_def[abs_def] by transfer_prover |
37 unfolding injective_on_def[abs_def] injective_def[abs_def] by transfer_prover |
38 |
38 |
39 text\<open>Similarly, we define the relativization of the internalization |
39 text\<open>Similarly, we define the relativization of the internalization |
40 of the type class finite, class.finite\<close> |
40 of the type class finite, class.finite\<close> |
41 |
41 |
42 definition finite_on :: "'a set => bool" where "finite_on A = finite A" |
42 definition finite_on :: "'a set => bool" where "finite_on A = finite A" |
43 |
43 |
44 lemma class_finite_transfer[transfer_rule]: |
44 lemma class_finite_transfer[transfer_rule]: |
45 assumes [transfer_rule]: "right_total (T::'a\<Rightarrow>'b\<Rightarrow>bool)" |
45 assumes [transfer_rule]: "right_total (T::'a\<Rightarrow>'b\<Rightarrow>bool)" |
46 assumes [transfer_rule]: "bi_unique T" |
46 assumes [transfer_rule]: "bi_unique T" |
47 shows "op= (finite_on (Collect(Domainp T))) (class.finite TYPE('b))" |
47 shows "(=) (finite_on (Collect(Domainp T))) (class.finite TYPE('b))" |
48 unfolding finite_on_def class.finite_def by transfer_prover |
48 unfolding finite_on_def class.finite_def by transfer_prover |
49 |
49 |
50 text\<open>The aforementioned development can be automated. The main part is already automated |
50 text\<open>The aforementioned development can be automated. The main part is already automated |
51 by the transfer_prover.\<close> |
51 by the transfer_prover.\<close> |
52 |
52 |