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

src/HOL/Typedef.thy

author | wenzelm |

Tue Oct 30 13:43:26 2001 +0100 (2001-10-30) | |

changeset 11982 | 65e2822d83dd |

parent 11979 | 0a3dace545c5 |

child 12023 | d982f98e0f0d |

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

lemma Least_mono moved from Typedef.thy to Set.thy;

1 (* Title: HOL/Typedef.thy

2 ID: $Id$

3 Author: Markus Wenzel, TU Munich

4 *)

6 header {* HOL type definitions *}

8 theory Typedef = Set

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

11 subsection {* HOL type definitions *}

13 constdefs

14 type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"

15 "type_definition Rep Abs A ==

16 (\<forall>x. Rep x \<in> A) \<and>

17 (\<forall>x. Abs (Rep x) = x) \<and>

18 (\<forall>y \<in> A. Rep (Abs y) = y)"

19 -- {* This will be stated as an axiom for each typedef! *}

21 lemma type_definitionI [intro]:

22 "(!!x. Rep x \<in> A) ==>

23 (!!x. Abs (Rep x) = x) ==>

24 (!!y. y \<in> A ==> Rep (Abs y) = y) ==>

25 type_definition Rep Abs A"

26 by (unfold type_definition_def) blast

28 theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A"

29 by (unfold type_definition_def) blast

31 theorem Rep_inverse: "type_definition Rep Abs A ==> Abs (Rep x) = x"

32 by (unfold type_definition_def) blast

34 theorem Abs_inverse: "type_definition Rep Abs A ==> y \<in> A ==> Rep (Abs y) = y"

35 by (unfold type_definition_def) blast

37 theorem Rep_inject: "type_definition Rep Abs A ==> (Rep x = Rep y) = (x = y)"

38 proof -

39 assume tydef: "type_definition Rep Abs A"

40 show ?thesis

41 proof

42 assume "Rep x = Rep y"

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

44 thus "x = y" by (simp only: Rep_inverse [OF tydef])

45 next

46 assume "x = y"

47 thus "Rep x = Rep y" by simp

48 qed

49 qed

51 theorem Abs_inject:

52 "type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)"

53 proof -

54 assume tydef: "type_definition Rep Abs A"

55 assume x: "x \<in> A" and y: "y \<in> A"

56 show ?thesis

57 proof

58 assume "Abs x = Abs y"

59 hence "Rep (Abs x) = Rep (Abs y)" by simp

60 moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef])

61 moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])

62 ultimately show "x = y" by (simp only:)

63 next

64 assume "x = y"

65 thus "Abs x = Abs y" by simp

66 qed

67 qed

69 theorem Rep_cases:

70 "type_definition Rep Abs A ==> y \<in> A ==> (!!x. y = Rep x ==> P) ==> P"

71 proof -

72 assume tydef: "type_definition Rep Abs A"

73 assume y: "y \<in> A" and r: "(!!x. y = Rep x ==> P)"

74 show P

75 proof (rule r)

76 from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])

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

78 qed

79 qed

81 theorem Abs_cases:

82 "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \<in> A ==> P) ==> P"

83 proof -

84 assume tydef: "type_definition Rep Abs A"

85 assume r: "!!y. x = Abs y ==> y \<in> A ==> P"

86 show P

87 proof (rule r)

88 have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])

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

90 show "Rep x \<in> A" by (rule Rep [OF tydef])

91 qed

92 qed

94 theorem Rep_induct:

95 "type_definition Rep Abs A ==> y \<in> A ==> (!!x. P (Rep x)) ==> P y"

96 proof -

97 assume tydef: "type_definition Rep Abs A"

98 assume "!!x. P (Rep x)" hence "P (Rep (Abs y))" .

99 moreover assume "y \<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])

100 ultimately show "P y" by (simp only:)

101 qed

103 theorem Abs_induct:

104 "type_definition Rep Abs A ==> (!!y. y \<in> A ==> P (Abs y)) ==> P x"

105 proof -

106 assume tydef: "type_definition Rep Abs A"

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

108 have "Rep x \<in> A" by (rule Rep [OF tydef])

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

110 moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])

111 ultimately show "P x" by (simp only:)

112 qed

114 use "Tools/typedef_package.ML"

116 end