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"


32 
hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)


33 
also have "Abs (Rep x) = x" by (rule Rep_inverse)


34 
also have "Abs (Rep y) = y" by (rule Rep_inverse)


35 
finally show "x = y" .


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"


46 
hence "Rep (Abs x) = Rep (Abs y)" by (simp only:)


47 
also from x have "Rep (Abs x) = x" by (rule Abs_inverse)


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


49 
finally show "x = y" .


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)


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


80 
finally show "P y" .

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)

11608

88 
hence "P (Abs (Rep x))" by (rule r)

13412

89 
also have "Abs (Rep x) = x" by (rule Rep_inverse)


90 
finally show "P x" .

11608

91 
qed


92 

23247

93 
end


94 

11608

95 
use "Tools/typedef_package.ML"

20426

96 
use "Tools/typecopy_package.ML"

19459

97 
use "Tools/typedef_codegen.ML"

11608

98 

20426

99 
setup {*

22846

100 
TypecopyPackage.setup

20426

101 
#> TypedefCodegen.setup


102 
*}

15260

103 

11608

104 
end
