src/HOLCF/holcf_logic.ML

refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function

(*  Title:      HOLCF/holcf_logic.ML
    Author:     David von Oheimb

Abstract syntax operations for HOLCF.
*)

infixr 6 ->>;

signature HOLCF_LOGIC =
sig
  val mk_btyp: string -> typ * typ -> typ
  val pcpoS: sort
  val mk_TFree: string -> typ
  val cfun_arrow: string
  val ->> : typ * typ -> typ
  val mk_ssumT: typ * typ -> typ
  val mk_sprodT: typ * typ -> typ
  val mk_uT: typ -> typ
  val trT: typ
  val oneT: typ
end;

structure HOLCFLogic: HOLCF_LOGIC =
struct

(* sort pcpo *)

val pcpoS = @{sort pcpo};
fun mk_TFree s = TFree ("'" ^ s, pcpoS);


(* basic types *)

fun mk_btyp t (S, T) = Type (t, [S, T]);

val cfun_arrow = @{type_name "cfun"};
val op ->> = mk_btyp cfun_arrow;
val mk_ssumT = mk_btyp (@{type_name "ssum"});
val mk_sprodT = mk_btyp (@{type_name "sprod"});
fun mk_uT T = Type (@{type_name u}, [T]);
val trT = @{typ tr};
val oneT = @{typ one};

end;