src/HOL/Induct/Term.thy
changeset 5191 8ceaa19f7717
parent 3120 c58423c20740
child 5717 0d28dbe484b6
equal deleted inserted replaced
5190:4ae031622592 5191:8ceaa19f7717
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 Terms over a given alphabet -- function applications; illustrates list functor
     6 Terms over a given alphabet -- function applications; illustrates list functor
     7   (essentially the same type as in Trees & Forests)
     7   (essentially the same type as in Trees & Forests)
     8 
     8 
     9 There is no constructor APP because it is simply cons ($) 
     9 There is no constructor APP because it is simply Scons
    10 *)
    10 *)
    11 
    11 
    12 Term = SList +
    12 Term = SList +
    13 
    13 
    14 types   'a term
    14 types   'a term
    25   Term_rec      :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
    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
    26   term_rec      :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
    27 
    27 
    28 inductive "term(A)"
    28 inductive "term(A)"
    29   intrs
    29   intrs
    30     APP_I "[| M: A;  N : list(term(A)) |] ==> M$N : term(A)"
    30     APP_I "[| M: A;  N : list(term(A)) |] ==> Scons M N : term(A)"
    31   monos   "[list_mono]"
    31   monos   "[list_mono]"
    32 
    32 
    33 defs
    33 defs
    34   (*defining abstraction/representation functions for term list...*)
    34   (*defining abstraction/representation functions for term list...*)
    35   Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
    35   Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
    36   Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
    36   Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
    37 
    37 
    38   (*defining the abstract constants*)
    38   (*defining the abstract constants*)
    39   App_def       "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
    39   App_def       "App a ts == Abs_term(Scons (Leaf a) (Rep_Tlist ts))"
    40 
    40 
    41   (*list recursion*)
    41   (*list recursion*)
    42   Term_rec_def  
    42   Term_rec_def  
    43    "Term_rec M d == wfrec (trancl pred_sexp)
    43    "Term_rec M d == wfrec (trancl pred_sexp)
    44            (%g. Split(%x y. d x y (Abs_map g y))) M"
    44            (%g. Split(%x y. d x y (Abs_map g y))) M"