author  kleing 
Mon, 21 Jun 2004 10:25:57 +0200  
changeset 14981  e73f8140af78 
parent 14274  0cb8a9a144d2 
child 15131  c69542757a4d 
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 

8 
theory Datatype = Datatype_Universe: 

9 

10 
subsection {* Representing primitive types *} 

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

11 

5759  12 
rep_datatype bool 
11954  13 
distinct True_not_False False_not_True 
14 
induction bool_induct 

15 

16 
declare case_split [cases type: bool] 

17 
 "prefer plain propositional version" 

18 

19 
rep_datatype unit 

20 
induction unit_induct 

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

21 

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

22 
rep_datatype prod 
11954  23 
inject Pair_eq 
24 
induction prod_induct 

25 

12918  26 
rep_datatype sum 
27 
distinct Inl_not_Inr Inr_not_Inl 

28 
inject Inl_eq Inr_eq 

29 
induction sum_induct 

30 

31 
ML {* 

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

33 
bind_thm ("sum_case_Inl", sum_case_Inl); 

34 
bind_thm ("sum_case_Inr", sum_case_Inr); 

35 
*}  {* compatibility *} 

36 

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

38 
apply (rule_tac s = s in sumE) 

39 
apply (erule ssubst) 

40 
apply (rule sum_case_Inl) 

41 
apply (erule ssubst) 

42 
apply (rule sum_case_Inr) 

43 
done 

44 

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

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

47 
by (erule arg_cong) 

48 

49 
lemma sum_case_inject: 

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

51 
proof  

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

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

54 
show P 

55 
apply (rule r) 

56 
apply (rule ext) 

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

62 

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

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

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

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

66 

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

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

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

69 

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

70 
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

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

72 

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

73 
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

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

75 

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

76 

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

77 
subsection {* Finishing the datatype package setup *} 
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 
text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *} 
14274  80 
hide const Push Node Atom Leaf Numb Lim Split Case Suml Sumr 
13635
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

81 
hide type node item 
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

82 

12918  83 

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

11954  85 

86 
lemma prod_cases3 [case_names fields, cases type]: 

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

88 
apply (cases y) 

14208  89 
apply (case_tac b, blast) 
11954  90 
done 
91 

92 
lemma prod_induct3 [case_names fields, induct type]: 

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

94 
by (cases x) blast 

95 

96 
lemma prod_cases4 [case_names fields, cases type]: 

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

98 
apply (cases y) 

14208  99 
apply (case_tac c, blast) 
11954  100 
done 
101 

102 
lemma prod_induct4 [case_names fields, induct type]: 

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

104 
by (cases x) blast 

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

105 

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

108 
apply (cases y) 

14208  109 
apply (case_tac d, blast) 
11954  110 
done 
111 

112 
lemma prod_induct5 [case_names fields, induct type]: 

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

114 
by (cases x) blast 

115 

116 
lemma prod_cases6 [case_names fields, cases type]: 

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

118 
apply (cases y) 

14208  119 
apply (case_tac e, blast) 
11954  120 
done 
121 

122 
lemma prod_induct6 [case_names fields, induct type]: 

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

124 
by (cases x) blast 

125 

126 
lemma prod_cases7 [case_names fields, cases type]: 

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

128 
apply (cases y) 

14208  129 
apply (case_tac f, blast) 
11954  130 
done 
131 

132 
lemma prod_induct7 [case_names fields, induct type]: 

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

134 
by (cases x) blast 

5759  135 

12918  136 

137 
subsection {* The option type *} 

138 

139 
datatype 'a option = None  Some 'a 

140 

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

142 
by (induct x) auto 

143 

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

145 
by (induct x) auto 

146 

147 
lemma option_caseE: 

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

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

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

151 
by (cases x) simp_all 

152 

153 

154 
subsubsection {* Operations *} 

155 

156 
consts 

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

158 
primrec 

159 
"the (Some x) = x" 

160 

161 
consts 

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

163 
primrec 

164 
"o2s None = {}" 

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

166 

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

168 
by simp 

169 

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

171 

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

173 
by (cases xo) auto 

174 

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

176 
by (cases xo) auto 

177 

178 

179 
constdefs 

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

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

182 

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

184 
by (simp add: option_map_def) 

185 

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

187 
by (simp add: option_map_def) 

188 

14187  189 
lemma option_map_is_None[iff]: 
190 
"(option_map f opt = None) = (opt = None)" 

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

192 

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

14187  195 
by (simp add: option_map_def split add: option.split) 
196 

197 
lemma option_map_comp: 

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

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

12918  200 

201 
lemma option_map_o_sum_case [simp]: 

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

203 
apply (rule ext) 

204 
apply (simp split add: sum.split) 

205 
done 

206 

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

207 
end 