author  wenzelm 
Thu, 15 Mar 2012 22:08:53 +0100  
changeset 46950  d0181abdbdac 
parent 46947  b8c7eb0c2f89 
child 48891  c0eafbd55de3 
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" 
38536
7e57a0dcbd4f
dropped SML typedef_codegen: does not fit to code equations for record operations any longer
haftmann
parents:
38393
diff
changeset

10 
uses ("Tools/typedef.ML") 
15131  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! *} 

23247  19 
begin 
11608  20 

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

24 
assume "Rep x = Rep y" 

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

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

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

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

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

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

32 
qed 

11608  33 

23247  34 
lemma Abs_inject: 
13412  35 
assumes x: "x \<in> A" and y: "y \<in> A" 
36 
shows "(Abs x = Abs y) = (x = y)" 

37 
proof 

38 
assume "Abs x = Abs y" 

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

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

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

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

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

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

11608  46 
qed 
47 

23247  48 
lemma Rep_cases [cases set]: 
13412  49 
assumes y: "y \<in> A" 
50 
and hyp: "!!x. y = Rep x ==> P" 

51 
shows P 

52 
proof (rule hyp) 

53 
from y have "Rep (Abs y) = y" by (rule Abs_inverse) 

54 
thus "y = Rep (Abs y)" .. 

11608  55 
qed 
56 

23247  57 
lemma Abs_cases [cases type]: 
13412  58 
assumes r: "!!y. x = Abs y ==> y \<in> A ==> P" 
59 
shows P 

60 
proof (rule r) 

61 
have "Abs (Rep x) = x" by (rule Rep_inverse) 

62 
thus "x = Abs (Rep x)" .. 

63 
show "Rep x \<in> A" by (rule Rep) 

11608  64 
qed 
65 

23247  66 
lemma Rep_induct [induct set]: 
13412  67 
assumes y: "y \<in> A" 
68 
and hyp: "!!x. P (Rep x)" 

69 
shows "P y" 

11608  70 
proof  
13412  71 
have "P (Rep (Abs y))" by (rule hyp) 
23710
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset

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

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

23247  76 
lemma Abs_induct [induct type]: 
13412  77 
assumes r: "!!y. y \<in> A ==> P (Abs y)" 
78 
shows "P x" 

11608  79 
proof  
13412  80 
have "Rep x \<in> A" by (rule Rep) 
23710
a8ac2305eaf2
removed proof dependency on transitivity theorems
haftmann
parents:
23433
diff
changeset

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

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

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

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

89 
show "A <= range Rep" 

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

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

23433  94 
qed 
95 
qed 

96 

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

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

100 
next 

101 
show "UNIV <= Abs ` A" 

102 
proof 

103 
fix x 

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

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

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

107 
qed 

108 
qed 

109 

23247  110 
end 
111 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
29797
diff
changeset

112 
use "Tools/typedef.ML" setup Typedef.setup 
11608  113 

114 
end 