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

src/HOL/Typedef.thy

author | nipkow |

Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) | |

changeset 15140 | 322485b816ac |

parent 15131 | c69542757a4d |

child 15260 | a12e999a0113 |

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

import -> imports

1 (* Title: HOL/Typedef.thy

2 ID: $Id$

3 Author: Markus Wenzel, TU Munich

4 *)

6 header {* HOL type definitions *}

8 theory Typedef

9 imports Set

10 files ("Tools/typedef_package.ML")

11 begin

13 locale type_definition =

14 fixes Rep and Abs and A

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

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

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

18 -- {* This will be axiomatized for each typedef! *}

20 lemma (in type_definition) Rep_inject:

21 "(Rep x = Rep y) = (x = y)"

22 proof

23 assume "Rep x = Rep y"

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

25 also have "Abs (Rep x) = x" by (rule Rep_inverse)

26 also have "Abs (Rep y) = y" by (rule Rep_inverse)

27 finally show "x = y" .

28 next

29 assume "x = y"

30 thus "Rep x = Rep y" by (simp only:)

31 qed

33 lemma (in type_definition) Abs_inject:

34 assumes x: "x \<in> A" and y: "y \<in> A"

35 shows "(Abs x = Abs y) = (x = y)"

36 proof

37 assume "Abs x = Abs y"

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

39 also from x have "Rep (Abs x) = x" by (rule Abs_inverse)

40 also from y have "Rep (Abs y) = y" by (rule Abs_inverse)

41 finally show "x = y" .

42 next

43 assume "x = y"

44 thus "Abs x = Abs y" by (simp only:)

45 qed

47 lemma (in type_definition) Rep_cases [cases set]:

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

49 and hyp: "!!x. y = Rep x ==> P"

50 shows P

51 proof (rule hyp)

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

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

54 qed

56 lemma (in type_definition) Abs_cases [cases type]:

57 assumes r: "!!y. x = Abs y ==> y \<in> A ==> P"

58 shows P

59 proof (rule r)

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

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

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

63 qed

65 lemma (in type_definition) Rep_induct [induct set]:

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

67 and hyp: "!!x. P (Rep x)"

68 shows "P y"

69 proof -

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

71 also from y have "Rep (Abs y) = y" by (rule Abs_inverse)

72 finally show "P y" .

73 qed

75 lemma (in type_definition) Abs_induct [induct type]:

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

77 shows "P x"

78 proof -

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

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

81 also have "Abs (Rep x) = x" by (rule Rep_inverse)

82 finally show "P x" .

83 qed

85 use "Tools/typedef_package.ML"

87 end