New syntax for definitions.
+ −
signature QUOTIENT_DEF =+ −
sig+ −
datatype flag = absF | repF+ −
val get_fun: flag -> Proof.context -> typ * typ -> term+ −
val make_def: mixfix -> Attrib.binding -> term -> term ->+ −
Proof.context -> (term * thm) * local_theory+ −
val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->+ −
local_theory -> local_theory+ −
end;+ −
+ −
structure Quotient_Def: QUOTIENT_DEF =+ −
struct+ −
+ −
(* wrapper for define *)+ −
fun define name mx attr rhs lthy =+ −
let+ −
val ((rhs, (_ , thm)), lthy') =+ −
Local_Theory.define ((name, mx), (attr, rhs)) lthy+ −
in+ −
((rhs, thm), lthy')+ −
end+ −
+ −
datatype flag = absF | repF+ −
+ −
fun negF absF = repF+ −
| negF repF = absF+ −
+ −
fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)+ −
+ −
fun get_fun_aux lthy s fs =+ −
case (maps_lookup (ProofContext.theory_of lthy) s) of+ −
SOME info => list_comb (Const (#mapfun info, dummyT), fs)+ −
| NONE => raise + −
(LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]))+ −
+ −
fun get_const flag lthy _ qty =+ −
(* FIXME: check here that _ and qty are related *)+ −
let + −
val thy = ProofContext.theory_of lthy+ −
val qty_name = Long_Name.base_name (fst (dest_Type qty))+ −
in+ −
case flag of+ −
absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)+ −
| repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)+ −
end+ −
+ −
+ −
(* calculates the aggregate abs and rep functions for a given type; + −
repF is for constants' arguments; absF is for constants;+ −
function types need to be treated specially, since repF and absF+ −
change *)+ −
+ −
fun get_fun flag lthy (rty, qty) =+ −
if rty = qty then mk_identity qty else+ −
case (rty, qty) of + −
(Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>+ −
let+ −
val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1')+ −
val fs_ty2 = get_fun flag lthy (ty2, ty2')+ −
in + −
get_fun_aux lthy "fun" [fs_ty1, fs_ty2]+ −
end + −
| (Type (s, []), Type (s', [])) =>+ −
if s = s'+ −
then mk_identity qty + −
else get_const flag lthy rty qty+ −
| (Type (s, tys), Type (s', tys')) =>+ −
if s = s'+ −
then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys'))+ −
else get_const flag lthy rty qty+ −
| (TFree x, TFree x') =>+ −
if x = x'+ −
then mk_identity qty + −
else raise (LIFT_MATCH "get_fun")+ −
| (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")+ −
| _ => raise (LIFT_MATCH "get_fun")+ −
+ −
fun make_def mx attr lhs rhs lthy =+ −
let+ −
val Free (lhs_str, lhs_ty) = lhs;+ −
val qconst_bname = Binding.name lhs_str;+ −
val absrep_trm = get_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs+ −
|> Syntax.check_term lthy+ −
val prop = Logic.mk_equals (lhs, absrep_trm)+ −
val (_, prop') = LocalDefs.cert_def lthy prop+ −
val (_, newrhs) = Primitive_Defs.abs_def prop'+ −
+ −
val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy+ −
+ −
fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}+ −
val lthy'' = Local_Theory.declaration true+ −
(fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'+ −
in+ −
((trm, thm), lthy'')+ −
end+ −
+ −
(* interface and syntax setup *)+ −
+ −
(* the ML-interface takes a 5-tuple consisting of *)+ −
(* *)+ −
(* - the name of the constant to be lifted *)+ −
(* - its type *)+ −
(* - its mixfix annotation *)+ −
(* - a meta-equation defining the constant, *)+ −
(* and the attributes of for this meta-equality *)+ −
+ −
fun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy = + −
let+ −
val lhs = Syntax.read_term lthy lhsstr+ −
val rhs = Syntax.read_term lthy rhsstr+ −
in+ −
make_def mx attr lhs rhs lthy |> snd+ −
end+ −
+ −
val _ = OuterKeyword.keyword "as";+ −
+ −
val quotdef_parser =+ −
(SpecParse.opt_thm_name ":" --+ −
OuterParse.term) --+ −
(OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --+ −
OuterParse.term)+ −
+ −
val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"+ −
OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)+ −
+ −
end; (* structure *)+ −
+ −
open Quotient_Def;+ −
+ −
+ −