author  nipkow 
Wed, 18 Aug 2004 11:09:40 +0200  
changeset 15140  322485b816ac 
parent 15131  c69542757a4d 
child 17458  e42bfad176eb 
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. *} 
14274  82 
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

83 
hide type node item 
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 

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)" 

147 
by (induct x) auto 

148 

149 
lemma option_caseE: 

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

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

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

153 
by (cases x) simp_all 

154 

155 

156 
subsubsection {* Operations *} 

157 

158 
consts 

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

160 
primrec 

161 
"the (Some x) = x" 

162 

163 
consts 

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

165 
primrec 

166 
"o2s None = {}" 

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

168 

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

170 
by simp 

171 

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

173 

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

175 
by (cases xo) auto 

176 

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

178 
by (cases xo) auto 

179 

180 

181 
constdefs 

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

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

184 

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

186 
by (simp add: option_map_def) 

187 

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

189 
by (simp add: option_map_def) 

190 

14187  191 
lemma option_map_is_None[iff]: 
192 
"(option_map f opt = None) = (opt = None)" 

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

194 

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

14187  197 
by (simp add: option_map_def split add: option.split) 
198 

199 
lemma option_map_comp: 

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

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

12918  202 

203 
lemma option_map_o_sum_case [simp]: 

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

205 
apply (rule ext) 

206 
apply (simp split add: sum.split) 

207 
done 

208 

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

209 
end 