author  paulson 
Mon, 30 Nov 1998 10:44:05 +0100  
changeset 5996  6b6e0ede3517 
parent 5977  9f0c8869cf71 
child 7256  0a69baf28961 
permissions  rwrr 
5089
f95e0a6eb775
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5086
diff
changeset

1 
(* Title: HOL/Induct/LList 
3120
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 
SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)? 
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 

4160  9 
bind_thm ("UN1_I", UNIV_I RS UN_I); 
10 

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

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

12 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

13 
Addsplits [option.split]; 
3120
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 
(*This justifies using llist in other recursive type definitions*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5102
diff
changeset

16 
Goalw llist.defs "A<=B ==> llist(A) <= llist(B)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

17 
by (rtac gfp_mono 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

18 
by (REPEAT (ares_tac basic_monos 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

19 
qed "llist_mono"; 
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 

5069  22 
Goal "llist(A) = {Numb(0)} <+> (A <*> llist(A))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

23 
let val rew = rewrite_rule [NIL_def, CONS_def] in 
4089  24 
by (fast_tac (claset() addSIs (map rew llist.intrs) 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

25 
addEs [rew llist.elim]) 1) 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

27 
qed "llist_unfold"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

28 

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

29 

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

30 
(*** Type checking by coinduction, using list_Fun 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

31 
THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS! 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

33 

5069  34 
Goalw [list_Fun_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

35 
"[ M : X; X <= list_Fun A (X Un llist(A)) ] ==> M : llist(A)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

36 
by (etac llist.coinduct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

37 
by (etac (subsetD RS CollectD) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

38 
by (assume_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

39 
qed "llist_coinduct"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

40 

5069  41 
Goalw [list_Fun_def, NIL_def] "NIL: list_Fun A X"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

42 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

43 
qed "list_Fun_NIL_I"; 
4521  44 
AddIffs [list_Fun_NIL_I]; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

45 

5069  46 
Goalw [list_Fun_def,CONS_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

47 
"[ M: A; N: X ] ==> CONS M N : list_Fun A X"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

48 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

49 
qed "list_Fun_CONS_I"; 
4521  50 
Addsimps [list_Fun_CONS_I]; 
51 
AddSIs [list_Fun_CONS_I]; 

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

52 

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

53 
(*Utilise the "strong" part, i.e. gfp(f)*) 
5069  54 
Goalw (llist.defs @ [list_Fun_def]) 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

55 
"M: llist(A) ==> M : list_Fun A (X Un llist(A))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

56 
by (etac (llist.mono RS gfp_fun_UnI2) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

57 
qed "list_Fun_llist_I"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

58 

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

59 
(*** LList_corec satisfies the desired recurion equation ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

60 

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

61 
(*A continuity result?*) 
5069  62 
Goalw [CONS_def] "CONS M (UN x. f(x)) = (UN x. CONS M (f x))"; 
4089  63 
by (simp_tac (simpset() addsimps [In1_UN1, Scons_UN1_y]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

64 
qed "CONS_UN1"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

65 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

66 
Goalw [CONS_def] "[ M<=M'; N<=N' ] ==> CONS M N <= CONS M' N'"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

67 
by (REPEAT (ares_tac [In1_mono,Scons_mono] 1)); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

68 
qed "CONS_mono"; 
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 
Addsimps [LList_corec_fun_def RS def_nat_rec_0, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

71 
LList_corec_fun_def RS def_nat_rec_Suc]; 
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 
(** The directions of the equality are proved separately **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

74 

5069  75 
Goalw [LList_corec_def] 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

76 
"LList_corec a f <= \ 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

77 
\ (case f a of None => NIL  Some(z,w) => CONS z (LList_corec w f))"; 
4160  78 
by (rtac UN_least 1); 
79 
by (exhaust_tac "k" 1); 

80 
by (ALLGOALS Asm_simp_tac); 

81 
by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, 

82 
UNIV_I RS UN_upper] 1)); 

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

83 
qed "LList_corec_subset1"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

84 

5069  85 
Goalw [LList_corec_def] 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

86 
"(case f a of None => NIL  Some(z,w) => CONS z (LList_corec w f)) <= \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

87 
\ LList_corec a f"; 
4089  88 
by (simp_tac (simpset() addsimps [CONS_UN1]) 1); 
4160  89 
by Safe_tac; 
90 
by (ALLGOALS (res_inst_tac [("a","Suc(?k)")] UN_I)); 

91 
by (ALLGOALS Asm_simp_tac); 

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

92 
qed "LList_corec_subset2"; 
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 
(*the recursion equation for LList_corec  NOT SUITABLE FOR REWRITING!*) 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

95 
Goal "LList_corec a f = \ 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

96 
\ (case f a of None => NIL  Some(z,w) => CONS z (LList_corec w f))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

97 
by (REPEAT (resolve_tac [equalityI, LList_corec_subset1, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

98 
LList_corec_subset2] 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

99 
qed "LList_corec"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

100 

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

101 
(*definitional version of same*) 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

102 
val [rew] = 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

103 
Goal "[ !!x. h(x) == LList_corec x f ] \ 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

104 
\ ==> h(a) = (case f a of None => NIL  Some(z,w) => CONS z (h w))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

105 
by (rewtac rew); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

106 
by (rtac LList_corec 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

107 
qed "def_LList_corec"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

108 

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

109 
(*A typical use of coinduction to show membership in the gfp. 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

110 
Bisimulation is range(%x. LList_corec x f) *) 
5069  111 
Goal "LList_corec a f : llist({u. True})"; 
3842  112 
by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

113 
by (rtac rangeI 1); 
4160  114 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

115 
by (stac LList_corec 1); 
4521  116 
by (Simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

117 
qed "LList_corec_type"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

118 

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 
(**** llist equality as a gfp; the bisimulation principle ****) 
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 
(*This theorem is actually used, unlike the many similar ones in ZF*) 
5069  123 
Goal "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

124 
let val rew = rewrite_rule [NIL_def, CONS_def] in 
4089  125 
by (fast_tac (claset() addSIs (map rew LListD.intrs) 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

126 
addEs [rew LListD.elim]) 1) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

128 
qed "LListD_unfold"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

129 

5788  130 
Goal "!M N. (M,N) : LListD(diag A) > ntrunc k M = ntrunc k N"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

131 
by (res_inst_tac [("n", "k")] less_induct 1); 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

132 
by (safe_tac (claset() delrules [equalityI])); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

133 
by (etac LListD.elim 1); 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

134 
by (safe_tac (claset() delrules [equalityI])); 
5184  135 
by (exhaust_tac "n" 1); 
4521  136 
by (Asm_simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

137 
by (rename_tac "n'" 1); 
5184  138 
by (exhaust_tac "n'" 1); 
4521  139 
by (asm_simp_tac (simpset() addsimps [CONS_def]) 1); 
140 
by (asm_simp_tac (simpset() addsimps [CONS_def, less_Suc_eq]) 1); 

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

141 
qed "LListD_implies_ntrunc_equality"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

142 

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

143 
(*The domain of the LListD relation*) 
5069  144 
Goalw (llist.defs @ [NIL_def, CONS_def]) 
5788  145 
"Domain (LListD(diag A)) <= llist(A)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

146 
by (rtac gfp_upperbound 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

147 
(*avoids unfolding LListD on the rhs*) 
5788  148 
by (res_inst_tac [("P", "%x. Domain x <= ?B")] (LListD_unfold RS ssubst) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

149 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

150 
by (Fast_tac 1); 
5788  151 
qed "Domain_LListD"; 
3120
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 
(*This inclusion justifies the use of coinduction to show M=N*) 
5788  154 
Goal "LListD(diag A) <= diag(llist(A))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

155 
by (rtac subsetI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

156 
by (res_inst_tac [("p","x")] PairE 1); 
4160  157 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

158 
by (rtac diag_eqI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

159 
by (rtac (LListD_implies_ntrunc_equality RS spec RS spec RS mp RS 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

161 
by (assume_tac 1); 
5788  162 
by (etac (DomainI RS (Domain_LListD RS subsetD)) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

163 
qed "LListD_subset_diag"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

164 

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

165 

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

166 
(** Coinduction, using LListD_Fun 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

167 
THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS! 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

169 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5102
diff
changeset

170 
Goalw [LListD_Fun_def] "A<=B ==> LListD_Fun r A <= LListD_Fun r B"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

171 
by (REPEAT (ares_tac basic_monos 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

172 
qed "LListD_Fun_mono"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

173 

5069  174 
Goalw [LListD_Fun_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

175 
"[ M : X; X <= LListD_Fun r (X Un LListD(r)) ] ==> M : LListD(r)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

176 
by (etac LListD.coinduct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

177 
by (etac (subsetD RS CollectD) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

178 
by (assume_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

179 
qed "LListD_coinduct"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

180 

5069  181 
Goalw [LListD_Fun_def,NIL_def] "(NIL,NIL) : LListD_Fun r s"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

182 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

183 
qed "LListD_Fun_NIL_I"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

184 

5069  185 
Goalw [LListD_Fun_def,CONS_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

186 
"[ x:A; (M,N):s ] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

187 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

188 
qed "LListD_Fun_CONS_I"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

189 

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

190 
(*Utilise the "strong" part, i.e. gfp(f)*) 
5069  191 
Goalw (LListD.defs @ [LListD_Fun_def]) 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

192 
"M: LListD(r) ==> M : LListD_Fun r (X Un LListD(r))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

193 
by (etac (LListD.mono RS gfp_fun_UnI2) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

194 
qed "LListD_Fun_LListD_I"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

195 

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

196 

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

197 
(*This converse inclusion helps to strengthen LList_equalityI*) 
5788  198 
Goal "diag(llist(A)) <= LListD(diag A)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

199 
by (rtac subsetI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

200 
by (etac LListD_coinduct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

201 
by (rtac subsetI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

202 
by (etac diagE 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

203 
by (etac ssubst 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

204 
by (eresolve_tac [llist.elim] 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

205 
by (ALLGOALS 
4089  206 
(asm_simp_tac (simpset() addsimps [diagI, LListD_Fun_NIL_I, 
4521  207 
LListD_Fun_CONS_I]))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

208 
qed "diag_subset_LListD"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

209 

5788  210 
Goal "LListD(diag A) = diag(llist(A))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

211 
by (REPEAT (resolve_tac [equalityI, LListD_subset_diag, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

212 
diag_subset_LListD] 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

213 
qed "LListD_eq_diag"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

214 

5278  215 
Goal "M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

216 
by (rtac (LListD_eq_diag RS subst) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

217 
by (rtac LListD_Fun_LListD_I 1); 
4089  218 
by (asm_simp_tac (simpset() addsimps [LListD_eq_diag, diagI]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

219 
qed "LListD_Fun_diag_I"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

220 

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

221 

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

222 
(** To show two LLists are equal, exhibit a bisimulation! 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

223 
[also admits true equality] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

224 
Replace "A" by some particular set, like {x.True}??? *) 
5278  225 
Goal "[ (M,N) : r; r <= LListD_Fun (diag A) (r Un diag(llist(A))) \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

226 
\ ] ==> M=N"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

227 
by (rtac (LListD_subset_diag RS subsetD RS diagE) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

228 
by (etac LListD_coinduct 1); 
4089  229 
by (asm_simp_tac (simpset() addsimps [LListD_eq_diag]) 1); 
4160  230 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

231 
qed "LList_equalityI"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

232 

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

233 

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

234 
(*** Finality of llist(A): Uniqueness of functions defined by corecursion ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

235 

4521  236 
(*We must remove Pair_eq because it may turn an instance of reflexivity 
237 
(h1 b, h2 b) = (h1 ?x17, h2 ?x17) into a conjunction! 

238 
(or strengthen the Solver?) 

239 
*) 

240 
Delsimps [Pair_eq]; 

241 

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

242 
(*abstract proof using a bisimulation*) 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

243 
val [prem1,prem2] = 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

244 
Goal 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

245 
"[ !!x. h1(x) = (case f x of None => NIL  Some(z,w) => CONS z (h1 w)); \ 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

246 
\ !!x. h2(x) = (case f x of None => NIL  Some(z,w) => CONS z (h2 w)) ]\ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

247 
\ ==> h1=h2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

248 
by (rtac ext 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

249 
(*next step avoids an unknown (and flexflex pair) in simplification*) 
3842  250 
by (res_inst_tac [("A", "{u. True}"), 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

251 
("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

252 
by (rtac rangeI 1); 
4160  253 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

254 
by (stac prem1 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

255 
by (stac prem2 1); 
4089  256 
by (simp_tac (simpset() addsimps [LListD_Fun_NIL_I, 
4521  257 
CollectI RS LListD_Fun_CONS_I]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

258 
qed "LList_corec_unique"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

259 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

260 
val [prem] = 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

261 
Goal 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

262 
"[ !!x. h(x) = (case f x of None => NIL  Some(z,w) => CONS z (h w)) ] \ 
3842  263 
\ ==> h = (%x. LList_corec x f)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

264 
by (rtac (LList_corec RS (prem RS LList_corec_unique)) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

265 
qed "equals_LList_corec"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

266 

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

267 

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

268 
(** Obsolete LList_corec_unique proof: complete induction, not coinduction **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

269 

5069  270 
Goalw [CONS_def] "ntrunc (Suc 0) (CONS M N) = {}"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

271 
by (rtac ntrunc_one_In1 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

272 
qed "ntrunc_one_CONS"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

273 

5069  274 
Goalw [CONS_def] 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

275 
"ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)"; 
4521  276 
by (Simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

277 
qed "ntrunc_CONS"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

278 

4521  279 
Addsimps [ntrunc_one_CONS, ntrunc_CONS]; 
280 

281 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

282 
val [prem1,prem2] = 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

283 
Goal 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

284 
"[ !!x. h1(x) = (case f x of None => NIL  Some(z,w) => CONS z (h1 w)); \ 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

285 
\ !!x. h2(x) = (case f x of None => NIL  Some(z,w) => CONS z (h2 w)) ]\ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

286 
\ ==> h1=h2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

287 
by (rtac (ntrunc_equality RS ext) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

288 
by (rename_tac "x k" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

289 
by (res_inst_tac [("x", "x")] spec 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

290 
by (res_inst_tac [("n", "k")] less_induct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

291 
by (rename_tac "n" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

292 
by (rtac allI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

293 
by (rename_tac "y" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

294 
by (stac prem1 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

295 
by (stac prem2 1); 
4831  296 
by (Simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

297 
by (strip_tac 1); 
5184  298 
by (exhaust_tac "n" 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

299 
by (rename_tac "m" 2); 
5184  300 
by (exhaust_tac "m" 2); 
4521  301 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq]))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

303 

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

304 

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

305 
(*** Lconst  defined directly using lfp, but equivalent to a LList_corec ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

306 

5069  307 
Goal "mono(CONS(M))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

308 
by (REPEAT (ares_tac [monoI, subset_refl, CONS_mono] 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

309 
qed "Lconst_fun_mono"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

310 

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

311 
(* Lconst(M) = CONS M (Lconst M) *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

312 
bind_thm ("Lconst", (Lconst_fun_mono RS (Lconst_def RS def_lfp_Tarski))); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

313 

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

314 
(*A typical use of coinduction to show membership in the gfp. 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

315 
The containing set is simply the singleton {Lconst(M)}. *) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5102
diff
changeset

316 
Goal "M:A ==> Lconst(M): llist(A)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

317 
by (rtac (singletonI RS llist_coinduct) 1); 
4160  318 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

319 
by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

320 
by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

321 
qed "Lconst_type"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

322 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

323 
Goal "Lconst(M) = LList_corec M (%x. Some((x,x)))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

324 
by (rtac (equals_LList_corec RS fun_cong) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

325 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

326 
by (rtac Lconst 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

327 
qed "Lconst_eq_LList_corec"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

328 

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

329 
(*Thus we could have used gfp in the definition of Lconst*) 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

330 
Goal "gfp(%N. CONS M N) = LList_corec M (%x. Some((x,x)))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

331 
by (rtac (equals_LList_corec RS fun_cong) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

332 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

333 
by (rtac (Lconst_fun_mono RS gfp_Tarski) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

334 
qed "gfp_Lconst_eq_LList_corec"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

335 

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

336 

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

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

338 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

339 
Goal "inj Rep_LList"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

340 
by (rtac inj_inverseI 1); 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

341 
by (rtac Rep_LList_inverse 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

342 
qed "inj_Rep_LList"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

343 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

344 
Goal "inj_on Abs_LList LList"; 
4831  345 
by (rtac inj_on_inverseI 1); 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

346 
by (etac Abs_LList_inverse 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

347 
qed "inj_on_Abs_LList"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

348 

9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

349 
Goalw [LList_def] "x : llist (range Leaf) ==> x : LList"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

350 
by (Asm_simp_tac 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

351 
qed "LListI"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

352 

9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

353 
Goalw [LList_def] "x : LList ==> x : llist (range Leaf)"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

354 
by (Asm_simp_tac 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

355 
qed "LListD"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

356 

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

357 

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

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

359 

5069  360 
Goalw [LNil_def,LCons_def] "~ LCons x xs = LNil"; 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

361 
by (rtac (CONS_not_NIL RS (inj_on_Abs_LList RS inj_on_contraD)) 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

362 
by (REPEAT (resolve_tac (llist.intrs @ 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

363 
[rangeI, LListI, Rep_LList RS LListD]) 1)); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

364 
qed "LCons_not_LNil"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

365 

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

366 
bind_thm ("LNil_not_LCons", LCons_not_LNil RS not_sym); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

367 

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

368 
AddIffs [LCons_not_LNil, LNil_not_LCons]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

369 

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

370 

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

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

372 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

373 
Goalw [LNil_def] "Rep_LList LNil = NIL"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

374 
by (rtac (llist.NIL_I RS LListI RS Abs_LList_inverse) 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

375 
qed "Rep_LList_LNil"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

376 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

377 
Goalw [LCons_def] "Rep_LList(LCons x l) = CONS (Leaf x) (Rep_LList l)"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

378 
by (REPEAT (resolve_tac [llist.CONS_I RS LListI RS Abs_LList_inverse, 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

379 
rangeI, Rep_LList RS LListD] 1)); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

380 
qed "Rep_LList_LCons"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

381 

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

382 
(** Injectiveness of CONS and LCons **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

383 

5069  384 
Goalw [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')"; 
4089  385 
by (fast_tac (claset() addSEs [Scons_inject]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

386 
qed "CONS_CONS_eq2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

387 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

388 
bind_thm ("CONS_inject", CONS_CONS_eq RS iffD1 RS conjE); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

389 

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

390 

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

391 
(*For reasoning about abstract llist constructors*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

392 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

393 
AddIs [Rep_LList RS LListD, LListI]; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

394 
AddIs llist.intrs; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

395 

9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

396 
AddSDs [inj_on_Abs_LList RS inj_onD, 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

397 
inj_Rep_LList RS injD]; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

398 

5069  399 
Goalw [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

400 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

401 
qed "LCons_LCons_eq"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

402 

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

403 
AddIffs [LCons_LCons_eq]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

404 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

405 
Goal "CONS M N: llist(A) ==> M: A & N: llist(A)"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

406 
by (etac llist.elim 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

407 
by (etac CONS_neq_NIL 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

408 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

409 
qed "CONS_D2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

410 

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

411 

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

412 
(****** Reasoning about llist(A) ******) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

413 

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

414 
Addsimps [List_case_NIL, List_case_CONS]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

415 

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

416 
(*A special case of list_equality for functions over lazy lists*) 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

417 
val [Mlist,gMlist,NILcase,CONScase] = 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

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

419 
"[ M: llist(A); g(NIL): llist(A); \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

420 
\ f(NIL)=g(NIL); \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

421 
\ !!x l. [ x:A; l: llist(A) ] ==> \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

422 
\ (f(CONS x l),g(CONS x l)) : \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

423 
\ LListD_Fun (diag A) ((%u.(f(u),g(u)))``llist(A) Un \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

424 
\ diag(llist(A))) \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

425 
\ ] ==> f(M) = g(M)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

426 
by (rtac LList_equalityI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

427 
by (rtac (Mlist RS imageI) 1); 
4521  428 
by (rtac image_subsetI 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

429 
by (etac llist.elim 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

430 
by (etac ssubst 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

431 
by (stac NILcase 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

432 
by (rtac (gMlist RS LListD_Fun_diag_I) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

433 
by (etac ssubst 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

434 
by (REPEAT (ares_tac [CONScase] 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

435 
qed "LList_fun_equalityI"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

436 

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

437 

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

438 
(*** The functional "Lmap" ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

439 

5069  440 
Goal "Lmap f NIL = NIL"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

441 
by (rtac (Lmap_def RS def_LList_corec RS trans) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

442 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

443 
qed "Lmap_NIL"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

444 

5069  445 
Goal "Lmap f (CONS M N) = CONS (f M) (Lmap f N)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

446 
by (rtac (Lmap_def RS def_LList_corec RS trans) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

447 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

448 
qed "Lmap_CONS"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

449 

4521  450 
Addsimps [Lmap_NIL, Lmap_CONS]; 
451 

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

452 
(*Another typechecking proof by coinduction*) 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

453 
val [major,minor] = 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

454 
Goal "[ M: llist(A); !!x. x:A ==> f(x):B ] ==> Lmap f M: llist(B)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

455 
by (rtac (major RS imageI RS llist_coinduct) 1); 
4160  456 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

457 
by (etac llist.elim 1); 
4521  458 
by (ALLGOALS Asm_simp_tac); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

459 
by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

460 
minor, imageI, UnI1] 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

461 
qed "Lmap_type"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

462 

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

463 
(*This type checking rule synthesises a sufficiently large set for f*) 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

464 
Goal "M: llist(A) ==> Lmap f M: llist(f``A)"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

465 
by (etac Lmap_type 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

466 
by (etac imageI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

467 
qed "Lmap_type2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

468 

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

469 
(** Two easy results about Lmap **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

470 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

471 
Goalw [o_def] "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

472 
by (dtac imageI 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

473 
by (etac LList_equalityI 1); 
4160  474 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

475 
by (etac llist.elim 1); 
4521  476 
by (ALLGOALS Asm_simp_tac); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

477 
by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

478 
rangeI RS LListD_Fun_CONS_I] 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

479 
qed "Lmap_compose"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

480 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

481 
Goal "M: llist(A) ==> Lmap (%x. x) M = M"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

482 
by (dtac imageI 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

483 
by (etac LList_equalityI 1); 
4160  484 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

485 
by (etac llist.elim 1); 
4521  486 
by (ALLGOALS Asm_simp_tac); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

487 
by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

488 
rangeI RS LListD_Fun_CONS_I] 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

489 
qed "Lmap_ident"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

490 

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

491 

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

492 
(*** Lappend  its two arguments cause some complications! ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

493 

5069  494 
Goalw [Lappend_def] "Lappend NIL NIL = NIL"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

495 
by (rtac (LList_corec RS trans) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

496 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

497 
qed "Lappend_NIL_NIL"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

498 

5069  499 
Goalw [Lappend_def] 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

500 
"Lappend NIL (CONS N N') = CONS N (Lappend NIL N')"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

501 
by (rtac (LList_corec RS trans) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

502 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

503 
qed "Lappend_NIL_CONS"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

504 

5069  505 
Goalw [Lappend_def] 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

506 
"Lappend (CONS M M') N = CONS M (Lappend M' N)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

507 
by (rtac (LList_corec RS trans) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

508 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

509 
qed "Lappend_CONS"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

510 

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

511 
Addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

512 
Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI]; 
4521  513 

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

514 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5102
diff
changeset

515 
Goal "M: llist(A) ==> Lappend NIL M = M"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

516 
by (etac LList_fun_equalityI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

517 
by (ALLGOALS Asm_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

518 
qed "Lappend_NIL"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

519 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5102
diff
changeset

520 
Goal "M: llist(A) ==> Lappend M NIL = M"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

521 
by (etac LList_fun_equalityI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

522 
by (ALLGOALS Asm_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

523 
qed "Lappend_NIL2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

524 

4521  525 
Addsimps [Lappend_NIL, Lappend_NIL2]; 
526 

527 

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

528 
(** Alternative typechecking proofs for Lappend **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

529 

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

530 
(*weak coinduction: bisimulation and case analysis on both variables*) 
5278  531 
Goal "[ M: llist(A); N: llist(A) ] ==> Lappend M N: llist(A)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

533 
[("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

534 
by (Fast_tac 1); 
4160  535 
by Safe_tac; 
5102  536 
by (eres_inst_tac [("aa", "u")] llist.elim 1); 
537 
by (eres_inst_tac [("aa", "v")] llist.elim 1); 

4521  538 
by (ALLGOALS Asm_simp_tac); 
539 
by (Blast_tac 1); 

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

540 
qed "Lappend_type"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

541 

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

542 
(*strong coinduction: bisimulation and case analysis on one variable*) 
5278  543 
Goal "[ M: llist(A); N: llist(A) ] ==> Lappend M N: llist(A)"; 
3842  544 
by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

545 
by (etac imageI 1); 
4521  546 
by (rtac image_subsetI 1); 
5102  547 
by (eres_inst_tac [("aa", "x")] llist.elim 1); 
4521  548 
by (asm_simp_tac (simpset() addsimps [list_Fun_llist_I]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

549 
by (Asm_simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

550 
qed "Lappend_type"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

551 

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

552 
(**** Lazy lists as the type 'a llist  strongly typed versions of above ****) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

553 

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

554 
(** llist_case: case analysis for 'a llist **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

555 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

556 
Addsimps ([LListI RS Abs_LList_inverse, Rep_LList_inverse, 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

557 
Rep_LList RS LListD, rangeI, inj_Leaf, inv_f_f] @ llist.intrs); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

558 

5069  559 
Goalw [llist_case_def,LNil_def] "llist_case c d LNil = c"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

560 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

561 
qed "llist_case_LNil"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

562 

5069  563 
Goalw [llist_case_def,LCons_def] 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

564 
"llist_case c d (LCons M N) = d M N"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

565 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

566 
qed "llist_case_LCons"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

567 

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

568 
(*Elimination is case analysis, not induction.*) 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

569 
val [prem1,prem2] = 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

570 
Goalw [NIL_def,CONS_def] 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

571 
"[ l=LNil ==> P; !!x l'. l=LCons x l' ==> P ] ==> P"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

572 
by (rtac (Rep_LList RS LListD RS llist.elim) 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

573 
by (rtac (inj_Rep_LList RS injD RS prem1) 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

574 
by (stac Rep_LList_LNil 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

575 
by (assume_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

576 
by (etac rangeE 1); 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

577 
by (rtac (inj_Rep_LList RS injD RS prem2) 1); 
4521  578 
by (asm_simp_tac (simpset() delsimps [CONS_CONS_eq] 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

579 
addsimps [Rep_LList_LCons]) 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

580 
by (etac (LListI RS Abs_LList_inverse RS ssubst) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

581 
by (rtac refl 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

582 
qed "llistE"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

583 

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

584 
(** llist_corec: corecursion for 'a llist **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

585 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

586 
(*Lemma for the proof of llist_corec*) 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

587 
Goal "LList_corec a \ 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

588 
\ (%z. case f z of None => None  Some(v,w) => Some(Leaf(v),w)) : \ 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

589 
\ llist(range Leaf)"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

590 
by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

591 
by (rtac rangeI 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

592 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

593 
by (stac LList_corec 1); 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

594 
by (Force_tac 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

595 
qed "LList_corec_type2"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

596 

9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

597 
Goalw [llist_corec_def,LNil_def,LCons_def] 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

598 
"llist_corec a f = \ 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

599 
\ (case f a of None => LNil  Some(z,w) => LCons z (llist_corec w f))"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

600 
by (stac LList_corec 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

601 
by (exhaust_tac "f a" 1); 
4089  602 
by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1); 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

603 
by (force_tac (claset(), simpset() addsimps [LList_corec_type2]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

604 
qed "llist_corec"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

605 

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

606 
(*definitional version of same*) 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

607 
val [rew] = 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

608 
Goal "[ !!x. h(x) == llist_corec x f ] ==> \ 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

609 
\ h(a) = (case f a of None => LNil  Some(z,w) => LCons z (h w))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

610 
by (rewtac rew); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

611 
by (rtac llist_corec 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

612 
qed "def_llist_corec"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

613 

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

614 
(**** Proofs about type 'a llist functions ****) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

615 

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

616 
(*** Deriving llist_equalityI  llist equality is a bisimulation ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

617 

5069  618 
Goalw [LListD_Fun_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

619 
"r <= (llist A) Times (llist A) ==> \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

620 
\ LListD_Fun (diag A) r <= (llist A) Times (llist A)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

621 
by (stac llist_unfold 1); 
4089  622 
by (simp_tac (simpset() addsimps [NIL_def, CONS_def]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

623 
by (Fast_tac 1); 
5996  624 
qed "LListD_Fun_subset_Times_llist"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

625 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

626 
Goal "prod_fun Rep_LList Rep_LList `` r <= \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

627 
\ (llist(range Leaf)) Times (llist(range Leaf))"; 
4521  628 
by (fast_tac (claset() delrules [image_subsetI] 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

629 
addIs [Rep_LList RS LListD]) 1); 
5996  630 
qed "subset_Times_llist"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

631 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

632 
Goal "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \ 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

633 
\ prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) `` r <= r"; 
4160  634 
by Safe_tac; 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

635 
by (etac (subsetD RS SigmaE2) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

636 
by (assume_tac 1); 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

637 
by (asm_simp_tac (simpset() addsimps [LListI RS Abs_LList_inverse]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

638 
qed "prod_fun_lemma"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

639 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

640 
Goal "prod_fun Rep_LList Rep_LList `` range(%x. (x, x)) = \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

641 
\ diag(llist(range Leaf))"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

642 
by (rtac equalityI 1); 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

643 
by (Blast_tac 1); 
4818
90dab9f7d81e
split_all_tac is now added to claset() _before_ other safe tactics
oheimb
parents:
4521
diff
changeset

644 
by (fast_tac (claset() delSWrapper "split_all_tac" 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

645 
addSEs [LListI RS Abs_LList_inverse RS subst]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

646 
qed "prod_fun_range_eq_diag"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

647 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

648 
(*Used with lfilter*) 
5069  649 
Goalw [llistD_Fun_def, prod_fun_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

650 
"A<=B ==> llistD_Fun A <= llistD_Fun B"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4160
diff
changeset

651 
by Auto_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

652 
by (rtac image_eqI 1); 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

653 
by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 2); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

654 
by (Force_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

655 
qed "llistD_Fun_mono"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

656 

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

657 
(** To show two llists are equal, exhibit a bisimulation! 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

658 
[also admits true equality] **) 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

659 
Goalw [llistD_Fun_def] 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

660 
"[ (l1,l2) : r; r <= llistD_Fun(r Un range(%x.(x,x))) ] ==> l1=l2"; 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

661 
by (rtac (inj_Rep_LList RS injD) 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

662 
by (res_inst_tac [("r", "prod_fun Rep_LList Rep_LList ``r"), 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

663 
("A", "range(Leaf)")] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

664 
LList_equalityI 1); 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

665 
by (etac prod_fun_imageI 1); 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

666 
by (etac (image_mono RS subset_trans) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

667 
by (rtac (image_compose RS subst) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

668 
by (rtac (prod_fun_compose RS subst) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

669 
by (stac image_Un 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

670 
by (stac prod_fun_range_eq_diag 1); 
5996  671 
by (rtac (LListD_Fun_subset_Times_llist RS prod_fun_lemma) 1); 
672 
by (rtac (subset_Times_llist RS Un_least) 1); 

673 
by (rtac diag_subset_Times 1); 

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

674 
qed "llist_equalityI"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

675 

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

676 
(** Rules to prove the 2nd premise of llist_equalityI **) 
5069  677 
Goalw [llistD_Fun_def,LNil_def] "(LNil,LNil) : llistD_Fun(r)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

678 
by (rtac (LListD_Fun_NIL_I RS prod_fun_imageI) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

679 
qed "llistD_Fun_LNil_I"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

680 

5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

681 
Goalw [llistD_Fun_def,LCons_def] 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

682 
"(l1,l2):r ==> (LCons x l1, LCons x l2) : llistD_Fun(r)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

683 
by (rtac (rangeI RS LListD_Fun_CONS_I RS prod_fun_imageI) 1); 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

684 
by (etac prod_fun_imageI 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

685 
qed "llistD_Fun_LCons_I"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

686 

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

687 
(*Utilise the "strong" part, i.e. gfp(f)*) 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

688 
Goalw [llistD_Fun_def] "(l,l) : llistD_Fun(r Un range(%x.(x,x)))"; 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

689 
by (rtac (Rep_LList_inverse RS subst) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

690 
by (rtac prod_fun_imageI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

691 
by (stac image_Un 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

692 
by (stac prod_fun_range_eq_diag 1); 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

693 
by (rtac (Rep_LList RS LListD RS LListD_Fun_diag_I) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

694 
qed "llistD_Fun_range_I"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

695 

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

696 
(*A special case of list_equality for functions over lazy lists*) 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

697 
val [prem1,prem2] = 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

698 
Goal "[ f(LNil)=g(LNil); \ 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

699 
\ !!x l. (f(LCons x l),g(LCons x l)) : \ 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

700 
\ llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v))) \ 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

701 
\ ] ==> f(l) = (g(l :: 'a llist) :: 'b llist)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

702 
by (res_inst_tac [("r", "range(%u. (f(u),g(u)))")] llist_equalityI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

703 
by (rtac rangeI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

704 
by (rtac subsetI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

705 
by (etac rangeE 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

706 
by (etac ssubst 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

707 
by (res_inst_tac [("l", "u")] llistE 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

708 
by (etac ssubst 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

709 
by (stac prem1 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

710 
by (rtac llistD_Fun_range_I 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

711 
by (etac ssubst 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

712 
by (rtac prem2 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

713 
qed "llist_fun_equalityI"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

714 

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

715 
(*simpset for llist bisimulations*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

716 
Addsimps [llist_case_LNil, llist_case_LCons, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

717 
llistD_Fun_LNil_I, llistD_Fun_LCons_I]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

718 

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

719 

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

720 
(*** The functional "lmap" ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

721 

5069  722 
Goal "lmap f LNil = LNil"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

723 
by (rtac (lmap_def RS def_llist_corec RS trans) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

724 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

725 
qed "lmap_LNil"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

726 

5069  727 
Goal "lmap f (LCons M N) = LCons (f M) (lmap f N)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

728 
by (rtac (lmap_def RS def_llist_corec RS trans) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

729 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

730 
qed "lmap_LCons"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

731 

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

732 
Addsimps [lmap_LNil, lmap_LCons]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

733 

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

734 

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

735 
(** Two easy results about lmap **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

736 

5069  737 
Goal "lmap (f o g) l = lmap f (lmap g l)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

738 
by (res_inst_tac [("l","l")] llist_fun_equalityI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

739 
by (ALLGOALS Simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

740 
qed "lmap_compose"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

741 

5069  742 
Goal "lmap (%x. x) l = l"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

743 
by (res_inst_tac [("l","l")] llist_fun_equalityI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

744 
by (ALLGOALS Simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

745 
qed "lmap_ident"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

746 

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

747 

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

748 
(*** iterates  llist_fun_equalityI cannot be used! ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

749 

5069  750 
Goal "iterates f x = LCons x (iterates f (f x))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

751 
by (rtac (iterates_def RS def_llist_corec RS trans) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

752 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

753 
qed "iterates"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

754 

5069  755 
Goal "lmap f (iterates f x) = iterates f (f x)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

756 
by (res_inst_tac [("r", "range(%u.(lmap f (iterates f u),iterates f (f u)))")] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

758 
by (rtac rangeI 1); 
4160  759 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

760 
by (res_inst_tac [("x1", "f(u)")] (iterates RS ssubst) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

761 
by (res_inst_tac [("x1", "u")] (iterates RS ssubst) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

762 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

763 
qed "lmap_iterates"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

764 

5069  765 
Goal "iterates f x = LCons x (lmap f (iterates f x))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

766 
by (stac lmap_iterates 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

767 
by (rtac iterates 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

768 
qed "iterates_lmap"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

769 

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

770 
(*** A rather complex proof about iterates  cf Andy Pitts ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

771 

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

772 
(** Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

773 

5278  774 
Goal "nat_rec (LCons b l) (%m. lmap(f)) n = \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

775 
\ LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)"; 
5184  776 
by (induct_tac "n" 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

777 
by (ALLGOALS Asm_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

778 
qed "fun_power_lmap"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

779 

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

780 
goal Nat.thy "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)"; 
5184  781 
by (induct_tac "n" 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

782 
by (ALLGOALS Asm_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

783 
qed "fun_power_Suc"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

784 

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

785 
val Pair_cong = read_instantiate_sg (sign_of Prod.thy) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

786 
[("f","Pair")] (standard(refl RS cong RS cong)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

787 

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

788 
(*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))} 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

789 
for all u and all n::nat.*) 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5788
diff
changeset

790 
val [prem] = Goal "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

791 
by (rtac ext 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

792 
by (res_inst_tac [("r", 
3842  793 
"UN u. range(%n. (nat_rec (h u) (%m y. lmap f y) n, \ 
794 
\ nat_rec (iterates f u) (%m y. lmap f y) n))")] 

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

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

796 
by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1)); 
4160  797 
by (Clarify_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

798 
by (stac iterates 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

799 
by (stac prem 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

800 
by (stac fun_power_lmap 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

801 
by (stac fun_power_lmap 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

802 
by (rtac llistD_Fun_LCons_I 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

803 
by (rtac (lmap_iterates RS subst) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

804 
by (stac fun_power_Suc 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

805 
by (stac fun_power_Suc 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

806 
by (rtac (UN1_I RS UnI1) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

807 
by (rtac rangeI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

808 
qed "iterates_equality"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

809 

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

810 

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

811 
(*** lappend  its two arguments cause some complications! ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

812 

5069  813 
Goalw [lappend_def] "lappend LNil LNil = LNil"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

814 
by (rtac (llist_corec RS trans) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

815 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

816 
qed "lappend_LNil_LNil"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

817 

5069  818 
Goalw [lappend_def] 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

819 
"lappend LNil (LCons l l') = LCons l (lappend LNil l')"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

820 
by (rtac (llist_corec RS trans) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

821 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

822 
qed "lappend_LNil_LCons"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

823 

5069  824 
Goalw [lappend_def] 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

825 
"lappend (LCons l l') N = LCons l (lappend l' N)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

826 
by (rtac (llist_corec RS trans) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

827 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

828 
qed "lappend_LCons"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

829 

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

830 
Addsimps [lappend_LNil_LNil, lappend_LNil_LCons, lappend_LCons]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

831 

5069  832 
Goal "lappend LNil l = l"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

833 
by (res_inst_tac [("l","l")] llist_fun_equalityI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

834 
by (ALLGOALS Simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

835 
qed "lappend_LNil"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

836 

5069  837 
Goal "lappend l LNil = l"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

838 
by (res_inst_tac [("l","l")] llist_fun_equalityI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

839 
by (ALLGOALS Simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

840 
qed "lappend_LNil2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

841 

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

842 
Addsimps [lappend_LNil, lappend_LNil2]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

843 

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

844 
(*The infinite first argument blocks the second*) 
5069  845 
Goal "lappend (iterates f x) N = iterates f x"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

846 
by (res_inst_tac [("r", "range(%u.(lappend (iterates f u) N,iterates f u))")] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

848 
by (rtac rangeI 1); 
4160  849 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

850 
by (stac iterates 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

851 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

852 
qed "lappend_iterates"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

853 

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

854 
(** Two proofs that lmap distributes over lappend **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

855 

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

856 
(*Long proof requiring case analysis on both both arguments*) 
5069  857 
Goal "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

859 
[("r", 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

860 
"UN n. range(%l.(lmap f (lappend l n),lappend (lmap f l) (lmap f n)))")] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

862 
by (rtac UN1_I 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

863 
by (rtac rangeI 1); 
4160  864 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

865 
by (res_inst_tac [("l", "l")] llistE 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

866 
by (res_inst_tac [("l", "n")] llistE 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

867 
by (ALLGOALS Asm_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

868 
by (REPEAT_SOME (ares_tac [llistD_Fun_LCons_I, UN1_I RS UnI1, rangeI])); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

869 
qed "lmap_lappend_distrib"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

870 

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

871 
(*Shorter proof of theorem above using llist_equalityI as strong coinduction*) 
5069  872 
Goal "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

873 
by (res_inst_tac [("l","l")] llist_fun_equalityI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

874 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

875 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

876 
qed "lmap_lappend_distrib"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

877 

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

878 
(*Without strong coinduction, three case analyses might be needed*) 
5069  879 
Goal "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

880 
by (res_inst_tac [("l","l1")] llist_fun_equalityI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

881 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

882 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

883 
qed "lappend_assoc"; 