author  haftmann 
Wed, 05 Dec 2007 14:15:48 +0100  
changeset 25535  4975b7529a14 
parent 24269  4b2aac7669b3 
child 26151  4a9b8f15ce7f 
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: 
24269  94 
shows "range Rep = A" 
95 
proof 

96 
show "range Rep <= A" using Rep by (auto simp add: image_def) 

97 
show "A <= range Rep" 

23433  98 
proof 
99 
fix x assume "x : A" 

24269  100 
hence "x = Rep (Abs x)" by (rule Abs_inverse [symmetric]) 
101 
thus "x : range Rep" by (rule range_eqI) 

23433  102 
qed 
103 
qed 

104 

23247  105 
end 
106 

11608  107 
use "Tools/typedef_package.ML" 
20426  108 
use "Tools/typecopy_package.ML" 
19459  109 
use "Tools/typedef_codegen.ML" 
11608  110 

20426  111 
setup {* 
25535  112 
TypedefPackage.setup 
113 
#> TypecopyPackage.setup 

20426  114 
#> TypedefCodegen.setup 
115 
*} 

15260  116 

11608  117 
end 