src/HOL/Tools/Quotient/quotient_def.ML
author kuncar
Fri Dec 09 14:14:37 2011 +0100 (2011-12-09)
changeset 45797 977cf00fb8d3
parent 45598 87a2624f57e4
child 45826 67110d6c66de
permissions -rw-r--r--
make ctxt the first parameter
     1 (*  Title:      HOL/Tools/Quotient/quotient_def.ML
     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:
    10     (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
    11     local_theory -> Quotient_Info.quotconsts * local_theory
    12 
    13   val quotient_def_cmd:
    14     (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
    15     local_theory -> Quotient_Info.quotconsts * local_theory
    16 
    17   val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
    18     Quotient_Info.quotconsts * local_theory
    19 end;
    20 
    21 structure Quotient_Def: QUOTIENT_DEF =
    22 struct
    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 stores the qconst_info in the quotconsts data slot.
    35 
    36    Restriction: At the moment the left- and right-hand
    37    side of the definition must be a constant.
    38 *)
    39 fun error_msg bind str =
    40   let
    41     val name = Binding.name_of bind
    42     val pos = Position.str_of (Binding.pos_of bind)
    43   in
    44     error ("Head of quotient_definition " ^
    45       quote str ^ " differs from declaration " ^ name ^ pos)
    46   end
    47 
    48 fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy =
    49   let
    50     val (vars, ctxt) = prep_vars (the_list raw_var) lthy
    51     val T_opt = (case vars of [(_, SOME T, _)] => SOME T | _ => NONE)
    52     val lhs = prep_term T_opt ctxt lhs_raw
    53     val rhs = prep_term NONE ctxt rhs_raw
    54 
    55     val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
    56     val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
    57     val _ = if is_Const rhs then () else warning "The definiens is not a constant"
    58 
    59     val var =
    60       (case vars of 
    61         [] => (Binding.name lhs_str, NoSyn)
    62       | [(binding, _, mx)] =>
    63           if Variable.check_name binding = lhs_str then (binding, mx)
    64           else error_msg binding lhs_str
    65       | _ => raise Match)
    66 
    67     val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, lhs_ty) $ rhs
    68     val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
    69     val (_, prop') = Local_Defs.cert_def lthy prop
    70     val (_, newrhs) = Local_Defs.abs_def prop'
    71 
    72     val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy
    73 
    74     (* data storage *)
    75     val qconst_data = {qconst = trm, rconst = rhs, def = thm}
    76 
    77     val lthy'' = lthy'
    78       |> Local_Theory.declaration {syntax = false, pervasive = true}
    79         (fn phi =>
    80           (case Quotient_Info.transform_quotconsts phi qconst_data of
    81             qcinfo as {qconst = Const (c, _), ...} =>
    82               Quotient_Info.update_quotconsts c qcinfo
    83           | _ => I));
    84   in
    85     (qconst_data, lthy'')
    86   end
    87 
    88 fun check_term' cnstr ctxt =
    89   Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I)
    90 
    91 fun read_term' cnstr ctxt =
    92   check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt
    93 
    94 val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term'
    95 val quotient_def_cmd = gen_quotient_def Proof_Context.read_vars read_term'
    96 
    97 
    98 (* a wrapper for automatically lifting a raw constant *)
    99 fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
   100   let
   101     val rty = fastype_of rconst
   102     val qty = Quotient_Term.derive_qtyp ctxt qtys rty
   103     val lhs = Free (qconst_name, qty)
   104   in
   105     quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
   106   end
   107 
   108 (* parser and command *)
   109 val quotdef_parser =
   110   Scan.option Parse_Spec.constdecl --
   111     Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
   112 
   113 val _ =
   114   Outer_Syntax.local_theory "quotient_definition"
   115     "definition for constants over the quotient type"
   116       Keyword.thy_decl (quotdef_parser >> (snd oo quotient_def_cmd))
   117 
   118 end; (* structure *)