24 end |
24 end |
25 |
25 |
26 |
26 |
27 (* interface and syntax setup *) |
27 (* interface and syntax setup *) |
28 |
28 |
29 (* the ML-interface takes a 4-tuple consisting of *) |
29 (* the ML-interface takes a 4-tuple consisting of *) |
30 (* *) |
30 (* *) |
31 (* - the mixfix annotation *) |
31 (* - the mixfix annotation *) |
32 (* - name and attributes of the meta eq *) |
32 (* - name and attributes *) |
33 (* - the new constant including its type *) |
33 (* - the new constant including its type *) |
34 (* - the rhs of the definition *) |
34 (* - the rhs of the definition *) |
|
35 (* *) |
|
36 (* returns the defined constant and its definition *) |
|
37 (* theorem; stores the data in the qconsts slot *) |
35 |
38 |
36 fun quotient_def mx attr lhs rhs lthy = |
39 fun quotient_def mx attr lhs rhs lthy = |
37 let |
40 let |
38 val Free (lhs_str, lhs_ty) = lhs; |
41 val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.) |
39 val qconst_bname = Binding.name lhs_str; |
42 val qconst_bname = Binding.name lhs_str; |
40 val absrep_trm = absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty) $ rhs |
43 val absrep_trm = absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty) $ rhs |
41 val prop = Logic.mk_equals (lhs, absrep_trm) |
44 val prop = Logic.mk_equals (lhs, absrep_trm) |
42 val (_, prop') = LocalDefs.cert_def lthy prop |
45 val (_, prop') = LocalDefs.cert_def lthy prop |
43 val (_, newrhs) = Primitive_Defs.abs_def prop' |
46 val (_, newrhs) = Primitive_Defs.abs_def prop' |
44 |
47 |
45 val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy |
48 val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy |
46 |
49 |
|
50 (* data storage *) |
47 fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm} |
51 fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm} |
48 val lthy'' = Local_Theory.declaration true |
52 val lthy'' = Local_Theory.declaration true |
49 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy' |
53 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy' |
50 in |
54 in |
51 ((trm, thm), lthy'') |
55 ((trm, thm), lthy'') |