62 val qty_args3 = qty_args2 ~~ alpha_equivp_thms |
62 val qty_args3 = qty_args2 ~~ alpha_equivp_thms |
63 in |
63 in |
64 fold_map Quotient_Type.add_quotient_type qty_args3 lthy |
64 fold_map Quotient_Type.add_quotient_type qty_args3 lthy |
65 end |
65 end |
66 |
66 |
|
67 (* a wrapper for lifting a raw constant *) |
|
68 fun lift_raw_const qtys (qconst_name, rconst, mx', rsp_thm) lthy = |
|
69 let |
|
70 val rty = fastype_of rconst |
|
71 val qty = Quotient_Term.derive_qtyp lthy qtys rty |
|
72 val lhs_raw = Free (qconst_name, qty) |
|
73 val rhs_raw = rconst |
|
74 |
|
75 val raw_var = (Binding.name qconst_name, NONE, mx') |
|
76 val ([(binding, _, mx)], ctxt) = Proof_Context.cert_vars [raw_var] lthy |
|
77 val lhs = Syntax.check_term ctxt lhs_raw |
|
78 val rhs = Syntax.check_term ctxt rhs_raw |
|
79 |
|
80 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
|
81 val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
|
82 val _ = if is_Const rhs then () else warning "The definiens is not a constant" |
|
83 |
|
84 in |
|
85 Quotient_Def.add_quotient_def (((binding, mx), Attrib.empty_binding), (lhs, rhs)) rsp_thm ctxt |
|
86 end |
|
87 |
67 |
88 |
68 (* defines quotient constants *) |
89 (* defines quotient constants *) |
69 fun define_qconsts qtys consts_specs lthy = |
90 fun define_qconsts qtys consts_specs lthy = |
70 let |
91 let |
71 val (qconst_infos, lthy') = |
92 val (qconst_infos, lthy') = |
72 fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy |
93 fold_map (lift_raw_const qtys) consts_specs lthy |
73 val phi = Proof_Context.export_morphism lthy' lthy |
94 val phi = Proof_Context.export_morphism lthy' lthy |
74 in |
95 in |
75 (map (Quotient_Info.transform_quotconsts phi) qconst_infos, lthy') |
96 (map (Quotient_Info.transform_quotconsts phi) qconst_infos, lthy') |
76 end |
97 end |
77 |
98 |