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
wenzelm@35788
     1
(*  Title:      HOL/Tools/Quotient/quotient_def.thy
kaliszyk@35222
     2
    Author:     Cezary Kaliszyk and Christian Urban
kaliszyk@35222
     3
wenzelm@35788
     4
Definitions for constants on quotient types.
kaliszyk@35222
     5
*)
kaliszyk@35222
     6
kaliszyk@35222
     7
signature QUOTIENT_DEF =
kaliszyk@35222
     8
sig
kaliszyk@35222
     9
  val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) ->
kaliszyk@35222
    10
    local_theory -> (term * thm) * local_theory
kaliszyk@35222
    11
kaliszyk@35222
    12
  val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
kaliszyk@35222
    13
    local_theory -> (term * thm) * local_theory
kaliszyk@35222
    14
kaliszyk@35990
    15
  val quotient_lift_const: typ list -> string * term -> local_theory ->
kaliszyk@35990
    16
    (term * thm) * local_theory
kaliszyk@35222
    17
end;
kaliszyk@35222
    18
kaliszyk@35222
    19
structure Quotient_Def: QUOTIENT_DEF =
kaliszyk@35222
    20
struct
kaliszyk@35222
    21
kaliszyk@35222
    22
open Quotient_Info;
kaliszyk@35222
    23
open Quotient_Term;
kaliszyk@35222
    24
kaliszyk@35222
    25
(** Interface and Syntax Setup **)
kaliszyk@35222
    26
kaliszyk@35222
    27
(* The ML-interface for a quotient definition takes
kaliszyk@35222
    28
   as argument:
kaliszyk@35222
    29
kaliszyk@35222
    30
    - an optional binding and mixfix annotation
kaliszyk@35222
    31
    - attributes
kaliszyk@35222
    32
    - the new constant as term
kaliszyk@35222
    33
    - the rhs of the definition as term
kaliszyk@35222
    34
kaliszyk@35222
    35
   It returns the defined constant and its definition
kaliszyk@35222
    36
   theorem; stores the data in the qconsts data slot.
kaliszyk@35222
    37
kaliszyk@35222
    38
   Restriction: At the moment the right-hand side of the
kaliszyk@35222
    39
   definition must be a constant. Similarly the left-hand 
kaliszyk@35222
    40
   side must be a constant.
kaliszyk@35222
    41
*)
kaliszyk@35222
    42
fun error_msg bind str = 
kaliszyk@35222
    43
let 
kaliszyk@35222
    44
  val name = Binding.name_of bind
kaliszyk@35222
    45
  val pos = Position.str_of (Binding.pos_of bind)
kaliszyk@35222
    46
in
kaliszyk@35222
    47
  error ("Head of quotient_definition " ^ 
kaliszyk@35222
    48
    (quote str) ^ " differs from declaration " ^ name ^ pos)
kaliszyk@35222
    49
end
kaliszyk@35222
    50
kaliszyk@35222
    51
fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
kaliszyk@35222
    52
let
kaliszyk@35222
    53
  val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
kaliszyk@35222
    54
  val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
kaliszyk@35222
    55
  
kaliszyk@35222
    56
  fun sanity_test NONE _ = true
kaliszyk@35222
    57
    | sanity_test (SOME bind) str =
kaliszyk@35222
    58
        if Name.of_binding bind = str then true
kaliszyk@35222
    59
        else error_msg bind str
kaliszyk@35222
    60
kaliszyk@35222
    61
  val _ = sanity_test optbind lhs_str
kaliszyk@35222
    62
kaliszyk@35222
    63
  val qconst_bname = Binding.name lhs_str
kaliszyk@35222
    64
  val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
kaliszyk@35222
    65
  val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
wenzelm@35624
    66
  val (_, prop') = Local_Defs.cert_def lthy prop
kaliszyk@35222
    67
  val (_, newrhs) = Primitive_Defs.abs_def prop'
kaliszyk@35222
    68
kaliszyk@35222
    69
  val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
kaliszyk@35222
    70
kaliszyk@35222
    71
  (* data storage *)
kaliszyk@35222
    72
  fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
kaliszyk@35222
    73
  fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
kaliszyk@35222
    74
  val lthy'' = Local_Theory.declaration true
kaliszyk@35222
    75
                 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
kaliszyk@35222
    76
in
kaliszyk@35222
    77
  ((trm, thm), lthy'')
kaliszyk@35222
    78
end
kaliszyk@35222
    79
kaliszyk@35222
    80
fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =
kaliszyk@35222
    81
let
kaliszyk@35222
    82
  val lhs = Syntax.read_term lthy lhs_str
kaliszyk@35222
    83
  val rhs = Syntax.read_term lthy rhs_str
kaliszyk@35222
    84
  val lthy' = Variable.declare_term lhs lthy
kaliszyk@35222
    85
  val lthy'' = Variable.declare_term rhs lthy'
kaliszyk@35222
    86
in
kaliszyk@35222
    87
  quotient_def (decl, (attr, (lhs, rhs))) lthy''
kaliszyk@35222
    88
end
kaliszyk@35222
    89
kaliszyk@35990
    90
fun quotient_lift_const qtys (b, t) ctxt =
kaliszyk@35222
    91
  quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
kaliszyk@35990
    92
    (Quotient_Term.quotient_lift_const qtys (b, t) ctxt, t))) ctxt
kaliszyk@35222
    93
kaliszyk@35222
    94
local
kaliszyk@35222
    95
  structure P = OuterParse;
kaliszyk@35222
    96
in
kaliszyk@35222
    97
kaliszyk@35222
    98
val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where"
kaliszyk@35222
    99
kaliszyk@35222
   100
val quotdef_parser =
kaliszyk@35222
   101
  Scan.optional quotdef_decl (NONE, NoSyn) -- 
kaliszyk@35222
   102
    P.!!! (SpecParse.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
kaliszyk@35222
   103
end
kaliszyk@35222
   104
kaliszyk@35222
   105
val _ =
kaliszyk@35222
   106
  OuterSyntax.local_theory "quotient_definition"
kaliszyk@35222
   107
    "definition for constants over the quotient type"
kaliszyk@35222
   108
      OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
kaliszyk@35222
   109
kaliszyk@35222
   110
end; (* structure *)