ex/term.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/term.thy	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,44 @@
+(*  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
+  (essentially the same type as in Trees & Forests)
+
+There is no constructor APP because it is simply cons (.) 
+*)
+
+Term = List +
+types term 1
+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"
+  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 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*)
+  Term_rec_def	
+   "Term_rec(M,d) == wfrec(trancl(pred_Sexp),  M, \
+\            %M g. Split(M, %x y. 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))"
+end