diff -r 872f866e630f -r d9527f97246e ex/Simult.thy
--- a/ex/Simult.thy	Wed Aug 24 18:49:29 1994 +0200
+++ b/ex/Simult.thy	Thu Aug 25 10:47:33 1994 +0200
@@ -1,4 +1,4 @@
-(*  Title: 	HOL/ex/simult
+(*  Title: 	HOL/ex/Simult
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
@@ -6,8 +6,11 @@
 A simultaneous recursive type definition: 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
+simpler because it uses list as a new type former.  The approach in this
 file may be superior for other simultaneous recursions.
+
+The inductive definition package does not help defining this sort of mutually
+recursive data structure because it uses Inl, Inr instead of In0, In1.
 *)
 
 Simult = List +
@@ -18,27 +21,38 @@
 arities  tree,forest :: (term)term
 
 consts
-  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"
+  TF          :: "'a item set => 'a item set"
+  FNIL        :: "'a item"
+  TCONS,FCONS :: "['a item, 'a item] => 'a item"
+  Rep_Tree    :: "'a tree => 'a item"
+  Abs_Tree    :: "'a item => 'a tree"
+  Rep_Forest  :: "'a forest => 'a item"
+  Abs_Forest  :: "'a item => '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"
+  TF_rec      :: "['a item, ['a item , 'a item, 'b]=>'b,     \
+\                 'b, ['a item , 'a item, '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
+defs
+     (*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)))"
+
   TF_def	"TF(A) == lfp(%Z. A <*> Part(Z,In1) \
 \                           <+> ({Numb(0)} <+> Part(Z,In0) <*> Part(Z,In1)))"
-    (*faking a type definition for tree...*)
+
+rules
+  (*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"
@@ -48,18 +62,11 @@
   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)))"
 
+defs
      (*recursion*)
   TF_rec_def	
-   "TF_rec(M,b,c,d) == wfrec(trancl(pred_Sexp), M, 			\
+   "TF_rec(M,b,c,d) == wfrec(trancl(pred_sexp), M, 			\
 \               Case(Split(%x y g. b(x,y,g(y))),		\
 \	              List_case(%g.c, %x y g. d(x,y,g(x),g(y)))))"