|
0
|
1 |
(* Title: ZF/ex/term-fn.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1993 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Terms over an alphabet.
|
|
|
7 |
Illustrates the list functor (essentially the same type as in Trees & Forests)
|
|
|
8 |
*)
|
|
|
9 |
|
|
|
10 |
TermFn = Term + ListFn +
|
|
|
11 |
consts
|
|
|
12 |
term_rec :: "[i, [i,i,i]=>i] => i"
|
|
|
13 |
term_map :: "[i=>i, i] => i"
|
|
|
14 |
term_size :: "i=>i"
|
|
|
15 |
reflect :: "i=>i"
|
|
|
16 |
preorder :: "i=>i"
|
|
|
17 |
|
|
|
18 |
rules
|
|
|
19 |
term_rec_def
|
|
|
20 |
"term_rec(t,d) == \
|
|
|
21 |
\ Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
|
|
|
22 |
|
|
|
23 |
term_map_def "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
|
|
|
24 |
|
|
|
25 |
term_size_def "term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))"
|
|
|
26 |
|
|
|
27 |
reflect_def "reflect(t) == term_rec(t, %x zs rs. Apply(x, rev(rs)))"
|
|
|
28 |
|
|
|
29 |
preorder_def "preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
|
|
|
30 |
|
|
|
31 |
end
|