equal
deleted
inserted
replaced
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: (Attrib.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: (Attrib.binding * mixfix) option * (Attrib.binding * (string * string)) -> |
14 local_theory -> local_theory |
14 local_theory -> local_theory |
15 end; |
15 end; |
35 |
35 |
36 Restriction: At the moment the right-hand side must |
36 Restriction: At the moment the right-hand side must |
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 mx 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 |
42 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
46 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" |
47 val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
44 |
48 |
45 val qconst_bname = Binding.name lhs_str |
49 val qconst_bname = Binding.name lhs_str |
46 val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs |
50 val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs |
64 val lhs = Syntax.read_term lthy lhs_str |
68 val lhs = Syntax.read_term lthy lhs_str |
65 val rhs = Syntax.read_term lthy rhs_str |
69 val rhs = Syntax.read_term lthy rhs_str |
66 val lthy' = Variable.declare_term lhs lthy |
70 val lthy' = Variable.declare_term lhs lthy |
67 val lthy'' = Variable.declare_term rhs lthy' |
71 val lthy'' = Variable.declare_term rhs lthy' |
68 in |
72 in |
69 case bindmx of |
73 quotient_def (bindmx, (attr, (lhs, rhs))) lthy'' |> snd |
70 SOME (b, mx) => quotient_def mx attr lhs rhs lthy'' |> snd |
|
71 | _ => quotient_def NoSyn attr lhs rhs lthy'' |> snd |
|
72 end |
74 end |
73 |
75 |
|
76 val binding_mixfix_parser = OuterParse.binding -- OuterParse.opt_mixfix' --| OuterParse.$$$ "where" |
74 val quotdef_parser = |
77 val quotdef_parser = |
75 (Scan.option (OuterParse.binding -- OuterParse.opt_mixfix' --| OuterParse.$$$ "where")) -- |
78 (Scan.option binding_mixfix_parser) -- |
76 OuterParse.!!! (SpecParse.opt_thm_name ":" -- ((OuterParse.term --| OuterParse.$$$ "is") -- OuterParse.term)) |
79 OuterParse.!!! (SpecParse.opt_thm_name ":" -- ((OuterParse.term --| OuterParse.$$$ "is") -- OuterParse.term)) |
77 |
80 |
78 val _ = |
81 val _ = |
79 OuterSyntax.local_theory "quotient_definition" |
82 OuterSyntax.local_theory "quotient_definition" |
80 "definition for constants over the quotient type" |
83 "definition for constants over the quotient type" |