get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
signature QUOTIENT_DEF =sig datatype flag = absF | repF val get_fun: flag -> Proof.context -> typ * typ -> term val quotient_def: mixfix -> Attrib.binding -> term -> term -> Proof.context -> (term * thm) * local_theory val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) -> local_theory -> local_theoryend;structure Quotient_Def: QUOTIENT_DEF =structopen Quotient_Info;open Quotient_Type;(* wrapper for define *)fun define name mx attr rhs lthy =let val ((rhs, (_ , thm)), lthy') = Local_Theory.define ((name, mx), (attr, rhs)) lthyin ((rhs, thm), lthy')enddatatype flag = absF | repFfun negF absF = repF | negF repF = absFfun mk_identity ty = Const (@{const_name "id"}, ty --> ty)fun mk_compose flag (trm1, trm2) = case flag of absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1fun get_fun_aux lthy s fs =let val thy = ProofContext.theory_of lthy val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]) val info = maps_lookup thy s handle NotFound => raise excin list_comb (Const (#mapfun info, dummyT), fs)endfun get_const flag lthy _ qty =(* FIXME: check here that the type-constructors of _ 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')) => let val args = map (get_fun flag lthy) (tys ~~ tys') in if s = s' then get_fun_aux lthy s args else mk_compose flag (get_const flag lthy rty qty, get_fun_aux lthy s args) end | (TFree x, TFree x') => if x = x' then mk_identity qty else raise (LIFT_MATCH "get_fun (frees)") | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)") | _ => raise (LIFT_MATCH "get_fun (default)")(* interface and syntax setup *)(* the ML-interface takes a 4-tuple consisting of *)(* *)(* - the mixfix annotation *)(* - name and attributes of the meta eq *)(* - the new constant including its type *)(* - the rhs of the definition *)fun quotient_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'')endfun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy =let val lhs = Syntax.read_term lthy lhsstr val rhs = Syntax.read_term lthy rhsstrin quotient_def mx attr lhs rhs lthy |> sndendval _ = OuterKeyword.keyword "as";val quotdef_parser = (SpecParse.opt_thm_name ":" -- OuterParse.term) -- (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" -- OuterParse.term)val _ = OuterSyntax.local_theory "quotient_definition" "definition for constants over the quotient type" OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)end; (* structure *)