287 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) = |
287 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) = |
288 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
288 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
289 val morphism_2_1 = ProofContext.export_morphism lthy2 lthy |
289 val morphism_2_1 = ProofContext.export_morphism lthy2 lthy |
290 val raw_bns_exp = map (apsnd (map (apfst (Morphism.term morphism_2_1)))) raw_bns; |
290 val raw_bns_exp = map (apsnd (map (apfst (Morphism.term morphism_2_1)))) raw_bns; |
291 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
291 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
292 |
|
293 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
292 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
294 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
293 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
|
294 |
295 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); |
295 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); |
296 val descr = #descr dtinfo; |
296 val descr = #descr dtinfo; |
297 val sorts = #sorts dtinfo; |
297 val sorts = #sorts dtinfo; |
298 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr) |
298 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr) |
299 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
299 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
306 val inducts = #inducts dtinfo; |
306 val inducts = #inducts dtinfo; |
307 val _ = tracing "Defining permutations, fv and alpha"; |
307 val _ = tracing "Defining permutations, fv and alpha"; |
308 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
308 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
309 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
309 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
310 val raw_binds_flat = map (map flat) raw_binds; |
310 val raw_binds_flat = map (map flat) raw_binds; |
311 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3; |
311 val (((fv_ts, fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) = |
312 val alpha_ts_loc = #preds alpha |
312 define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3; |
313 val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms) |
|
314 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; |
|
315 val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc; |
|
316 val (fv_ts_loc_nobn, fv_ts_loc_bn) = chop (length perms) fv_ts_loc; |
|
317 val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts; |
313 val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts; |
318 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; |
|
319 val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts |
314 val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts |
320 val alpha_induct_loc = #induct alpha |
|
321 val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc]; |
|
322 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct |
315 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct |
323 val fv_def = ProofContext.export lthy4 lthy3 fv_def_loc; |
|
324 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
316 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
325 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
317 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; |
318 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
327 val bns = raw_bn_funs ~~ bn_nos; (* Are exported *) |
319 val bns = raw_bn_funs ~~ bn_nos; |
328 val alpha_intros_loc = #intrs alpha; |
|
329 val alpha_cases_loc = #elims alpha |
|
330 val alpha_intros = ProofContext.export lthy4 lthy3 alpha_intros_loc |
|
331 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
|
332 val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
320 val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
333 val _ = tracing "Proving equivariance"; |
321 val _ = tracing "Proving equivariance"; |
334 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
322 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
335 val fv_eqvt_tac = |
323 val fv_eqvt_tac = |
336 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
324 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
382 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts |
370 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts |
383 val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12; |
371 val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12; |
384 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
372 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
385 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |
373 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |
386 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
374 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
|
375 val (qbn_defs, lthy12c) = fold_map Quotient_Def.quotient_lift_const (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; |
387 val _ = tracing "Lifting permutations"; |
376 val _ = tracing "Lifting permutations"; |
388 val (qbn_defs, lthy12c) = fold_map Quotient_Def.quotient_lift_const (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; |
|
389 val thy = Local_Theory.exit_global lthy12c; |
377 val thy = Local_Theory.exit_global lthy12c; |
390 val perm_names = map (fn x => "permute_" ^ x) qty_names |
378 val perm_names = map (fn x => "permute_" ^ x) qty_names |
391 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
379 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
392 val lthy13 = Theory_Target.init NONE thy'; |
380 val lthy13 = Theory_Target.init NONE thy'; |
393 val q_name = space_implode "_" qty_names; |
381 val q_name = space_implode "_" qty_names; |