equal
deleted
inserted
replaced
|
1 (* Title: HOL/Induct/Sexp.thy |
|
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 |
|
7 structures by hand. |
|
8 *) |
|
9 |
|
10 Sexp = Univ + Inductive + |
|
11 consts |
|
12 sexp :: 'a item set |
|
13 |
|
14 sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, |
|
15 'a item] => 'b" |
|
16 |
|
17 sexp_rec :: "['a item, 'a=>'b, nat=>'b, |
|
18 ['a item, 'a item, 'b, 'b]=>'b] => 'b" |
|
19 |
|
20 pred_sexp :: "('a item * 'a item)set" |
|
21 |
|
22 inductive sexp |
|
23 intrs |
|
24 LeafI "Leaf(a): sexp" |
|
25 NumbI "Numb(i): sexp" |
|
26 SconsI "[| M: sexp; N: sexp |] ==> Scons M N : sexp" |
|
27 |
|
28 defs |
|
29 |
|
30 sexp_case_def |
|
31 "sexp_case c d e M == @ z. (? x. M=Leaf(x) & z=c(x)) |
|
32 | (? k. M=Numb(k) & z=d(k)) |
|
33 | (? N1 N2. M = Scons N1 N2 & z=e N1 N2)" |
|
34 |
|
35 pred_sexp_def |
|
36 "pred_sexp == UN M: sexp. UN N: sexp. {(M, Scons M N), (N, Scons M N)}" |
|
37 |
|
38 sexp_rec_def |
|
39 "sexp_rec M c d e == wfrec pred_sexp |
|
40 (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M" |
|
41 end |