322 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct |
322 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct |
323 val fv_def = ProofContext.export lthy4 lthy3 fv_def_loc; |
323 val fv_def = ProofContext.export lthy4 lthy3 fv_def_loc; |
324 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
324 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
325 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; |
326 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; |
327 val bns = raw_bn_funs ~~ bn_nos; |
327 val bns = raw_bn_funs ~~ bn_nos; (* Are exported *) |
328 val alpha_intros_loc = #intrs alpha; |
328 val alpha_intros_loc = #intrs alpha; |
329 val alpha_cases_loc = #elims alpha |
329 val alpha_cases_loc = #elims alpha |
330 val alpha_intros = ProofContext.export lthy4 lthy3 alpha_intros_loc |
330 val alpha_intros = ProofContext.export lthy4 lthy3 alpha_intros_loc |
331 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
331 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
332 val alpha_inj_loc = build_alpha_inj alpha_intros_loc (inject @ distincts) alpha_cases_loc lthy4 |
332 val alpha_inj_loc = build_alpha_inj alpha_intros_loc (inject @ distincts) alpha_cases_loc lthy4 |
333 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
333 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
334 val _ = tracing "Proving equivariance"; |
334 val _ = tracing "Proving equivariance"; |
335 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; |
336 val fv_eqvt_tac = |
336 val fv_eqvt_tac = |
337 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) |
338 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5 |
338 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) lthy5 |
339 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc_nobn fv_eqvt_tac lthy5; |
339 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_nobn fv_eqvt_tac lthy5; |
340 val (fv_bn_eqvts, lthy6a) = |
340 val (fv_bn_eqvts, lthy6a) = |
341 if fv_ts_loc_bn = [] then ([], lthy6) else |
341 if fv_ts_bn = [] then ([], lthy6) else |
342 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 @ raw_perm_def) inducts) |
343 (fv_ts_loc_bn ~~ (map snd bns)) lthy6; |
343 (fv_ts_bn ~~ (map snd bns)) lthy6; |
344 val lthy6 = lthy6a; |
344 val raw_fv_bv_eqvt = flat (map snd bv_eqvts) @ (snd fv_eqvts) @ flat (map snd fv_bn_eqvts) |
345 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
|
346 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy2 raw_fv_bv_eqvt_loc; |
|
347 fun alpha_eqvt_tac' _ = |
345 fun alpha_eqvt_tac' _ = |
348 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
346 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
349 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_inj @ raw_fv_bv_eqvt) lthy6 1 |
347 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_inj @ raw_fv_bv_eqvt) lthy6a 1 |
350 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; |
348 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a; |
351 val _ = tracing "Proving equivalence"; |
349 val _ = tracing "Proving equivalence"; |
352 val alpha_equivp = |
350 val alpha_equivp = |
353 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn |
351 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn |
354 else build_equivps alpha_ts induct alpha_induct |
352 else build_equivps alpha_ts induct alpha_induct |
355 inject alpha_inj distincts alpha_cases alpha_eqvt lthy6; |
353 inject alpha_inj distincts alpha_cases alpha_eqvt lthy6a; |
356 val qty_binds = map (fn (_, b, _, _) => b) dts; |
354 val qty_binds = map (fn (_, b, _, _) => b) dts; |
357 val qty_names = map Name.of_binding qty_binds; |
355 val qty_names = map Name.of_binding qty_binds; |
358 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
356 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
359 val lthy7 = define_quotient_type |
357 val lthy7 = define_quotient_type |
360 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn)) |
358 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn)) |
361 (ALLGOALS (resolve_tac alpha_equivp)) lthy6; |
359 (ALLGOALS (resolve_tac alpha_equivp)) lthy6a; |
362 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
360 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
363 val raw_consts = |
361 val raw_consts = |
364 flat (map (fn (i, (_, _, l)) => |
362 flat (map (fn (i, (_, _, l)) => |
365 map (fn (cname, dts) => |
363 map (fn (cname, dts) => |
366 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
364 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |