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