author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 48891  c0eafbd55de3 
child 58239  1c5bc387bd4c 
permissions  rwrr 
11608  1 
(* Title: HOL/Typedef.thy 
2 
Author: Markus Wenzel, TU Munich 

11743  3 
*) 
11608  4 

11979  5 
header {* HOL type definitions *} 
11608  6 

15131  7 
theory Typedef 
15140  8 
imports Set 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46947
diff
changeset

9 
keywords "typedef" :: thy_goal and "morphisms" 
15131  10 
begin 
11608  11 

13412  12 
locale type_definition = 
13 
fixes Rep and Abs and A 

14 
assumes Rep: "Rep x \<in> A" 

15 
and Rep_inverse: "Abs (Rep x) = x" 

16 
and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y" 

17 
 {* This will be axiomatized for each typedef! *} 

23247  18 
begin 
11608  19 

23247  20 
lemma Rep_inject: 
13412  21 
"(Rep x = Rep y) = (x = y)" 
22 
proof 

23 
assume "Rep x = Rep y" 

23710
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset

24 
then have "Abs (Rep x) = Abs (Rep y)" by (simp only:) 
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset

25 
moreover have "Abs (Rep x) = x" by (rule Rep_inverse) 
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset

26 
moreover have "Abs (Rep y) = y" by (rule Rep_inverse) 
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset

27 
ultimately show "x = y" by simp 
13412  28 
next 
29 
assume "x = y" 

30 
thus "Rep x = Rep y" by (simp only:) 

31 
qed 

11608  32 

23247  33 
lemma Abs_inject: 
13412  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" 

23710
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset

38 
then have "Rep (Abs x) = Rep (Abs y)" by (simp only:) 
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset

39 
moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse) 
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset

40 
moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse) 
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset

41 
ultimately show "x = y" by simp 
13412  42 
next 
43 
assume "x = y" 

44 
thus "Abs x = Abs y" by (simp only:) 

11608  45 
qed 
46 

23247  47 
lemma Rep_cases [cases set]: 
13412  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 

23247  56 
lemma Abs_cases [cases type]: 
13412  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 

23247  65 
lemma Rep_induct [induct set]: 
13412  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) 
23710
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset

71 
moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse) 
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset

72 
ultimately show "P y" by simp 
11608  73 
qed 
74 

23247  75 
lemma Abs_induct [induct type]: 
13412  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) 
23710
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset

80 
then have "P (Abs (Rep x))" by (rule r) 
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset

81 
moreover have "Abs (Rep x) = x" by (rule Rep_inverse) 
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset

82 
ultimately show "P x" by simp 
11608  83 
qed 
84 

27295  85 
lemma Rep_range: "range Rep = A" 
24269  86 
proof 
87 
show "range Rep <= A" using Rep by (auto simp add: image_def) 

88 
show "A <= range Rep" 

23433  89 
proof 
90 
fix x assume "x : A" 

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

23433  93 
qed 
94 
qed 

95 

27295  96 
lemma Abs_image: "Abs ` A = UNIV" 
97 
proof 

98 
show "Abs ` A <= UNIV" by (rule subset_UNIV) 

99 
next 

100 
show "UNIV <= Abs ` A" 

101 
proof 

102 
fix x 

103 
have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric]) 

104 
moreover have "Rep x : A" by (rule Rep) 

105 
ultimately show "x : Abs ` A" by (rule image_eqI) 

106 
qed 

107 
qed 

108 

23247  109 
end 
110 

48891  111 
ML_file "Tools/typedef.ML" setup Typedef.setup 
11608  112 

113 
end 