diff -r 000000000000 -r 7949f97df77a ex/simult.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/simult.thy	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,77 @@
+(*  Title: 	HOL/ex/simult
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Primitives for simultaneous recursive type definitions
+  includes worked example of trees & forests
+
+This is essentially the same data structure that on ex/term.ML, which is
+simpler because it uses List as a new type former.  The approach in this
+file may be superior for other simultaneous recursions.
+*)
+
+Simult = List +
+types tree,forest 1
+arities tree,forest :: (term)term
+consts
+  Part        :: "['a set, 'a=>'a] => 'a set"
+  TF          :: "'a node set set => 'a node set set"
+  FNIL        :: "'a node set"
+  TCONS,FCONS :: "['a node set, 'a node set] => 'a node set"
+  Rep_Tree    :: "'a tree => 'a node set"
+  Abs_Tree    :: "'a node set => 'a tree"
+  Rep_Forest  :: "'a forest => 'a node set"
+  Abs_Forest  :: "'a node set => 'a forest"
+  Tcons       :: "['a, 'a forest] => 'a tree"
+  Fcons       :: "['a tree, 'a forest] => 'a forest"
+  Fnil        :: "'a forest"
+  TF_rec      :: "['a node set, ['a node set , 'a node set, 'b]=>'b,     \
+\                 'b, ['a node set , 'a node set, 'b, 'b]=>'b] => 'b"
+  tree_rec    :: "['a tree, ['a, 'a forest, 'b]=>'b,          \
+\                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
+  forest_rec  :: "['a forest, ['a, 'a forest, 'b]=>'b,        \
+\                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
+
+rules
+    (*operator for selecting out the various types*)
+  Part_def	"Part(A,h) == {x. x:A & (? z. x = h(z))}"
+
+  TF_def	"TF(A) == lfp(%Z. A <*> Part(Z,In1) \
+\                           <+> ({Numb(0)} <+> Part(Z,In0) <*> Part(Z,In1)))"
+    (*faking a type definition for tree...*)
+  Rep_Tree 	   "Rep_Tree(n): Part(TF(range(Leaf)),In0)"
+  Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t"
+  Abs_Tree_inverse "z: Part(TF(range(Leaf)),In0) ==> Rep_Tree(Abs_Tree(z)) = z"
+    (*faking a type definition for forest...*)
+  Rep_Forest 	     "Rep_Forest(n): Part(TF(range(Leaf)),In1)"
+  Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts"
+  Abs_Forest_inverse 
+	"z: Part(TF(range(Leaf)),In1) ==> Rep_Forest(Abs_Forest(z)) = z"
+
+     (*the concrete constants*)
+  TCONS_def 	"TCONS(M,N) == In0(M . N)"
+  FNIL_def	"FNIL       == In1(NIL)"
+  FCONS_def	"FCONS(M,N) == In1(CONS(M,N))"
+     (*the abstract constants*)
+  Tcons_def 	"Tcons(a,ts) == Abs_Tree(TCONS(Leaf(a), Rep_Forest(ts)))"
+  Fnil_def  	"Fnil        == Abs_Forest(FNIL)"
+  Fcons_def 	"Fcons(t,ts) == Abs_Forest(FCONS(Rep_Tree(t), Rep_Forest(ts)))"
+
+     (*recursion*)
+  TF_rec_def	
+   "TF_rec(M,b,c,d) == wfrec(trancl(pred_Sexp), M, 			\
+\               %Z g. Case(Z, %U. Split(U, %x y. b(x,y,g(y))),		\
+\			      %V. List_case(V, c, 			\
+\                                           %x y. d(x,y,g(x),g(y)))))"
+
+  tree_rec_def
+   "tree_rec(t,b,c,d) == \
+\   TF_rec(Rep_Tree(t), %x y r. b(Inv(Leaf,x), Abs_Forest(y), r), \
+\          c, %x y rt rf. d(Abs_Tree(x), Abs_Forest(y), rt, rf))"
+
+  forest_rec_def
+   "forest_rec(tf,b,c,d) == \
+\   TF_rec(Rep_Forest(tf), %x y r. b(Inv(Leaf,x), Abs_Forest(y), r), \
+\          c, %x y rt rf. d(Abs_Tree(x), Abs_Forest(y), rt, rf))"
+end