author  haftmann 
Tue, 10 Jul 2007 17:30:51 +0200  
changeset 23710  a8ac2305eaf2 
parent 23433  c2c10abd2a1e 
child 24269  4b2aac7669b3 
permissions  rwrr 
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 