80 val sorts = #sorts info; |
80 val sorts = #sorts info; |
81 val nos = map fst descr |
81 val nos = map fst descr |
82 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) nos |
82 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) nos |
83 val typs = List.take (all_typs, number) |
83 val typs = List.take (all_typs, number) |
84 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
84 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
85 val full_tnames = List.take (all_full_tnames, number); |
|
86 val induct = #induct info; |
85 val induct = #induct info; |
87 val inducts = #inducts info; |
86 val inducts = #inducts info; |
88 val infos = map (Datatype.the_info thy1) all_full_tnames; |
87 val infos = map (Datatype.the_info thy1) all_full_tnames; |
89 val inject = flat (map #inject infos); |
88 val inject = flat (map #inject infos); |
90 val distinct = flat (map #distinct infos); |
89 val distinct = flat (map #distinct infos); |
104 val alpha_inj = ProofContext.export lthy2 lthy1 alpha_inj_loc |
103 val alpha_inj = ProofContext.export lthy2 lthy1 alpha_inj_loc |
105 val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc |
104 val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc |
106 val morphism = ProofContext.export_morphism lthy2 lthy1 |
105 val morphism = ProofContext.export_morphism lthy2 lthy1 |
107 val fv_ts = map (Morphism.term morphism) fv_ts_loc |
106 val fv_ts = map (Morphism.term morphism) fv_ts_loc |
108 val alpha_ts = map (Morphism.term morphism) alpha_ts_loc |
107 val alpha_ts = map (Morphism.term morphism) alpha_ts_loc |
109 fun build_bv_eqvt (t, n) = |
108 val (bv_eqvts, lthy3) = fold_map (build_bv_eqvt perms (bv_simps @ raw_perm_def) inducts) bvs lthy2; |
110 build_eqvts Binding.empty [t] [nth perms n] |
|
111 (bv_simps @ raw_perm_def) (nth inducts n) |
|
112 val (bv_eqvts, lthy3) = fold_map build_bv_eqvt bvs lthy2; |
|
113 val (fv_eqvts, lthy4) = build_eqvts Binding.empty fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3; |
109 val (fv_eqvts, lthy4) = build_eqvts Binding.empty fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3; |
114 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy4; |
110 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy4; |
115 val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc; |
111 val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc; |
116 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy4; |
112 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy4; |
117 val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc |
113 val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc |