author  haftmann 
Fri, 20 Jun 2008 21:00:22 +0200  
changeset 27300  4cb3101d2bf7 
parent 27002  215d64dc971e 
child 29270  0eade173f77e 
permissions  rwrr 
5177  1 
(* Title: HOL/Tools/datatype_prop.ML 
2 
ID: $Id$ 

11539  3 
Author: Stefan Berghofer, TU Muenchen 
5177  4 

11539  5 
Characteristic properties of datatypes. 
5177  6 
*) 
7 

8 
signature DATATYPE_PROP = 

9 
sig 

8434  10 
val indexify_names: string list > string list 
13465  11 
val make_tnames: typ list > string list 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

12 
val make_injs : DatatypeAux.descr list > (string * sort) list > term list list 
26969
cf3f998d0631
moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
haftmann
parents:
25154
diff
changeset

13 
val make_distincts : DatatypeAux.descr list > 
27300
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

14 
(string * sort) list > (int * term list) list (*no symmetric inequalities*) 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

15 
val make_ind : DatatypeAux.descr list > (string * sort) list > term 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

16 
val make_casedists : DatatypeAux.descr list > (string * sort) list > term list 
15459
16dd63c78049
Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
berghofe
parents:
14981
diff
changeset

17 
val make_primrec_Ts : DatatypeAux.descr list > (string * sort) list > 
16dd63c78049
Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
berghofe
parents:
14981
diff
changeset

18 
string list > typ list * typ list 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

19 
val make_primrecs : string list > DatatypeAux.descr list > 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

20 
(string * sort) list > theory > term list 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

21 
val make_cases : string list > DatatypeAux.descr list > 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

22 
(string * sort) list > theory > term list list 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

23 
val make_splits : string list > DatatypeAux.descr list > 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

24 
(string * sort) list > theory > (term * term) list 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

25 
val make_weak_case_congs : string list > DatatypeAux.descr list > 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

26 
(string * sort) list > theory > term list 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

27 
val make_case_congs : string list > DatatypeAux.descr list > 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

28 
(string * sort) list > theory > term list 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

29 
val make_nchotomys : DatatypeAux.descr list > 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

30 
(string * sort) list > term list 
5177  31 
end; 
32 

33 
structure DatatypeProp : DATATYPE_PROP = 

34 
struct 

35 

36 
open DatatypeAux; 

37 

8434  38 
fun indexify_names names = 
39 
let 

40 
fun index (x :: xs) tab = 

17521  41 
(case AList.lookup (op =) tab x of 
25154  42 
NONE => if member (op =) xs x then (x ^ "1") :: index xs ((x, 2) :: tab) else x :: index xs tab 
43 
 SOME i => (x ^ string_of_int i) :: index xs ((x, i + 1) :: tab)) 

8434  44 
 index [] _ = []; 
45 
in index names [] end; 

46 

5177  47 
fun make_tnames Ts = 
48 
let 

49 
fun type_name (TFree (name, _)) = implode (tl (explode name)) 

50 
 type_name (Type (name, _)) = 

51 
let val name' = Sign.base_name name 

8434  52 
in if Syntax.is_identifier name' then name' else "x" end; 
53 
in indexify_names (map type_name Ts) end; 

5177  54 

55 

56 
(************************* injectivity of constructors ************************) 

57 

58 
fun make_injs descr sorts = 

59 
let 

21078  60 
val descr' = flat descr; 
61 
fun make_inj T (cname, cargs) = 

62 
if null cargs then I else 

5177  63 
let 
64 
val Ts = map (typ_of_dtyp descr' sorts) cargs; 

65 
val constr_t = Const (cname, Ts > T); 

66 
val tnames = make_tnames Ts; 

67 
val frees = map Free (tnames ~~ Ts); 

68 
val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts); 

21078  69 
in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq 
5177  70 
(HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')), 
71 
foldr1 (HOLogic.mk_binop "op &") 

21078  72 
(map HOLogic.mk_eq (frees ~~ frees'))))) 
5177  73 
end; 
21078  74 
in 
75 
map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) []) 

76 
(hd descr) (Library.take (length (hd descr), get_rec_types descr' sorts)) 

5177  77 
end; 
78 

27300
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

79 

4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

80 
(************************* distinctness of constructors ***********************) 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

81 

4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

82 
fun make_distincts descr sorts = 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

83 
let 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

84 
val descr' = flat descr; 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

85 
val recTs = get_rec_types descr' sorts; 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

86 
val newTs = Library.take (length (hd descr), recTs); 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

87 

4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

88 
fun prep_constr (cname, cargs) = (cname, map (typ_of_dtyp descr' sorts) cargs); 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

89 

4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

90 
fun make_distincts' _ [] = [] 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

91 
 make_distincts' T ((cname, cargs)::constrs) = 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

92 
let 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

93 
val frees = map Free ((make_tnames cargs) ~~ cargs); 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

94 
val t = list_comb (Const (cname, cargs > T), frees); 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

95 

4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

96 
fun make_distincts'' (cname', cargs') = 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

97 
let 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

98 
val frees' = map Free ((map ((op ^) o (rpair "'")) 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

99 
(make_tnames cargs')) ~~ cargs'); 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

100 
val t' = list_comb (Const (cname', cargs' > T), frees') 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

101 
in 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

102 
HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t')) 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

103 
end 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

104 

4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

105 
in map make_distincts'' constrs @ make_distincts' T constrs end; 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

106 

4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

107 
in 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

108 
map2 (fn ((_, (_, _, constrs))) => fn T => 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

109 
(length constrs, make_distincts' T (map prep_constr constrs))) (hd descr) newTs 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

110 
end; 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

111 

4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

112 

5177  113 
(********************************* induction **********************************) 
114 

115 
fun make_ind descr sorts = 

116 
let 

15570  117 
val descr' = List.concat descr; 
5177  118 
val recTs = get_rec_types descr' sorts; 
119 
val pnames = if length descr' = 1 then ["P"] 

120 
else map (fn i => "P" ^ string_of_int i) (1 upto length descr'); 

121 

122 
fun make_pred i T = 

123 
let val T' = T > HOLogic.boolT 

15570  124 
in Free (List.nth (pnames, i), T') end; 
5177  125 

126 
fun make_ind_prem k T (cname, cargs) = 

127 
let 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

128 
fun mk_prem ((dt, s), T) = 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

129 
let val (Us, U) = strip_type T 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

130 
in list_all (map (pair "x") Us, HOLogic.mk_Trueprop 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

131 
(make_pred (body_index dt) U $ app_bnds (Free (s, T)) (length Us))) 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

132 
end; 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6394
diff
changeset

133 

15570  134 
val recs = List.filter is_rec_type cargs; 
5177  135 
val Ts = map (typ_of_dtyp descr' sorts) cargs; 
136 
val recTs' = map (typ_of_dtyp descr' sorts) recs; 

20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19233
diff
changeset

137 
val tnames = Name.variant_list pnames (make_tnames Ts); 
15570  138 
val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs)); 
5177  139 
val frees = tnames ~~ Ts; 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6394
diff
changeset

140 
val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs'); 
5177  141 

142 
in list_all_free (frees, Logic.list_implies (prems, 

143 
HOLogic.mk_Trueprop (make_pred k T $ 

144 
list_comb (Const (cname, Ts > T), map Free frees)))) 

145 
end; 

146 

15570  147 
val prems = List.concat (map (fn ((i, (_, _, constrs)), T) => 
5177  148 
map (make_ind_prem i T) constrs) (descr' ~~ recTs)); 
149 
val tnames = make_tnames recTs; 

150 
val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &") 

151 
(map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T)) 

152 
(descr' ~~ recTs ~~ tnames))) 

153 

154 
in Logic.list_implies (prems, concl) end; 

155 

156 
(******************************* case distinction *****************************) 

157 

158 
fun make_casedists descr sorts = 

159 
let 

15570  160 
val descr' = List.concat descr; 
5177  161 

162 
fun make_casedist_prem T (cname, cargs) = 

163 
let 

164 
val Ts = map (typ_of_dtyp descr' sorts) cargs; 

20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19233
diff
changeset

165 
val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts; 
5177  166 
val free_ts = map Free frees 
167 
in list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop 

168 
(HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts > T), free_ts))), 

169 
HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)))) 

170 
end; 

171 

172 
fun make_casedist ((_, (_, _, constrs)), T) = 

173 
let val prems = map (make_casedist_prem T) constrs 

174 
in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))) 

175 
end 

176 

177 
in map make_casedist 

15570  178 
((hd descr) ~~ Library.take (length (hd descr), get_rec_types descr' sorts)) 
5177  179 
end; 
180 

181 
(*************** characteristic equations for primrec combinator **************) 

182 

15459
16dd63c78049
Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
berghofe
parents:
14981
diff
changeset

183 
fun make_primrec_Ts descr sorts used = 
5177  184 
let 
15570  185 
val descr' = List.concat descr; 
5177  186 

20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19233
diff
changeset

187 
val rec_result_Ts = map TFree (Name.variant_list used (replicate (length descr') "'t") ~~ 
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11957
diff
changeset

188 
replicate (length descr') HOLogic.typeS); 
5177  189 

15570  190 
val reccomb_fn_Ts = List.concat (map (fn (i, (_, _, constrs)) => 
5177  191 
map (fn (_, cargs) => 
192 
let 

7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6394
diff
changeset

193 
val Ts = map (typ_of_dtyp descr' sorts) cargs; 
15570  194 
val recs = List.filter (is_rec_type o fst) (cargs ~~ Ts); 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6394
diff
changeset

195 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

196 
fun mk_argT (dt, T) = 
15570  197 
binder_types T > List.nth (rec_result_Ts, body_index dt); 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6394
diff
changeset

198 

85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6394
diff
changeset

199 
val argTs = Ts @ map mk_argT recs 
15570  200 
in argTs > List.nth (rec_result_Ts, i) 
5177  201 
end) constrs) descr'); 
202 

15459
16dd63c78049
Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
berghofe
parents:
14981
diff
changeset

203 
in (rec_result_Ts, reccomb_fn_Ts) end; 
16dd63c78049
Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
berghofe
parents:
14981
diff
changeset

204 

16dd63c78049
Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
berghofe
parents:
14981
diff
changeset

205 
fun make_primrecs new_type_names descr sorts thy = 
16dd63c78049
Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
berghofe
parents:
14981
diff
changeset

206 
let 
15570  207 
val descr' = List.concat descr; 
15459
16dd63c78049
Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
berghofe
parents:
14981
diff
changeset

208 
val recTs = get_rec_types descr' sorts; 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

209 
val used = foldr add_typ_tfree_names [] recTs; 
15459
16dd63c78049
Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
berghofe
parents:
14981
diff
changeset

210 

16dd63c78049
Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
berghofe
parents:
14981
diff
changeset

211 
val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used; 
16dd63c78049
Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
berghofe
parents:
14981
diff
changeset

212 

5177  213 
val rec_fns = map (uncurry (mk_Free "f")) 
214 
(reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts))); 

215 

216 
val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec"; 

22578  217 
val reccomb_names = map (Sign.intern_const thy) 
5177  218 
(if length descr' = 1 then [big_reccomb_name] else 
219 
(map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int) 

220 
(1 upto (length descr')))); 

221 
val reccombs = map (fn ((name, T), T') => list_comb 

222 
(Const (name, reccomb_fn_Ts @ [T] > T'), rec_fns)) 

223 
(reccomb_names ~~ recTs ~~ rec_result_Ts); 

224 

225 
fun make_primrec T comb_t ((ts, f::fs), (cname, cargs)) = 

226 
let 

15570  227 
val recs = List.filter is_rec_type cargs; 
5177  228 
val Ts = map (typ_of_dtyp descr' sorts) cargs; 
229 
val recTs' = map (typ_of_dtyp descr' sorts) recs; 

230 
val tnames = make_tnames Ts; 

15570  231 
val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs)); 
5177  232 
val frees = map Free (tnames ~~ Ts); 
233 
val frees' = map Free (rec_tnames ~~ recTs'); 

7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6394
diff
changeset

234 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

235 
fun mk_reccomb ((dt, T), t) = 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

236 
let val (Us, U) = strip_type T 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

237 
in list_abs (map (pair "x") Us, 
15570  238 
List.nth (reccombs, body_index dt) $ app_bnds t (length Us)) 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

239 
end; 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6394
diff
changeset

240 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

241 
val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees') 
5177  242 

243 
in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq 

244 
(comb_t $ list_comb (Const (cname, Ts > T), frees), 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

245 
list_comb (f, frees @ reccombs')))], fs) 
5177  246 
end 
247 

15570  248 
in fst (Library.foldl (fn (x, ((dt, T), comb_t)) => 
249 
Library.foldl (make_primrec T comb_t) (x, #3 (snd dt))) 

5177  250 
(([], rec_fns), descr' ~~ recTs ~~ reccombs)) 
251 
end; 

252 

253 
(****************** make terms of form t_case f1 ... fn *********************) 

254 

255 
fun make_case_combs new_type_names descr sorts thy fname = 

256 
let 

15570  257 
val descr' = List.concat descr; 
5177  258 
val recTs = get_rec_types descr' sorts; 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

259 
val used = foldr add_typ_tfree_names [] recTs; 
15570  260 
val newTs = Library.take (length (hd descr), recTs); 
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19233
diff
changeset

261 
val T' = TFree (Name.variant used "'t", HOLogic.typeS); 
5177  262 

263 
val case_fn_Ts = map (fn (i, (_, _, constrs)) => 

264 
map (fn (_, cargs) => 

265 
let val Ts = map (typ_of_dtyp descr' sorts) cargs 

266 
in Ts > T' end) constrs) (hd descr); 

267 

268 
val case_names = map (fn s => 

22578  269 
Sign.intern_const thy (s ^ "_case")) new_type_names 
5177  270 
in 
271 
map (fn ((name, Ts), T) => list_comb 

272 
(Const (name, Ts @ [T] > T'), 

273 
map (uncurry (mk_Free fname)) (Ts ~~ (1 upto length Ts)))) 

274 
(case_names ~~ case_fn_Ts ~~ newTs) 

275 
end; 

276 

277 
(**************** characteristic equations for case combinator ****************) 

278 

279 
fun make_cases new_type_names descr sorts thy = 

280 
let 

15570  281 
val descr' = List.concat descr; 
5177  282 
val recTs = get_rec_types descr' sorts; 
15570  283 
val newTs = Library.take (length (hd descr), recTs); 
5177  284 

285 
fun make_case T comb_t ((cname, cargs), f) = 

286 
let 

287 
val Ts = map (typ_of_dtyp descr' sorts) cargs; 

288 
val frees = map Free ((make_tnames Ts) ~~ Ts) 

289 
in HOLogic.mk_Trueprop (HOLogic.mk_eq 

290 
(comb_t $ list_comb (Const (cname, Ts > T), frees), 

291 
list_comb (f, frees))) 

292 
end 

293 

294 
in map (fn (((_, (_, _, constrs)), T), comb_t) => 

295 
map (make_case T comb_t) (constrs ~~ (snd (strip_comb comb_t)))) 

296 
((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f")) 

297 
end; 

298 

7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6394
diff
changeset

299 

5177  300 
(*************************** the "split"  equations **************************) 
301 

302 
fun make_splits new_type_names descr sorts thy = 

303 
let 

15570  304 
val descr' = List.concat descr; 
5177  305 
val recTs = get_rec_types descr' sorts; 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

306 
val used' = foldr add_typ_tfree_names [] recTs; 
15570  307 
val newTs = Library.take (length (hd descr), recTs); 
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19233
diff
changeset

308 
val T' = TFree (Name.variant used' "'t", HOLogic.typeS); 
5177  309 
val P = Free ("P", T' > HOLogic.boolT); 
310 

311 
fun make_split (((_, (_, _, constrs)), T), comb_t) = 

312 
let 

313 
val (_, fs) = strip_comb comb_t; 

314 
val used = ["P", "x"] @ (map (fst o dest_Free) fs); 

315 

316 
fun process_constr (((cname, cargs), f), (t1s, t2s)) = 

317 
let 

318 
val Ts = map (typ_of_dtyp descr' sorts) cargs; 

20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19233
diff
changeset

319 
val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts); 
5177  320 
val eqn = HOLogic.mk_eq (Free ("x", T), 
321 
list_comb (Const (cname, Ts > T), frees)); 

322 
val P' = P $ list_comb (f, frees) 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

323 
in ((foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t)) 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

324 
(HOLogic.imp $ eqn $ P') frees)::t1s, 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

325 
(foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t)) 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

326 
(HOLogic.conj $ eqn $ (HOLogic.Not $ P')) frees)::t2s) 
5177  327 
end; 
328 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

329 
val (t1s, t2s) = foldr process_constr ([], []) (constrs ~~ fs); 
5177  330 
val lhs = P $ (comb_t $ Free ("x", T)) 
331 
in 

332 
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)), 

8434  333 
HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ mk_disj t2s))) 
5177  334 
end 
335 

336 
in map make_split ((hd descr) ~~ newTs ~~ 

337 
(make_case_combs new_type_names descr sorts thy "f")) 

338 
end; 

339 

340 
(************************* additional rules for TFL ***************************) 

341 

8601  342 
fun make_weak_case_congs new_type_names descr sorts thy = 
343 
let 

344 
val case_combs = make_case_combs new_type_names descr sorts thy "f"; 

345 

346 
fun mk_case_cong comb = 

347 
let 

348 
val Type ("fun", [T, _]) = fastype_of comb; 

349 
val M = Free ("M", T); 

350 
val M' = Free ("M'", T); 

351 
in 

352 
Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')), 

353 
HOLogic.mk_Trueprop (HOLogic.mk_eq (comb $ M, comb $ M'))) 

354 
end 

355 
in 

356 
map mk_case_cong case_combs 

357 
end; 

358 

359 

5177  360 
(* 
361 
* Structure of case congruence theorem looks like this: 

362 
* 

363 
* (M = M') 

364 
* ==> (!!x1,...,xk. (M' = C1 x1..xk) ==> (f1 x1..xk = g1 x1..xk)) 

365 
* ==> ... 

366 
* ==> (!!x1,...,xj. (M' = Cn x1..xj) ==> (fn x1..xj = gn x1..xj)) 

367 
* ==> 

368 
* (ty_case f1..fn M = ty_case g1..gn M') 

369 
**) 

370 

371 
fun make_case_congs new_type_names descr sorts thy = 

372 
let 

373 
val case_combs = make_case_combs new_type_names descr sorts thy "f"; 

374 
val case_combs' = make_case_combs new_type_names descr sorts thy "g"; 

375 

376 
fun mk_case_cong ((comb, comb'), (_, (_, _, constrs))) = 

377 
let 

378 
val Type ("fun", [T, _]) = fastype_of comb; 

379 
val (_, fs) = strip_comb comb; 

380 
val (_, gs) = strip_comb comb'; 

381 
val used = ["M", "M'"] @ map (fst o dest_Free) (fs @ gs); 

382 
val M = Free ("M", T); 

383 
val M' = Free ("M'", T); 

384 

385 
fun mk_clause ((f, g), (cname, _)) = 

386 
let 

387 
val (Ts, _) = strip_type (fastype_of f); 

20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19233
diff
changeset

388 
val tnames = Name.variant_list used (make_tnames Ts); 
5177  389 
val frees = map Free (tnames ~~ Ts) 
390 
in 

391 
list_all_free (tnames ~~ Ts, Logic.mk_implies 

392 
(HOLogic.mk_Trueprop 

393 
(HOLogic.mk_eq (M', list_comb (Const (cname, Ts > T), frees))), 

394 
HOLogic.mk_Trueprop 

395 
(HOLogic.mk_eq (list_comb (f, frees), list_comb (g, frees))))) 

396 
end 

397 

398 
in 

399 
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')) :: 

400 
map mk_clause (fs ~~ gs ~~ constrs), 

401 
HOLogic.mk_Trueprop (HOLogic.mk_eq (comb $ M, comb' $ M'))) 

402 
end 

403 

404 
in 

405 
map mk_case_cong (case_combs ~~ case_combs' ~~ hd descr) 

406 
end; 

407 

408 
(* 

409 
* Structure of exhaustion theorem looks like this: 

410 
* 

411 
* !v. (? y1..yi. v = C1 y1..yi)  ...  (? y1..yj. v = Cn y1..yj) 

412 
**) 

413 

414 
fun make_nchotomys descr sorts = 

415 
let 

15570  416 
val descr' = List.concat descr; 
5177  417 
val recTs = get_rec_types descr' sorts; 
15570  418 
val newTs = Library.take (length (hd descr), recTs); 
5177  419 

420 
fun mk_eqn T (cname, cargs) = 

421 
let 

422 
val Ts = map (typ_of_dtyp descr' sorts) cargs; 

20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19233
diff
changeset

423 
val tnames = Name.variant_list ["v"] (make_tnames Ts); 
5177  424 
val frees = tnames ~~ Ts 
425 
in 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

426 
foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t)) 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

427 
(HOLogic.mk_eq (Free ("v", T), 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

428 
list_comb (Const (cname, Ts > T), map Free frees))) frees 
5177  429 
end 
430 

431 
in map (fn ((_, (_, _, constrs)), T) => 

432 
HOLogic.mk_Trueprop (HOLogic.mk_all ("v", T, mk_disj (map (mk_eqn T) constrs)))) 

433 
(hd descr ~~ newTs) 

434 
end; 

435 

436 
end; 