(*  Title:      quotient_def.thy+
−
    Author:     Cezary Kaliszyk and Christian Urban+
−
+
−
    Definitions for constants on quotient types.+
−
+
−
*)+
−
+
−
signature QUOTIENT_DEF =+
−
sig+
−
  val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) ->+
−
    local_theory -> (term * thm) * local_theory+
−
+
−
  val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->+
−
    local_theory -> (term * thm) * local_theory+
−
end;+
−
+
−
structure Quotient_Def: QUOTIENT_DEF =+
−
struct+
−
+
−
open Quotient_Info;+
−
open Quotient_Term;+
−
+
−
(** Interface and Syntax Setup **)+
−
+
−
(* The ML-interface for a quotient definition takes+
−
   as argument:+
−
+
−
    - an optional binding and mixfix annotation+
−
    - attributes+
−
    - the new constant as term+
−
    - the rhs of the definition as term+
−
+
−
   It returns the defined constant and its definition+
−
   theorem; stores the data in the qconsts data slot.+
−
+
−
   Restriction: At the moment the right-hand side of the+
−
   definition must be a constant. Similarly the left-hand +
−
   side must be a constant.+
−
*)+
−
fun error_msg bind str = +
−
let +
−
  val name = Binding.name_of bind+
−
  val pos = Position.str_of (Binding.pos_of bind)+
−
in+
−
  error ("Head of quotient_definition " ^ +
−
    (quote str) ^ " differs from declaration " ^ name ^ pos)+
−
end+
−
+
−
fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =+
−
let+
−
  val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."+
−
  val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"+
−
  +
−
  fun sanity_test NONE _ = true+
−
    | sanity_test (SOME bind) str =+
−
        if Name.of_binding bind = str then true+
−
        else error_msg bind str+
−
+
−
  val _ = sanity_test optbind lhs_str+
−
+
−
  val qconst_bname = Binding.name lhs_str+
−
  val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs+
−
  val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)+
−
  val (_, prop') = LocalDefs.cert_def lthy prop+
−
  val (_, newrhs) = Primitive_Defs.abs_def prop'+
−
+
−
  val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy+
−
+
−
  (* data storage *)+
−
  fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}+
−
  fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)+
−
  val lthy'' = Local_Theory.declaration true+
−
                 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'+
−
in+
−
  ((trm, thm), lthy'')+
−
end+
−
+
−
fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =+
−
let+
−
  val lhs = Syntax.read_term lthy lhs_str+
−
  val rhs = Syntax.read_term lthy rhs_str+
−
  val lthy' = Variable.declare_term lhs lthy+
−
  val lthy'' = Variable.declare_term rhs lthy'+
−
in+
−
  quotient_def (decl, (attr, (lhs, rhs))) lthy''+
−
end+
−
+
−
local+
−
  structure P = OuterParse;+
−
in+
−
+
−
val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where"+
−
+
−
val quotdef_parser =+
−
  Scan.optional quotdef_decl (NONE, NoSyn) -- +
−
    P.!!! (SpecParse.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))+
−
end+
−
+
−
val _ =+
−
  OuterSyntax.local_theory "quotient_definition"+
−
    "definition for constants over the quotient type"+
−
      OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))+
−
+
−
end; (* structure *)+
−