389 val raw_binds_flat = map (map flat) raw_binds; |
389 val raw_binds_flat = map (map flat) raw_binds; |
390 val ((((_, fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) = |
390 val ((((_, fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) = |
391 define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3; |
391 define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3; |
392 val (fv, fvbn) = chop (length perms) fv_ts; |
392 val (fv, fvbn) = chop (length perms) fv_ts; |
393 |
393 |
394 val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts |
394 val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts |
395 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct; |
|
396 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
395 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
397 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
396 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
398 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
397 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
399 val bns = raw_bn_funs ~~ bn_nos; |
398 val bns = raw_bn_funs ~~ bn_nos; |
400 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) |
399 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) |
474 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
473 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
475 fun note_simp_suffix s th ctxt = |
474 fun note_simp_suffix s th ctxt = |
476 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
475 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
477 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
476 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
478 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13; |
477 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13; |
479 val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct |
478 val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct |
480 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
479 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
481 val q_perm = map (lift_thm qtys lthy14) raw_perm_def; |
480 val q_perm = map (lift_thm qtys lthy14) raw_perm_def; |
482 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
481 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
483 val q_fv = map (lift_thm qtys lthy15) fv_def; |
482 val q_fv = map (lift_thm qtys lthy15) fv_def; |
484 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
483 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |