src/HOL/HOLCF/Tools/domaindef.ML
author huffman
Sun Dec 19 18:15:21 2010 -0800 (2010-12-19)
changeset 41296 6aaf80ea9715
parent 41292 2b7bc8d9fd6e
child 41436 480978f80eae
permissions -rw-r--r--
switch to transparent ascription, to avoid warning messages
     1 (*  Title:      HOLCF/Tools/repdef.ML
     2     Author:     Brian Huffman
     3 
     4 Defining representable domains using algebraic deflations.
     5 *)
     6 
     7 signature DOMAINDEF =
     8 sig
     9   type rep_info =
    10     {
    11       emb_def : thm,
    12       prj_def : thm,
    13       defl_def : thm,
    14       liftemb_def : thm,
    15       liftprj_def : thm,
    16       liftdefl_def : thm,
    17       DEFL : thm
    18     }
    19 
    20   val add_domaindef: bool -> binding option -> binding * (string * sort) list * mixfix ->
    21     term -> (binding * binding) option -> theory ->
    22     (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory
    23 
    24   val domaindef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string
    25     * (binding * binding) option -> theory -> theory
    26 end
    27 
    28 structure Domaindef : DOMAINDEF =
    29 struct
    30 
    31 open HOLCF_Library
    32 
    33 infixr 6 ->>
    34 infix -->>
    35 
    36 (** type definitions **)
    37 
    38 type rep_info =
    39   {
    40     emb_def : thm,
    41     prj_def : thm,
    42     defl_def : thm,
    43     liftemb_def : thm,
    44     liftprj_def : thm,
    45     liftdefl_def : thm,
    46     DEFL : thm
    47   }
    48 
    49 (* building types and terms *)
    50 
    51 val udomT = @{typ udom}
    52 val deflT = @{typ "udom defl"}
    53 val udeflT = @{typ "udom u defl"}
    54 fun emb_const T = Const (@{const_name emb}, T ->> udomT)
    55 fun prj_const T = Const (@{const_name prj}, udomT ->> T)
    56 fun defl_const T = Const (@{const_name defl}, Term.itselfT T --> deflT)
    57 fun liftemb_const T = Const (@{const_name liftemb}, mk_upT T ->> mk_upT udomT)
    58 fun liftprj_const T = Const (@{const_name liftprj}, mk_upT udomT ->> mk_upT T)
    59 fun liftdefl_const T = Const (@{const_name liftdefl}, Term.itselfT T --> udeflT)
    60 
    61 fun mk_u_map t =
    62   let
    63     val (T, U) = dest_cfunT (fastype_of t)
    64     val u_map_type = (T ->> U) ->> (mk_upT T ->> mk_upT U)
    65     val u_map_const = Const (@{const_name u_map}, u_map_type)
    66   in
    67     mk_capply (u_map_const, t)
    68   end
    69 
    70 fun mk_cast (t, x) =
    71   capply_const (udomT, udomT)
    72   $ (capply_const (deflT, udomT ->> udomT) $ @{term "cast :: udom defl -> udom -> udom"} $ t)
    73   $ x
    74 
    75 (* manipulating theorems *)
    76 
    77 (* proving class instances *)
    78 
    79 fun declare_type_name a =
    80   Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)))
    81 
    82 fun gen_add_domaindef
    83       (prep_term: Proof.context -> 'a -> term)
    84       (def: bool)
    85       (name: binding)
    86       (typ as (tname, raw_args, mx) : binding * (string * sort) list * mixfix)
    87       (raw_defl: 'a)
    88       (opt_morphs: (binding * binding) option)
    89       (thy: theory)
    90     : (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory =
    91   let
    92     val _ = Theory.requires thy "Domain" "domaindefs"
    93 
    94     (*rhs*)
    95     val tmp_ctxt =
    96       ProofContext.init_global thy
    97       |> fold (Variable.declare_typ o TFree) raw_args
    98     val defl = prep_term tmp_ctxt raw_defl
    99     val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl
   100 
   101     val deflT = Term.fastype_of defl
   102     val _ = if deflT = @{typ "udom defl"} then ()
   103             else error ("Not type defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT))
   104 
   105     (*lhs*)
   106     val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt) raw_args
   107     val lhs_sorts = map snd lhs_tfrees
   108     val full_tname = Sign.full_name thy tname
   109     val newT = Type (full_tname, map TFree lhs_tfrees)
   110 
   111     (*morphisms*)
   112     val morphs = opt_morphs
   113       |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
   114 
   115     (*set*)
   116     val set = @{term "defl_set :: udom defl => udom => bool"} $ defl
   117 
   118     (*pcpodef*)
   119     val tac1 = rtac @{thm defl_set_bottom} 1
   120     val tac2 = rtac @{thm adm_defl_set} 1
   121     val ((info, cpo_info, pcpo_info), thy) = thy
   122       |> Cpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2)
   123 
   124     (*definitions*)
   125     val Rep_const = Const (#Rep_name (#1 info), newT --> udomT)
   126     val Abs_const = Const (#Abs_name (#1 info), udomT --> newT)
   127     val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const)
   128     val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $
   129       Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0)))
   130     val defl_eqn = Logic.mk_equals (defl_const newT,
   131       Abs ("x", Term.itselfT newT, defl))
   132     val liftemb_eqn =
   133       Logic.mk_equals (liftemb_const newT, mk_u_map (emb_const newT))
   134     val liftprj_eqn =
   135       Logic.mk_equals (liftprj_const newT, mk_u_map (prj_const newT))
   136     val liftdefl_eqn =
   137       Logic.mk_equals (liftdefl_const newT,
   138         Abs ("t", Term.itselfT newT,
   139           mk_capply (@{const pdefl}, defl_const newT $ Logic.mk_type newT)))
   140 
   141     val name_def = Binding.suffix_name "_def" name
   142     val emb_bind = (Binding.prefix_name "emb_" name_def, [])
   143     val prj_bind = (Binding.prefix_name "prj_" name_def, [])
   144     val defl_bind = (Binding.prefix_name "defl_" name_def, [])
   145     val liftemb_bind = (Binding.prefix_name "liftemb_" name_def, [])
   146     val liftprj_bind = (Binding.prefix_name "liftprj_" name_def, [])
   147     val liftdefl_bind = (Binding.prefix_name "liftdefl_" name_def, [])
   148 
   149     (*instantiate class rep*)
   150     val lthy = thy
   151       |> Class.instantiation ([full_tname], lhs_tfrees, @{sort domain})
   152     val ((_, (_, emb_ldef)), lthy) =
   153         Specification.definition (NONE, (emb_bind, emb_eqn)) lthy
   154     val ((_, (_, prj_ldef)), lthy) =
   155         Specification.definition (NONE, (prj_bind, prj_eqn)) lthy
   156     val ((_, (_, defl_ldef)), lthy) =
   157         Specification.definition (NONE, (defl_bind, defl_eqn)) lthy
   158     val ((_, (_, liftemb_ldef)), lthy) =
   159         Specification.definition (NONE, (liftemb_bind, liftemb_eqn)) lthy
   160     val ((_, (_, liftprj_ldef)), lthy) =
   161         Specification.definition (NONE, (liftprj_bind, liftprj_eqn)) lthy
   162     val ((_, (_, liftdefl_ldef)), lthy) =
   163         Specification.definition (NONE, (liftdefl_bind, liftdefl_eqn)) lthy
   164     val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy)
   165     val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef
   166     val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef
   167     val defl_def = singleton (ProofContext.export lthy ctxt_thy) defl_ldef
   168     val liftemb_def = singleton (ProofContext.export lthy ctxt_thy) liftemb_ldef
   169     val liftprj_def = singleton (ProofContext.export lthy ctxt_thy) liftprj_ldef
   170     val liftdefl_def = singleton (ProofContext.export lthy ctxt_thy) liftdefl_ldef
   171     val type_definition_thm =
   172       Raw_Simplifier.rewrite_rule
   173         (the_list (#set_def (#2 info)))
   174         (#type_definition (#2 info))
   175     val typedef_thms =
   176       [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def,
   177       liftemb_def, liftprj_def, liftdefl_def]
   178     val thy = lthy
   179       |> Class.prove_instantiation_instance
   180           (K (Tactic.rtac (@{thm typedef_domain_class} OF typedef_thms) 1))
   181       |> Local_Theory.exit_global
   182 
   183     (*other theorems*)
   184     val defl_thm' = Thm.transfer thy defl_def
   185     val (DEFL_thm, thy) = thy
   186       |> Sign.add_path (Binding.name_of name)
   187       |> Global_Theory.add_thm
   188          ((Binding.prefix_name "DEFL_" name,
   189           Drule.zero_var_indexes (@{thm typedef_DEFL} OF [defl_thm'])), [])
   190       ||> Sign.restore_naming thy
   191 
   192     val rep_info =
   193       { emb_def = emb_def, prj_def = prj_def, defl_def = defl_def,
   194         liftemb_def = liftemb_def, liftprj_def = liftprj_def,
   195         liftdefl_def = liftdefl_def, DEFL = DEFL_thm }
   196   in
   197     ((info, cpo_info, pcpo_info, rep_info), thy)
   198   end
   199   handle ERROR msg =>
   200     cat_error msg ("The error(s) above occurred in domaindef " ^ quote (Binding.str_of name))
   201 
   202 fun add_domaindef def opt_name typ defl opt_morphs thy =
   203   let
   204     val name = the_default (#1 typ) opt_name
   205   in
   206     gen_add_domaindef Syntax.check_term def name typ defl opt_morphs thy
   207   end
   208 
   209 fun domaindef_cmd ((def, name), (b, raw_args, mx), A, morphs) thy =
   210   let
   211     val ctxt = ProofContext.init_global thy
   212     val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args
   213   in snd (gen_add_domaindef Syntax.read_term def name (b, args, mx) A morphs thy) end
   214 
   215 
   216 (** outer syntax **)
   217 
   218 val domaindef_decl =
   219   Scan.optional (Parse.$$$ "(" |--
   220       ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
   221         Parse.binding >> (fn s => (true, SOME s)))
   222         --| Parse.$$$ ")") (true, NONE) --
   223     (Parse.type_args_constrained -- Parse.binding) --
   224     Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
   225     Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
   226 
   227 fun mk_domaindef ((((((def, opt_name), (args, t)), mx), A), morphs)) =
   228   domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)
   229 
   230 val _ =
   231   Outer_Syntax.command "domaindef" "HOLCF definition of domains from deflations" Keyword.thy_decl
   232     (domaindef_decl >>
   233       (Toplevel.print oo (Toplevel.theory o mk_domaindef)))
   234 
   235 end