author  haftmann 
Tue, 17 Jan 2006 16:36:57 +0100  
changeset 18702  7dc7dcd63224 
parent 18576  8d98b7711e47 
child 18757  f0d901bc0686 
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 
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

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

5 

12918  6 
header {* Datatypes *} 
11954  7 

15131  8 
theory Datatype 
15140  9 
imports Datatype_Universe 
15131  10 
begin 
11954  11 

12 
subsection {* Representing primitive types *} 

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

13 

5759  14 
rep_datatype bool 
11954  15 
distinct True_not_False False_not_True 
16 
induction bool_induct 

17 

18 
declare case_split [cases type: bool] 

19 
 "prefer plain propositional version" 

20 

21 
rep_datatype unit 

22 
induction unit_induct 

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

23 

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

24 
rep_datatype prod 
11954  25 
inject Pair_eq 
26 
induction prod_induct 

27 

12918  28 
rep_datatype sum 
29 
distinct Inl_not_Inr Inr_not_Inl 

30 
inject Inl_eq Inr_eq 

31 
induction sum_induct 

32 

33 
ML {* 

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

35 
bind_thm ("sum_case_Inl", sum_case_Inl); 

36 
bind_thm ("sum_case_Inr", sum_case_Inr); 

37 
*}  {* compatibility *} 

38 

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

40 
apply (rule_tac s = s in sumE) 

41 
apply (erule ssubst) 

42 
apply (rule sum_case_Inl) 

43 
apply (erule ssubst) 

44 
apply (rule sum_case_Inr) 

45 
done 

46 

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

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

49 
by (erule arg_cong) 

50 

51 
lemma sum_case_inject: 

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

53 
proof  

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

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

56 
show P 

57 
apply (rule r) 

58 
apply (rule ext) 

14208  59 
apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp) 
12918  60 
apply (rule ext) 
14208  61 
apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp) 
12918  62 
done 
63 
qed 

64 

13635
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

65 
constdefs 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

66 
Suml :: "('a => 'c) => 'a + 'b => 'c" 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

67 
"Suml == (%f. sum_case f arbitrary)" 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

68 

c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

69 
Sumr :: "('b => 'c) => 'a + 'b => 'c" 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

70 
"Sumr == sum_case arbitrary" 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

71 

c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

72 
lemma Suml_inject: "Suml f = Suml g ==> f = g" 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

73 
by (unfold Suml_def) (erule sum_case_inject) 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

74 

c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

75 
lemma Sumr_inject: "Sumr f = Sumr g ==> f = g" 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

76 
by (unfold Sumr_def) (erule sum_case_inject) 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

77 

c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

78 

c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

79 
subsection {* Finishing the datatype package setup *} 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

80 

c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

81 
text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *} 
18230  82 
hide (open) const Push Node Atom Leaf Numb Lim Split Case Suml Sumr 
83 
hide (open) type node item 

13635
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

84 

12918  85 

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

11954  87 

88 
lemma prod_cases3 [case_names fields, cases type]: 

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

90 
apply (cases y) 

14208  91 
apply (case_tac b, blast) 
11954  92 
done 
93 

94 
lemma prod_induct3 [case_names fields, induct type]: 

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

96 
by (cases x) blast 

97 

98 
lemma prod_cases4 [case_names fields, cases type]: 

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

100 
apply (cases y) 

14208  101 
apply (case_tac c, blast) 
11954  102 
done 
103 

104 
lemma prod_induct4 [case_names fields, induct type]: 

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

106 
by (cases x) blast 

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

107 

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

110 
apply (cases y) 

14208  111 
apply (case_tac d, blast) 
11954  112 
done 
113 

114 
lemma prod_induct5 [case_names fields, induct type]: 

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

116 
by (cases x) blast 

117 

118 
lemma prod_cases6 [case_names fields, cases type]: 

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

120 
apply (cases y) 

14208  121 
apply (case_tac e, blast) 
11954  122 
done 
123 

124 
lemma prod_induct6 [case_names fields, induct type]: 

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

126 
by (cases x) blast 

127 

128 
lemma prod_cases7 [case_names fields, cases type]: 

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

130 
apply (cases y) 

14208  131 
apply (case_tac f, blast) 
11954  132 
done 
133 

134 
lemma prod_induct7 [case_names fields, induct type]: 

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

136 
by (cases x) blast 

5759  137 

12918  138 

139 
subsection {* The option type *} 

140 

141 
datatype 'a option = None  Some 'a 

142 

18576  143 
lemma not_None_eq[iff]: "(x ~= None) = (EX y. x = Some y)" 
144 
by (induct x) auto 

145 

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

18447  147 
by (induct x) auto 
148 

18576  149 
text{*Although it may appear that both of these equalities are helpful 
150 
only when applied to assumptions, in practice it seems better to give 

151 
them the uniform iff attribute. *} 

12918  152 

18576  153 
(* 
18447  154 
lemmas not_None_eq_D = not_None_eq [THEN iffD1] 
155 
declare not_None_eq_D [dest!] 

156 

157 
lemmas not_Some_eq_D = not_Some_eq [THEN iffD1] 

158 
declare not_Some_eq_D [dest!] 

18576  159 
*) 
12918  160 

161 
lemma option_caseE: 

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

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

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

165 
by (cases x) simp_all 

166 

167 

168 
subsubsection {* Operations *} 

169 

170 
consts 

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

172 
primrec 

173 
"the (Some x) = x" 

174 

175 
consts 

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

177 
primrec 

178 
"o2s None = {}" 

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

180 

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

182 
by simp 

183 

17876  184 
ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *} 
12918  185 

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

187 
by (cases xo) auto 

188 

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

190 
by (cases xo) auto 

191 

192 

193 
constdefs 

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

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

196 

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

198 
by (simp add: option_map_def) 

199 

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

201 
by (simp add: option_map_def) 

202 

14187  203 
lemma option_map_is_None[iff]: 
204 
"(option_map f opt = None) = (opt = None)" 

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

206 

12918  207 
lemma option_map_eq_Some [iff]: 
208 
"(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)" 

14187  209 
by (simp add: option_map_def split add: option.split) 
210 

211 
lemma option_map_comp: 

212 
"option_map f (option_map g opt) = option_map (f o g) opt" 

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

12918  214 

215 
lemma option_map_o_sum_case [simp]: 

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

217 
apply (rule ext) 

218 
apply (simp split add: sum.split) 

219 
done 

220 

17458
e42bfad176eb
lemmas [code] = imp_conv_disj (from Main.thy)  Why does it need Datatype?
wenzelm
parents:
15140
diff
changeset

221 
lemmas [code] = imp_conv_disj 
e42bfad176eb
lemmas [code] = imp_conv_disj (from Main.thy)  Why does it need Datatype?
wenzelm
parents:
15140
diff
changeset

222 

18702  223 
subsubsection {* Codegenerator setup *} 
224 

225 
code_syntax_const 

226 
True 

227 
ml (atom "true") 

228 
haskell (atom "True") 

229 
False 

230 
ml (atom "false") 

231 
haskell (atom "False") 

232 

233 
code_syntax_const 

234 
Pair 

235 
ml (atom "(__,/ __)") 

236 
haskell (atom "(__,/ __)") 

237 

238 
code_syntax_const 

239 
1 :: "nat" 

240 
ml ("{*Suc 0*}") 

241 
haskell ("{*Suc 0*}") 

242 

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

243 
end 