243 val alpha_cases = #elims alpha |
243 val alpha_cases = #elims alpha |
244 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy4 |
244 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy4 |
245 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
245 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
246 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
246 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
247 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
247 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
248 (* val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms |
248 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms |
249 (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6; |
249 (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6; |
250 val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; |
250 val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; |
251 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |
251 (* val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |
252 inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6; |
252 inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6; |
253 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
253 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
254 val qty_names = map (fn (_, b, _, _) => b) dts; |
254 val qty_names = map (fn (_, b, _, _) => b) dts; |
255 val lthy7 = define_quotient_type |
255 val lthy7 = define_quotient_type |
256 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_names ~~ all_typs) ~~ alpha_ts)) |
256 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_names ~~ all_typs) ~~ alpha_ts)) |