39 *) |
39 *) |
40 fun quotient_def (bindmx, (attr, (lhs, rhs))) lthy = |
40 fun quotient_def (bindmx, (attr, (lhs, rhs))) lthy = |
41 let |
41 let |
42 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
42 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
43 val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
43 val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
44 val der_bname = Binding.name lhs_str |
44 val derived_bname = Binding.name lhs_str |
45 val (qconst_bname, mx) = |
45 val (qconst_bname, mx) = |
46 case bindmx of |
46 case bindmx of |
47 SOME (bname, mx) => |
47 SOME (bname, mx) => |
48 let |
48 let |
49 val _ = (Name.of_binding bname = lhs_str) orelse error ("Head of quotient_definition " ^ |
49 val _ = (Name.of_binding bname = lhs_str) orelse error ("Head of quotient_definition " ^ |
50 (quote lhs_str) ^ " differs from declaration " ^ (Binding.name_of bname) ^ |
50 (quote lhs_str) ^ " differs from declaration " ^ (Binding.name_of bname) ^ |
51 Position.str_of (Binding.pos_of bname)) |
51 Position.str_of (Binding.pos_of bname)) |
52 in |
52 in |
53 (der_bname, mx) |
53 (derived_bname, mx) |
54 end |
54 end |
55 | NONE => (der_bname, NoSyn) |
55 | NONE => (derived_bname, NoSyn) |
56 val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs |
56 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) |
57 val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
58 val (_, prop') = LocalDefs.cert_def lthy prop |
58 val (_, prop') = LocalDefs.cert_def lthy prop |
59 val (_, newrhs) = Primitive_Defs.abs_def prop' |
59 val (_, newrhs) = Primitive_Defs.abs_def prop' |
60 |
60 |