5 |
5 |
6 *) |
6 *) |
7 |
7 |
8 signature QUOTIENT_DEF = |
8 signature QUOTIENT_DEF = |
9 sig |
9 sig |
10 val quotient_def: (binding * mixfix) option * (Attrib.binding * (term * term)) -> |
10 val quotient_def: (binding option * 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: (binding * mixfix) option * (Attrib.binding * (string * string)) -> |
13 val quotdef_cmd: (binding option * mixfix) * (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 |
23 (** Interface and Syntax Setup **) |
23 (** Interface and Syntax Setup **) |
24 |
24 |
25 (* The ML-interface for a quotient definition takes |
25 (* The ML-interface for a quotient definition takes |
26 as argument: |
26 as argument: |
27 |
27 |
28 - the mixfix annotation |
28 - an optional binding and mixfix annotation |
29 - name and attributes |
29 - attributes |
30 - the new constant as term |
30 - the new constant as term |
31 - the rhs of the definition as term |
31 - the rhs of the definition as term |
32 |
32 |
33 It returns the defined constant and its definition |
33 It returns the defined constant and its definition |
34 theorem; stores the data in the qconsts data slot. |
34 theorem; stores the data in the qconsts data slot. |
35 |
35 |
36 Restriction: At the moment the right-hand side must |
36 Restriction: At the moment the right-hand side of the |
37 be a terms composed of constant. Similarly the |
37 definition must be a constant. Similarly the left-hand |
38 left-hand side must be a single constant. |
38 side must be a constant. |
39 *) |
39 *) |
40 fun quotient_def (bindmx, (attr, (lhs, rhs))) lthy = |
40 fun error_msg bind str = |
|
41 error ("Head of quotient_definition " ^ |
|
42 (quote str) ^ " differs from declaration " ^ (Binding.name_of bind) ^ |
|
43 Position.str_of (Binding.pos_of bind)) |
|
44 |
|
45 fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy = |
41 let |
46 let |
42 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
47 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" |
48 val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
44 val derived_bname = Binding.name lhs_str |
49 |
45 val (qconst_bname, mx) = |
50 fun sanity_test NONE _ = true |
46 case bindmx of |
51 | sanity_test (SOME bind) str = |
47 SOME (bname, mx) => |
52 if Name.of_binding bind = str then true |
48 let |
53 else error_msg bind str |
49 val _ = (Name.of_binding bname = lhs_str) orelse error ("Head of quotient_definition " ^ |
54 |
50 (quote lhs_str) ^ " differs from declaration " ^ (Binding.name_of bname) ^ |
55 val _ = sanity_test optbind lhs_str |
51 Position.str_of (Binding.pos_of bname)) |
56 |
52 in |
57 val qconst_bname = Binding.name lhs_str |
53 (derived_bname, mx) |
|
54 end |
|
55 | NONE => (derived_bname, NoSyn) |
|
56 val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs |
58 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) |
59 val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
58 val (_, prop') = LocalDefs.cert_def lthy prop |
60 val (_, prop') = LocalDefs.cert_def lthy prop |
59 val (_, newrhs) = Primitive_Defs.abs_def prop' |
61 val (_, newrhs) = Primitive_Defs.abs_def prop' |
60 |
62 |
67 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' |
69 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' |
68 in |
70 in |
69 ((trm, thm), lthy'') |
71 ((trm, thm), lthy'') |
70 end |
72 end |
71 |
73 |
72 fun quotdef_cmd (bindmx, (attr, (lhs_str, rhs_str))) lthy = |
74 fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy = |
73 let |
75 let |
74 val lhs = Syntax.read_term lthy lhs_str |
76 val lhs = Syntax.read_term lthy lhs_str |
75 val rhs = Syntax.read_term lthy rhs_str |
77 val rhs = Syntax.read_term lthy rhs_str |
76 val lthy' = Variable.declare_term lhs lthy |
78 val lthy' = Variable.declare_term lhs lthy |
77 val lthy'' = Variable.declare_term rhs lthy' |
79 val lthy'' = Variable.declare_term rhs lthy' |
78 in |
80 in |
79 quotient_def (bindmx, (attr, (lhs, rhs))) lthy'' |
81 quotient_def (decl, (attr, (lhs, rhs))) lthy'' |
80 end |
82 end |
81 |
83 |
82 val binding_mixfix_parser = OuterParse.binding -- OuterParse.opt_mixfix' --| OuterParse.$$$ "where" |
84 local |
|
85 structure P = OuterParse; |
|
86 in |
|
87 |
|
88 val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where" |
|
89 |
83 val quotdef_parser = |
90 val quotdef_parser = |
84 (Scan.option binding_mixfix_parser) -- |
91 Scan.optional quotdef_decl (NONE, NoSyn) -- |
85 OuterParse.!!! (SpecParse.opt_thm_name ":" -- ((OuterParse.term --| OuterParse.$$$ "is") -- OuterParse.term)) |
92 P.!!! (SpecParse.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term)) |
|
93 end |
86 |
94 |
87 val _ = |
95 val _ = |
88 OuterSyntax.local_theory "quotient_definition" |
96 OuterSyntax.local_theory "quotient_definition" |
89 "definition for constants over the quotient type" |
97 "definition for constants over the quotient type" |
90 OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd)) |
98 OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd)) |