author | clasohm |
Fri, 15 Jul 1994 13:34:31 +0200 | |
changeset 477 | 53fc8ad84b33 |
parent 445 | 7b6d8b8d4580 |
child 486 | 6b58082796f6 |
permissions | -rw-r--r-- |
0 | 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; |
|
477 | 17 |
val thy_name = "Comb"; |
0 | 18 |
val rec_specs = |
19 |
[("comb", "univ(0)", |
|
445 | 20 |
[(["K","S"], "i", NoSyn), |
21 |
(["#"], "[i,i]=>i", Infixl 90)])]; |
|
0 | 22 |
val rec_styp = "i"; |
23 |
val sintrs = |
|
24 |
["K : comb", |
|
25 |
"S : comb", |
|
26 |
"[| p: comb; q: comb |] ==> p#q : comb"]; |
|
27 |
val monos = []; |
|
71
729fe026c5f3
sample datatype defs now use datatype_intrs, datatype_elims
lcp
parents:
16
diff
changeset
|
28 |
val type_intrs = datatype_intrs; |
0 | 29 |
val type_elims = []); |
30 |
||
31 |
val [K_comb,S_comb,Ap_comb] = Comb.intrs; |
|
32 |
||
33 |
val Ap_E = Comb.mk_cases Comb.con_defs "p#q : comb"; |
|
34 |