src/HOL/Induct/Term.thy
changeset 3120 c58423c20740
child 5191 8ceaa19f7717
equal deleted inserted replaced
3119:bb2ee88aa43f 3120:c58423c20740
       
     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 = SList +
       
    13 
       
    14 types   'a term
       
    15 
       
    16 arities term :: (term)term
       
    17 
       
    18 consts
       
    19   term          :: 'a item set => 'a item set
       
    20   Rep_term      :: 'a term => 'a item
       
    21   Abs_term      :: 'a item => 'a term
       
    22   Rep_Tlist     :: 'a term list => 'a item
       
    23   Abs_Tlist     :: 'a item => 'a term list
       
    24   App           :: ['a, ('a term)list] => 'a term
       
    25   Term_rec      :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
       
    26   term_rec      :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
       
    27 
       
    28 inductive "term(A)"
       
    29   intrs
       
    30     APP_I "[| M: A;  N : list(term(A)) |] ==> M$N : term(A)"
       
    31   monos   "[list_mono]"
       
    32 
       
    33 defs
       
    34   (*defining abstraction/representation functions for term list...*)
       
    35   Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
       
    36   Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
       
    37 
       
    38   (*defining the abstract constants*)
       
    39   App_def       "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
       
    40 
       
    41   (*list recursion*)
       
    42   Term_rec_def  
       
    43    "Term_rec M d == wfrec (trancl pred_sexp)
       
    44            (%g. Split(%x y. d x y (Abs_map g y))) M"
       
    45 
       
    46   term_rec_def
       
    47    "term_rec t d == 
       
    48    Term_rec (Rep_term t) (%x y r. d (inv Leaf x) (Abs_Tlist(y)) r)"
       
    49 
       
    50 rules
       
    51     (*faking a type definition for term...*)
       
    52   Rep_term              "Rep_term(n): term(range(Leaf))"
       
    53   Rep_term_inverse      "Abs_term(Rep_term(t)) = t"
       
    54   Abs_term_inverse      "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
       
    55 end