5 |
5 |
6 *) |
6 *) |
7 |
7 |
8 signature QUOTIENT_DEF = |
8 signature QUOTIENT_DEF = |
9 sig |
9 sig |
10 val quotient_def: (Attrib.binding * mixfix) option * (Attrib.binding * (term * term)) -> |
10 val quotient_def: (binding * mixfix) option * (Attrib.binding * (term * term)) -> |
11 local_theory -> (term * thm) * local_theory |
11 local_theory -> (term * thm) * local_theory |
12 |
12 |
13 val quotdef_cmd: (Attrib.binding * mixfix) option * (Attrib.binding * (string * string)) -> |
13 val quotdef_cmd: (binding * mixfix) option * (Attrib.binding * (string * string)) -> |
14 local_theory -> (term * thm) * local_theory |
14 local_theory -> (term * thm) * local_theory |
15 end; |
15 end; |
16 |
16 |
17 structure Quotient_Def: QUOTIENT_DEF = |
17 structure Quotient_Def: QUOTIENT_DEF = |
18 struct |
18 struct |
37 be a terms composed of constant. Similarly the |
37 be a terms composed of constant. Similarly the |
38 left-hand side must be a single constant. |
38 left-hand side must be a single constant. |
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 mx = |
|
43 case bindmx of |
|
44 SOME (_, mx) => mx |
|
45 | _ => NoSyn |
|
46 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." |
47 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" |
48 |
44 val der_bname = Binding.name lhs_str |
49 val qconst_bname = Binding.name lhs_str |
45 val (qconst_bname, mx) = |
|
46 case bindmx of |
|
47 SOME (bname, mx) => |
|
48 let |
|
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) ^ |
|
51 Position.str_of (Binding.pos_of bname)) |
|
52 in |
|
53 (der_bname, mx) |
|
54 end |
|
55 | NONE => (der_bname, NoSyn) |
50 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 |
51 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) |
52 val (_, prop') = LocalDefs.cert_def lthy prop |
58 val (_, prop') = LocalDefs.cert_def lthy prop |
53 val (_, newrhs) = Primitive_Defs.abs_def prop' |
59 val (_, newrhs) = Primitive_Defs.abs_def prop' |
54 |
60 |