author  haftmann 
Thu, 04 Dec 2008 14:43:33 +0100  
changeset 28965  1de908189869 
parent 28394  b9c8e3a12a98 
child 29056  dc08e3990c77 
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 

27295  93 
lemma Rep_range: "range Rep = A" 
24269  94 
proof 
95 
show "range Rep <= A" using Rep by (auto simp add: image_def) 

96 
show "A <= range Rep" 

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

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

23433  101 
qed 
102 
qed 

103 

27295  104 
lemma Abs_image: "Abs ` A = UNIV" 
105 
proof 

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

107 
next 

108 
show "UNIV <= Abs ` A" 

109 
proof 

110 
fix x 

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

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

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

114 
qed 

115 
qed 

116 

23247  117 
end 
118 

11608  119 
use "Tools/typedef_package.ML" 
20426  120 
use "Tools/typecopy_package.ML" 
19459  121 
use "Tools/typedef_codegen.ML" 
11608  122 

20426  123 
setup {* 
25535  124 
TypedefPackage.setup 
125 
#> TypecopyPackage.setup 

20426  126 
#> TypedefCodegen.setup 
127 
*} 

15260  128 

26151
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

129 
text {* This class is just a workaround for classes without parameters; 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

130 
it shall disappear as soon as possible. *} 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

131 

4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

132 
class itself = type + 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

133 
fixes itself :: "'a itself" 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

134 

4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

135 
setup {* 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

136 
let fun add_itself tyco thy = 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

137 
let 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

138 
val vs = Name.names Name.context "'a" 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

139 
(replicate (Sign.arity_number thy tyco) @{sort type}); 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

140 
val ty = Type (tyco, map TFree vs); 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

141 
val lhs = Const (@{const_name itself}, Term.itselfT ty); 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

142 
val rhs = Logic.mk_type ty; 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

143 
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

144 
in 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

145 
thy 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

146 
> TheoryTarget.instantiation ([tyco], vs, @{sort itself}) 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

147 
> `(fn lthy => Syntax.check_term lthy eq) 
28965  148 
> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) 
26151
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

149 
> snd 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

150 
> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) 
28394  151 
> LocalTheory.exit_global 
26151
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

152 
end 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

153 
in TypedefPackage.interpretation add_itself end 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

154 
*} 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

155 

4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

156 
instantiation bool :: itself 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

157 
begin 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

158 

4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

159 
definition "itself = TYPE(bool)" 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

160 

4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

161 
instance .. 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

162 

11608  163 
end 
26151
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

164 

4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

165 
instantiation "fun" :: ("type", "type") itself 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

166 
begin 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

167 

4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

168 
definition "itself = TYPE('a \<Rightarrow> 'b)" 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

169 

4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

170 
instance .. 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

171 

4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

172 
end 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

173 

4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

174 
hide (open) const itself 
4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

175 

4a9b8f15ce7f
class itself works around a problem with class interpretation in class finite
haftmann
parents:
25535
diff
changeset

176 
end 