author  berghofe 
Fri, 24 Jul 1998 13:39:47 +0200  
changeset 5191  8ceaa19f7717 
parent 5184  9b8547a9496a 
child 5278  a903b66822e2 
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 

5089
f95e0a6eb775
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5086
diff
changeset

13 
Addsplits [split_split, split_sum_case]; 
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) 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

25 
addEs [rew llist.elim]) 1) 
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 

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

66 
(*UNUSED; obsolete? 
3842  67 
goal Prod.thy "split p (%x y. UN z. f x y z) = (UN z. split p (%x y. f x y z))"; 
4831  68 
by (Simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

70 

3842  71 
goal Sum.thy "sum_case s f (%y. UN z. g y z) = (UN z. sum_case s f (%y. g y z))"; 
4831  72 
by (Simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

75 

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

76 
val prems = goalw LList.thy [CONS_def] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

77 
"[ M<=M'; N<=N' ] ==> CONS M N <= CONS M' N'"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

78 
by (REPEAT (resolve_tac ([In1_mono,Scons_mono]@prems) 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

80 

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

81 
Addsimps [LList_corec_fun_def RS def_nat_rec_0, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

82 
LList_corec_fun_def RS def_nat_rec_Suc]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

83 

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

84 
(** The directions of the equality are proved separately **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

85 

5069  86 
Goalw [LList_corec_def] 
3842  87 
"LList_corec a f <= sum_case (%u. NIL) \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

88 
\ (split(%z w. CONS z (LList_corec w f))) (f a)"; 
4160  89 
by (rtac UN_least 1); 
90 
by (exhaust_tac "k" 1); 

91 
by (ALLGOALS Asm_simp_tac); 

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

93 
UNIV_I RS UN_upper] 1)); 

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

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

95 

5069  96 
Goalw [LList_corec_def] 
3842  97 
"sum_case (%u. NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

98 
\ LList_corec a f"; 
4089  99 
by (simp_tac (simpset() addsimps [CONS_UN1]) 1); 
4160  100 
by Safe_tac; 
101 
by (ALLGOALS (res_inst_tac [("a","Suc(?k)")] UN_I)); 

102 
by (ALLGOALS Asm_simp_tac); 

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

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

104 

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

105 
(*the recursion equation for LList_corec  NOT SUITABLE FOR REWRITING!*) 
5069  106 
Goal 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

107 
"LList_corec a f = sum_case (%u. NIL) \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

108 
\ (split(%z w. CONS z (LList_corec w f))) (f a)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

112 

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

113 
(*definitional version of same*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

114 
val [rew] = goal LList.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

115 
"[ !!x. h(x) == LList_corec x f ] ==> \ 
3842  116 
\ h(a) = sum_case (%u. NIL) (split(%z w. CONS z (h w))) (f a)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

120 

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

121 
(*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

122 
Bisimulation is range(%x. LList_corec x f) *) 
5069  123 
Goal "LList_corec a f : llist({u. True})"; 
3842  124 
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

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

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

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

130 

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

131 
(*Lemma for the proof of llist_corec*) 
5069  132 
Goal 
3842  133 
"LList_corec a (%z. sum_case Inl (split(%v w. Inr((Leaf(v),w)))) (f z)) : \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

134 
\ llist(range Leaf)"; 
3842  135 
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

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

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

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

141 

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

142 

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

143 
(**** llist equality as a gfp; the bisimulation principle ****) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

144 

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

145 
(*This theorem is actually used, unlike the many similar ones in ZF*) 
5069  146 
Goal "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

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

152 

5069  153 
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

154 
by (res_inst_tac [("n", "k")] less_induct 1); 
4089  155 
by (safe_tac ((claset_of Fun.thy) delrules [equalityI])); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

156 
by (etac LListD.elim 1); 
4089  157 
by (safe_tac (claset_of Prod.thy delrules [equalityI] addSEs [diagE])); 
5184  158 
by (exhaust_tac "n" 1); 
4521  159 
by (Asm_simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

160 
by (rename_tac "n'" 1); 
5184  161 
by (exhaust_tac "n'" 1); 
4521  162 
by (asm_simp_tac (simpset() addsimps [CONS_def]) 1); 
163 
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

164 
qed "LListD_implies_ntrunc_equality"; 
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 
(*The domain of the LListD relation*) 
5069  167 
Goalw (llist.defs @ [NIL_def, CONS_def]) 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

168 
"fst``LListD(diag(A)) <= llist(A)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

170 
(*avoids unfolding LListD on the rhs*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

171 
by (res_inst_tac [("P", "%x. fst``x <= ?B")] (LListD_unfold RS ssubst) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

175 

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

176 
(*This inclusion justifies the use of coinduction to show M=N*) 
5069  177 
Goal "LListD(diag(A)) <= diag(llist(A))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

182 
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

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

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

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

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

187 

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

188 

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

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

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

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

192 

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

193 
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

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

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

196 

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

198 
"[ 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

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

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

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

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

203 

5069  204 
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

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

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

207 

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

209 
"[ 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

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

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

212 

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

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

215 
"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

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

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

218 

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

219 

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

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

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

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

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

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

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

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

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

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

232 

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

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

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

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

237 

5069  238 
Goal 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

239 
"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

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

241 
by (rtac LListD_Fun_LListD_I 1); 
4089  242 
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

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

244 

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

245 

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

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

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

248 
Replace "A" by some particular set, like {x.True}??? *) 
5069  249 
Goal 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

250 
"[ (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

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

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

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

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

257 

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

258 

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

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

260 

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

263 
(or strengthen the Solver?) 

264 
*) 

265 
Delsimps [Pair_eq]; 

266 

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

267 
(*abstract proof using a bisimulation*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

268 
val [prem1,prem2] = goal LList.thy 
3842  269 
"[ !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x); \ 
270 
\ !!x. h2(x) = sum_case (%u. NIL) (split(%z w. CONS z (h2 w))) (f x) ]\ 

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

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

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

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

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

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

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

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

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

283 

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

284 
val [prem] = goal LList.thy 
3842  285 
"[ !!x. h(x) = sum_case (%u. NIL) (split(%z w. CONS z (h w))) (f x) ] \ 
286 
\ ==> h = (%x. LList_corec x f)"; 

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

287 
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

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

289 

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

290 

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

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

292 

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

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

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

296 

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

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

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

301 

4521  302 
Addsimps [ntrunc_one_CONS, ntrunc_CONS]; 
303 

304 

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

305 
val [prem1,prem2] = goal LList.thy 
3842  306 
"[ !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x); \ 
307 
\ !!x. h2(x) = sum_case (%u. NIL) (split(%z w. CONS z (h2 w))) (f x) ]\ 

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

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

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

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

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

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

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

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

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

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

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

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

321 
by (rename_tac "m" 2); 
5184  322 
by (exhaust_tac "m" 2); 
4521  323 
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

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

325 

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

326 

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

327 
(*** 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

328 

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

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

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

332 

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

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

334 
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

335 

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

336 
(*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

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

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

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

341 
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

342 
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

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

344 

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

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

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

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

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

350 

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

351 
(*Thus we could have used gfp in the definition of Lconst*) 
5069  352 
Goal "gfp(%N. CONS M N) = LList_corec M (%x. Inr((x,x)))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

356 
qed "gfp_Lconst_eq_LList_corec"; 
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 

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

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

360 

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

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

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

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

365 

5069  366 
Goal "inj_on Abs_llist (llist(range Leaf))"; 
4831  367 
by (rtac inj_on_inverseI 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

368 
by (etac Abs_llist_inverse 1); 
4831  369 
qed "inj_on_Abs_llist"; 
3120
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 
(** Distinctness of constructors **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

372 

5069  373 
Goalw [LNil_def,LCons_def] "~ LCons x xs = LNil"; 
4831  374 
by (rtac (CONS_not_NIL RS (inj_on_Abs_llist RS inj_on_contraD)) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

375 
by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

377 

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

378 
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

379 

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

380 
AddIffs [LCons_not_LNil, LNil_not_LCons]; 
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 

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

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

384 

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

386 
"Rep_llist(LNil) = NIL"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

387 
by (rtac (llist.NIL_I RS Abs_llist_inverse) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

389 

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

391 
"Rep_llist(LCons x l) = CONS (Leaf x) (Rep_llist l)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

392 
by (REPEAT (resolve_tac [llist.CONS_I RS Abs_llist_inverse, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

393 
rangeI, Rep_llist] 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

395 

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

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

397 

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

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

401 

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

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

403 

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

404 

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

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

406 

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

407 
AddIs ([Rep_llist]@llist.intrs); 
4831  408 
AddSDs [inj_on_Abs_llist RS inj_onD, 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

409 
inj_Rep_llist RS injD, Leaf_inject]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

410 

5069  411 
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

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

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

414 

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

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

416 

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

417 
val [major] = goal LList.thy "CONS M N: llist(A) ==> M: A & N: llist(A)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

418 
by (rtac (major RS llist.elim) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

422 

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

423 

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

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

425 

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

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

427 

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

428 
(*A special case of list_equality for functions over lazy lists*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

429 
val [Mlist,gMlist,NILcase,CONScase] = goal LList.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

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

434 
\ 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

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

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

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

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

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

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

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

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

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

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

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

447 

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

448 

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

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

450 

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

452 
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

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

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

455 

5069  456 
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

457 
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

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

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

460 

4521  461 
Addsimps [Lmap_NIL, Lmap_CONS]; 
462 

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

463 
(*Another typechecking proof by coinduction*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

464 
val [major,minor] = goal LList.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

470 
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

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

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

473 

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

474 
(*This type checking rule synthesises a sufficiently large set for f*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

475 
val [major] = goal LList.thy "M: llist(A) ==> Lmap f M: llist(f``A)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

476 
by (rtac (major RS Lmap_type) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

479 

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

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

481 

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

482 
val [prem] = goalw LList.thy [o_def] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

483 
"M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

484 
by (rtac (prem RS imageI RS LList_equalityI) 1); 
4160  485 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

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

491 

3842  492 
val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x. x) M = M"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

493 
by (rtac (prem RS imageI RS LList_equalityI) 1); 
4160  494 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

497 
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

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

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

500 

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

501 

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

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

503 

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

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

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

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

508 

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

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

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

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

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

514 

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

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

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

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

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

520 

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

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

522 
Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI]; 
4521  523 

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

524 

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

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

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

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

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

529 

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

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

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

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

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

534 

4521  535 
Addsimps [Lappend_NIL, Lappend_NIL2]; 
536 

537 

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

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

539 

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

540 
(*weak coinduction: bisimulation and case analysis on both variables*) 
5069  541 
Goal 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

542 
"[ 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

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

544 
[("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

545 
by (Fast_tac 1); 
4160  546 
by Safe_tac; 
5102  547 
by (eres_inst_tac [("aa", "u")] llist.elim 1); 
548 
by (eres_inst_tac [("aa", "v")] llist.elim 1); 

4521  549 
by (ALLGOALS Asm_simp_tac); 
550 
by (Blast_tac 1); 

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

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

552 

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

553 
(*strong coinduction: bisimulation and case analysis on one variable*) 
5069  554 
Goal 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

555 
"[ M: llist(A); N: llist(A) ] ==> Lappend M N: llist(A)"; 
3842  556 
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

557 
by (etac imageI 1); 
4521  558 
by (rtac image_subsetI 1); 
5102  559 
by (eres_inst_tac [("aa", "x")] llist.elim 1); 
4521  560 
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

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

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

563 

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

564 
(**** 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

565 

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

566 
(** llist_case: case analysis for 'a llist **) 
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 
Addsimps ([Abs_llist_inverse, Rep_llist_inverse, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

569 
Rep_llist, rangeI, inj_Leaf, inv_f_f] @ llist.intrs); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

570 

5069  571 
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

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

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

574 

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

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

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

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

579 

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

580 
(*Elimination is case analysis, not induction.*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

581 
val [prem1,prem2] = goalw LList.thy [NIL_def,CONS_def] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

582 
"[ l=LNil ==> P; !!x l'. l=LCons x l' ==> P \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

584 
by (rtac (Rep_llist RS llist.elim) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

585 
by (rtac (inj_Rep_llist RS injD RS prem1) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

589 
by (rtac (inj_Rep_llist RS injD RS prem2) 1); 
4521  590 
by (asm_simp_tac (simpset() delsimps [CONS_CONS_eq] 
591 
addsimps [Rep_llist_LCons]) 1); 

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

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

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

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

595 

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

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

597 

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

599 
"llist_corec a f = sum_case (%u. LNil) \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

600 
\ (split(%z w. LCons z (llist_corec w f))) (f a)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

602 
by (res_inst_tac [("s","f(a)")] sumE 1); 
4089  603 
by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

604 
by (res_inst_tac [("p","y")] PairE 1); 
4089  605 
by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

606 
(*FIXME: correct case splits usd to be found automatically: 
4089  607 
by (ASM_SIMP_TAC(simpset() addsimps [LList_corec_type2]) 1);*) 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

609 

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

610 
(*definitional version of same*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

611 
val [rew] = goal LList.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

612 
"[ !!x. h(x) == llist_corec x f ] ==> \ 
3842  613 
\ h(a) = sum_case (%u. LNil) (split(%z w. LCons z (h w))) (f a)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

617 

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

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

619 

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

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

621 

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

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

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

625 
by (stac llist_unfold 1); 
4089  626 
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

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

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

629 

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

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

632 
\ (llist(range Leaf)) Times (llist(range Leaf))"; 
4521  633 
by (fast_tac (claset() delrules [image_subsetI] 
634 
addIs [Rep_llist]) 1); 

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

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

636 

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

637 
val [prem] = goal LList.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

639 
\ prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r"; 
4160  640 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

641 
by (rtac (prem RS subsetD RS SigmaE2) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

642 
by (assume_tac 1); 
4521  643 
by (asm_simp_tac (simpset() addsimps [Abs_llist_inverse]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

645 

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

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

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

649 
by (rtac equalityI 1); 
4089  650 
by (fast_tac (claset() addIs [Rep_llist]) 1); 
4818
90dab9f7d81e
split_all_tac is now added to claset() _before_ other safe tactics
oheimb
parents:
4521
diff
changeset

651 
by (fast_tac (claset() delSWrapper "split_all_tac" 
90dab9f7d81e
split_all_tac is now added to claset() _before_ other safe tactics
oheimb
parents:
4521
diff
changeset

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

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

654 

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

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

657 
"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

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

659 
by (rtac image_eqI 1); 
4089  660 
by (fast_tac (claset() addss (simpset())) 1); 
661 
by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 1); 

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

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

663 

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

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

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

666 
val [prem1,prem2] = goalw LList.thy [llistD_Fun_def] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

667 
"[ (l1,l2) : r; r <= llistD_Fun(r Un range(%x.(x,x))) ] ==> l1=l2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

679 
by (rtac (subset_Sigma_llist RS Un_least) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

682 

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

683 
(** Rules to prove the 2nd premise of llist_equalityI **) 
5069  684 
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

685 
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

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

687 

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

688 
val [prem] = goalw LList.thy [llistD_Fun_def,LCons_def] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

689 
"(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

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

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

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

693 

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

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

696 
"(l,l) : llistD_Fun(r Un range(%x.(x,x)))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

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

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

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

703 

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

704 
(*A special case of list_equality for functions over lazy lists*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

705 
val [prem1,prem2] = goal LList.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

706 
"[ f(LNil)=g(LNil); \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

707 
\ !!x l. (f(LCons x l),g(LCons x l)) : \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

708 
\ llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v))) \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

710 
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

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

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

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

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

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

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

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

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

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

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

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

722 

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

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

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

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

726 

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

727 

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

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

729 

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

731 
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

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

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

734 

5069  735 
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

736 
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

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

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

739 

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

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

741 

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

742 

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

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

744 

5069  745 
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

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

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

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

749 

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

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

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

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

754 

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

755 

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

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

757 

5069  758 
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

759 
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

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

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

762 

5069  763 
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

764 
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

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

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

768 
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

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

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

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

772 

5069  773 
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

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

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

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

777 

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

778 
(*** A rather complex proof about iterates  cf Andy Pitts ***) 
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 
(** 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

781 

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

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

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

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

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

788 

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

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

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

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

793 

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

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

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

796 

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

797 
(*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

798 
for all u and all n::nat.*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

799 
val [prem] = goal LList.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

800 
"(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

802 
by (res_inst_tac [("r", 
3842  803 
"UN u. range(%n. (nat_rec (h u) (%m y. lmap f y) n, \ 
804 
\ 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

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

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

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

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

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

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

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

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

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

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

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

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

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

819 

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

820 

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

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

822 

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

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

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

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

827 

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

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

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

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

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

833 

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

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

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

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

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

839 

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

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

841 

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

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

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

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

846 

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

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

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

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

851 

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

852 
Addsimps [lappend_LNil, lappend_LNil2]; 
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 
(*The infinite first argument blocks the second*) 
5069  855 
Goal "lappend (iterates f x) N = iterates f x"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

856 
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

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

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

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

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

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

863 

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

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

865 

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

866 
(*Long proof requiring case analysis on both both arguments*) 
5069  867 
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

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

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

870 
"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

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

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

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

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

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

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

878 
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

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

880 

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

881 
(*Shorter proof of theorem above using llist_equalityI as strong coinduction*) 
5069  882 
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

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

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

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

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

887 

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

888 
(*Without strong coinduction, three case analyses might be needed*) 
5069  889 
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

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

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

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

893 
qed "lappend_assoc"; 