src/ZF/ex/Comb.ML
changeset 0 a5a9c433f639
child 16 0b033d50ca1c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/ex/Comb.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,45 @@
     1.4 +(*  Title: 	ZF/ex/comb.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Datatype definition of combinators S and K
    1.10 +
    1.11 +J. Camilleri and T. F. Melham.
    1.12 +Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
    1.13 +Report 265, University of Cambridge Computer Laboratory, 1992.
    1.14 +*)
    1.15 +
    1.16 +
    1.17 +(*Example of a datatype with mixfix syntax for some constructors*)
    1.18 +structure Comb = Datatype_Fun
    1.19 + (val thy = Univ.thy;
    1.20 +  val rec_specs = 
    1.21 +      [("comb", "univ(0)",
    1.22 +	  [(["K","S"],	"i"),
    1.23 +	   (["op #"],	"[i,i]=>i")])];
    1.24 +  val rec_styp = "i";
    1.25 +  val ext = Some (NewSext {
    1.26 +	     mixfix =
    1.27 +	      [Infixl("#", "[i,i] => i", 90)],
    1.28 +	     xrules = [],
    1.29 +	     parse_ast_translation = [],
    1.30 +	     parse_preproc = None,
    1.31 +	     parse_postproc = None,
    1.32 +	     parse_translation = [],
    1.33 +	     print_translation = [],
    1.34 +	     print_preproc = None,
    1.35 +	     print_postproc = None,
    1.36 +	     print_ast_translation = []});
    1.37 +  val sintrs = 
    1.38 +	  ["K : comb",
    1.39 +	   "S : comb",
    1.40 +	   "[| p: comb;  q: comb |] ==> p#q : comb"];
    1.41 +  val monos = [];
    1.42 +  val type_intrs = data_typechecks;
    1.43 +  val type_elims = []);
    1.44 +
    1.45 +val [K_comb,S_comb,Ap_comb] = Comb.intrs;
    1.46 +
    1.47 +val Ap_E = Comb.mk_cases Comb.con_defs "p#q : comb";
    1.48 +