1 (* Title: HOL/Tools/Quotient/quotient_def.ML
2 Author: Cezary Kaliszyk and Christian Urban
4 Definitions for constants on quotient types.
7 signature QUOTIENT_DEF =
10 (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
11 local_theory -> Quotient_Info.quotconsts * local_theory
14 (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
15 local_theory -> Quotient_Info.quotconsts * local_theory
17 val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
18 Quotient_Info.quotconsts * local_theory
21 structure Quotient_Def: QUOTIENT_DEF =
24 (** Interface and Syntax Setup **)
26 (* The ML-interface for a quotient definition takes
29 - an optional binding and mixfix annotation
31 - the new constant as term
32 - the rhs of the definition as term
34 It stores the qconst_info in the quotconsts data slot.
36 Restriction: At the moment the left- and right-hand
37 side of the definition must be a constant.
39 fun error_msg bind str =
41 val name = Binding.name_of bind
42 val pos = Position.str_of (Binding.pos_of bind)
44 error ("Head of quotient_definition " ^
45 quote str ^ " differs from declaration " ^ name ^ pos)
48 fun gen_quotient_def prep_vars prep_term (raw_var, ((name, atts), (lhs_raw, rhs_raw))) lthy =
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
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"
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
67 val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, lhs_ty) $ rhs
68 val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm))
69 val (_, prop') = Local_Defs.cert_def lthy prop
70 val (_, newrhs) = Local_Defs.abs_def prop'
72 val ((trm, (_ , thm)), lthy') =
73 Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy
76 val qconst_data = {qconst = trm, rconst = rhs, def = thm}
79 |> Local_Theory.declaration {syntax = false, pervasive = true}
81 (case Quotient_Info.transform_quotconsts phi qconst_data of
82 qcinfo as {qconst = Const (c, _), ...} =>
83 Quotient_Info.update_quotconsts c qcinfo
89 fun check_term' cnstr ctxt =
90 Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I)
92 fun read_term' cnstr ctxt =
93 check_term' cnstr ctxt o Syntax.parse_term ctxt
95 val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term'
96 val quotient_def_cmd = gen_quotient_def Proof_Context.read_vars read_term'
99 (* a wrapper for automatically lifting a raw constant *)
100 fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
102 val rty = fastype_of rconst
103 val qty = Quotient_Term.derive_qtyp ctxt qtys rty
104 val lhs = Free (qconst_name, qty)
106 quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
109 (* parser and command *)
111 Scan.option Parse_Spec.constdecl --
112 Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
115 Outer_Syntax.local_theory "quotient_definition"
116 "definition for constants over the quotient type"
117 Keyword.thy_decl (quotdef_parser >> (snd oo quotient_def_cmd))