summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Typedef.thy

author | haftmann |

Thu Aug 12 17:56:41 2010 +0200 (2010-08-12) | |

changeset 38393 | 7c045c03598f |

parent 37863 | 7f113caabcf4 |

child 38536 | 7e57a0dcbd4f |

permissions | -rw-r--r-- |

group record-related ML files

1 (* Title: HOL/Typedef.thy

2 Author: Markus Wenzel, TU Munich

3 *)

5 header {* HOL type definitions *}

7 theory Typedef

8 imports Set

9 uses

10 ("Tools/typedef.ML")

11 ("Tools/typedef_codegen.ML")

12 begin

14 ML {*

15 structure HOL = struct val thy = @{theory HOL} end;

16 *} -- "belongs to theory HOL"

18 locale type_definition =

19 fixes Rep and Abs and A

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

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

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

23 -- {* This will be axiomatized for each typedef! *}

24 begin

26 lemma Rep_inject:

27 "(Rep x = Rep y) = (x = y)"

28 proof

29 assume "Rep x = Rep y"

30 then have "Abs (Rep x) = Abs (Rep y)" by (simp only:)

31 moreover have "Abs (Rep x) = x" by (rule Rep_inverse)

32 moreover have "Abs (Rep y) = y" by (rule Rep_inverse)

33 ultimately show "x = y" by simp

34 next

35 assume "x = y"

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

37 qed

39 lemma Abs_inject:

40 assumes x: "x \<in> A" and y: "y \<in> A"

41 shows "(Abs x = Abs y) = (x = y)"

42 proof

43 assume "Abs x = Abs y"

44 then have "Rep (Abs x) = Rep (Abs y)" by (simp only:)

45 moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse)

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

47 ultimately show "x = y" by simp

48 next

49 assume "x = y"

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

51 qed

53 lemma Rep_cases [cases set]:

54 assumes y: "y \<in> A"

55 and hyp: "!!x. y = Rep x ==> P"

56 shows P

57 proof (rule hyp)

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

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

60 qed

62 lemma Abs_cases [cases type]:

63 assumes r: "!!y. x = Abs y ==> y \<in> A ==> P"

64 shows P

65 proof (rule r)

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

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

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

69 qed

71 lemma Rep_induct [induct set]:

72 assumes y: "y \<in> A"

73 and hyp: "!!x. P (Rep x)"

74 shows "P y"

75 proof -

76 have "P (Rep (Abs y))" by (rule hyp)

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

78 ultimately show "P y" by simp

79 qed

81 lemma Abs_induct [induct type]:

82 assumes r: "!!y. y \<in> A ==> P (Abs y)"

83 shows "P x"

84 proof -

85 have "Rep x \<in> A" by (rule Rep)

86 then have "P (Abs (Rep x))" by (rule r)

87 moreover have "Abs (Rep x) = x" by (rule Rep_inverse)

88 ultimately show "P x" by simp

89 qed

91 lemma Rep_range: "range Rep = A"

92 proof

93 show "range Rep <= A" using Rep by (auto simp add: image_def)

94 show "A <= range Rep"

95 proof

96 fix x assume "x : A"

97 hence "x = Rep (Abs x)" by (rule Abs_inverse [symmetric])

98 thus "x : range Rep" by (rule range_eqI)

99 qed

100 qed

102 lemma Abs_image: "Abs ` A = UNIV"

103 proof

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

105 next

106 show "UNIV <= Abs ` A"

107 proof

108 fix x

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

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

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

112 qed

113 qed

115 end

117 use "Tools/typedef.ML" setup Typedef.setup

118 use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup

120 end