author  berghofe 
Wed, 10 Jul 2002 18:35:34 +0200  
changeset 13340  9b0332344ae2 
parent 12922  ed70a600f0ea 
child 13585  db4005b40cc6 
permissions  rwrr 
5177  1 
(* Title: HOL/Tools/datatype_rep_proofs.ML 
2 
ID: $Id$ 

11539  3 
Author: Stefan Berghofer, TU Muenchen 
4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 

5177  5 

6 
Definitional introduction of datatypes 

7 
Proof of characteristic theorems: 

8 

9 
 injectivity of constructors 

7228  10 
 distinctness of constructors 
5177  11 
 induction theorem 
12 

13 
*) 

14 

15 
signature DATATYPE_REP_PROOFS = 

16 
sig 

5661  17 
val representation_proofs : bool > DatatypeAux.datatype_info Symtab.table > 
5177  18 
string list > (int * (string * DatatypeAux.dtyp list * 
19 
(string * DatatypeAux.dtyp list) list)) list list > (string * sort) list > 

8436  20 
(string * mixfix) list > (string * mixfix) list list > theory attribute 
21 
> theory > theory * thm list list * thm list list * thm list list * 

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

22 
DatatypeAux.simproc_dist list * thm 
5177  23 
end; 
24 

25 
structure DatatypeRepProofs : DATATYPE_REP_PROOFS = 

26 
struct 

27 

28 
open DatatypeAux; 

29 

30 
val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma); 

31 

11435  32 

33 
(** theory context references **) 

5177  34 

11435  35 
val f_myinv_f = thm "f_myinv_f"; 
36 
val myinv_f_f = thm "myinv_f_f"; 

37 

5177  38 

39 
fun exh_thm_of (dt_info : datatype_info Symtab.table) tname = 

40 
#exhaustion (the (Symtab.lookup (dt_info, tname))); 

41 

42 
(******************************************************************************) 

43 

5661  44 
fun representation_proofs flat_names (dt_info : datatype_info Symtab.table) 
8436  45 
new_type_names descr sorts types_syntax constr_syntax case_names_induct thy = 
5177  46 
let 
12922  47 
val Datatype_thy = 
48 
if PureThy.get_name thy = "Datatype" then thy 

49 
else theory "Datatype"; 

11957  50 
val node_name = "Datatype_Universe.node"; 
51 
val In0_name = "Datatype_Universe.In0"; 

52 
val In1_name = "Datatype_Universe.In1"; 

53 
val Scons_name = "Datatype_Universe.Scons"; 

54 
val Leaf_name = "Datatype_Universe.Leaf"; 

55 
val Numb_name = "Datatype_Universe.Numb"; 

56 
val Lim_name = "Datatype_Universe.Lim"; 

57 
val Funs_name = "Datatype_Universe.Funs"; 

58 
val o_name = "Fun.op o"; 

59 
val sum_case_name = "Datatype.sum.sum_case"; 

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

60 

5177  61 
val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq, 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

62 
In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject, 
7293  63 
Funs_inv, FunsD, Funs_rangeE, Funs_nonempty, sum_case_inject] = map (get_thm Datatype_thy) 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

64 
["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq", 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

65 
"In0_not_In1", "In1_not_In0", "Funs_mono", "FunsI", "Lim_inject", 
7293  66 
"Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty", "sum_case_inject"]; 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

67 

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

68 
val Funs_IntE = (Int_lower2 RS Funs_mono RS 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

69 
(Int_lower1 RS Funs_mono RS Int_greatest) RS subsetD) RS IntE; 
5177  70 

71 
val descr' = flat descr; 

72 

5661  73 
val big_name = space_implode "_" new_type_names; 
74 
val thy1 = add_path flat_names big_name thy; 

75 
val big_rec_name = big_name ^ "_rep_set"; 

6394  76 
val rep_set_names = map (Sign.full_name (Theory.sign_of thy1)) 
5177  77 
(if length descr' = 1 then [big_rec_name] else 
78 
(map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int) 

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

80 

5661  81 
val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr); 
82 
val leafTs' = get_nonrec_types descr' sorts; 

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

83 
val branchTs = get_branching_types descr' sorts; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

84 
val branchT = if null branchTs then HOLogic.unitT 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

85 
else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

86 
val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs' @ branchTs, []); 
5661  87 
val leafTs = leafTs' @ (map (fn n => TFree (n, the (assoc (sorts, n)))) unneeded_vars); 
5177  88 
val recTs = get_rec_types descr' sorts; 
89 
val newTs = take (length (hd descr), recTs); 

90 
val oldTs = drop (length (hd descr), recTs); 

91 
val sumT = if null leafTs then HOLogic.unitT 

92 
else fold_bal (fn (T, U) => Type ("+", [T, U])) leafTs; 

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

93 
val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT])); 
5177  94 
val UnivT = HOLogic.mk_setT Univ_elT; 
95 

96 
val In0 = Const (In0_name, Univ_elT > Univ_elT); 

97 
val In1 = Const (In1_name, Univ_elT > Univ_elT); 

98 
val Leaf = Const (Leaf_name, sumT > Univ_elT); 

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

99 
val Lim = Const (Lim_name, (branchT > Univ_elT) > Univ_elT); 
5177  100 

101 
(* make injections needed for embedding types in leaves *) 

102 

103 
fun mk_inj T' x = 

104 
let 

105 
fun mk_inj' T n i = 

106 
if n = 1 then x else 

107 
let val n2 = n div 2; 

108 
val Type (_, [T1, T2]) = T 

109 
in 

110 
if i <= n2 then 

111 
Const ("Inl", T1 > T) $ (mk_inj' T1 n2 i) 

112 
else 

113 
Const ("Inr", T2 > T) $ (mk_inj' T2 (n  n2) (i  n2)) 

114 
end 

115 
in mk_inj' sumT (length leafTs) (1 + find_index_eq T' leafTs) 

116 
end; 

117 

118 
(* make injections for constructors *) 

119 

7704  120 
fun mk_univ_inj ts = access_bal (fn t => In0 $ t, fn t => In1 $ t, if ts = [] then 
5177  121 
Const ("arbitrary", Univ_elT) 
122 
else 

123 
foldr1 (HOLogic.mk_binop Scons_name) ts); 

124 

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

125 
(* function spaces *) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

126 

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

127 
fun mk_fun_inj T' x = 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

128 
let 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

129 
fun mk_inj T n i = 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

130 
if n = 1 then x else 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

131 
let 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

132 
val n2 = n div 2; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

133 
val Type (_, [T1, T2]) = T; 
7293  134 
val sum_case = Const (sum_case_name, [T1 > Univ_elT, T2 > Univ_elT, T] > Univ_elT) 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

135 
in 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

136 
if i <= n2 then 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

137 
sum_case $ (mk_inj T1 n2 i) $ Const ("arbitrary", T2 > Univ_elT) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

138 
else 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

139 
sum_case $ Const ("arbitrary", T1 > Univ_elT) $ mk_inj T2 (n  n2) (i  n2) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

140 
end 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

141 
in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

142 
end; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

143 

5177  144 
(************** generate introduction rules for representing set **********) 
145 

6427  146 
val _ = message "Constructing representing sets ..."; 
5177  147 

148 
(* make introduction rule for a single constructor *) 

149 

150 
fun make_intr s n (i, (_, cargs)) = 

151 
let 

152 
fun mk_prem (DtRec k, (j, prems, ts)) = 

153 
let val free_t = mk_Free "x" Univ_elT j 

154 
in (j + 1, (HOLogic.mk_mem (free_t, 

155 
Const (nth_elem (k, rep_set_names), UnivT)))::prems, free_t::ts) 

156 
end 

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

157 
 mk_prem (DtType ("fun", [T, DtRec k]), (j, prems, ts)) = 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

158 
let val T' = typ_of_dtyp descr' sorts T; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

159 
val free_t = mk_Free "x" (T' > Univ_elT) j 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

160 
in (j + 1, (HOLogic.mk_mem (free_t, 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

161 
Const (Funs_name, UnivT > HOLogic.mk_setT (T' > Univ_elT)) $ 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

162 
Const (nth_elem (k, rep_set_names), UnivT)))::prems, 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

163 
Lim $ mk_fun_inj T' free_t::ts) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

164 
end 
5177  165 
 mk_prem (dt, (j, prems, ts)) = 
166 
let val T = typ_of_dtyp descr' sorts dt 

167 
in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts) 

168 
end; 

169 

170 
val (_, prems, ts) = foldr mk_prem (cargs, (1, [], [])); 

171 
val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem 

172 
(mk_univ_inj ts n i, Const (s, UnivT))) 

173 
in Logic.list_implies (map HOLogic.mk_Trueprop prems, concl) 

174 
end; 

175 

176 
val consts = map (fn s => Const (s, UnivT)) rep_set_names; 

177 

178 
val intr_ts = flat (map (fn ((_, (_, _, constrs)), rep_set_name) => 

179 
map (make_intr rep_set_name (length constrs)) 

180 
((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names)); 

181 

182 
val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) = 

5661  183 
setmp InductivePackage.quiet_mode (!quiet_mode) 
184 
(InductivePackage.add_inductive_i false true big_rec_name false true false 

12180  185 
consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono]) thy1; 
5177  186 

187 
(********************************* typedef ********************************) 

188 

5661  189 
val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) => 
5696  190 
setmp TypedefPackage.quiet_mode true 
11827  191 
(TypedefPackage.add_typedef_i false (Some name') (name, tvs, mx) c None 
192 
(rtac exI 1 THEN 

193 
QUIET_BREADTH_FIRST (has_fewer_prems 1) 

11822  194 
(resolve_tac (Funs_nonempty::rep_intrs) 1))) thy > #1) 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

195 
(parent_path flat_names thy2, types_syntax ~~ tyvars ~~ 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

196 
(take (length newTs, consts)) ~~ new_type_names)); 
5177  197 

198 
(*********************** definition of constructors ***********************) 

199 

200 
val big_rep_name = (space_implode "_" new_type_names) ^ "_Rep_"; 

201 
val rep_names = map (curry op ^ "Rep_") new_type_names; 

202 
val rep_names' = map (fn i => big_rep_name ^ (string_of_int i)) 

203 
(1 upto (length (flat (tl descr)))); 

6394  204 
val all_rep_names = map (Sign.intern_const (Theory.sign_of thy3)) rep_names @ 
205 
map (Sign.full_name (Theory.sign_of thy3)) rep_names'; 

5177  206 

207 
(* isomorphism declarations *) 

208 

209 
val iso_decls = map (fn (T, s) => (s, T > Univ_elT, NoSyn)) 

210 
(oldTs ~~ rep_names'); 

211 

212 
(* constructor definitions *) 

213 

214 
fun make_constr_def tname T n ((thy, defs, eqns, i), ((cname, cargs), (cname', mx))) = 

215 
let 

216 
fun constr_arg (dt, (j, l_args, r_args)) = 

217 
let val T = typ_of_dtyp descr' sorts dt; 

218 
val free_t = mk_Free "x" T j 

219 
in (case dt of 

220 
DtRec m => (j + 1, free_t::l_args, (Const (nth_elem (m, all_rep_names), 

221 
T > Univ_elT) $ free_t)::r_args) 

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

222 
 DtType ("fun", [T', DtRec m]) => 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

223 
let val ([T''], T''') = strip_type T 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

224 
in (j + 1, free_t::l_args, (Lim $ mk_fun_inj T'' 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

225 
(Const (o_name, [T''' > Univ_elT, T, T''] > Univ_elT) $ 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

226 
Const (nth_elem (m, all_rep_names), T''' > Univ_elT) $ free_t))::r_args) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

227 
end 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

228 

5177  229 
 _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args)) 
230 
end; 

231 

232 
val (_, l_args, r_args) = foldr constr_arg (cargs, (1, [], [])); 

233 
val constrT = (map (typ_of_dtyp descr' sorts) cargs) > T; 

6394  234 
val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname); 
235 
val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname); 

5177  236 
val lhs = list_comb (Const (cname, constrT), l_args); 
237 
val rhs = mk_univ_inj r_args n i; 

238 
val def = equals T $ lhs $ (Const (abs_name, Univ_elT > T) $ rhs); 

239 
val def_name = (Sign.base_name cname) ^ "_def"; 

240 
val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq 

241 
(Const (rep_name, T > Univ_elT) $ lhs, rhs)); 

8436  242 
val (thy', [def_thm]) = thy > 
5177  243 
Theory.add_consts_i [(cname', constrT, mx)] > 
9315  244 
(PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]; 
5177  245 

8436  246 
in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end; 
5177  247 

248 
(* constructor definitions for datatype *) 

249 

250 
fun dt_constr_defs ((thy, defs, eqns, rep_congs, dist_lemmas), 

251 
((((_, (_, _, constrs)), tname), T), constr_syntax)) = 

252 
let 

253 
val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong; 

6394  254 
val sg = Theory.sign_of thy; 
5177  255 
val rep_const = cterm_of sg 
256 
(Const (Sign.intern_const sg ("Rep_" ^ tname), T > Univ_elT)); 

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

257 
val cong' = standard (cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong); 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

258 
val dist = standard (cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma); 
5177  259 
val (thy', defs', eqns', _) = foldl ((make_constr_def tname T) (length constrs)) 
5661  260 
((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax) 
5177  261 
in 
5661  262 
(parent_path flat_names thy', defs', eqns @ [eqns'], 
5177  263 
rep_congs @ [cong'], dist_lemmas @ [dist]) 
264 
end; 

265 

266 
val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = foldl dt_constr_defs 

5661  267 
((thy3 > Theory.add_consts_i iso_decls > parent_path flat_names, [], [], [], []), 
5177  268 
hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax); 
269 

270 
(*********** isomorphisms for new types (introduced by typedef) ***********) 

271 

6427  272 
val _ = message "Proving isomorphism properties ..."; 
5177  273 

274 
(* get axioms from theory *) 

275 

276 
val newT_iso_axms = map (fn s => 

7904  277 
(get_thm thy4 ("Abs_" ^ s ^ "_inverse"), 
278 
get_thm thy4 ("Rep_" ^ s ^ "_inverse"), 

279 
get_thm thy4 ("Rep_" ^ s))) new_type_names; 

5177  280 

281 
(**) 

282 
(* prove additional theorems: *) 

283 
(* inj_on dt_Abs_i rep_set_i and inj dt_Rep_i *) 

284 
(**) 

285 

286 
fun prove_newT_iso_inj_thm (((s, (thm1, thm2, _)), T), rep_set_name) = 

287 
let 

6394  288 
val sg = Theory.sign_of thy4; 
5177  289 
val RepT = T > Univ_elT; 
290 
val Rep_name = Sign.intern_const sg ("Rep_" ^ s); 

291 
val AbsT = Univ_elT > T; 

292 
val Abs_name = Sign.intern_const sg ("Abs_" ^ s); 

293 

6171  294 
val inj_Abs_thm = 
295 
prove_goalw_cterm [] 

296 
(cterm_of sg 

297 
(HOLogic.mk_Trueprop 

11435  298 
(Const ("Fun.inj_on", [AbsT, UnivT] > HOLogic.boolT) $ 
6171  299 
Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT)))) 
5177  300 
(fn _ => [rtac inj_on_inverseI 1, etac thm1 1]); 
301 

6171  302 
val setT = HOLogic.mk_setT T 
303 

304 
val inj_Rep_thm = 

305 
prove_goalw_cterm [] 

306 
(cterm_of sg 

307 
(HOLogic.mk_Trueprop 

11435  308 
(Const ("Fun.inj_on", [RepT, setT] > HOLogic.boolT) $ 
309 
Const (Rep_name, RepT) $ Const ("UNIV", setT)))) 

5177  310 
(fn _ => [rtac inj_inverseI 1, rtac thm2 1]) 
311 

6171  312 
in (inj_Abs_thm, inj_Rep_thm) end; 
5177  313 

314 
val newT_iso_inj_thms = map prove_newT_iso_inj_thm 

315 
(new_type_names ~~ newT_iso_axms ~~ newTs ~~ 

316 
take (length newTs, rep_set_names)); 

317 

318 
(********* isomorphisms between existing types and "unfolded" types *******) 

319 

320 
(**) 

321 
(* isomorphisms are defined using primreccombinators: *) 

322 
(* generate appropriate functions for instantiating primreccombinator *) 

323 
(* *) 

324 
(* e.g. dt_Rep_i = list_rec ... (%h t y. In1 ((Leaf h) $ y)) *) 

325 
(* *) 

326 
(* also generate characteristic equations for isomorphisms *) 

327 
(* *) 

328 
(* e.g. dt_Rep_i (cons h t) = In1 ((dt_Rep_j h) $ (dt_Rep_i t)) *) 

329 
(**) 

330 

331 
fun make_iso_def k ks n ((fs, eqns, i), (cname, cargs)) = 

332 
let 

333 
val argTs = map (typ_of_dtyp descr' sorts) cargs; 

334 
val T = nth_elem (k, recTs); 

335 
val rep_name = nth_elem (k, all_rep_names); 

336 
val rep_const = Const (rep_name, T > Univ_elT); 

337 
val constr = Const (cname, argTs > T); 

338 

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

339 
fun process_arg ks' ((i2, i2', ts, Ts), dt) = 
5177  340 
let val T' = typ_of_dtyp descr' sorts dt 
341 
in (case dt of 

342 
DtRec j => if j mem ks' then 

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

343 
(i2 + 1, i2' + 1, ts @ [mk_Free "y" Univ_elT i2'], Ts @ [Univ_elT]) 
5177  344 
else 
345 
(i2 + 1, i2', ts @ [Const (nth_elem (j, all_rep_names), 

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

346 
T' > Univ_elT) $ mk_Free "x" T' i2], Ts) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

347 
 (DtType ("fun", [_, DtRec j])) => 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

348 
let val ([T''], T''') = strip_type T' 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

349 
in if j mem ks' then 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

350 
(i2 + 1, i2' + 1, ts @ [Lim $ mk_fun_inj T'' 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

351 
(mk_Free "y" (T'' > Univ_elT) i2')], Ts @ [T'' > Univ_elT]) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

352 
else 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

353 
(i2 + 1, i2', ts @ [Lim $ mk_fun_inj T'' 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

354 
(Const (o_name, [T''' > Univ_elT, T', T''] > Univ_elT) $ 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

355 
Const (nth_elem (j, all_rep_names), T''' > Univ_elT) $ 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

356 
mk_Free "x" T' i2)], Ts) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

357 
end 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

358 
 _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts)) 
5177  359 
end; 
360 

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

361 
val (i2, i2', ts, Ts) = foldl (process_arg ks) ((1, 1, [], []), cargs); 
5177  362 
val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2  1))); 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

363 
val ys = map (uncurry (mk_Free "y")) (Ts ~~ (1 upto (i2'  1))); 
5177  364 
val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i); 
365 

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

366 
val (_, _, ts', _) = foldl (process_arg []) ((1, 1, [], []), cargs); 
5177  367 
val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq 
368 
(rep_const $ list_comb (constr, xs), mk_univ_inj ts' n i)) 

369 

370 
in (fs @ [f], eqns @ [eqn], i + 1) end; 

371 

372 
(* define isomorphisms for all mutually recursive datatypes in list ds *) 

373 

374 
fun make_iso_defs (ds, (thy, char_thms)) = 

375 
let 

376 
val ks = map fst ds; 

377 
val (_, (tname, _, _)) = hd ds; 

378 
val {rec_rewrites, rec_names, ...} = the (Symtab.lookup (dt_info, tname)); 

379 

380 
fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) = 

381 
let 

382 
val (fs', eqns', _) = foldl (make_iso_def k ks (length constrs)) 

383 
((fs, eqns, 1), constrs); 

384 
val iso = (nth_elem (k, recTs), nth_elem (k, all_rep_names)) 

385 
in (fs', eqns', isos @ [iso]) end; 

386 

387 
val (fs, eqns, isos) = foldl process_dt (([], [], []), ds); 

388 
val fTs = map fastype_of fs; 

389 
val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def", 

390 
equals (T > Univ_elT) $ Const (iso_name, T > Univ_elT) $ 

391 
list_comb (Const (rec_name, fTs @ [T] > Univ_elT), fs))) (rec_names ~~ isos); 

9315  392 
val (thy', def_thms) = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy; 
5177  393 

394 
(* prove characteristic equations *) 

395 

5553  396 
val rewrites = def_thms @ (map mk_meta_eq rec_rewrites); 
5177  397 
val char_thms' = map (fn eqn => prove_goalw_cterm rewrites 
6394  398 
(cterm_of (Theory.sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns; 
5177  399 

400 
in (thy', char_thms' @ char_thms) end; 

401 

5661  402 
val (thy5, iso_char_thms) = foldr make_iso_defs 
403 
(tl descr, (add_path flat_names big_name thy4, [])); 

5177  404 

405 
(* prove isomorphism properties *) 

406 

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

407 
fun mk_funs_inv thm = 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

408 
let 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

409 
val [_, t] = prems_of Funs_inv; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

410 
val [_ $ (_ $ _ $ R)] = Logic.strip_assums_hyp t; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

411 
val _ $ (_ $ (r $ (a $ _)) $ _) = Logic.strip_assums_concl t; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

412 
val [_ $ (_ $ _ $ R')] = prems_of thm; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

413 
val _ $ (_ $ (r' $ (a' $ _)) $ _) = concl_of thm; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

414 
val inv' = cterm_instantiate (map 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

415 
((pairself (cterm_of (sign_of_thm thm))) o 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

416 
(apsnd (map_term_types (incr_tvar 1)))) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

417 
[(R, R'), (r, r'), (a, a')]) Funs_inv 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

418 
in 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

419 
rule_by_tactic (atac 2) (thm RSN (2, inv')) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

420 
end; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

421 

5177  422 
(* prove inj dt_Rep_i and dt_Rep_i x : dt_rep_set_i *) 
423 

424 
fun prove_iso_thms (ds, (inj_thms, elem_thms)) = 

425 
let 

426 
val (_, (tname, _, _)) = hd ds; 

427 
val {induction, ...} = the (Symtab.lookup (dt_info, tname)); 

428 

429 
fun mk_ind_concl (i, _) = 

430 
let 

431 
val T = nth_elem (i, recTs); 

432 
val Rep_t = Const (nth_elem (i, all_rep_names), T > Univ_elT); 

433 
val rep_set_name = nth_elem (i, rep_set_names) 

434 
in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $ 

435 
HOLogic.mk_eq (Rep_t $ mk_Free "x" T i, Rep_t $ Bound 0) $ 

436 
HOLogic.mk_eq (mk_Free "x" T i, Bound 0)), 

437 
HOLogic.mk_mem (Rep_t $ mk_Free "x" T i, Const (rep_set_name, UnivT))) 

438 
end; 

439 

440 
val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds); 

441 

5553  442 
val rewrites = map mk_meta_eq iso_char_thms; 
11471
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

443 
val inj_thms' = flat (map (fn r => [r RS injD, r RS inj_o]) 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

444 
(map snd newT_iso_inj_thms @ inj_thms)); 
5177  445 

6394  446 
val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) 
5177  447 
(HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ => 
11951
381135c295ef
Fixed several bugs concerning arbitrarily branching datatypes.
berghofe
parents:
11827
diff
changeset

448 
[(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1, 
5177  449 
REPEAT (EVERY 
450 
[rtac allI 1, rtac impI 1, 

451 
exh_tac (exh_thm_of dt_info) 1, 

452 
REPEAT (EVERY 

453 
[hyp_subst_tac 1, 

454 
rewrite_goals_tac rewrites, 

455 
REPEAT (dresolve_tac [In0_inject, In1_inject] 1), 

456 
(eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1) 

457 
ORELSE (EVERY 

11951
381135c295ef
Fixed several bugs concerning arbitrarily branching datatypes.
berghofe
parents:
11827
diff
changeset

458 
[REPEAT (eresolve_tac (Scons_inject :: sum_case_inject :: 
381135c295ef
Fixed several bugs concerning arbitrarily branching datatypes.
berghofe
parents:
11827
diff
changeset

459 
map make_elim (inj_thms' @ 
381135c295ef
Fixed several bugs concerning arbitrarily branching datatypes.
berghofe
parents:
11827
diff
changeset

460 
[Leaf_inject, Lim_inject, Inl_inject, Inr_inject])) 1), 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

461 
REPEAT ((EVERY [etac allE 1, dtac mp 1, atac 1]) ORELSE 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

462 
(dtac inj_fun_lemma 1 THEN atac 1)), 
11951
381135c295ef
Fixed several bugs concerning arbitrarily branching datatypes.
berghofe
parents:
11827
diff
changeset

463 
REPEAT (hyp_subst_tac 1), 
5177  464 
rtac refl 1])])])]); 
465 

6171  466 
val inj_thms'' = map (fn r => r RS datatype_injI) 
467 
(split_conj_thm inj_thm); 

5177  468 

6171  469 
val elem_thm = 
470 
prove_goalw_cterm [] 

6394  471 
(cterm_of (Theory.sign_of thy5) 
6171  472 
(HOLogic.mk_Trueprop (mk_conj ind_concl2))) 
473 
(fn _ => 

11951
381135c295ef
Fixed several bugs concerning arbitrarily branching datatypes.
berghofe
parents:
11827
diff
changeset

474 
[(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1, 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

475 
rewrite_goals_tac (o_def :: rewrites), 
6171  476 
REPEAT (EVERY 
477 
[resolve_tac rep_intrs 1, 

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

478 
REPEAT (FIRST [atac 1, etac spec 1, 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

479 
resolve_tac (FunsI :: elem_thms) 1])])]); 
5177  480 

11471
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

481 
in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm)) 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

482 
end; 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

483 

ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

484 
val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

485 
(tl descr, ([], map #3 newT_iso_axms)); 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

486 
val iso_inj_thms = map snd newT_iso_inj_thms @ iso_inj_thms_unfolded; 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

487 

ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

488 
(* prove x : dt_rep_set_i > x : range dt_Rep_i *) 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

489 

ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

490 
fun mk_iso_t (((set_name, iso_name), i), T) = 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

491 
let val isoT = T > Univ_elT 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

492 
in HOLogic.imp $ 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

493 
HOLogic.mk_mem (mk_Free "x" Univ_elT i, Const (set_name, UnivT)) $ 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

494 
(if i < length newTs then Const ("True", HOLogic.boolT) 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

495 
else HOLogic.mk_mem (mk_Free "x" Univ_elT i, 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

496 
Const ("image", [isoT, HOLogic.mk_setT T] > UnivT) $ 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

497 
Const (iso_name, isoT) $ Const ("UNIV", HOLogic.mk_setT T))) 
5177  498 
end; 
499 

11471
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

500 
val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

501 
(rep_set_names ~~ all_rep_names ~~ (0 upto (length descr'  1)) ~~ recTs))); 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

502 

ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

503 
(* all the theorems are proved by one single simultaneous induction *) 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

504 

ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

505 
val iso_thms = if length descr = 1 then [] else 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

506 
drop (length newTs, split_conj_thm 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

507 
(prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ => 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

508 
[indtac rep_induct 1, 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

509 
REPEAT (rtac TrueI 1), 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

510 
REPEAT (EVERY 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

511 
[rewrite_goals_tac [mk_meta_eq Collect_mem_eq], 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

512 
REPEAT (etac Funs_IntE 1), 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

513 
REPEAT (eresolve_tac (rangeE :: 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

514 
map (fn r => r RS Funs_rangeE) iso_inj_thms_unfolded) 1), 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

515 
REPEAT (eresolve_tac (map (fn (iso, _, _) => iso RS subst) newT_iso_axms @ 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

516 
map (fn (iso, _, _) => mk_funs_inv iso RS subst) newT_iso_axms) 1), 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

517 
TRY (hyp_subst_tac 1), 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

518 
rtac (sym RS range_eqI) 1, 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

519 
resolve_tac iso_char_thms 1])]))); 
11435  520 

521 
val Abs_inverse_thms' = 

522 
map #1 newT_iso_axms @ 

11471
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

523 
map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp]) 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

524 
(iso_inj_thms_unfolded, iso_thms); 
11435  525 

526 
val Abs_inverse_thms = map (fn r => r RS subst) (Abs_inverse_thms' @ 

527 
map mk_funs_inv Abs_inverse_thms'); 

5177  528 

529 
(******************* freeness theorems for constructors *******************) 

530 

6427  531 
val _ = message "Proving freeness of constructors ..."; 
5177  532 

533 
(* prove theorem Rep_i (Constr_j ...) = Inj_j ... *) 

534 

535 
fun prove_constr_rep_thm eqn = 

536 
let 

537 
val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms; 

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

538 
val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms) 
6394  539 
in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) eqn) (fn _ => 
5177  540 
[resolve_tac inj_thms 1, 
541 
rewrite_goals_tac rewrites, 

542 
rtac refl 1, 

543 
resolve_tac rep_intrs 2, 

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

544 
REPEAT (resolve_tac (FunsI :: iso_elem_thms) 1)]) 
5177  545 
end; 
546 

547 
(**) 

548 
(* constr_rep_thms and rep_congs are used to prove distinctness *) 

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

549 
(* of constructors. *) 
5177  550 
(**) 
551 

552 
val constr_rep_thms = map (map prove_constr_rep_thm) constr_rep_eqns; 

553 

554 
val dist_rewrites = map (fn (rep_thms, dist_lemma) => 

555 
dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])) 

556 
(constr_rep_thms ~~ dist_lemmas); 

557 

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

558 
fun prove_distinct_thms (_, []) = [] 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

559 
 prove_distinct_thms (dist_rewrites', t::_::ts) = 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

560 
let 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

561 
val dist_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ => 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

562 
[simp_tac (HOL_ss addsimps dist_rewrites') 1]) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

563 
in dist_thm::(standard (dist_thm RS not_sym)):: 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

564 
(prove_distinct_thms (dist_rewrites', ts)) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

565 
end; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

566 

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

567 
val distinct_thms = map prove_distinct_thms (dist_rewrites ~~ 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

568 
DatatypeProp.make_distincts new_type_names descr sorts thy5); 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

569 

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

570 
val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) => 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

571 
if length constrs < !DatatypeProp.dtK then FewConstrs dists 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

572 
else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~ 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

573 
constr_rep_thms ~~ rep_congs ~~ distinct_thms); 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

574 

5177  575 
(* prove injectivity of constructors *) 
576 

577 
fun prove_constr_inj_thm rep_thms t = 

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

578 
let val inj_thms = Scons_inject::sum_case_inject::(map make_elim 
5177  579 
((map (fn r => r RS injD) iso_inj_thms) @ 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

580 
[In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject, Lim_inject])) 
6394  581 
in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ => 
5177  582 
[rtac iffI 1, 
583 
REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2, 

584 
dresolve_tac rep_congs 1, dtac box_equals 1, 

7499  585 
REPEAT (resolve_tac rep_thms 1), rewtac o_def, 
5177  586 
REPEAT (eresolve_tac inj_thms 1), 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

587 
REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [rtac ext 1, dtac fun_cong 1, 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

588 
eresolve_tac inj_thms 1, atac 1]))]) 
5177  589 
end; 
590 

591 
val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts) 

592 
((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms); 

593 

8479
5d327a46dc61
Now returns theorems with correct names in derivations.
berghofe
parents:
8436
diff
changeset

594 
val (thy6, (constr_inject', distinct_thms'))= thy5 > parent_path flat_names > 
5d327a46dc61
Now returns theorems with correct names in derivations.
berghofe
parents:
8436
diff
changeset

595 
store_thmss "inject" new_type_names constr_inject >>> 
5d327a46dc61
Now returns theorems with correct names in derivations.
berghofe
parents:
8436
diff
changeset

596 
store_thmss "distinct" new_type_names distinct_thms; 
5177  597 

598 
(*************************** induction theorem ****************************) 

599 

6427  600 
val _ = message "Proving induction rule for datatypes ..."; 
5177  601 

602 
val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @ 

11471
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

603 
(map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded); 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

604 
val Rep_inverse_thms' = map (fn r => r RS myinv_f_f) iso_inj_thms_unfolded; 
5177  605 

606 
fun mk_indrule_lemma ((prems, concls), ((i, _), T)) = 

607 
let 

608 
val Rep_t = Const (nth_elem (i, all_rep_names), T > Univ_elT) $ 

609 
mk_Free "x" T i; 

610 

611 
val Abs_t = if i < length newTs then 

6394  612 
Const (Sign.intern_const (Theory.sign_of thy6) 
5177  613 
("Abs_" ^ (nth_elem (i, new_type_names))), Univ_elT > T) 
11435  614 
else Const ("Inductive.myinv", [T > Univ_elT, Univ_elT] > T) $ 
5177  615 
Const (nth_elem (i, all_rep_names), T > Univ_elT) 
616 

617 
in (prems @ [HOLogic.imp $ HOLogic.mk_mem (Rep_t, 

618 
Const (nth_elem (i, rep_set_names), UnivT)) $ 

619 
(mk_Free "P" (T > HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))], 

620 
concls @ [mk_Free "P" (T > HOLogic.boolT) (i + 1) $ mk_Free "x" T i]) 

621 
end; 

622 

623 
val (indrule_lemma_prems, indrule_lemma_concls) = 

624 
foldl mk_indrule_lemma (([], []), (descr' ~~ recTs)); 

625 

6394  626 
val cert = cterm_of (Theory.sign_of thy6); 
5177  627 

628 
val indrule_lemma = prove_goalw_cterm [] (cert 

629 
(Logic.mk_implies 

630 
(HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems), 

631 
HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls)))) (fn prems => 

632 
[cut_facts_tac prems 1, REPEAT (etac conjE 1), 

633 
REPEAT (EVERY 

634 
[TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1, 

635 
etac mp 1, resolve_tac iso_elem_thms 1])]); 

636 

8305  637 
val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma))); 
5177  638 
val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else 
639 
map (Free o apfst fst o dest_Var) Ps; 

640 
val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma; 

641 

13340
9b0332344ae2
Simplified proof of induction rule for datatypes involving function types.
berghofe
parents:
12922
diff
changeset

642 
val dt_induct = prove_goalw_cterm [] (cert 
5177  643 
(DatatypeProp.make_ind descr sorts)) (fn prems => 
644 
[rtac indrule_lemma' 1, indtac rep_induct 1, 

645 
EVERY (map (fn (prem, r) => (EVERY 

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

646 
[REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1), 
5177  647 
simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1, 
7499  648 
DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewtac o_def, 
13340
9b0332344ae2
Simplified proof of induction rule for datatypes involving function types.
berghofe
parents:
12922
diff
changeset

649 
dtac FunsD 1, etac CollectD 1]))])) 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

650 
(prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]); 
5177  651 

8436  652 
val (thy7, [dt_induct']) = thy6 > 
5661  653 
Theory.add_path big_name > 
13340
9b0332344ae2
Simplified proof of induction rule for datatypes involving function types.
berghofe
parents:
12922
diff
changeset

654 
PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] >> 
5661  655 
Theory.parent_path; 
5177  656 

8479
5d327a46dc61
Now returns theorems with correct names in derivations.
berghofe
parents:
8436
diff
changeset

657 
in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct') 
5177  658 
end; 
659 

660 
end; 