src/ZF/ex/prop.ML
author lcp
Fri Oct 22 11:42:02 1993 +0100 (1993-10-22)
changeset 71 729fe026c5f3
parent 16 0b033d50ca1c
permissions -rw-r--r--
sample datatype defs now use datatype_intrs, datatype_elims
     1 (*  Title: 	ZF/ex/prop.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson
     4     Copyright   1993  University of Cambridge
     5 
     6 Datatype definition of propositional logic formulae and inductive definition
     7 of the propositional tautologies.
     8 *)
     9 
    10 (*Example of a datatype with mixfix syntax for some constructors*)
    11 structure Prop = Datatype_Fun
    12  (val thy = Univ.thy;
    13   val rec_specs = 
    14       [("prop", "univ(0)",
    15 	  [(["Fls"],	"i"),
    16 	   (["Var"],	"i=>i"),
    17 	   (["op =>"],	"[i,i]=>i")])];
    18   val rec_styp = "i";
    19   val ext = Some (Syntax.simple_sext
    20 		    [Mixfix("#_", "i => i", "Var", [100], 100),
    21 		     Infixr("=>", "[i,i] => i", 90)]);
    22   val sintrs = 
    23 	  ["Fls : prop",
    24 	   "n: nat ==> #n : prop",
    25 	   "[| p: prop;  q: prop |] ==> p=>q : prop"];
    26   val monos = [];
    27   val type_intrs = datatype_intrs;
    28   val type_elims = []);
    29 
    30 val [FlsI,VarI,ImpI] = Prop.intrs;
    31 
    32 
    33 (** Type-checking rules **)
    34 
    35 val ImpE = Prop.mk_cases Prop.con_defs "p=>q : prop";
    36 
    37 writeln"Reached end of file.";