author | clasohm |
Fri, 01 Jul 1994 11:04:12 +0200 | |
changeset 445 | 7b6d8b8d4580 |
parent 419 | 7c7e71be40c8 |
child 477 | 53fc8ad84b33 |
permissions | -rw-r--r-- |
0 | 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)", |
|
445 | 15 |
[(["Fls"], "i",NoSyn), |
16 |
(["Var"], "i=>i", Mixfix ("#_", [100], 100)), |
|
17 |
(["=>"], "[i,i]=>i", Infixr 90)])]; |
|
0 | 18 |
val rec_styp = "i"; |
19 |
val sintrs = |
|
20 |
["Fls : prop", |
|
21 |
"n: nat ==> #n : prop", |
|
22 |
"[| p: prop; q: prop |] ==> p=>q : prop"]; |
|
23 |
val monos = []; |
|
71
729fe026c5f3
sample datatype defs now use datatype_intrs, datatype_elims
lcp
parents:
16
diff
changeset
|
24 |
val type_intrs = datatype_intrs; |
0 | 25 |
val type_elims = []); |
26 |
||
27 |
val [FlsI,VarI,ImpI] = Prop.intrs; |
|
28 |
||
29 |
||
30 |
(** Type-checking rules **) |
|
31 |
||
32 |
val ImpE = Prop.mk_cases Prop.con_defs "p=>q : prop"; |
|
33 |
||
34 |
writeln"Reached end of file."; |