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 * mixfix) option * (Attrib.binding * (string * string)) -> |
14 local_theory -> local_theory |
14 local_theory -> local_theory |
15 end; |
15 end; |
16 |
16 |
17 structure Quotient_Def: QUOTIENT_DEF = |
17 structure Quotient_Def: QUOTIENT_DEF = |
18 struct |
18 struct |
57 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' |
57 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' |
58 in |
58 in |
59 ((trm, thm), lthy'') |
59 ((trm, thm), lthy'') |
60 end |
60 end |
61 |
61 |
62 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy = |
62 fun quotdef_cmd (bindmx, (attr, (lhs_str, rhs_str))) lthy = |
63 let |
63 let |
64 val lhs = Syntax.read_term lthy lhs_str |
64 val lhs = Syntax.read_term lthy lhs_str |
65 val rhs = Syntax.read_term lthy rhs_str |
65 val rhs = Syntax.read_term lthy rhs_str |
66 val lthy' = Variable.declare_term lhs lthy |
66 val lthy' = Variable.declare_term lhs lthy |
67 val lthy'' = Variable.declare_term rhs lthy' |
67 val lthy'' = Variable.declare_term rhs lthy' |
68 in |
68 in |
69 quotient_def mx attr lhs rhs lthy'' |> snd |
69 case bindmx of |
|
70 SOME (b, mx) => quotient_def mx attr lhs rhs lthy'' |> snd |
|
71 | _ => quotient_def NoSyn attr lhs rhs lthy'' |> snd |
70 end |
72 end |
71 |
73 |
72 val quotdef_parser = |
74 val quotdef_parser = |
73 (SpecParse.opt_thm_name ":" -- |
75 (Scan.option (OuterParse.binding -- OuterParse.opt_mixfix' --| OuterParse.$$$ "where")) -- |
74 OuterParse.term) -- |
76 OuterParse.!!! (SpecParse.opt_thm_name ":" -- ((OuterParse.term --| OuterParse.$$$ "is") -- OuterParse.term)) |
75 (OuterParse.opt_mixfix' --| OuterParse.$$$ "is" -- |
|
76 OuterParse.term) |
|
77 |
77 |
78 val _ = OuterSyntax.local_theory "quotient_definition" |
78 val _ = |
79 "definition for constants over the quotient type" |
79 OuterSyntax.local_theory "quotient_definition" |
80 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |
80 "definition for constants over the quotient type" |
|
81 OuterKeyword.thy_decl (quotdef_parser >> (quotdef_cmd)) |
81 |
82 |
82 end; (* structure *) |
83 end; (* structure *) |