author  wenzelm 
Thu, 21 Feb 2002 20:08:09 +0100  
changeset 12918  bca45be2d25b 
parent 12029  7df1d840d01d 
child 13635  c41e88151b54 
permissions  rwrr 
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

1 
(* Title: HOL/Datatype.thy 
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

2 
ID: $Id$ 
11954  3 
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen 
4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 

5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

5 
*) 
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

6 

12918  7 
header {* Datatypes *} 
11954  8 

9 
theory Datatype = Datatype_Universe: 

10 

12918  11 
subsection {* Finishing the datatype package setup *} 
12 

12029  13 
text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *} 
11954  14 
hide const Node Atom Leaf Numb Lim Funs Split Case 
15 
hide type node item 

16 

17 

18 
subsection {* Representing primitive types *} 

5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

19 

5759  20 
rep_datatype bool 
11954  21 
distinct True_not_False False_not_True 
22 
induction bool_induct 

23 

24 
declare case_split [cases type: bool] 

25 
 "prefer plain propositional version" 

26 

27 
rep_datatype unit 

28 
induction unit_induct 

5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

29 

4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

30 
rep_datatype prod 
11954  31 
inject Pair_eq 
32 
induction prod_induct 

33 

12918  34 
rep_datatype sum 
35 
distinct Inl_not_Inr Inr_not_Inl 

36 
inject Inl_eq Inr_eq 

37 
induction sum_induct 

38 

39 
ML {* 

40 
val [sum_case_Inl, sum_case_Inr] = thms "sum.cases"; 

41 
bind_thm ("sum_case_Inl", sum_case_Inl); 

42 
bind_thm ("sum_case_Inr", sum_case_Inr); 

43 
*}  {* compatibility *} 

44 

45 
lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)" 

46 
apply (rule_tac s = s in sumE) 

47 
apply (erule ssubst) 

48 
apply (rule sum_case_Inl) 

49 
apply (erule ssubst) 

50 
apply (rule sum_case_Inr) 

51 
done 

52 

53 
lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t" 

54 
 {* Prevents simplification of @{text f} and @{text g}: much faster. *} 

55 
by (erule arg_cong) 

56 

57 
lemma sum_case_inject: 

58 
"sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P" 

59 
proof  

60 
assume a: "sum_case f1 f2 = sum_case g1 g2" 

61 
assume r: "f1 = g1 ==> f2 = g2 ==> P" 

62 
show P 

63 
apply (rule r) 

64 
apply (rule ext) 

65 
apply (cut_tac x = "Inl x" in a [THEN fun_cong]) 

66 
apply simp 

67 
apply (rule ext) 

68 
apply (cut_tac x = "Inr x" in a [THEN fun_cong]) 

69 
apply simp 

70 
done 

71 
qed 

72 

73 

74 
subsection {* Further cases/induct rules for tuples *} 

11954  75 

76 
lemma prod_cases3 [case_names fields, cases type]: 

77 
"(!!a b c. y = (a, b, c) ==> P) ==> P" 

78 
apply (cases y) 

79 
apply (case_tac b) 

80 
apply blast 

81 
done 

82 

83 
lemma prod_induct3 [case_names fields, induct type]: 

84 
"(!!a b c. P (a, b, c)) ==> P x" 

85 
by (cases x) blast 

86 

87 
lemma prod_cases4 [case_names fields, cases type]: 

88 
"(!!a b c d. y = (a, b, c, d) ==> P) ==> P" 

89 
apply (cases y) 

90 
apply (case_tac c) 

91 
apply blast 

92 
done 

93 

94 
lemma prod_induct4 [case_names fields, induct type]: 

95 
"(!!a b c d. P (a, b, c, d)) ==> P x" 

96 
by (cases x) blast 

5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

97 

11954  98 
lemma prod_cases5 [case_names fields, cases type]: 
99 
"(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P" 

100 
apply (cases y) 

101 
apply (case_tac d) 

102 
apply blast 

103 
done 

104 

105 
lemma prod_induct5 [case_names fields, induct type]: 

106 
"(!!a b c d e. P (a, b, c, d, e)) ==> P x" 

107 
by (cases x) blast 

108 

109 
lemma prod_cases6 [case_names fields, cases type]: 

110 
"(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P" 

111 
apply (cases y) 

112 
apply (case_tac e) 

113 
apply blast 

114 
done 

115 

116 
lemma prod_induct6 [case_names fields, induct type]: 

117 
"(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" 

118 
by (cases x) blast 

119 

120 
lemma prod_cases7 [case_names fields, cases type]: 

121 
"(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P" 

122 
apply (cases y) 

123 
apply (case_tac f) 

124 
apply blast 

125 
done 

126 

127 
lemma prod_induct7 [case_names fields, induct type]: 

128 
"(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" 

129 
by (cases x) blast 

5759  130 

12918  131 

132 
subsection {* The option type *} 

133 

134 
datatype 'a option = None  Some 'a 

135 

136 
lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)" 

137 
by (induct x) auto 

138 

139 
lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)" 

140 
by (induct x) auto 

141 

142 
lemma option_caseE: 

143 
"(case x of None => P  Some y => Q y) ==> 

144 
(x = None ==> P ==> R) ==> 

145 
(!!y. x = Some y ==> Q y ==> R) ==> R" 

146 
by (cases x) simp_all 

147 

148 

149 
subsubsection {* Operations *} 

150 

151 
consts 

152 
the :: "'a option => 'a" 

153 
primrec 

154 
"the (Some x) = x" 

155 

156 
consts 

157 
o2s :: "'a option => 'a set" 

158 
primrec 

159 
"o2s None = {}" 

160 
"o2s (Some x) = {x}" 

161 

162 
lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x" 

163 
by simp 

164 

165 
ML_setup {* claset_ref() := claset() addSD2 ("ospec", thm "ospec") *} 

166 

167 
lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)" 

168 
by (cases xo) auto 

169 

170 
lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)" 

171 
by (cases xo) auto 

172 

173 

174 
constdefs 

175 
option_map :: "('a => 'b) => ('a option => 'b option)" 

176 
"option_map == %f y. case y of None => None  Some x => Some (f x)" 

177 

178 
lemma option_map_None [simp]: "option_map f None = None" 

179 
by (simp add: option_map_def) 

180 

181 
lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)" 

182 
by (simp add: option_map_def) 

183 

184 
lemma option_map_eq_Some [iff]: 

185 
"(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)" 

186 
by (simp add: option_map_def split add: option.split) 

187 

188 
lemma option_map_o_sum_case [simp]: 

189 
"option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)" 

190 
apply (rule ext) 

191 
apply (simp split add: sum.split) 

192 
done 

193 

5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

194 
end 