224 ordered' |
224 ordered' |
225 end |
225 end |
226 *} |
226 *} |
227 |
227 |
228 ML {* |
228 ML {* |
229 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = |
229 fun define_raw_dts dts bn_funs bn_eqs binds lthy = |
230 let |
230 let |
231 val thy = ProofContext.theory_of lthy |
231 val thy = ProofContext.theory_of lthy |
232 val thy_name = Context.theory_name thy |
232 val thy_name = Context.theory_name thy |
233 |
233 |
234 val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts |
234 val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts |
259 (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) |
259 (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) |
260 end |
260 end |
261 *} |
261 *} |
262 |
262 |
263 ML {* |
263 ML {* |
264 fun raw_bn_decls dt_names dts raw_bn_funs raw_bn_eqs constr_thms lthy = |
264 (* should be in nominal_dt_rawfuns *) |
|
265 fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy = |
265 if null raw_bn_funs |
266 if null raw_bn_funs |
266 then ([], [], [], [], lthy) |
267 then ([], [], [], [], lthy) |
267 else |
268 else |
268 let |
269 let |
269 val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs |
270 val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs |
270 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
271 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
271 |
272 |
272 val (info, lthy2) = prove_termination (Local_Theory.restore lthy1) |
273 val (info, lthy2) = prove_termination size_thms (Local_Theory.restore lthy1) |
273 val {fs, simps, inducts, ...} = info; |
274 val {fs, simps, inducts, ...} = info |
274 |
275 |
275 val raw_bn_induct = (the inducts) |
276 val raw_bn_induct = (the inducts) |
276 val raw_bn_eqs = the simps |
277 val raw_bn_eqs = the simps |
277 |
278 |
278 val raw_bn_info = |
279 val raw_bn_info = |
299 let |
300 let |
300 (* definition of the raw datatypes *) |
301 (* definition of the raw datatypes *) |
301 val _ = warning "Definition of raw datatypes"; |
302 val _ = warning "Definition of raw datatypes"; |
302 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
303 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
303 if get_STEPS lthy > 0 |
304 if get_STEPS lthy > 0 |
304 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
305 then define_raw_dts dts bn_funs bn_eqs bclauses lthy |
305 else raise TEST lthy |
306 else raise TEST lthy |
306 |
307 |
307 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
308 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
308 val {descr, sorts, ...} = dtinfo |
309 val {descr, sorts, ...} = dtinfo |
309 |
310 |
337 |
338 |
338 (* definition of raw fv_functions *) |
339 (* definition of raw fv_functions *) |
339 val _ = warning "Definition of raw fv-functions"; |
340 val _ = warning "Definition of raw fv-functions"; |
340 val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) = |
341 val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) = |
341 if get_STEPS lthy3 > 2 |
342 if get_STEPS lthy3 > 2 |
342 then raw_bn_decls raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs |
343 then define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs |
343 (raw_inject_thms @ raw_distinct_thms) lthy3 |
344 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 |
344 else raise TEST lthy3 |
345 else raise TEST lthy3 |
345 |
346 |
346 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = |
347 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = |
347 if get_STEPS lthy3a > 3 |
348 if get_STEPS lthy3a > 3 |
348 then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses |
349 then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses |
349 (raw_inject_thms @ raw_distinct_thms) lthy3a |
350 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a |
350 else raise TEST lthy3a |
351 else raise TEST lthy3a |
351 |
352 |
352 (* definition of raw alphas *) |
353 (* definition of raw alphas *) |
353 val _ = warning "Definition of alphas"; |
354 val _ = warning "Definition of alphas"; |
354 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
355 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |