--- a/ex/Simult.thy Thu Aug 18 12:42:19 1994 +0200
+++ b/ex/Simult.thy Thu Aug 18 12:48:03 1994 +0200
@@ -3,8 +3,7 @@
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
+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
@@ -19,7 +18,6 @@
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"
@@ -38,9 +36,6 @@
\ '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...*)
@@ -65,9 +60,8 @@
(*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)))))"
+\ Case(Split(%x y g. b(x,y,g(y))), \
+\ List_case(%g.c, %x y g. d(x,y,g(x),g(y)))))"
tree_rec_def
"tree_rec(t,b,c,d) == \