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 


8 
theory Typedef = Set

11979

9 
files ("Tools/typedef_package.ML"):

11608

10 

13412

11 
locale type_definition =


12 
fixes Rep and Abs and A


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


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


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


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

11608

17 

13412

18 
lemmas type_definitionI [intro] =


19 
type_definition.intro [OF type_definition_axioms.intro]

11608

20 

13412

21 
lemma (in type_definition) Rep_inject:


22 
"(Rep x = Rep y) = (x = y)"


23 
proof


24 
assume "Rep x = Rep y"


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


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


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


28 
finally show "x = y" .


29 
next


30 
assume "x = y"


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


32 
qed

11608

33 

13412

34 
lemma (in type_definition) Abs_inject:


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"


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


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


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


42 
finally show "x = y" .


43 
next


44 
assume "x = y"


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

11608

46 
qed


47 

13412

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


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 

13412

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


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 

13412

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


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)


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


73 
finally show "P y" .

11608

74 
qed


75 

13412

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


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)

11608

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

13412

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


83 
finally show "P x" .

11608

84 
qed


85 


86 
use "Tools/typedef_package.ML"


87 


88 
end
