src/HOLCF/holcf_logic.ML
author huffman
Mon May 11 08:28:09 2009 -0700 (2009-05-11)
changeset 31095 b79d140f6d0b
parent 16843 8ff9a80f3c93
child 32010 cb1a1c94b4cd
permissions -rw-r--r--
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
     1 (*  Title:      HOLCF/holcf_logic.ML
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4 
     5 Abstract syntax operations for HOLCF.
     6 *)
     7 
     8 infixr 6 ->>;
     9 
    10 signature HOLCF_LOGIC =
    11 sig
    12   val mk_btyp: string -> typ * typ -> typ
    13   val pcpoC: class
    14   val pcpoS: sort
    15   val mk_TFree: string -> typ
    16   val cfun_arrow: string
    17   val ->> : typ * typ -> typ
    18   val mk_ssumT: typ * typ -> typ
    19   val mk_sprodT: typ * typ -> typ
    20   val mk_uT: typ -> typ
    21   val trT: typ
    22   val oneT: typ
    23 end;
    24 
    25 structure HOLCFLogic: HOLCF_LOGIC =
    26 struct
    27 
    28 (* sort pcpo *)
    29 
    30 val pcpoC = Sign.intern_class (the_context ()) "pcpo";
    31 val pcpoS = [pcpoC];
    32 fun mk_TFree s = TFree ("'" ^ s, pcpoS);
    33 
    34 
    35 (* basic types *)
    36 
    37 fun mk_btyp t (S,T) = Type (t,[S,T]);
    38 
    39 local
    40   val intern_type = Sign.intern_type (the_context ());
    41   val u = intern_type "u";
    42 in
    43 
    44 val cfun_arrow = intern_type "->";
    45 val op ->> = mk_btyp cfun_arrow;
    46 val mk_ssumT = mk_btyp (intern_type "++");
    47 val mk_sprodT = mk_btyp (intern_type "**");
    48 fun mk_uT T = Type (u, [T]);
    49 val trT = Type (intern_type "tr" , []);
    50 val oneT = Type (intern_type "one", []);
    51 
    52 end;
    53 
    54 end;