author | lcp |
Tue, 25 Apr 1995 11:14:03 +0200 | |
changeset 1072 | 0140ff702b23 |
parent 972 | e61b058d58d2 |
child 1151 | c820b3cc3df0 |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/Sexp |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1992 University of Cambridge |
|
5 |
||
6 |
S-expressions, general binary trees for defining recursive data structures |
|
7 |
*) |
|
8 |
||
9 |
Sexp = Univ + |
|
10 |
consts |
|
11 |
sexp :: "'a item set" |
|
12 |
||
13 |
sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, \ |
|
14 |
\ 'a item] => 'b" |
|
15 |
||
16 |
sexp_rec :: "['a item, 'a=>'b, nat=>'b, \ |
|
17 |
\ ['a item, 'a item, 'b, 'b]=>'b] => 'b" |
|
18 |
||
19 |
pred_sexp :: "('a item * 'a item)set" |
|
20 |
||
21 |
inductive "sexp" |
|
22 |
intrs |
|
23 |
LeafI "Leaf(a): sexp" |
|
24 |
NumbI "Numb(a): sexp" |
|
25 |
SconsI "[| M: sexp; N: sexp |] ==> M$N : sexp" |
|
26 |
||
27 |
defs |
|
28 |
||
29 |
sexp_case_def |
|
30 |
"sexp_case c d e M == @ z. (? x. M=Leaf(x) & z=c(x)) \ |
|
31 |
\ | (? k. M=Numb(k) & z=d(k)) \ |
|
32 |
\ | (? N1 N2. M = N1 $ N2 & z=e N1 N2)" |
|
33 |
||
34 |
pred_sexp_def |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
35 |
"pred_sexp == UN M: sexp. UN N: sexp. {(M, M$N), (N, M$N)}" |
923 | 36 |
|
37 |
sexp_rec_def |
|
38 |
"sexp_rec M c d e == wfrec pred_sexp M \ |
|
39 |
\ (%M g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)) M)" |
|
40 |
end |