src/HOLCF/holcf_logic.ML
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 14981 e73f8140af78
child 16364 dc9f7066d80a
permissions -rw-r--r--
New theory with lemmas for the fixrec package
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 mk_prodT:          typ * typ -> typ
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    14
  val mk_not:  term -> term
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    15
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    16
  val HOLCF_sg: Sign.sg
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    17
  val pcpoC: class
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    18
  val pcpoS: sort
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    19
  val mk_TFree: string -> typ
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    20
  val cfun_arrow: string
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    21
  val ->>      : typ * typ -> typ
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    22
  val mk_ssumT : typ * typ -> typ
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    23
  val mk_sprodT: typ * typ -> typ
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    24
  val mk_uT: typ -> typ
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    25
  val trT: typ
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    26
  val oneT: typ
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    27
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    28
end;
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    29
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    30
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    31
structure HOLCFLogic: HOLCF_LOGIC =
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    32
struct
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    33
12030
wenzelm
parents: 4129
diff changeset
    34
open HOLogic;
4129
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    35
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    36
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
    37
val mk_prodT = mk_btyp "*";
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    38
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    39
fun mk_not P  = Const ("Not", boolT --> boolT) $ P;
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    40
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    41
(* basics *)
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    42
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    43
val HOLCF_sg    = sign_of HOLCF.thy;
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    44
val pcpoC       = Sign.intern_class HOLCF_sg "pcpo";
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    45
val pcpoS       = [pcpoC];
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    46
fun mk_TFree s  = TFree ("'"^s, pcpoS);
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    47
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    48
(*cfun, ssum, sprod, u, tr, one *)
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    49
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    50
local val intern = Sign.intern_tycon HOLCF_sg;
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    51
in
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    52
val cfun_arrow = intern "->";
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    53
val op   ->>  = mk_btyp cfun_arrow;
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    54
val mk_ssumT  = mk_btyp (intern "++");
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    55
val mk_sprodT = mk_btyp (intern "**");
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    56
fun mk_uT T   = Type (intern "u"  ,[T]);
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    57
val trT       = Type (intern "tr" ,[ ]);
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    58
val oneT      = Type (intern "one",[ ]);
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    59
end;
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
wenzelm
parents:
diff changeset
    60
12030
wenzelm
parents: 4129
diff changeset
    61
end;