4 Definitions for constants on quotient types. |
4 Definitions for constants on quotient types. |
5 |
5 |
6 *) |
6 *) |
7 |
7 |
8 signature QUOTIENT_DEF = |
8 signature QUOTIENT_DEF = |
9 sig |
9 sig |
10 val quotient_def: mixfix -> Attrib.binding -> term -> term -> |
10 val quotient_def: mixfix -> 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 * string) * (mixfix * string) -> |
13 val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) -> |
14 local_theory -> local_theory |
14 local_theory -> local_theory |
30 end |
30 end |
31 |
31 |
32 |
32 |
33 (** Interface and Syntax Setup **) |
33 (** Interface and Syntax Setup **) |
34 |
34 |
35 (* The ML-interface for a quotient definition takes |
35 (* The ML-interface for a quotient definition takes |
36 as argument: |
36 as argument: |
37 |
37 |
38 - the mixfix annotation |
38 - the mixfix annotation |
39 - name and attributes |
39 - name and attributes |
40 - the new constant as term |
40 - the new constant as term |
41 - the rhs of the definition as term |
41 - the rhs of the definition as term |
42 |
42 |
43 It returns the defined constant and its definition |
43 It returns the defined constant and its definition |
44 theorem; stores the data in the qconsts data slot. |
44 theorem; stores the data in the qconsts data slot. |
45 |
45 |
46 Restriction: At the moment the right-hand side must |
46 Restriction: At the moment the right-hand side must |
47 be a terms composed of constant. Similarly the |
47 be a terms composed of constant. Similarly the |
48 left-hand side must be a single constant. |
48 left-hand side must be a single constant. |
49 *) |
49 *) |
50 fun quotient_def mx attr lhs rhs lthy = |
50 fun quotient_def mx attr lhs rhs lthy = |
51 let |
51 let |
52 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
52 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
53 val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
53 val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
85 (SpecParse.opt_thm_name ":" -- |
85 (SpecParse.opt_thm_name ":" -- |
86 OuterParse.term) -- |
86 OuterParse.term) -- |
87 (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" -- |
87 (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" -- |
88 OuterParse.term) |
88 OuterParse.term) |
89 |
89 |
90 val _ = OuterSyntax.local_theory "quotient_definition" |
90 val _ = OuterSyntax.local_theory "quotient_definition" |
91 "definition for constants over the quotient type" |
91 "definition for constants over the quotient type" |
92 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |
92 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |
93 |
93 |
94 end; (* structure *) |
94 end; (* structure *) |