969
|
1 |
(* Title: HOL/ex/Simult
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
|
6 |
A simultaneous recursive type definition: trees & forests
|
|
7 |
|
|
8 |
This is essentially the same data structure that on ex/term.ML, which is
|
|
9 |
simpler because it uses list as a new type former. The approach in this
|
|
10 |
file may be superior for other simultaneous recursions.
|
|
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.
|
|
14 |
*)
|
|
15 |
|
|
16 |
Simult = SList +
|
|
17 |
|
|
18 |
types 'a tree
|
|
19 |
'a forest
|
|
20 |
|
|
21 |
arities tree,forest :: (term)term
|
|
22 |
|
|
23 |
consts
|
1376
|
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
|
|
31 |
Tcons :: ['a, 'a forest] => 'a tree
|
|
32 |
Fcons :: ['a tree, 'a forest] => 'a forest
|
|
33 |
Fnil :: 'a forest
|
1381
|
34 |
TF_rec :: ['a item, ['a item , 'a item, 'b]=>'b,
|
|
35 |
'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b
|
|
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
|
969
|
40 |
|
|
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 |
|
1151
|
51 |
TF_def "TF(A) == lfp(%Z. A <*> Part Z In1
|
|
52 |
<+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"
|
969
|
53 |
|
|
54 |
rules
|
|
55 |
(*faking a type definition for tree...*)
|
|
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 |
|
|
66 |
defs
|
|
67 |
(*recursion*)
|
|
68 |
TF_rec_def
|
1151
|
69 |
"TF_rec M b c d == wfrec (trancl pred_sexp) M
|
|
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))))"
|
969
|
72 |
|
|
73 |
tree_rec_def
|
1151
|
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)"
|
969
|
77 |
|
|
78 |
forest_rec_def
|
1151
|
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)"
|
969
|
82 |
end
|