249 |> add_datatype_wrapper raw_dt_names raw_dts |
249 |> add_datatype_wrapper raw_dt_names raw_dts |
250 ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs |
250 ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs |
251 ||>> pair raw_binds |
251 ||>> pair raw_binds |
252 ||>> pair raw_bns |
252 ||>> pair raw_bns |
253 end |
253 end |
254 *} |
|
255 |
|
256 ML {* |
|
257 fun un_raw name = unprefix "_raw" name handle Fail _ => name |
|
258 fun add_under names = hd names :: (map (prefix "_") (tl names)) |
|
259 fun un_raws name = implode (map un_raw (add_under (space_explode "_" name))) |
|
260 val un_raw_names = rename_vars un_raws |
|
261 fun lift_thm ctxt thm = un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm))) |
|
262 *} |
254 *} |
263 |
255 |
264 lemma equivp_hack: "equivp x" |
256 lemma equivp_hack: "equivp x" |
265 sorry |
257 sorry |
266 ML {* |
258 ML {* |
331 val fv_def = ProofContext.export lthy4 lthy3 fv_def_loc; |
323 val fv_def = ProofContext.export lthy4 lthy3 fv_def_loc; |
332 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
324 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
333 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
325 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
334 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
326 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
335 val bns = raw_bn_funs ~~ bn_nos; |
327 val bns = raw_bn_funs ~~ bn_nos; |
336 val alpha_intros = #intrs alpha; |
328 val alpha_intros_loc = #intrs alpha; |
337 val alpha_cases_loc = #elims alpha |
329 val alpha_cases_loc = #elims alpha |
|
330 val alpha_intros = ProofContext.export lthy4 lthy3 alpha_intros_loc |
338 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
331 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
339 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4 |
332 val alpha_inj_loc = build_alpha_inj alpha_intros_loc (inject @ distincts) alpha_cases_loc lthy4 |
340 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
333 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
341 val _ = tracing "Proving equivariance"; |
334 val _ = tracing "Proving equivariance"; |
342 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
335 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
343 val fv_eqvt_tac = |
336 val fv_eqvt_tac = |
344 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
337 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
348 if fv_ts_loc_bn = [] then ([], lthy6) else |
341 if fv_ts_loc_bn = [] then ([], lthy6) else |
349 fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) |
342 fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) |
350 (fv_ts_loc_bn ~~ (map snd bns)) lthy6; |
343 (fv_ts_loc_bn ~~ (map snd bns)) lthy6; |
351 val lthy6 = lthy6a; |
344 val lthy6 = lthy6a; |
352 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
345 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
353 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
346 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy2 raw_fv_bv_eqvt_loc; |
354 fun alpha_eqvt_tac' _ = |
347 fun alpha_eqvt_tac' _ = |
355 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
348 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
356 else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc @ raw_fv_bv_eqvt_loc) lthy6 1 |
349 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_inj @ raw_fv_bv_eqvt) lthy6 1 |
357 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy6; |
350 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; |
358 val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; |
|
359 val _ = tracing "Proving equivalence"; |
351 val _ = tracing "Proving equivalence"; |
360 val alpha_equivp_loc = |
352 val alpha_equivp = |
361 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_loc_nobn |
353 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn |
362 else build_equivps alpha_ts_loc induct alpha_induct_loc |
354 else build_equivps alpha_ts induct alpha_induct |
363 inject alpha_inj_loc distincts alpha_cases_loc alpha_eqvt_loc lthy6; |
355 inject alpha_inj distincts alpha_cases alpha_eqvt lthy6; |
364 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
|
365 val qty_binds = map (fn (_, b, _, _) => b) dts; |
356 val qty_binds = map (fn (_, b, _, _) => b) dts; |
366 val qty_names = map Name.of_binding qty_binds; |
357 val qty_names = map Name.of_binding qty_binds; |
367 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
358 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
368 val lthy7 = define_quotient_type |
359 val lthy7 = define_quotient_type |
369 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn)) |
360 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn)) |
372 val raw_consts = |
363 val raw_consts = |
373 flat (map (fn (i, (_, _, l)) => |
364 flat (map (fn (i, (_, _, l)) => |
374 map (fn (cname, dts) => |
365 map (fn (cname, dts) => |
375 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
366 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
376 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
367 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
377 val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7; |
368 val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7; |
378 val (consts_loc, const_defs) = split_list consts_defs; |
|
379 val morphism_8_7 = ProofContext.export_morphism lthy8 lthy7; |
|
380 val consts = map (Morphism.term morphism_8_7) consts_loc; |
|
381 (* Could be done nicer *) |
369 (* Could be done nicer *) |
382 val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts); |
370 val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts); |
383 val _ = tracing "Proving respects"; |
371 val _ = tracing "Proving respects"; |
384 val (bns_rsp_pre, lthy9) = fold_map ( |
372 val (bns_rsp_pre, lthy9) = fold_map ( |
385 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] |
373 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] |