|
127
|
1 |
(* Title: HOL/ex/Simult
|
|
0
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1993 University of Cambridge
|
|
|
5 |
|
|
114
|
6 |
A simultaneous recursive type definition: trees & forests
|
|
0
|
7 |
|
|
|
8 |
This is essentially the same data structure that on ex/term.ML, which is
|
|
127
|
9 |
simpler because it uses list as a new type former. The approach in this
|
|
0
|
10 |
file may be superior for other simultaneous recursions.
|
|
127
|
11 |
|
|
|
12 |
The inductive definition package does not help defining this sort of mutually
|
|
|
13 |
recursive data structure because it uses Inl, Inr instead of In0, In1.
|
|
0
|
14 |
*)
|
|
|
15 |
|
|
|
16 |
Simult = List +
|
|
72
|
17 |
|
|
|
18 |
types 'a tree
|
|
|
19 |
'a forest
|
|
|
20 |
|
|
|
21 |
arities tree,forest :: (term)term
|
|
|
22 |
|
|
0
|
23 |
consts
|
|
127
|
24 |
TF :: "'a item set => 'a item set"
|
|
|
25 |
FNIL :: "'a item"
|
|
|
26 |
TCONS,FCONS :: "['a item, 'a item] => 'a item"
|
|
|
27 |
Rep_Tree :: "'a tree => 'a item"
|
|
|
28 |
Abs_Tree :: "'a item => 'a tree"
|
|
|
29 |
Rep_Forest :: "'a forest => 'a item"
|
|
|
30 |
Abs_Forest :: "'a item => 'a forest"
|
|
0
|
31 |
Tcons :: "['a, 'a forest] => 'a tree"
|
|
|
32 |
Fcons :: "['a tree, 'a forest] => 'a forest"
|
|
|
33 |
Fnil :: "'a forest"
|
|
127
|
34 |
TF_rec :: "['a item, ['a item , 'a item, 'b]=>'b, \
|
|
|
35 |
\ 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
|
|
0
|
36 |
tree_rec :: "['a tree, ['a, 'a forest, 'b]=>'b, \
|
|
|
37 |
\ 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
|
|
|
38 |
forest_rec :: "['a forest, ['a, 'a forest, 'b]=>'b, \
|
|
|
39 |
\ 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
|
|
|
40 |
|
|
127
|
41 |
defs
|
|
|
42 |
(*the concrete constants*)
|
|
|
43 |
TCONS_def "TCONS(M,N) == In0(M $ N)"
|
|
|
44 |
FNIL_def "FNIL == In1(NIL)"
|
|
|
45 |
FCONS_def "FCONS(M,N) == In1(CONS(M,N))"
|
|
|
46 |
(*the abstract constants*)
|
|
|
47 |
Tcons_def "Tcons(a,ts) == Abs_Tree(TCONS(Leaf(a), Rep_Forest(ts)))"
|
|
|
48 |
Fnil_def "Fnil == Abs_Forest(FNIL)"
|
|
|
49 |
Fcons_def "Fcons(t,ts) == Abs_Forest(FCONS(Rep_Tree(t), Rep_Forest(ts)))"
|
|
|
50 |
|
|
0
|
51 |
TF_def "TF(A) == lfp(%Z. A <*> Part(Z,In1) \
|
|
|
52 |
\ <+> ({Numb(0)} <+> Part(Z,In0) <*> Part(Z,In1)))"
|
|
127
|
53 |
|
|
|
54 |
rules
|
|
|
55 |
(*faking a type definition for tree...*)
|
|
0
|
56 |
Rep_Tree "Rep_Tree(n): Part(TF(range(Leaf)),In0)"
|
|
|
57 |
Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t"
|
|
|
58 |
Abs_Tree_inverse "z: Part(TF(range(Leaf)),In0) ==> Rep_Tree(Abs_Tree(z)) = z"
|
|
|
59 |
(*faking a type definition for forest...*)
|
|
|
60 |
Rep_Forest "Rep_Forest(n): Part(TF(range(Leaf)),In1)"
|
|
|
61 |
Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts"
|
|
|
62 |
Abs_Forest_inverse
|
|
|
63 |
"z: Part(TF(range(Leaf)),In1) ==> Rep_Forest(Abs_Forest(z)) = z"
|
|
|
64 |
|
|
|
65 |
|
|
127
|
66 |
defs
|
|
0
|
67 |
(*recursion*)
|
|
|
68 |
TF_rec_def
|
|
127
|
69 |
"TF_rec(M,b,c,d) == wfrec(trancl(pred_sexp), M, \
|
|
114
|
70 |
\ Case(Split(%x y g. b(x,y,g(y))), \
|
|
|
71 |
\ List_case(%g.c, %x y g. d(x,y,g(x),g(y)))))"
|
|
0
|
72 |
|
|
|
73 |
tree_rec_def
|
|
|
74 |
"tree_rec(t,b,c,d) == \
|
|
|
75 |
\ TF_rec(Rep_Tree(t), %x y r. b(Inv(Leaf,x), Abs_Forest(y), r), \
|
|
|
76 |
\ c, %x y rt rf. d(Abs_Tree(x), Abs_Forest(y), rt, rf))"
|
|
|
77 |
|
|
|
78 |
forest_rec_def
|
|
|
79 |
"forest_rec(tf,b,c,d) == \
|
|
|
80 |
\ TF_rec(Rep_Forest(tf), %x y r. b(Inv(Leaf,x), Abs_Forest(y), r), \
|
|
|
81 |
\ c, %x y rt rf. d(Abs_Tree(x), Abs_Forest(y), rt, rf))"
|
|
|
82 |
end
|