1 (*  Title:      quotient_def.thy

     2     Author:     Cezary Kaliszyk and Christian Urban

     3 

     4     Definitions for constants on quotient types.

     5 

     6 *)

     7 

     8 signature QUOTIENT_DEF =

     9 sig

    10   val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) ->

    11     local_theory -> (term * thm) * local_theory

    12 

    13   val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->

    14     local_theory -> (term * thm) * local_theory

    15 

    16   val quotient_lift_const: string * term -> local_theory -> (term * thm) * local_theory

    17 end;

    18 

    19 structure Quotient_Def: QUOTIENT_DEF =

    20 struct

    21 

    22 open Quotient_Info;

    23 open Quotient_Term;

    24 

    25 (** Interface and Syntax Setup **)

    26 

    27 (* The ML-interface for a quotient definition takes

    28    as argument:

    29 

    30     - an optional binding and mixfix annotation

    31     - attributes

    32     - the new constant as term

    33     - the rhs of the definition as term

    34 

    35    It returns the defined constant and its definition

    36    theorem; stores the data in the qconsts data slot.

    37 

    38    Restriction: At the moment the right-hand side of the

    39    definition must be a constant. Similarly the left-hand 

    40    side must be a constant.

    41 *)

    42 fun error_msg bind str = 

    43 let 

    44   val name = Binding.name_of bind

    45   val pos = Position.str_of (Binding.pos_of bind)

    46 in

    47   error ("Head of quotient_definition " ^ 

    48     (quote str) ^ " differs from declaration " ^ name ^ pos)

    49 end

    50 

    51 fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =

    52 let

    53   val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."

    54   val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"

    55   

    56   fun sanity_test NONE _ = true

    57     | sanity_test (SOME bind) str =

    58         if Name.of_binding bind = str then true

    59         else error_msg bind str

    60 

    61   val _ = sanity_test optbind lhs_str

    62 

    63   val qconst_bname = Binding.name lhs_str

    64   val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs

    65   val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)

    66   val (_, prop') = LocalDefs.cert_def lthy prop

    67   val (_, newrhs) = Primitive_Defs.abs_def prop'

    68 

    69   val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy

    70 

    71   (* data storage *)

    72   fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}

    73   fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)

    74   val lthy'' = Local_Theory.declaration true

    75                  (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'

    76 in

    77   ((trm, thm), lthy'')

    78 end

    79 

    80 fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =

    81 let

    82   val lhs = Syntax.read_term lthy lhs_str

    83   val rhs = Syntax.read_term lthy rhs_str

    84   val lthy' = Variable.declare_term lhs lthy

    85   val lthy'' = Variable.declare_term rhs lthy'

    86 in

    87   quotient_def (decl, (attr, (lhs, rhs))) lthy''

    88 end

    89 

    90 fun quotient_lift_const (b, t) ctxt =

    91   quotient_def ((NONE, NoSyn), (Attrib.empty_binding,

    92     (Quotient_Term.quotient_lift_const (b, t) ctxt, t))) ctxt

    93 

    94 local

    95   structure P = OuterParse;

    96 in

    97 

    98 val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where"

    99 

   100 val quotdef_parser =

   101   Scan.optional quotdef_decl (NONE, NoSyn) -- 

   102     P.!!! (SpecParse.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))

   103 end

   104 

   105 val _ =

   106   OuterSyntax.local_theory "quotient_definition"

   107     "definition for constants over the quotient type"

   108       OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))

   109 

   110 end; (* structure *)