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

src/HOL/Typedef.thy

author | wenzelm |

Sat Nov 03 01:33:54 2001 +0100 (2001-11-03) | |

changeset 12023 | d982f98e0f0d |

parent 11982 | 65e2822d83dd |

child 13412 | 666137b488a4 |

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

tuned;

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 constdefs

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

13 "type_definition Rep Abs A ==

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

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

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

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

19 lemma type_definitionI [intro]:

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

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

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

23 type_definition Rep Abs A"

24 by (unfold type_definition_def) blast

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

27 by (unfold type_definition_def) blast

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

30 by (unfold type_definition_def) blast

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

33 by (unfold type_definition_def) blast

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

36 proof -

37 assume tydef: "type_definition Rep Abs A"

38 show ?thesis

39 proof

40 assume "Rep x = Rep y"

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

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

43 next

44 assume "x = y"

45 thus "Rep x = Rep y" by simp

46 qed

47 qed

49 theorem Abs_inject:

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

51 proof -

52 assume tydef: "type_definition Rep Abs A"

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

54 show ?thesis

55 proof

56 assume "Abs x = Abs y"

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

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

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

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

61 next

62 assume "x = y"

63 thus "Abs x = Abs y" by simp

64 qed

65 qed

67 theorem Rep_cases:

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

69 proof -

70 assume tydef: "type_definition Rep Abs A"

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

72 show P

73 proof (rule r)

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

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

76 qed

77 qed

79 theorem Abs_cases:

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

81 proof -

82 assume tydef: "type_definition Rep Abs A"

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

84 show P

85 proof (rule r)

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

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

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

89 qed

90 qed

92 theorem Rep_induct:

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

94 proof -

95 assume tydef: "type_definition Rep Abs A"

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

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

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

99 qed

101 theorem Abs_induct:

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

103 proof -

104 assume tydef: "type_definition Rep Abs A"

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

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

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

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

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

110 qed

112 use "Tools/typedef_package.ML"

114 end