src/ZF/ex/Prop.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 477 53fc8ad84b33
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     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 thy_name = "Prop";
    14   val rec_specs = 
    15       [("prop", "univ(0)",
    16 	  [(["Fls"],	"i",NoSyn),
    17 	   (["Var"],	"i=>i", Mixfix ("#_", [100], 100)),
    18 	   (["=>"],	"[i,i]=>i", Infixr 90)])];
    19   val rec_styp = "i";
    20   val sintrs = 
    21 	  ["Fls : prop",
    22 	   "n: nat ==> #n : prop",
    23 	   "[| p: prop;  q: prop |] ==> p=>q : prop"];
    24   val monos = [];
    25   val type_intrs = datatype_intrs;
    26   val type_elims = []);
    27 
    28 val [FlsI,VarI,ImpI] = Prop.intrs;
    29 
    30 
    31 (** Type-checking rules **)
    32 
    33 val ImpE = Prop.mk_cases Prop.con_defs "p=>q : prop";
    34 
    35 writeln"Reached end of file.";