src/HOL/Induct/Term.thy
changeset 3120 c58423c20740
child 5191 8ceaa19f7717
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Induct/Term.thy	Wed May 07 12:50:26 1997 +0200
     1.3 @@ -0,0 +1,55 @@
     1.4 +(*  Title:      HOL/ex/Term
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +Terms over a given alphabet -- function applications; illustrates list functor
    1.10 +  (essentially the same type as in Trees & Forests)
    1.11 +
    1.12 +There is no constructor APP because it is simply cons ($) 
    1.13 +*)
    1.14 +
    1.15 +Term = SList +
    1.16 +
    1.17 +types   'a term
    1.18 +
    1.19 +arities term :: (term)term
    1.20 +
    1.21 +consts
    1.22 +  term          :: 'a item set => 'a item set
    1.23 +  Rep_term      :: 'a term => 'a item
    1.24 +  Abs_term      :: 'a item => 'a term
    1.25 +  Rep_Tlist     :: 'a term list => 'a item
    1.26 +  Abs_Tlist     :: 'a item => 'a term list
    1.27 +  App           :: ['a, ('a term)list] => 'a term
    1.28 +  Term_rec      :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
    1.29 +  term_rec      :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
    1.30 +
    1.31 +inductive "term(A)"
    1.32 +  intrs
    1.33 +    APP_I "[| M: A;  N : list(term(A)) |] ==> M$N : term(A)"
    1.34 +  monos   "[list_mono]"
    1.35 +
    1.36 +defs
    1.37 +  (*defining abstraction/representation functions for term list...*)
    1.38 +  Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
    1.39 +  Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
    1.40 +
    1.41 +  (*defining the abstract constants*)
    1.42 +  App_def       "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
    1.43 +
    1.44 +  (*list recursion*)
    1.45 +  Term_rec_def  
    1.46 +   "Term_rec M d == wfrec (trancl pred_sexp)
    1.47 +           (%g. Split(%x y. d x y (Abs_map g y))) M"
    1.48 +
    1.49 +  term_rec_def
    1.50 +   "term_rec t d == 
    1.51 +   Term_rec (Rep_term t) (%x y r. d (inv Leaf x) (Abs_Tlist(y)) r)"
    1.52 +
    1.53 +rules
    1.54 +    (*faking a type definition for term...*)
    1.55 +  Rep_term              "Rep_term(n): term(range(Leaf))"
    1.56 +  Rep_term_inverse      "Abs_term(Rep_term(t)) = t"
    1.57 +  Abs_term_inverse      "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
    1.58 +end