ex/term.thy

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