author  berghofe 
Fri, 24 Jul 1998 13:39:47 +0200  
changeset 5191  8ceaa19f7717 
parent 3842  b55686a7b22c 
child 5977  9f0c8869cf71 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/LList.thy 
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 1994 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 
Definition of type 'a llist by a greatest fixed point 
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 
Shares NIL, CONS, List_case with List.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

9 

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

10 
Still needs filter and flatten functions  hard because they need 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

11 
bounds on the amount of lookahead required. 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

12 

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

13 
Could try (but would it work for the gfp analogue of term?) 
3842  14 
LListD_Fun_def "LListD_Fun(A) == (%Z. diag({Numb(0)}) <++> diag(A) <**> Z)" 
3120
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 
A nice but complex example would be [ML for the Working Programmer, page 176] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

17 
from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1)))) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

18 

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

19 
Previous definition of llistD_Fun was explicit: 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

21 
"llistD_Fun(r) == 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

22 
{(LNil,LNil)} Un 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

23 
(UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

25 

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

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

27 

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

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

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

30 

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

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

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

33 

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

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

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

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

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

38 
('a item * 'a item)set" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

39 

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

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

41 
LListD :: "('a item * 'a item)set => ('a item * 'a item)set" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

42 
llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

43 

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

44 
Rep_llist :: 'a llist => 'a item 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

45 
Abs_llist :: 'a item => 'a llist 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

46 
LNil :: 'a llist 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

48 

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

49 
llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b 
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 
LList_corec_fun :: "[nat, 'a=>unit+('b item * 'a), 'a] => 'b item" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

52 
LList_corec :: "['a, 'a => unit + ('b item * 'a)] => 'b item" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

53 
llist_corec :: "['a, 'a => unit + ('b * 'a)] => 'b llist" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

54 

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

55 
Lmap :: ('a item => 'b item) => ('a item => 'b item) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

56 
lmap :: ('a=>'b) => ('a llist => 'b llist) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

57 

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

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

59 

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

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

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

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

63 

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 
coinductive "llist(A)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

67 
NIL_I "NIL: llist(A)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

68 
CONS_I "[ a: A; M: llist(A) ] ==> CONS a M : llist(A)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

69 

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

70 
coinductive "LListD(r)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

72 
NIL_I "(NIL, NIL) : LListD(r)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

73 
CONS_I "[ (a,b): r; (M,N) : LListD(r) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

74 
] ==> (CONS a M, CONS b N) : LListD(r)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

75 

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

76 
translations 
3842  77 
"case p of LNil => a  LCons x l => b" == "llist_case a (%x l. b) p" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

78 

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

79 

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

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

81 
(*Now used exclusively for abbreviating the coinduction rule*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

82 
list_Fun_def "list_Fun A X == 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

83 
{z. z = NIL  (? M a. z = CONS a M & a : A & M : X)}" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

84 

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

85 
LListD_Fun_def "LListD_Fun r X == 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

86 
{z. z = (NIL, NIL)  
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

87 
(? M N a b. z = (CONS a M, CONS b N) & 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

88 
(a, b) : r & (M, N) : X)}" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

89 

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

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

91 
LNil_def "LNil == Abs_llist(NIL)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

92 
LCons_def "LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

93 

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

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

95 
"llist_case c d l == 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

96 
List_case c (%x y. d (inv Leaf x) (Abs_llist y)) (Rep_llist l)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

97 

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

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

99 
"LList_corec_fun k f == 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

100 
nat_rec (%x. {}) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

101 
(%j r x. case f x of Inl u => NIL 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

102 
 Inr(z,w) => CONS z (r w)) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

104 

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

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

106 
"LList_corec a f == UN k. LList_corec_fun k f a" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

107 

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

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

109 
"llist_corec a f == 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

110 
Abs_llist(LList_corec a 
3842  111 
(%z. case f z of Inl x => Inl(x) 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

112 
 Inr(v,w) => Inr(Leaf(v), w)))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

113 

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

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

115 
"llistD_Fun(r) == 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

117 
LListD_Fun (diag(range Leaf)) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

118 
(prod_fun Rep_llist Rep_llist `` r)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

119 

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

120 
Lconst_def "Lconst(M) == lfp(%N. CONS M N)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

121 

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

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

123 
"Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

124 

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

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

126 
"lmap f l == llist_corec l (%z. case z of LNil => (Inl ()) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

127 
 LCons y z => Inr(f(y), z))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

128 

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

129 
iterates_def "iterates f a == llist_corec a (%x. Inr((x, f(x))))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

130 

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

131 
(*Append generates its result by applying f, where 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

132 
f((NIL,NIL)) = Inl(()) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

133 
f((NIL, CONS N1 N2)) = Inr((N1, (NIL,N2)) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

134 
f((CONS M1 M2, N)) = Inr((M1, (M2,N)) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

136 

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

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

138 
"Lappend M N == LList_corec (M,N) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

139 
(split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

140 
(%M1 M2 N. Inr((M1, (M2,N))))))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

141 

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

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

143 
"lappend l n == llist_corec (l,n) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

144 
(split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

145 
(%l1 l2 n. Inr((l1, (l2,n))))))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

146 

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

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

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

149 
Rep_llist "Rep_llist(xs): llist(range(Leaf))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

150 
Rep_llist_inverse "Abs_llist(Rep_llist(xs)) = xs" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

151 
Abs_llist_inverse "M: llist(range(Leaf)) ==> Rep_llist(Abs_llist(M)) = M" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

152 

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

153 
end 