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

19459

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

11608

19 

13412

20 
lemma (in type_definition) Rep_inject:


21 
"(Rep x = Rep y) = (x = y)"


22 
proof


23 
assume "Rep x = Rep y"


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


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


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


27 
finally show "x = y" .


28 
next


29 
assume "x = y"


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


31 
qed

11608

32 

13412

33 
lemma (in type_definition) Abs_inject:


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"


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


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


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


41 
finally show "x = y" .


42 
next


43 
assume "x = y"


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

11608

45 
qed


46 

13412

47 
lemma (in type_definition) Rep_cases [cases set]:


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 

13412

56 
lemma (in type_definition) Abs_cases [cases type]:


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 

13412

65 
lemma (in type_definition) Rep_induct [induct set]:


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)


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


72 
finally show "P y" .

11608

73 
qed


74 

13412

75 
lemma (in type_definition) Abs_induct [induct type]:


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)

11608

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

13412

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


82 
finally show "P x" .

11608

83 
qed


84 


85 
use "Tools/typedef_package.ML"

19459

86 
use "Tools/typedef_codegen.ML"

11608

87 

19459

88 
setup {* TypedefPackage.setup #> TypedefCodegen.setup *}

15260

89 

11608

90 
end
