--- a/src/HOL/Induct/Term.thy Fri Oct 23 12:55:36 1998 +0200
+++ b/src/HOL/Induct/Term.thy Fri Oct 23 12:56:13 1998 +0200
@@ -1,55 +1,31 @@
-(* Title: HOL/ex/Term
+(* Title: HOL/Induct/Term.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
+ Author: Stefan Berghofer, TU Muenchen
+ Copyright 1998 TU Muenchen
-Terms over a given alphabet -- function applications; illustrates list functor
- (essentially the same type as in Trees & Forests)
-
-There is no constructor APP because it is simply Scons
+Terms over a given alphabet -- function applications
*)
-Term = SList +
+Term = Main +
-types 'a term
+datatype
+ ('a, 'b) term = Var 'a
+ | App 'b ((('a, 'b) term) list)
-arities term :: (term)term
+
+(** substitution function on terms **)
consts
- term :: 'a item set => 'a item set
- Rep_term :: 'a term => 'a item
- Abs_term :: 'a item => 'a term
- Rep_Tlist :: 'a term list => 'a item
- Abs_Tlist :: 'a item => 'a term list
- App :: ['a, ('a term)list] => 'a term
- Term_rec :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
- term_rec :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
-
-inductive "term(A)"
- intrs
- APP_I "[| M: A; N : list(term(A)) |] ==> Scons M N : term(A)"
- monos list_mono
-
-defs
- (*defining abstraction/representation functions for term list...*)
- Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
- Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
+ subst_term :: "['a => ('a, 'b) term, ('a, 'b) term] => ('a, 'b) term"
+ subst_term_list ::
+ "['a => ('a, 'b) term, ('a, 'b) term list] => ('a, 'b) term list"
- (*defining the abstract constants*)
- App_def "App a ts == Abs_term(Scons (Leaf a) (Rep_Tlist ts))"
-
- (*list recursion*)
- Term_rec_def
- "Term_rec M d == wfrec (trancl pred_sexp)
- (%g. Split(%x y. d x y (Abs_map g y))) M"
+primrec
+ "subst_term f (Var a) = f a"
+ "subst_term f (App b ts) = App b (subst_term_list f ts)"
- term_rec_def
- "term_rec t d ==
- Term_rec (Rep_term t) (%x y r. d (inv Leaf x) (Abs_Tlist(y)) r)"
+ "subst_term_list f [] = []"
+ "subst_term_list f (t # ts) =
+ subst_term f t # subst_term_list f ts"
-rules
- (*faking a type definition for term...*)
- Rep_term "Rep_term(n): term(range(Leaf))"
- Rep_term_inverse "Abs_term(Rep_term(t)) = t"
- Abs_term_inverse "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
end