1 (*  Title:      HOL/Tools/Quotient/quotient_def.thy

     2     Author:     Cezary Kaliszyk and Christian Urban

     3 

     4 Definitions for constants on quotient types.

     5 *)

     6 

     7 signature QUOTIENT_DEF =

     8 sig

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

    10     local_theory -> (term * thm) * local_theory

    11 

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

    13     local_theory -> (term * thm) * local_theory

    14 

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

    16 end;

    17 

    18 structure Quotient_Def: QUOTIENT_DEF =

    19 struct

    20 

    21 open Quotient_Info;

    22 open Quotient_Term;

    23 

    24 (** Interface and Syntax Setup **)

    25 

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

    27    as argument:

    28 

    29     - an optional binding and mixfix annotation

    30     - attributes

    31     - the new constant as term

    32     - the rhs of the definition as term

    33 

    34    It returns the defined constant and its definition

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

    36 

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

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

    39    side must be a constant.

    40 *)

    41 fun error_msg bind str = 

    42 let 

    43   val name = Binding.name_of bind

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

    45 in

    46   error ("Head of quotient_definition " ^ 

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

    48 end

    49 

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

    51 let

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

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

    54   

    55   fun sanity_test NONE _ = true

    56     | sanity_test (SOME bind) str =

    57         if Name.of_binding bind = str then true

    58         else error_msg bind str

    59 

    60   val _ = sanity_test optbind lhs_str

    61 

    62   val qconst_bname = Binding.name lhs_str

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

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

    65   val (_, prop') = Local_Defs.cert_def lthy prop

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

    67 

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

    69 

    70   (* data storage *)

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

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

    73   val lthy'' = Local_Theory.declaration true

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

    75 in

    76   ((trm, thm), lthy'')

    77 end

    78 

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

    80 let

    81   val lhs = Syntax.read_term lthy lhs_str

    82   val rhs = Syntax.read_term lthy rhs_str

    83   val lthy' = Variable.declare_term lhs lthy

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

    85 in

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

    87 end

    88 

    89 fun quotient_lift_const (b, t) ctxt =

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

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

    92 

    93 local

    94   structure P = OuterParse;

    95 in

    96 

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

    98 

    99 val quotdef_parser =

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

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

   102 end

   103 

   104 val _ =

   105   OuterSyntax.local_theory "quotient_definition"

   106     "definition for constants over the quotient type"

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

   108 

   109 end; (* structure *)