author | clasohm |
Sun, 24 Apr 1994 11:27:38 +0200 | |
changeset 70 | 9459592608e2 |
parent 48 | 21291189b51e |
child 110 | 7c6476c53a6c |
permissions | -rw-r--r-- |
0 | 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 node set set" |
|
12 |
||
13 |
Sexp_case :: "['a node set, 'a=>'b, nat=>'b, \ |
|
14 |
\ ['a node set,'a node set]=>'b] => 'b" |
|
15 |
||
16 |
Sexp_rec :: "['a node set, 'a=>'b, nat=>'b, \ |
|
17 |
\ ['a node set,'a node set,'b,'b]=>'b] => 'b" |
|
18 |
||
19 |
pred_Sexp :: "('a node set * 'a node set)set" |
|
20 |
||
21 |
rules |
|
22 |
Sexp_def "Sexp == lfp(%Z. range(Leaf) Un range(Numb) Un Z<*>Z)" |
|
23 |
||
24 |
Sexp_case_def |
|
25 |
"Sexp_case(M,c,d,e) == @ z. (? x. M=Leaf(x) & z=c(x)) \ |
|
26 |
\ | (? k. M=Numb(k) & z=d(k)) \ |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
27 |
\ | (? N1 N2. M = N1 $ N2 & z=e(N1,N2))" |
0 | 28 |
|
29 |
pred_Sexp_def |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
0
diff
changeset
|
30 |
"pred_Sexp == UN M: Sexp. UN N: Sexp. {<M, M$N>, <N, M$N>}" |
0 | 31 |
|
32 |
Sexp_rec_def |
|
33 |
"Sexp_rec(M,c,d,e) == wfrec(pred_Sexp, M, \ |
|
34 |
\ %M g. Sexp_case(M, c, d, %N1 N2. e(N1, N2, g(N1), g(N2))))" |
|
35 |
end |
|
36 |