5 *) |
5 *) |
6 |
6 |
7 signature QUOTIENT_DEF = |
7 signature QUOTIENT_DEF = |
8 sig |
8 sig |
9 val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) -> |
9 val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) -> |
10 local_theory -> (term * thm) * local_theory |
10 local_theory -> Quotient_Info.qconsts_info * local_theory |
11 |
11 |
12 val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) -> |
12 val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) -> |
13 local_theory -> (term * thm) * local_theory |
13 local_theory -> Quotient_Info.qconsts_info * local_theory |
14 |
14 |
15 val quotient_lift_const: typ list -> string * term -> local_theory -> |
15 val quotient_lift_const: typ list -> string * term -> local_theory -> |
16 (term * thm) * local_theory |
16 Quotient_Info.qconsts_info * 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 |
43 let |
43 let |
44 val name = Binding.name_of bind |
44 val name = Binding.name_of bind |
45 val pos = Position.str_of (Binding.pos_of bind) |
45 val pos = Position.str_of (Binding.pos_of bind) |
46 in |
46 in |
47 error ("Head of quotient_definition " ^ |
47 error ("Head of quotient_definition " ^ |
48 (quote str) ^ " differs from declaration " ^ name ^ pos) |
48 quote str ^ " differs from declaration " ^ name ^ pos) |
49 end |
49 end |
50 |
50 |
51 fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy = |
51 fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy = |
52 let |
52 let |
53 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
53 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
67 val (_, newrhs) = Local_Defs.abs_def prop' |
67 val (_, newrhs) = Local_Defs.abs_def prop' |
68 |
68 |
69 val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy |
69 val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy |
70 |
70 |
71 (* data storage *) |
71 (* data storage *) |
72 fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm} |
72 val qconst_data = {qconst = trm, rconst = rhs, def = thm} |
|
73 |
|
74 fun qcinfo phi = transform_qconsts phi qconst_data |
73 fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) |
75 fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) |
74 val lthy'' = Local_Theory.declaration true |
76 val lthy'' = Local_Theory.declaration true |
75 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' |
77 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' |
76 in |
78 in |
77 ((trm, thm), lthy'') |
79 (qconst_data, lthy'') |
78 end |
80 end |
79 |
81 |
80 fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy = |
82 fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy = |
81 let |
83 let |
82 val lhs = Syntax.read_term lthy lhs_str |
84 val lhs = Syntax.read_term lthy lhs_str |