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

src/HOL/Typedef.thy

author | wenzelm |

Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) | |

changeset 63915 | bab633745c7f |

parent 63434 | c956d995bec6 |

child 69605 | a96320074298 |

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

tuned proofs;

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

10 "typedef" :: thy_goal and

11 "morphisms" :: quasi_command

12 begin

14 locale type_definition =

15 fixes Rep and Abs and A

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

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

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

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

20 begin

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

23 proof

24 assume "Rep x = Rep y"

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

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

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

28 ultimately show "x = y" by simp

29 next

30 assume "x = y"

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

32 qed

34 lemma Abs_inject:

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

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

37 proof

38 assume "Abs x = Abs y"

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

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

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

42 ultimately show "x = y" by simp

43 next

44 assume "x = y"

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

46 qed

48 lemma Rep_cases [cases set]:

49 assumes "y \<in> A"

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

51 shows P

52 proof (rule hyp)

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

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

55 qed

57 lemma Abs_cases [cases type]:

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

59 shows P

60 proof (rule r)

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

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

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

64 qed

66 lemma Rep_induct [induct set]:

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

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

69 shows "P y"

70 proof -

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

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

73 ultimately show "P y" by simp

74 qed

76 lemma Abs_induct [induct type]:

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

78 shows "P x"

79 proof -

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

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

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

83 ultimately show "P x" by simp

84 qed

86 lemma Rep_range: "range Rep = A"

87 proof

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

89 show "A \<subseteq> range Rep"

90 proof

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

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

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

94 qed

95 qed

97 lemma Abs_image: "Abs ` A = UNIV"

98 proof

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

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

101 proof

102 fix x

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

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

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

106 qed

107 qed

109 end

111 ML_file "Tools/typedef.ML"

113 end