--- a/ex/Term.thy Wed Aug 24 18:49:29 1994 +0200
+++ b/ex/Term.thy Thu Aug 25 10:47:33 1994 +0200
@@ -1,12 +1,12 @@
-(* Title: HOL/ex/term
+(* Title: HOL/ex/Term
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-Terms over a given alphabet -- function applications; illustrates List functor
+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 cons (.)
+There is no constructor APP because it is simply cons ($)
*)
Term = List +
@@ -16,33 +16,40 @@
arities term :: (term)term
consts
- Term :: "'a node set set => 'a node set set"
- Rep_Term :: "'a term => 'a node set"
- Abs_Term :: "'a node set => 'a term"
- Rep_TList :: "'a term list => 'a node set"
- Abs_TList :: "'a node set => 'a term list"
+ 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 node set, ['a node set , 'a node set, 'b list]=>'b] => 'b"
+ Term_rec :: "['a item, ['a item , 'a item, 'b list]=>'b] => 'b"
term_rec :: "['a term, ['a ,'a term list, 'b list]=>'b] => 'b"
-rules
- Term_def "Term(A) == lfp(%Z. A <*> List(Z))"
- (*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"
- (*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)"
- (*defining the abstract constants*)
- App_def "App(a,ts) == Abs_Term(Leaf(a) $ Rep_TList(ts))"
- (*list recursion*)
+inductive "term(A)"
+ intrs
+ APP_I "[| M: A; N : list(term(A)) |] ==> 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)"
+
+ (*defining the abstract constants*)
+ App_def "App(a,ts) == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
+
+ (*list recursion*)
Term_rec_def
- "Term_rec(M,d) == wfrec(trancl(pred_Sexp), M, \
+ "Term_rec(M,d) == wfrec(trancl(pred_sexp), M, \
\ Split(%x y g. d(x,y, Abs_map(g,y))))"
term_rec_def
"term_rec(t,d) == \
-\ Term_rec(Rep_Term(t), %x y r. d(Inv(Leaf,x), Abs_TList(y), r))"
+\ Term_rec(Rep_term(t), %x y r. d(Inv(Leaf,x), Abs_Tlist(y), r))"
+
+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