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 _ => |
481 val q_fv = map (lift_thm qtys lthy15) fv_def; |
481 val q_fv = map (lift_thm qtys lthy15) fv_def; |
482 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
482 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
483 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; |
483 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; |
484 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
484 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
485 val _ = tracing "Lifting eq-iff"; |
485 val _ = tracing "Lifting eq-iff"; |
486 val _ = map tracing (map PolyML.makestring alpha_eq_iff); |
486 (* val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |
487 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff |
487 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff |
488 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0 |
488 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0 |
489 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1 |
489 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1 |
490 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2; |
490 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2; |
491 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0 |
491 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0 |