238 val descr = #descr dtinfo; |
238 val descr = #descr dtinfo; |
239 val sorts = #sorts dtinfo; |
239 val sorts = #sorts dtinfo; |
240 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr) |
240 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr) |
241 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
241 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
242 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames; |
242 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames; |
|
243 val rel_dtinfos = List.take (dtinfos, (length dts)); |
243 val inject = flat (map #inject dtinfos); |
244 val inject = flat (map #inject dtinfos); |
244 val distinct = flat (map #distinct dtinfos); |
245 val distinct = flat (map #distinct dtinfos); |
|
246 val rel_distinct = map #distinct rel_dtinfos; |
245 val induct = #induct dtinfo; |
247 val induct = #induct dtinfo; |
246 val inducts = #inducts dtinfo; |
248 val inducts = #inducts dtinfo; |
247 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
249 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
248 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
250 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
249 val raw_binds_flat = map (map flat) raw_binds; |
251 val raw_binds_flat = map (map flat) raw_binds; |
259 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
261 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
260 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
262 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
261 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
263 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
262 val bns = raw_bn_funs ~~ bn_nos; |
264 val bns = raw_bn_funs ~~ bn_nos; |
263 val alpha_intros = #intrs alpha; |
265 val alpha_intros = #intrs alpha; |
264 val alpha_cases = #elims alpha |
266 val alpha_cases_loc = #elims alpha |
265 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy4 |
267 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
|
268 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4 |
266 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
269 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
267 (* val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
270 (* val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
268 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
271 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
269 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
272 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
270 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms |
273 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms |
271 (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6; |
274 (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6; |
272 val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; |
275 val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; |
273 val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc |
276 val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc |
274 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |
277 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |
275 inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6; |
278 inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6; |
276 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
279 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
277 val qty_binds = map (fn (_, b, _, _) => b) dts; |
280 val qty_binds = map (fn (_, b, _, _) => b) dts; |
278 val qty_names = map Name.of_binding qty_binds; |
281 val qty_names = map Name.of_binding qty_binds; |
279 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
282 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
280 val lthy7 = define_quotient_type |
283 val lthy7 = define_quotient_type |
316 val q_bn = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs; |
319 val q_bn = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs; |
317 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; |
320 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; |
318 val inj_unfolded = map (LocalDefs.unfold lthy17 @{thms alpha_gen}) alpha_inj |
321 val inj_unfolded = map (LocalDefs.unfold lthy17 @{thms alpha_gen}) alpha_inj |
319 val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded; |
322 val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded; |
320 val q_inj = map (LocalDefs.fold lthy17 @{thms alpha_gen}) q_inj_pre |
323 val q_inj = map (LocalDefs.fold lthy17 @{thms alpha_gen}) q_inj_pre |
321 val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;*) |
324 val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17; |
|
325 val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) |
|
326 (rel_distinct ~~ (List.take (alpha_ts, (length dts))))) |
|
327 val q_dis = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy18, th))) rel_dists; |
|
328 val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18;*) |
322 in |
329 in |
323 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
330 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
324 end |
331 end |
325 *} |
332 *} |
326 ML fold |
333 ML fold |