equal
deleted
inserted
replaced
17 structure Quotient_Def: QUOTIENT_DEF = |
17 structure Quotient_Def: QUOTIENT_DEF = |
18 struct |
18 struct |
19 |
19 |
20 open Quotient_Info; |
20 open Quotient_Info; |
21 open Quotient_Term; |
21 open Quotient_Term; |
22 |
|
23 (* wrapper for define *) |
|
24 fun define name mx attr rhs lthy = |
|
25 let |
|
26 val ((rhs, (_ , thm)), lthy') = |
|
27 Local_Theory.define ((name, mx), (attr, rhs)) lthy |
|
28 in |
|
29 ((rhs, thm), lthy') |
|
30 end |
|
31 |
|
32 |
22 |
33 (** Interface and Syntax Setup **) |
23 (** Interface and Syntax Setup **) |
34 |
24 |
35 (* The ML-interface for a quotient definition takes |
25 (* The ML-interface for a quotient definition takes |
36 as argument: |
26 as argument: |
56 val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs |
46 val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs |
57 val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
47 val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
58 val (_, prop') = LocalDefs.cert_def lthy prop |
48 val (_, prop') = LocalDefs.cert_def lthy prop |
59 val (_, newrhs) = Primitive_Defs.abs_def prop' |
49 val (_, newrhs) = Primitive_Defs.abs_def prop' |
60 |
50 |
61 val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy |
51 val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy |
62 |
52 |
63 (* data storage *) |
53 (* data storage *) |
64 fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm} |
54 fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm} |
65 fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) |
55 fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) |
66 val lthy'' = Local_Theory.declaration true |
56 val lthy'' = Local_Theory.declaration true |