src/ZF/ex/comb.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 16 0b033d50ca1c
permissions -rw-r--r--
Initial revision
     1 (*  Title: 	ZF/ex/comb.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson
     4     Copyright   1993  University of Cambridge
     5 
     6 Datatype definition of combinators S and K
     7 
     8 J. Camilleri and T. F. Melham.
     9 Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
    10 Report 265, University of Cambridge Computer Laboratory, 1992.
    11 *)
    12 
    13 
    14 (*Example of a datatype with mixfix syntax for some constructors*)
    15 structure Comb = Datatype_Fun
    16  (val thy = Univ.thy;
    17   val rec_specs = 
    18       [("comb", "univ(0)",
    19 	  [(["K","S"],	"i"),
    20 	   (["op #"],	"[i,i]=>i")])];
    21   val rec_styp = "i";
    22   val ext = Some (NewSext {
    23 	     mixfix =
    24 	      [Infixl("#", "[i,i] => i", 90)],
    25 	     xrules = [],
    26 	     parse_ast_translation = [],
    27 	     parse_preproc = None,
    28 	     parse_postproc = None,
    29 	     parse_translation = [],
    30 	     print_translation = [],
    31 	     print_preproc = None,
    32 	     print_postproc = None,
    33 	     print_ast_translation = []});
    34   val sintrs = 
    35 	  ["K : comb",
    36 	   "S : comb",
    37 	   "[| p: comb;  q: comb |] ==> p#q : comb"];
    38   val monos = [];
    39   val type_intrs = data_typechecks;
    40   val type_elims = []);
    41 
    42 val [K_comb,S_comb,Ap_comb] = Comb.intrs;
    43 
    44 val Ap_E = Comb.mk_cases Comb.con_defs "p#q : comb";
    45