--- 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)))))"