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
|
15131
|
10 |
files ("Tools/typedef_package.ML")
|
|
11 |
begin
|
11608
|
12 |
|
13412
|
13 |
locale type_definition =
|
|
14 |
fixes Rep and Abs and A
|
|
15 |
assumes Rep: "Rep x \<in> A"
|
|
16 |
and Rep_inverse: "Abs (Rep x) = x"
|
|
17 |
and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y"
|
|
18 |
-- {* This will be axiomatized for each typedef! *}
|
11608
|
19 |
|
13412
|
20 |
lemma (in type_definition) Rep_inject:
|
|
21 |
"(Rep x = Rep y) = (x = y)"
|
|
22 |
proof
|
|
23 |
assume "Rep x = Rep y"
|
|
24 |
hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
|
|
25 |
also have "Abs (Rep x) = x" by (rule Rep_inverse)
|
|
26 |
also have "Abs (Rep y) = y" by (rule Rep_inverse)
|
|
27 |
finally show "x = y" .
|
|
28 |
next
|
|
29 |
assume "x = y"
|
|
30 |
thus "Rep x = Rep y" by (simp only:)
|
|
31 |
qed
|
11608
|
32 |
|
13412
|
33 |
lemma (in type_definition) Abs_inject:
|
|
34 |
assumes x: "x \<in> A" and y: "y \<in> A"
|
|
35 |
shows "(Abs x = Abs y) = (x = y)"
|
|
36 |
proof
|
|
37 |
assume "Abs x = Abs y"
|
|
38 |
hence "Rep (Abs x) = Rep (Abs y)" by (simp only:)
|
|
39 |
also from x have "Rep (Abs x) = x" by (rule Abs_inverse)
|
|
40 |
also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
|
|
41 |
finally show "x = y" .
|
|
42 |
next
|
|
43 |
assume "x = y"
|
|
44 |
thus "Abs x = Abs y" by (simp only:)
|
11608
|
45 |
qed
|
|
46 |
|
13412
|
47 |
lemma (in type_definition) Rep_cases [cases set]:
|
|
48 |
assumes y: "y \<in> A"
|
|
49 |
and hyp: "!!x. y = Rep x ==> P"
|
|
50 |
shows P
|
|
51 |
proof (rule hyp)
|
|
52 |
from y have "Rep (Abs y) = y" by (rule Abs_inverse)
|
|
53 |
thus "y = Rep (Abs y)" ..
|
11608
|
54 |
qed
|
|
55 |
|
13412
|
56 |
lemma (in type_definition) Abs_cases [cases type]:
|
|
57 |
assumes r: "!!y. x = Abs y ==> y \<in> A ==> P"
|
|
58 |
shows P
|
|
59 |
proof (rule r)
|
|
60 |
have "Abs (Rep x) = x" by (rule Rep_inverse)
|
|
61 |
thus "x = Abs (Rep x)" ..
|
|
62 |
show "Rep x \<in> A" by (rule Rep)
|
11608
|
63 |
qed
|
|
64 |
|
13412
|
65 |
lemma (in type_definition) Rep_induct [induct set]:
|
|
66 |
assumes y: "y \<in> A"
|
|
67 |
and hyp: "!!x. P (Rep x)"
|
|
68 |
shows "P y"
|
11608
|
69 |
proof -
|
13412
|
70 |
have "P (Rep (Abs y))" by (rule hyp)
|
|
71 |
also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
|
|
72 |
finally show "P y" .
|
11608
|
73 |
qed
|
|
74 |
|
13412
|
75 |
lemma (in type_definition) Abs_induct [induct type]:
|
|
76 |
assumes r: "!!y. y \<in> A ==> P (Abs y)"
|
|
77 |
shows "P x"
|
11608
|
78 |
proof -
|
13412
|
79 |
have "Rep x \<in> A" by (rule Rep)
|
11608
|
80 |
hence "P (Abs (Rep x))" by (rule r)
|
13412
|
81 |
also have "Abs (Rep x) = x" by (rule Rep_inverse)
|
|
82 |
finally show "P x" .
|
11608
|
83 |
qed
|
|
84 |
|
|
85 |
use "Tools/typedef_package.ML"
|
|
86 |
|
15260
|
87 |
setup TypedefPackage.setup
|
|
88 |
|
11608
|
89 |
end
|