11608
|
1 |
(* Title: HOL/Typedef.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Munich
|
11743
|
4 |
*)
|
11608
|
5 |
|
11979
|
6 |
header {* HOL type definitions *}
|
11608
|
7 |
|
15131
|
8 |
theory Typedef
|
15140
|
9 |
imports Set
|
20426
|
10 |
uses
|
|
11 |
("Tools/typedef_package.ML")
|
|
12 |
("Tools/typecopy_package.ML")
|
|
13 |
("Tools/typedef_codegen.ML")
|
15131
|
14 |
begin
|
11608
|
15 |
|
23247
|
16 |
ML {*
|
|
17 |
structure HOL = struct val thy = theory "HOL" end;
|
|
18 |
*} -- "belongs to theory HOL"
|
|
19 |
|
13412
|
20 |
locale type_definition =
|
|
21 |
fixes Rep and Abs and A
|
|
22 |
assumes Rep: "Rep x \<in> A"
|
|
23 |
and Rep_inverse: "Abs (Rep x) = x"
|
|
24 |
and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y"
|
|
25 |
-- {* This will be axiomatized for each typedef! *}
|
23247
|
26 |
begin
|
11608
|
27 |
|
23247
|
28 |
lemma Rep_inject:
|
13412
|
29 |
"(Rep x = Rep y) = (x = y)"
|
|
30 |
proof
|
|
31 |
assume "Rep x = Rep y"
|
|
32 |
hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
|
|
33 |
also have "Abs (Rep x) = x" by (rule Rep_inverse)
|
|
34 |
also have "Abs (Rep y) = y" by (rule Rep_inverse)
|
|
35 |
finally show "x = y" .
|
|
36 |
next
|
|
37 |
assume "x = y"
|
|
38 |
thus "Rep x = Rep y" by (simp only:)
|
|
39 |
qed
|
11608
|
40 |
|
23247
|
41 |
lemma Abs_inject:
|
13412
|
42 |
assumes x: "x \<in> A" and y: "y \<in> A"
|
|
43 |
shows "(Abs x = Abs y) = (x = y)"
|
|
44 |
proof
|
|
45 |
assume "Abs x = Abs y"
|
|
46 |
hence "Rep (Abs x) = Rep (Abs y)" by (simp only:)
|
|
47 |
also from x have "Rep (Abs x) = x" by (rule Abs_inverse)
|
|
48 |
also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
|
|
49 |
finally show "x = y" .
|
|
50 |
next
|
|
51 |
assume "x = y"
|
|
52 |
thus "Abs x = Abs y" by (simp only:)
|
11608
|
53 |
qed
|
|
54 |
|
23247
|
55 |
lemma Rep_cases [cases set]:
|
13412
|
56 |
assumes y: "y \<in> A"
|
|
57 |
and hyp: "!!x. y = Rep x ==> P"
|
|
58 |
shows P
|
|
59 |
proof (rule hyp)
|
|
60 |
from y have "Rep (Abs y) = y" by (rule Abs_inverse)
|
|
61 |
thus "y = Rep (Abs y)" ..
|
11608
|
62 |
qed
|
|
63 |
|
23247
|
64 |
lemma Abs_cases [cases type]:
|
13412
|
65 |
assumes r: "!!y. x = Abs y ==> y \<in> A ==> P"
|
|
66 |
shows P
|
|
67 |
proof (rule r)
|
|
68 |
have "Abs (Rep x) = x" by (rule Rep_inverse)
|
|
69 |
thus "x = Abs (Rep x)" ..
|
|
70 |
show "Rep x \<in> A" by (rule Rep)
|
11608
|
71 |
qed
|
|
72 |
|
23247
|
73 |
lemma Rep_induct [induct set]:
|
13412
|
74 |
assumes y: "y \<in> A"
|
|
75 |
and hyp: "!!x. P (Rep x)"
|
|
76 |
shows "P y"
|
11608
|
77 |
proof -
|
13412
|
78 |
have "P (Rep (Abs y))" by (rule hyp)
|
|
79 |
also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
|
|
80 |
finally show "P y" .
|
11608
|
81 |
qed
|
|
82 |
|
23247
|
83 |
lemma Abs_induct [induct type]:
|
13412
|
84 |
assumes r: "!!y. y \<in> A ==> P (Abs y)"
|
|
85 |
shows "P x"
|
11608
|
86 |
proof -
|
13412
|
87 |
have "Rep x \<in> A" by (rule Rep)
|
11608
|
88 |
hence "P (Abs (Rep x))" by (rule r)
|
13412
|
89 |
also have "Abs (Rep x) = x" by (rule Rep_inverse)
|
|
90 |
finally show "P x" .
|
11608
|
91 |
qed
|
|
92 |
|
23433
|
93 |
lemma Rep_range:
|
|
94 |
assumes "type_definition Rep Abs A"
|
|
95 |
shows "range Rep = A"
|
|
96 |
proof -
|
|
97 |
from assms have A1: "!!x. Rep x : A"
|
|
98 |
and A2: "!!y. y : A ==> y = Rep(Abs y)"
|
|
99 |
by (auto simp add: type_definition_def)
|
|
100 |
have "range Rep <= A" using A1 by (auto simp add: image_def)
|
|
101 |
moreover have "A <= range Rep"
|
|
102 |
proof
|
|
103 |
fix x assume "x : A"
|
|
104 |
hence "x = Rep (Abs x)" by (rule A2)
|
|
105 |
thus "x : range Rep" by (auto simp add: image_def)
|
|
106 |
qed
|
|
107 |
ultimately show ?thesis ..
|
|
108 |
qed
|
|
109 |
|
23247
|
110 |
end
|
|
111 |
|
11608
|
112 |
use "Tools/typedef_package.ML"
|
20426
|
113 |
use "Tools/typecopy_package.ML"
|
19459
|
114 |
use "Tools/typedef_codegen.ML"
|
11608
|
115 |
|
20426
|
116 |
setup {*
|
22846
|
117 |
TypecopyPackage.setup
|
20426
|
118 |
#> TypedefCodegen.setup
|
|
119 |
*}
|
15260
|
120 |
|
11608
|
121 |
end
|