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

src/HOL/Typedef.thy

author | wenzelm |

Mon Dec 07 10:38:04 2015 +0100 (2015-12-07) | |

changeset 61799 | 4cf66f21b764 |

parent 61102 | 0ec9fd8d8119 |

child 63434 | c956d995bec6 |

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

isabelle update_cartouches -c -t;

1 (* Title: HOL/Typedef.thy

2 Author: Markus Wenzel, TU Munich

3 *)

5 section \<open>HOL type definitions\<close>

7 theory Typedef

8 imports Set

9 keywords "typedef" :: thy_goal and "morphisms"

10 begin

12 locale type_definition =

13 fixes Rep and Abs and A

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

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

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

17 \<comment> \<open>This will be axiomatized for each typedef!\<close>

18 begin

20 lemma Rep_inject: "Rep x = Rep y \<longleftrightarrow> x = y"

21 proof

22 assume "Rep x = Rep y"

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

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

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

26 ultimately show "x = y" by simp

27 next

28 assume "x = y"

29 then show "Rep x = Rep y" by (simp only:)

30 qed

32 lemma Abs_inject:

33 assumes "x \<in> A" and "y \<in> A"

34 shows "Abs x = Abs y \<longleftrightarrow> x = y"

35 proof

36 assume "Abs x = Abs y"

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

38 moreover from \<open>x \<in> A\<close> have "Rep (Abs x) = x" by (rule Abs_inverse)

39 moreover from \<open>y \<in> A\<close> have "Rep (Abs y) = y" by (rule Abs_inverse)

40 ultimately show "x = y" by simp

41 next

42 assume "x = y"

43 then show "Abs x = Abs y" by (simp only:)

44 qed

46 lemma Rep_cases [cases set]:

47 assumes "y \<in> A"

48 and hyp: "\<And>x. y = Rep x \<Longrightarrow> P"

49 shows P

50 proof (rule hyp)

51 from \<open>y \<in> A\<close> have "Rep (Abs y) = y" by (rule Abs_inverse)

52 then show "y = Rep (Abs y)" ..

53 qed

55 lemma Abs_cases [cases type]:

56 assumes r: "\<And>y. x = Abs y \<Longrightarrow> y \<in> A \<Longrightarrow> P"

57 shows P

58 proof (rule r)

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

60 then show "x = Abs (Rep x)" ..

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

62 qed

64 lemma Rep_induct [induct set]:

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

66 and hyp: "\<And>x. P (Rep x)"

67 shows "P y"

68 proof -

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

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

71 ultimately show "P y" by simp

72 qed

74 lemma Abs_induct [induct type]:

75 assumes r: "\<And>y. y \<in> A \<Longrightarrow> P (Abs y)"

76 shows "P x"

77 proof -

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

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

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

81 ultimately show "P x" by simp

82 qed

84 lemma Rep_range: "range Rep = A"

85 proof

86 show "range Rep \<subseteq> A" using Rep by (auto simp add: image_def)

87 show "A \<subseteq> range Rep"

88 proof

89 fix x assume "x \<in> A"

90 then have "x = Rep (Abs x)" by (rule Abs_inverse [symmetric])

91 then show "x \<in> range Rep" by (rule range_eqI)

92 qed

93 qed

95 lemma Abs_image: "Abs ` A = UNIV"

96 proof

97 show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV)

98 show "UNIV \<subseteq> Abs ` A"

99 proof

100 fix x

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

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

103 ultimately show "x \<in> Abs ` A" by (rule image_eqI)

104 qed

105 qed

107 end

109 ML_file "Tools/typedef.ML"

111 end