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 |
6 val quotient_def: mixfix -> Attrib.binding -> term -> term -> |
7 val quotient_def: mixfix -> Attrib.binding -> term -> term -> |
7 Proof.context -> (term * thm) * local_theory |
8 Proof.context -> (term * thm) * local_theory |
8 val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) -> |
9 val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) -> |
9 local_theory -> local_theory |
10 local_theory -> local_theory |
10 end; |
11 end; |
27 | negF repF = absF |
28 | negF repF = absF |
28 |
29 |
29 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
30 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
30 |
31 |
31 fun get_fun_aux lthy s fs = |
32 fun get_fun_aux lthy s fs = |
32 case (maps_lookup (ProofContext.theory_of lthy) s) of |
33 let |
33 SOME info => list_comb (Const (#mapfun info, dummyT), fs) |
34 val thy = ProofContext.theory_of lthy |
34 | NONE => raise |
35 val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]) |
35 (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."])) |
36 val info = maps_lookup thy s handle NotFound => raise exc |
|
37 in |
|
38 list_comb (Const (#mapfun info, dummyT), fs) |
|
39 end |
36 |
40 |
37 fun get_const flag lthy _ qty = |
41 fun get_const flag lthy _ qty = |
38 (* FIXME: check here that _ and qty are related *) |
42 (* FIXME: check here that _ and qty are related *) |
39 let |
43 let |
40 val thy = ProofContext.theory_of lthy |
44 val thy = ProofContext.theory_of lthy |
70 then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys')) |
74 then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys')) |
71 else get_const flag lthy rty qty |
75 else get_const flag lthy rty qty |
72 | (TFree x, TFree x') => |
76 | (TFree x, TFree x') => |
73 if x = x' |
77 if x = x' |
74 then mk_identity qty |
78 then mk_identity qty |
75 else raise (LIFT_MATCH "get_fun") |
79 else raise (LIFT_MATCH "get_fun (frees)") |
76 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun") |
80 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)") |
77 | _ => raise (LIFT_MATCH "get_fun") |
81 | _ => raise (LIFT_MATCH "get_fun (default)") |
78 |
82 |
79 (* interface and syntax setup *) |
83 (* interface and syntax setup *) |
80 |
84 |
81 (* the ML-interface takes a 4-tuple consisting of *) |
85 (* the ML-interface takes a 4-tuple consisting of *) |
82 (* *) |
86 (* *) |
83 (* - the mixfix annotation *) |
87 (* - the mixfix annotation *) |
84 (* - name and attributes of the meta eq *) |
88 (* - name and attributes of the meta eq *) |
85 (* - the new constant including its type *) |
89 (* - the new constant including its type *) |
86 (* - the rhs of the definition *) |
90 (* - the rhs of the definition *) |
|
91 |
87 fun quotient_def mx attr lhs rhs lthy = |
92 fun quotient_def mx attr lhs rhs lthy = |
88 let |
93 let |
89 val Free (lhs_str, lhs_ty) = lhs; |
94 val Free (lhs_str, lhs_ty) = lhs; |
90 val qconst_bname = Binding.name lhs_str; |
95 val qconst_bname = Binding.name lhs_str; |
91 val absrep_trm = get_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs |
96 val absrep_trm = get_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs |
113 |
118 |
114 val _ = OuterKeyword.keyword "as"; |
119 val _ = OuterKeyword.keyword "as"; |
115 |
120 |
116 val quotdef_parser = |
121 val quotdef_parser = |
117 (SpecParse.opt_thm_name ":" -- |
122 (SpecParse.opt_thm_name ":" -- |
118 OuterParse.term) -- |
123 OuterParse.term) -- |
119 (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" -- |
124 (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" -- |
120 OuterParse.term) |
125 OuterParse.term) |
121 |
126 |
122 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
127 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
123 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |
128 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |
124 |
129 |
125 end; (* structure *) |
130 end; (* structure *) |