paulson@3120: (*  Title:      HOL/ex/Term
paulson@3120:     ID:         $Id$
paulson@3120:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3120:     Copyright   1992  University of Cambridge
paulson@3120: 
paulson@3120: Terms over a given alphabet -- function applications; illustrates list functor
paulson@3120:   (essentially the same type as in Trees & Forests)
paulson@3120: 
paulson@3120: There is no constructor APP because it is simply cons ($) 
paulson@3120: *)
paulson@3120: 
paulson@3120: Term = SList +
paulson@3120: 
paulson@3120: types   'a term
paulson@3120: 
paulson@3120: arities term :: (term)term
paulson@3120: 
paulson@3120: consts
paulson@3120:   term          :: 'a item set => 'a item set
paulson@3120:   Rep_term      :: 'a term => 'a item
paulson@3120:   Abs_term      :: 'a item => 'a term
paulson@3120:   Rep_Tlist     :: 'a term list => 'a item
paulson@3120:   Abs_Tlist     :: 'a item => 'a term list
paulson@3120:   App           :: ['a, ('a term)list] => 'a term
paulson@3120:   Term_rec      :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
paulson@3120:   term_rec      :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
paulson@3120: 
paulson@3120: inductive "term(A)"
paulson@3120:   intrs
paulson@3120:     APP_I "[| M: A;  N : list(term(A)) |] ==> M$N : term(A)"
paulson@3120:   monos   "[list_mono]"
paulson@3120: 
paulson@3120: defs
paulson@3120:   (*defining abstraction/representation functions for term list...*)
paulson@3120:   Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
paulson@3120:   Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
paulson@3120: 
paulson@3120:   (*defining the abstract constants*)
paulson@3120:   App_def       "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
paulson@3120: 
paulson@3120:   (*list recursion*)
paulson@3120:   Term_rec_def  
paulson@3120:    "Term_rec M d == wfrec (trancl pred_sexp)
paulson@3120:            (%g. Split(%x y. d x y (Abs_map g y))) M"
paulson@3120: 
paulson@3120:   term_rec_def
paulson@3120:    "term_rec t d == 
paulson@3120:    Term_rec (Rep_term t) (%x y r. d (inv Leaf x) (Abs_Tlist(y)) r)"
paulson@3120: 
paulson@3120: rules
paulson@3120:     (*faking a type definition for term...*)
paulson@3120:   Rep_term              "Rep_term(n): term(range(Leaf))"
paulson@3120:   Rep_term_inverse      "Abs_term(Rep_term(t)) = t"
paulson@3120:   Abs_term_inverse      "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
paulson@3120: end