equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 signature QUOTIENT_DEF = |
7 signature QUOTIENT_DEF = |
8 sig |
8 sig |
9 val quotient_def: (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) -> |
9 val quotient_def: (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) -> |
10 local_theory -> Quotient_Info.qconsts_info * local_theory |
10 local_theory -> Quotient_Info.quotconsts * local_theory |
11 |
11 |
12 val quotdef_cmd: (binding * string option * mixfix) option * (Attrib.binding * (string * string)) -> |
12 val quotdef_cmd: (binding * string option * mixfix) option * (Attrib.binding * (string * string)) -> |
13 local_theory -> Quotient_Info.qconsts_info * local_theory |
13 local_theory -> Quotient_Info.quotconsts * local_theory |
14 |
14 |
15 val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory -> |
15 val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory -> |
16 Quotient_Info.qconsts_info * local_theory |
16 Quotient_Info.quotconsts * local_theory |
17 end; |
17 end; |
18 |
18 |
19 structure Quotient_Def: QUOTIENT_DEF = |
19 structure Quotient_Def: QUOTIENT_DEF = |
20 struct |
20 struct |
21 |
21 |
27 - an optional binding and mixfix annotation |
27 - an optional binding and mixfix annotation |
28 - attributes |
28 - attributes |
29 - the new constant as term |
29 - the new constant as term |
30 - the rhs of the definition as term |
30 - the rhs of the definition as term |
31 |
31 |
32 It stores the qconst_info in the qconsts data slot. |
32 It stores the qconst_info in the quotconsts data slot. |
33 |
33 |
34 Restriction: At the moment the left- and right-hand |
34 Restriction: At the moment the left- and right-hand |
35 side of the definition must be a constant. |
35 side of the definition must be a constant. |
36 *) |
36 *) |
37 fun error_msg bind str = |
37 fun error_msg bind str = |
70 val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy |
70 val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy |
71 |
71 |
72 (* data storage *) |
72 (* data storage *) |
73 val qconst_data = {qconst = trm, rconst = rhs, def = thm} |
73 val qconst_data = {qconst = trm, rconst = rhs, def = thm} |
74 |
74 |
75 fun qcinfo phi = Quotient_Info.transform_qconsts phi qconst_data |
75 fun qcinfo phi = Quotient_Info.transform_quotconsts phi qconst_data |
76 fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) |
76 fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) |
77 val lthy'' = |
77 val lthy'' = |
78 Local_Theory.declaration true |
78 Local_Theory.declaration true |
79 (fn phi => Quotient_Info.qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' |
79 (fn phi => Quotient_Info.update_quotconsts (trans_name phi) (qcinfo phi)) lthy' |
80 in |
80 in |
81 (qconst_data, lthy'') |
81 (qconst_data, lthy'') |
82 end |
82 end |
83 |
83 |
84 fun check_term' cnstr ctxt = |
84 fun check_term' cnstr ctxt = |