author | wenzelm |
Tue, 17 Jul 2007 13:19:18 +0200 | |
changeset 23823 | 441148ca8323 |
parent 23710 | a8ac2305eaf2 |
child 24269 | 4b2aac7669b3 |
permissions | -rw-r--r-- |
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" |
|
23710
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset
|
32 |
then have "Abs (Rep x) = Abs (Rep y)" by (simp only:) |
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset
|
33 |
moreover have "Abs (Rep x) = x" by (rule Rep_inverse) |
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset
|
34 |
moreover have "Abs (Rep y) = y" by (rule Rep_inverse) |
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset
|
35 |
ultimately show "x = y" by simp |
13412 | 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" |
|
23710
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset
|
46 |
then have "Rep (Abs x) = Rep (Abs y)" by (simp only:) |
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset
|
47 |
moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse) |
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset
|
48 |
moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse) |
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset
|
49 |
ultimately show "x = y" by simp |
13412 | 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) |
23710
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset
|
79 |
moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse) |
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset
|
80 |
ultimately show "P y" by simp |
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) |
23710
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset
|
88 |
then have "P (Abs (Rep x))" by (rule r) |
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset
|
89 |
moreover have "Abs (Rep x) = x" by (rule Rep_inverse) |
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset
|
90 |
ultimately show "P x" by simp |
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 |