1 theory Parser |
1 theory Parser |
2 imports "../Nominal-General/Nominal2_Atoms" |
2 imports "../Nominal-General/Nominal2_Atoms" |
3 "../Nominal-General/Nominal2_Eqvt" |
3 "../Nominal-General/Nominal2_Eqvt" |
4 "../Nominal-General/Nominal2_Supp" |
4 "../Nominal-General/Nominal2_Supp" |
5 "Perm" "Equivp" "Rsp" "Lift" |
5 "Perm" "Equivp" "Rsp" "Lift" "Fv" |
6 begin |
6 begin |
7 |
7 |
8 section{* Interface for nominal_datatype *} |
8 section{* Interface for nominal_datatype *} |
9 |
9 |
10 text {* |
10 text {* |
370 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
370 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
371 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
371 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
372 |
372 |
373 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); |
373 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); |
374 val {descr, sorts, ...} = dtinfo; |
374 val {descr, sorts, ...} = dtinfo; |
375 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
375 fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i); |
376 val raw_tys = map (fn (i, _) => nth_dtyp i) descr; |
376 val raw_tys = map (fn (i, _) => nth_dtyp i) descr; |
377 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr) |
377 val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr) |
378 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
378 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
379 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames; |
379 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames; |
380 val rel_dtinfos = List.take (dtinfos, (length dts)); |
380 val rel_dtinfos = List.take (dtinfos, (length dts)); |
381 val inject = flat (map #inject dtinfos); |
381 val inject = flat (map #inject dtinfos); |
382 val distincts = flat (map #distinct dtinfos); |
382 val distincts = flat (map #distinct dtinfos); |
421 val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; |
421 val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; |
422 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
422 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
423 val raw_consts = |
423 val raw_consts = |
424 flat (map (fn (i, (_, _, l)) => |
424 flat (map (fn (i, (_, _, l)) => |
425 map (fn (cname, dts) => |
425 map (fn (cname, dts) => |
426 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
426 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
427 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
427 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); |
428 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; |
428 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; |
429 val _ = tracing "Proving respects"; |
429 val _ = tracing "Proving respects"; |
430 val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; |
430 val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; |
431 val (bns_rsp_pre, lthy9) = fold_map ( |
431 val (bns_rsp_pre, lthy9) = fold_map ( |
432 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
432 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |