1 |
1 |
2 signature QUOTIENT_DEF = |
2 signature QUOTIENT_DEF = |
3 sig |
3 sig |
4 datatype flag = absF | repF |
4 datatype flag = absF | repF |
5 val get_fun: flag -> Proof.context -> typ * typ -> term |
5 val get_fun: flag -> Proof.context -> typ * typ -> term |
6 val make_def: binding -> mixfix -> Attrib.binding -> term -> term -> |
6 val make_def: mixfix -> Attrib.binding -> term -> term -> |
7 Proof.context -> (term * thm) * local_theory |
7 Proof.context -> (term * thm) * local_theory |
8 |
8 val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) -> |
9 val quotdef: (binding * term * mixfix) * (Attrib.binding * term) -> |
|
10 local_theory -> (term * thm) * local_theory |
|
11 val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) -> |
|
12 local_theory -> local_theory |
9 local_theory -> local_theory |
13 end; |
10 end; |
14 |
11 |
15 structure Quotient_Def: QUOTIENT_DEF = |
12 structure Quotient_Def: QUOTIENT_DEF = |
16 struct |
13 struct |
77 then mk_identity qty |
74 then mk_identity qty |
78 else raise (LIFT_MATCH "get_fun") |
75 else raise (LIFT_MATCH "get_fun") |
79 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun") |
76 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun") |
80 | _ => raise (LIFT_MATCH "get_fun") |
77 | _ => raise (LIFT_MATCH "get_fun") |
81 |
78 |
82 fun make_def qconst_bname mx attr lhs rhs lthy = |
79 fun make_def mx attr lhs rhs lthy = |
83 let |
80 let |
84 val absrep_trm = get_fun absF lthy (fastype_of rhs, fastype_of lhs) $ rhs |
81 val Free (lhs_str, lhs_ty) = lhs; |
|
82 val qconst_bname = Binding.name lhs_str; |
|
83 val absrep_trm = get_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs |
85 |> Syntax.check_term lthy |
84 |> Syntax.check_term lthy |
86 val prop = Logic.mk_equals (lhs, absrep_trm) |
85 val prop = Logic.mk_equals (lhs, absrep_trm) |
87 val (_, prop') = LocalDefs.cert_def lthy prop |
86 val (_, prop') = LocalDefs.cert_def lthy prop |
88 val (_, newrhs) = Primitive_Defs.abs_def prop' |
87 val (_, newrhs) = Primitive_Defs.abs_def prop' |
89 |
88 |
90 val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy |
89 val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy |
91 |
90 |
92 fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm} |
91 fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm} |
93 val lthy'' = Local_Theory.declaration true |
92 val lthy'' = Local_Theory.declaration true |
94 (fn phi => |
93 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy' |
95 let |
|
96 val qconst_str = Binding.name_of qconst_bname |
|
97 in |
|
98 qconsts_update_gen qconst_str (qcinfo phi) |
|
99 end) lthy' |
|
100 in |
94 in |
101 ((trm, thm), lthy'') |
95 ((trm, thm), lthy'') |
102 end |
96 end |
103 |
97 |
104 (* interface and syntax setup *) |
98 (* interface and syntax setup *) |
109 (* - its type *) |
103 (* - its type *) |
110 (* - its mixfix annotation *) |
104 (* - its mixfix annotation *) |
111 (* - a meta-equation defining the constant, *) |
105 (* - a meta-equation defining the constant, *) |
112 (* and the attributes of for this meta-equality *) |
106 (* and the attributes of for this meta-equality *) |
113 |
107 |
114 fun quotdef ((bind, lhs, mx), (attr, rhs)) lthy = |
108 fun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy = |
115 make_def bind mx attr lhs rhs lthy |
|
116 |
|
117 fun quotdef_cmd ((bind, lhsstr, mx), (attr, rhsstr)) lthy = |
|
118 let |
109 let |
119 val lhs = Syntax.read_term lthy lhsstr |
110 val lhs = Syntax.read_term lthy lhsstr |
120 val rhs = Syntax.read_term lthy rhsstr |
111 val rhs = Syntax.read_term lthy rhsstr |
121 in |
112 in |
122 quotdef ((bind, lhs, mx), (attr, rhs)) lthy |> snd |
113 make_def mx attr lhs rhs lthy |> snd |
123 end |
114 end |
124 |
115 |
|
116 val _ = OuterKeyword.keyword "as"; |
|
117 |
125 val quotdef_parser = |
118 val quotdef_parser = |
126 (OuterParse.binding -- |
119 (SpecParse.opt_thm_name ":" -- |
127 (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.term -- |
120 OuterParse.term) -- |
128 OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) -- |
121 (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" -- |
129 (SpecParse.opt_thm_name ":" -- OuterParse.term) |
122 OuterParse.term) |
130 |
123 |
131 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
124 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
132 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |
125 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |
133 |
126 |
134 end; (* structure *) |
127 end; (* structure *) |