equal
deleted
inserted
replaced
36 it returns the defined constant and its definition |
36 it returns the defined constant and its definition |
37 theorem; stores the data in the qconsts slot |
37 theorem; stores the data in the qconsts slot |
38 *) |
38 *) |
39 fun quotient_def mx attr lhs rhs lthy = |
39 fun quotient_def mx attr lhs rhs lthy = |
40 let |
40 let |
41 val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*) |
41 val (lhs_str, lhs_ty) = |
|
42 dest_Free lhs |
|
43 handle TERM _ => error "The name for the new constant has to be a Free; check that it is not defined yet." |
42 val qconst_bname = Binding.name lhs_str; |
44 val qconst_bname = Binding.name lhs_str; |
43 val absrep_trm = absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs |
45 val absrep_trm = absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs |
44 val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
46 val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
45 val (_, prop') = LocalDefs.cert_def lthy prop |
47 val (_, prop') = LocalDefs.cert_def lthy prop |
46 val (_, newrhs) = Primitive_Defs.abs_def prop' |
48 val (_, newrhs) = Primitive_Defs.abs_def prop' |