310 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
310 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
311 else raise TEST lthy |
311 else raise TEST lthy |
312 |
312 |
313 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
313 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
314 val {descr, sorts, ...} = dtinfo |
314 val {descr, sorts, ...} = dtinfo |
315 val raw_constrs = |
315 |
316 flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts)) |
|
317 val raw_tys = all_dtyps descr sorts |
316 val raw_tys = all_dtyps descr sorts |
318 val raw_full_ty_names = map (fst o dest_Type) raw_tys |
317 val raw_full_ty_names = map (fst o dest_Type) raw_tys |
319 |
318 |
320 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names |
319 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names |
321 |
320 |
|
321 val raw_cns_info = all_dtyp_constrs_types descr sorts |
|
322 val raw_constrs = flat (map (map (fn (c, _, _, _) => c)) raw_cns_info) |
|
323 |
322 val raw_inject_thms = flat (map #inject dtinfos) |
324 val raw_inject_thms = flat (map #inject dtinfos) |
323 val raw_distinct_thms = flat (map #distinct dtinfos) |
325 val raw_distinct_thms = flat (map #distinct dtinfos) |
324 val raw_induct_thm = #induct dtinfo |
326 val raw_induct_thm = #induct dtinfo |
325 val raw_induct_thms = #inducts dtinfo |
327 val raw_induct_thms = #inducts dtinfo |
326 val raw_exhaust_thms = map #exhaust dtinfos |
328 val raw_exhaust_thms = map #exhaust dtinfos |
347 (raw_inject_thms @ raw_distinct_thms) lthy3 |
349 (raw_inject_thms @ raw_distinct_thms) lthy3 |
348 else raise TEST lthy3 |
350 else raise TEST lthy3 |
349 |
351 |
350 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = |
352 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = |
351 if get_STEPS lthy3a > 3 |
353 if get_STEPS lthy3a > 3 |
352 then define_raw_fvs descr sorts raw_bn_info raw_bclauses (raw_inject_thms @ raw_distinct_thms) lthy3a |
354 then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses |
|
355 (raw_inject_thms @ raw_distinct_thms) lthy3a |
353 else raise TEST lthy3a |
356 else raise TEST lthy3a |
354 |
357 |
355 (* definition of raw alphas *) |
358 (* definition of raw alphas *) |
356 val _ = warning "Definition of alphas"; |
359 val _ = warning "Definition of alphas"; |
357 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
360 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
358 if get_STEPS lthy3b > 4 |
361 if get_STEPS lthy3b > 4 |
359 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b |
362 then define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3b |
360 else raise TEST lthy3b |
363 else raise TEST lthy3b |
361 val alpha_tys = map (domain_type o fastype_of) alpha_trms |
364 val alpha_tys = map (domain_type o fastype_of) alpha_trms |
362 |
365 |
363 (* definition of alpha-distinct lemmas *) |
366 (* definition of alpha-distinct lemmas *) |
364 val _ = warning "Distinct theorems"; |
367 val _ = warning "Distinct theorems"; |