|
0
|
1 |
(* Title: HOL/ex/term
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1992 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Terms over a given alphabet -- function applications; illustrates List functor
|
|
|
7 |
(essentially the same type as in Trees & Forests)
|
|
|
8 |
|
|
|
9 |
There is no constructor APP because it is simply cons (.)
|
|
|
10 |
*)
|
|
|
11 |
|
|
|
12 |
Term = List +
|
|
|
13 |
types term 1
|
|
|
14 |
arities term :: (term)term
|
|
|
15 |
consts
|
|
|
16 |
Term :: "'a node set set => 'a node set set"
|
|
|
17 |
Rep_Term :: "'a term => 'a node set"
|
|
|
18 |
Abs_Term :: "'a node set => 'a term"
|
|
|
19 |
Rep_TList :: "'a term list => 'a node set"
|
|
|
20 |
Abs_TList :: "'a node set => 'a term list"
|
|
|
21 |
App :: "['a, ('a term)list] => 'a term"
|
|
|
22 |
Term_rec ::
|
|
|
23 |
"['a node set, ['a node set , 'a node set, 'b list]=>'b] => 'b"
|
|
|
24 |
term_rec :: "['a term, ['a ,'a term list, 'b list]=>'b] => 'b"
|
|
|
25 |
rules
|
|
|
26 |
Term_def "Term(A) == lfp(%Z. A <*> List(Z))"
|
|
|
27 |
(*faking a type definition for term...*)
|
|
|
28 |
Rep_Term "Rep_Term(n): Term(range(Leaf))"
|
|
|
29 |
Rep_Term_inverse "Abs_Term(Rep_Term(t)) = t"
|
|
|
30 |
Abs_Term_inverse "M: Term(range(Leaf)) ==> Rep_Term(Abs_Term(M)) = M"
|
|
|
31 |
(*defining abstraction/representation functions for term list...*)
|
|
|
32 |
Rep_TList_def "Rep_TList == Rep_map(Rep_Term)"
|
|
|
33 |
Abs_TList_def "Abs_TList == Abs_map(Abs_Term)"
|
|
|
34 |
(*defining the abstract constants*)
|
|
|
35 |
App_def "App(a,ts) == Abs_Term(Leaf(a) . Rep_TList(ts))"
|
|
|
36 |
(*list recursion*)
|
|
|
37 |
Term_rec_def
|
|
|
38 |
"Term_rec(M,d) == wfrec(trancl(pred_Sexp), M, \
|
|
|
39 |
\ %M g. Split(M, %x y. d(x,y, Abs_map(g,y))))"
|
|
|
40 |
|
|
|
41 |
term_rec_def
|
|
|
42 |
"term_rec(t,d) == \
|
|
|
43 |
\ Term_rec(Rep_Term(t), %x y r. d(Inv(Leaf,x), Abs_TList(y), r))"
|
|
|
44 |
end
|