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

src/HOL/Typedef.thy

author | wenzelm |

Wed Oct 03 20:54:05 2001 +0200 (2001-10-03) | |

changeset 11654 | 53d18ab990f6 |

parent 11608 | c760ea8154ee |

child 11659 | a68f930bafb2 |

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

moved linorder_cases to theory Ord;

1 (* Title: HOL/Typedef.thy

2 ID: $Id$

3 Author: Markus Wenzel, TU Munich

5 Misc set-theory lemmas and HOL type definitions.

6 *)

8 theory Typedef = Set

9 files "subset.ML" "equalities.ML" "mono.ML"

10 "Tools/induct_attrib.ML" ("Tools/typedef_package.ML"):

12 (* Courtesy of Stephan Merz *)

13 lemma Least_mono:

14 "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y

15 ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"

16 apply clarify

17 apply (erule_tac P = "%x. x : S" in LeastI2)

18 apply fast

19 apply (rule LeastI2)

20 apply (auto elim: monoD intro!: order_antisym)

21 done

24 (*belongs to theory Set*)

25 setup Rulify.setup

28 section {* HOL type definitions *}

30 constdefs

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

32 "type_definition Rep Abs A ==

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

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

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

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

38 lemma type_definitionI [intro]:

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

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

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

42 type_definition Rep Abs A"

43 by (unfold type_definition_def) blast

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

46 by (unfold type_definition_def) blast

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

49 by (unfold type_definition_def) blast

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

52 by (unfold type_definition_def) blast

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

55 proof -

56 assume tydef: "type_definition Rep Abs A"

57 show ?thesis

58 proof

59 assume "Rep x = Rep y"

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

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

62 next

63 assume "x = y"

64 thus "Rep x = Rep y" by simp

65 qed

66 qed

68 theorem Abs_inject:

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

70 proof -

71 assume tydef: "type_definition Rep Abs A"

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

73 show ?thesis

74 proof

75 assume "Abs x = Abs y"

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

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

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

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

80 next

81 assume "x = y"

82 thus "Abs x = Abs y" by simp

83 qed

84 qed

86 theorem Rep_cases:

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

88 proof -

89 assume tydef: "type_definition Rep Abs A"

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

91 show P

92 proof (rule r)

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

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

95 qed

96 qed

98 theorem Abs_cases:

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

100 proof -

101 assume tydef: "type_definition Rep Abs A"

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

103 show P

104 proof (rule r)

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

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

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

108 qed

109 qed

111 theorem Rep_induct:

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

113 proof -

114 assume tydef: "type_definition Rep Abs A"

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

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

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

118 qed

120 theorem Abs_induct:

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

122 proof -

123 assume tydef: "type_definition Rep Abs A"

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

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

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

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

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

129 qed

131 setup InductAttrib.setup

132 use "Tools/typedef_package.ML"

134 end