author  paulson 
Wed, 07 May 1997 12:50:26 +0200  
changeset 3120  c58423c20740 
child 5191  8ceaa19f7717 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/ex/Simult 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

2 
ID: $Id$ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

4 
Copyright 1993 University of Cambridge 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

5 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

6 
A simultaneous recursive type definition: trees & forests 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

7 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

8 
This is essentially the same data structure that on ex/term.ML, which is 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

9 
simpler because it uses list as a new type former. The approach in this 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

10 
file may be superior for other simultaneous recursions. 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

11 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

12 
The inductive definition package does not help defining this sort of mutually 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

13 
recursive data structure because it uses Inl, Inr instead of In0, In1. 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

14 
*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

15 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

16 
Simult = SList + 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

17 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

18 
types 'a tree 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

19 
'a forest 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

20 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

21 
arities tree,forest :: (term)term 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

22 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

23 
consts 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

24 
TF :: 'a item set => 'a item set 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

25 
FNIL :: 'a item 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

26 
TCONS,FCONS :: ['a item, 'a item] => 'a item 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

27 
Rep_Tree :: 'a tree => 'a item 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

28 
Abs_Tree :: 'a item => 'a tree 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

29 
Rep_Forest :: 'a forest => 'a item 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

30 
Abs_Forest :: 'a item => 'a forest 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

31 
Tcons :: ['a, 'a forest] => 'a tree 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

32 
Fcons :: ['a tree, 'a forest] => 'a forest 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

33 
Fnil :: 'a forest 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

34 
TF_rec :: ['a item, ['a item , 'a item, 'b]=>'b, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

35 
'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

36 
tree_rec :: ['a tree, ['a, 'a forest, 'b]=>'b, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

37 
'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

38 
forest_rec :: ['a forest, ['a, 'a forest, 'b]=>'b, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

39 
'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

40 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

41 
defs 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

42 
(*the concrete constants*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

43 
TCONS_def "TCONS M N == In0(M $ N)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

44 
FNIL_def "FNIL == In1(NIL)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

45 
FCONS_def "FCONS M N == In1(CONS M N)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

46 
(*the abstract constants*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

47 
Tcons_def "Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

48 
Fnil_def "Fnil == Abs_Forest(FNIL)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

49 
Fcons_def "Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

50 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

51 
TF_def "TF(A) == lfp(%Z. A <*> Part Z In1 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

52 
<+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

53 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

54 
rules 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

55 
(*faking a type definition for tree...*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

56 
Rep_Tree "Rep_Tree(n): Part (TF(range Leaf)) In0" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

57 
Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

58 
Abs_Tree_inverse "z: Part (TF(range Leaf)) In0 ==> Rep_Tree(Abs_Tree(z)) = z" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

59 
(*faking a type definition for forest...*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

60 
Rep_Forest "Rep_Forest(n): Part (TF(range Leaf)) In1" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

61 
Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

62 
Abs_Forest_inverse 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

63 
"z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

64 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

65 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

66 
defs 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

67 
(*recursion*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

68 
TF_rec_def 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

69 
"TF_rec M b c d == wfrec (trancl pred_sexp) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

70 
(%g. Case (Split(%x y. b x y (g y))) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

71 
(List_case c (%x y. d x y (g x) (g y)))) M" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

72 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

73 
tree_rec_def 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

74 
"tree_rec t b c d == 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

75 
TF_rec (Rep_Tree t) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

76 
c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

77 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

78 
forest_rec_def 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

79 
"forest_rec tf b c d == 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

80 
TF_rec (Rep_Forest tf) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

81 
c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

82 
end 