Deleted extra space in clos_mk.
(* Title: HOL/ex/term
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Terms over a given alphabet -- function applications; illustrates List functor
(essentially the same type as in Trees & Forests)
There is no constructor APP because it is simply cons (.)
*)
Term = List +
types term 1
arities term :: (term)term
consts
Term :: "'a node set set => 'a node set set"
Rep_Term :: "'a term => 'a node set"
Abs_Term :: "'a node set => 'a term"
Rep_TList :: "'a term list => 'a node set"
Abs_TList :: "'a node set => 'a term list"
App :: "['a, ('a term)list] => 'a term"
Term_rec ::
"['a node set, ['a node set , 'a node set, 'b list]=>'b] => 'b"
term_rec :: "['a term, ['a ,'a term list, 'b list]=>'b] => 'b"
rules
Term_def "Term(A) == lfp(%Z. A <*> List(Z))"
(*faking a type definition for term...*)
Rep_Term "Rep_Term(n): Term(range(Leaf))"
Rep_Term_inverse "Abs_Term(Rep_Term(t)) = t"
Abs_Term_inverse "M: Term(range(Leaf)) ==> Rep_Term(Abs_Term(M)) = M"
(*defining abstraction/representation functions for term list...*)
Rep_TList_def "Rep_TList == Rep_map(Rep_Term)"
Abs_TList_def "Abs_TList == Abs_map(Abs_Term)"
(*defining the abstract constants*)
App_def "App(a,ts) == Abs_Term(Leaf(a) $ Rep_TList(ts))"
(*list recursion*)
Term_rec_def
"Term_rec(M,d) == wfrec(trancl(pred_Sexp), M, \
\ %M g. Split(M, %x y. d(x,y, Abs_map(g,y))))"
term_rec_def
"term_rec(t,d) == \
\ Term_rec(Rep_Term(t), %x y r. d(Inv(Leaf,x), Abs_TList(y), r))"
end