src/HOL/Induct/Term.thy
author wenzelm
Thu, 26 Jun 1997 11:14:46 +0200
changeset 3462 3472fa00b1d4
parent 3120 c58423c20740
child 5191 8ceaa19f7717
permissions -rw-r--r--
rearrange pages of ps file to be printed as booklet (duplex);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     1
(*  Title:      HOL/ex/Term
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     2
    ID:         $Id$
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     5
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     6
Terms over a given alphabet -- function applications; illustrates list functor
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     7
  (essentially the same type as in Trees & Forests)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     8
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     9
There is no constructor APP because it is simply cons ($) 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    10
*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    11
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    12
Term = SList +
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    13
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    14
types   'a term
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    15
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    16
arities term :: (term)term
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    17
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    18
consts
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    19
  term          :: 'a item set => 'a item set
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    20
  Rep_term      :: 'a term => 'a item
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    21
  Abs_term      :: 'a item => 'a term
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    22
  Rep_Tlist     :: 'a term list => 'a item
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    23
  Abs_Tlist     :: 'a item => 'a term list
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    24
  App           :: ['a, ('a term)list] => 'a term
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    25
  Term_rec      :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    26
  term_rec      :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    27
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    28
inductive "term(A)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    29
  intrs
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    30
    APP_I "[| M: A;  N : list(term(A)) |] ==> M$N : term(A)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    31
  monos   "[list_mono]"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    32
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    33
defs
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    34
  (*defining abstraction/representation functions for term list...*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    35
  Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    36
  Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    37
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    38
  (*defining the abstract constants*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    39
  App_def       "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    40
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    41
  (*list recursion*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    42
  Term_rec_def  
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    43
   "Term_rec M d == wfrec (trancl pred_sexp)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    44
           (%g. Split(%x y. d x y (Abs_map g y))) M"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    45
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    46
  term_rec_def
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    47
   "term_rec t d == 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    48
   Term_rec (Rep_term t) (%x y r. d (inv Leaf x) (Abs_Tlist(y)) r)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    49
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    50
rules
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    51
    (*faking a type definition for term...*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    52
  Rep_term              "Rep_term(n): term(range(Leaf))"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    53
  Rep_term_inverse      "Abs_term(Rep_term(t)) = t"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    54
  Abs_term_inverse      "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    55
end