src/HOL/Tools/Quotient/quotient_def.ML
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Sat Mar 27 14:48:46 2010 +0100 (2010-03-27)
changeset 35990 5ceedb86aa9d
parent 35788 f1deaca15ca3
child 36108 03aa51cf85a2
permissions -rw-r--r--
Automated lifting can be restricted to specific quotient types
     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: typ list -> string * term -> local_theory ->
    16     (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') = Local_Defs.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 qtys (b, t) ctxt =
    91   quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
    92     (Quotient_Term.quotient_lift_const qtys (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 *)