src/HOLCF/holcf_logic.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 16843 8ff9a80f3c93
child 32010 cb1a1c94b4cd
permissions -rw-r--r--
filtering out some package theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOLCF/holcf_logic.ML
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
     3
    Author:     David von Oheimb
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
     4
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
     5
Abstract syntax operations for HOLCF.
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
     6
*)
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
     7
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
     8
infixr 6 ->>;
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
     9
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    10
signature HOLCF_LOGIC =
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    11
sig
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    12
  val mk_btyp: string -> typ * typ -> typ
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    13
  val pcpoC: class
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    14
  val pcpoS: sort
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    15
  val mk_TFree: string -> typ
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    16
  val cfun_arrow: string
16843
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    17
  val ->> : typ * typ -> typ
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    18
  val mk_ssumT: typ * typ -> typ
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    19
  val mk_sprodT: typ * typ -> typ
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    20
  val mk_uT: typ -> typ
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    21
  val trT: typ
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    22
  val oneT: typ
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    23
end;
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    24
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    25
structure HOLCFLogic: HOLCF_LOGIC =
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    26
struct
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    27
16843
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    28
(* sort pcpo *)
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    29
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    30
val pcpoC = Sign.intern_class (the_context ()) "pcpo";
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    31
val pcpoS = [pcpoC];
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    32
fun mk_TFree s = TFree ("'" ^ s, pcpoS);
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    33
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    34
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    35
(* basic types *)
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    36
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    37
fun mk_btyp t (S,T) = Type (t,[S,T]);
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    38
16843
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    39
local
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    40
  val intern_type = Sign.intern_type (the_context ());
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    41
  val u = intern_type "u";
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    42
in
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    43
16843
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    44
val cfun_arrow = intern_type "->";
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    45
val op ->> = mk_btyp cfun_arrow;
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    46
val mk_ssumT = mk_btyp (intern_type "++");
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    47
val mk_sprodT = mk_btyp (intern_type "**");
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    48
fun mk_uT T = Type (u, [T]);
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    49
val trT = Type (intern_type "tr" , []);
8ff9a80f3c93 removed mk_prodT, mk_not (cf. HOL/hologic.ML);
wenzelm
parents: 16364
diff changeset
    50
val oneT = Type (intern_type "one", []);
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    51
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    52
end;
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    53
12030
wenzelm
parents: 4129
diff changeset
    54
end;