author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10291  a88d347db404 
child 11083  d8fda557e476 
permissions  rwrr 
1475  1 
(* Title: HOL/subset.thy 
923  2 
ID: $Id$ 
1475  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
923  4 
Copyright 1994 University of Cambridge 
10276  5 

6 
Subset lemmas and HOL type definitions. 

923  7 
*) 
8 

7705  9 
theory subset = Set 
10276  10 
files "Tools/induct_attrib.ML" ("Tools/typedef_package.ML"): 
7705  11 

9895  12 
(*belongs to theory Ord*) 
13 
theorems linorder_cases [case_names less equal greater] = 

14 
linorder_less_split 

15 

16 
(*belongs to theory Set*) 

17 
setup Rulify.setup 

7717
e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7705
diff
changeset

18 

10276  19 

20 
section {* HOL type definitions *} 

21 

22 
constdefs 

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

24 
"type_definition Rep Abs A == 

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

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

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

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

29 

10290  30 
lemma type_definitionI [intro]: 
10291  31 
"(!!x. Rep x \<in> A) ==> 
32 
(!!x. Abs (Rep x) = x) ==> 

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

10290  34 
type_definition Rep Abs A" 
35 
by (unfold type_definition_def) blast 

36 

10276  37 
theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A" 
38 
by (unfold type_definition_def) blast 

39 

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

41 
by (unfold type_definition_def) blast 

42 

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

44 
by (unfold type_definition_def) blast 

45 

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

47 
proof  

48 
assume tydef: "type_definition Rep Abs A" 

49 
show ?thesis 

50 
proof 

51 
assume "Rep x = Rep y" 

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

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

54 
next 

55 
assume "x = y" 

56 
thus "Rep x = Rep y" by simp 

57 
qed 

58 
qed 

59 

10284  60 
theorem Abs_inject: 
61 
"type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)" 

62 
proof  

63 
assume tydef: "type_definition Rep Abs A" 

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

65 
show ?thesis 

66 
proof 

67 
assume "Abs x = Abs y" 

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

69 
moreover note x hence "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef]) 

70 
moreover note y hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef]) 

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

72 
next 

73 
assume "x = y" 

74 
thus "Abs x = Abs y" by simp 

75 
qed 

76 
qed 

77 

10276  78 
theorem Rep_cases: 
79 
"type_definition Rep Abs A ==> y \<in> A ==> (!!x. y = Rep x ==> P) ==> P" 

80 
proof  

81 
assume tydef: "type_definition Rep Abs A" 

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

83 
show P 

84 
proof (rule r) 

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

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

87 
qed 

88 
qed 

89 

90 
theorem Abs_cases: 

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

92 
proof  

93 
assume tydef: "type_definition Rep Abs A" 

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

95 
show P 

96 
proof (rule r) 

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

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

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

100 
qed 

101 
qed 

102 

103 
theorem Rep_induct: 

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

105 
proof  

106 
assume tydef: "type_definition Rep Abs A" 

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

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

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

110 
qed 

111 

112 
theorem Abs_induct: 

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

114 
proof  

115 
assume tydef: "type_definition Rep Abs A" 

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

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

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

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

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

121 
qed 

122 

123 
setup InductAttrib.setup 

124 
use "Tools/typedef_package.ML" 

125 

7705  126 
end 