|
64551
|
1 |
(* Title: HOL/Types_To_Sets/Examples/Prerequisites.thy
|
|
|
2 |
Author: Ondřej Kunčar, TU München
|
|
|
3 |
*)
|
|
|
4 |
|
|
|
5 |
theory Prerequisites
|
|
|
6 |
imports Main
|
|
|
7 |
begin
|
|
|
8 |
|
|
|
9 |
context
|
|
|
10 |
fixes Rep Abs A T
|
|
|
11 |
assumes type: "type_definition Rep Abs A"
|
|
|
12 |
assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
|
|
|
13 |
begin
|
|
|
14 |
|
|
|
15 |
lemma type_definition_Domainp: "Domainp T = (\<lambda>x. x \<in> A)"
|
|
|
16 |
proof -
|
|
|
17 |
interpret type_definition Rep Abs A by(rule type)
|
|
|
18 |
show ?thesis
|
|
|
19 |
unfolding Domainp_iff[abs_def] T_def fun_eq_iff
|
|
|
20 |
by (metis Abs_inverse Rep)
|
|
|
21 |
qed
|
|
|
22 |
|
|
|
23 |
end
|
|
|
24 |
|
|
|
25 |
end
|