|
515
|
1 |
(* Title: ZF/ex/Term.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1994 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 |
Term = List +
|
|
|
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 |
term :: "i=>i"
|
|
|
19 |
|
|
|
20 |
datatype
|
|
|
21 |
"term(A)" = Apply ("a: A", "l: list(term(A))")
|
|
|
22 |
monos "[list_mono]"
|
|
740
|
23 |
|
|
|
24 |
type_elims "[make_elim (list_univ RS subsetD)]"
|
|
|
25 |
(*Or could have
|
|
|
26 |
type_intrs "[list_univ RS subsetD]"
|
|
|
27 |
*)
|
|
515
|
28 |
|
|
753
|
29 |
defs
|
|
515
|
30 |
term_rec_def
|
|
1155
|
31 |
"term_rec(t,d) ==
|
|
|
32 |
Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
|
|
515
|
33 |
|
|
|
34 |
term_map_def "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
|
|
|
35 |
|
|
|
36 |
term_size_def "term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))"
|
|
|
37 |
|
|
|
38 |
reflect_def "reflect(t) == term_rec(t, %x zs rs. Apply(x, rev(rs)))"
|
|
|
39 |
|
|
|
40 |
preorder_def "preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
|
|
|
41 |
|
|
|
42 |
end
|