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

src/HOL/Typedef.thy

author | wenzelm |

Wed Jul 24 00:10:52 2002 +0200 (2002-07-24) | |

changeset 13412 | 666137b488a4 |

parent 12023 | d982f98e0f0d |

child 13421 | 8fcdf4a26468 |

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

predicate defs via locales;

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 locale type_definition =

12 fixes Rep and Abs and A

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

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

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

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

18 lemmas type_definitionI [intro] =

19 type_definition.intro [OF type_definition_axioms.intro]

21 lemma (in type_definition) Rep_inject:

22 "(Rep x = Rep y) = (x = y)"

23 proof

24 assume "Rep x = Rep y"

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

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

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

28 finally show "x = y" .

29 next

30 assume "x = y"

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

32 qed

34 lemma (in type_definition) Abs_inject:

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

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

37 proof

38 assume "Abs x = Abs y"

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

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

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

42 finally show "x = y" .

43 next

44 assume "x = y"

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

46 qed

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

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

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

51 shows P

52 proof (rule hyp)

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

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

55 qed

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

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

59 shows P

60 proof (rule r)

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

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

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

64 qed

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

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

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

69 shows "P y"

70 proof -

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

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

73 finally show "P y" .

74 qed

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

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

78 shows "P x"

79 proof -

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

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

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

83 finally show "P x" .

84 qed

86 use "Tools/typedef_package.ML"

88 end