src/HOL/Tools/Quotient/quotient_def.ML
changeset 45598 87a2624f57e4
parent 45292 90106a351a11
child 45797 977cf00fb8d3
equal deleted inserted replaced
45597:ce23193a42a4 45598:87a2624f57e4
     4 Definitions for constants on quotient types.
     4 Definitions for constants on quotient types.
     5 *)
     5 *)
     6 
     6 
     7 signature QUOTIENT_DEF =
     7 signature QUOTIENT_DEF =
     8 sig
     8 sig
     9   val quotient_def: (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
     9   val quotient_def:
       
    10     (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
    10     local_theory -> Quotient_Info.quotconsts * local_theory
    11     local_theory -> Quotient_Info.quotconsts * local_theory
    11 
    12 
    12   val quotdef_cmd: (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
    13   val quotient_def_cmd:
       
    14     (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
    13     local_theory -> Quotient_Info.quotconsts * local_theory
    15     local_theory -> Quotient_Info.quotconsts * local_theory
    14 
    16 
    15   val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
    17   val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
    16     Quotient_Info.quotconsts * local_theory
    18     Quotient_Info.quotconsts * local_theory
    17 end;
    19 end;
    83     (qconst_data, lthy'')
    85     (qconst_data, lthy'')
    84   end
    86   end
    85 
    87 
    86 fun check_term' cnstr ctxt =
    88 fun check_term' cnstr ctxt =
    87   Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I)
    89   Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I)
    88 fun read_term' cnstr ctxt = check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt
    90 
       
    91 fun read_term' cnstr ctxt =
       
    92   check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt
    89 
    93 
    90 val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term'
    94 val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term'
    91 val quotdef_cmd = gen_quotient_def Proof_Context.read_vars read_term'
    95 val quotient_def_cmd = gen_quotient_def Proof_Context.read_vars read_term'
    92 
    96 
    93 
    97 
    94 (* a wrapper for automatically lifting a raw constant *)
    98 (* a wrapper for automatically lifting a raw constant *)
    95 fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
    99 fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
    96   let
   100   let
   107     Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
   111     Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
   108 
   112 
   109 val _ =
   113 val _ =
   110   Outer_Syntax.local_theory "quotient_definition"
   114   Outer_Syntax.local_theory "quotient_definition"
   111     "definition for constants over the quotient type"
   115     "definition for constants over the quotient type"
   112       Keyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
   116       Keyword.thy_decl (quotdef_parser >> (snd oo quotient_def_cmd))
   113 
   117 
   114 end; (* structure *)
   118 end; (* structure *)