author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 25  3ac1c0c0016e 
permissions  rwrr 
0  1 
(* Title: ZF/listfn.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

5 

6 
For listfn.thy. Lists in ZermeloFraenkel Set Theory 

7 
*) 

8 

9 
open ListFn; 

10 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

11 
(** hd and tl **) 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

12 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

13 
goalw ListFn.thy [hd_def] "hd(Cons(a,l)) = a"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

14 
by (resolve_tac List.case_eqns 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

15 
val hd_Cons = result(); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

16 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

17 
goalw ListFn.thy [tl_def] "tl(Nil) = Nil"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

18 
by (resolve_tac List.case_eqns 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

19 
val tl_Nil = result(); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

20 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

21 
goalw ListFn.thy [tl_def] "tl(Cons(a,l)) = l"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

22 
by (resolve_tac List.case_eqns 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

23 
val tl_Cons = result(); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

24 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

25 
goal ListFn.thy "!!l. l: list(A) ==> tl(l) : list(A)"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

26 
by (etac List.elim 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

27 
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (List.intrs @ [tl_Nil,tl_Cons])))); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

28 
val tl_type = result(); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

29 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

30 
(** drop **) 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

31 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

32 
goalw ListFn.thy [drop_def] "drop(0, l) = l"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

33 
by (rtac rec_0 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

34 
val drop_0 = result(); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

35 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

36 
goalw ListFn.thy [drop_def] "!!i. i:nat ==> drop(i, Nil) = Nil"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

37 
by (etac nat_induct 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

38 
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Nil]))); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

39 
val drop_Nil = result(); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

40 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

41 
goalw ListFn.thy [drop_def] 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

42 
"!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

43 
by (etac nat_induct 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

44 
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Cons]))); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

45 
val drop_succ_Cons = result(); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

46 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

47 
goalw ListFn.thy [drop_def] 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

48 
"!!i l. [ i:nat; l: list(A) ] ==> drop(i,l) : list(A)"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

49 
by (etac nat_induct 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

50 
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_type]))); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

51 
val drop_type = result(); 
0  52 

53 
(** list_rec  by Vset recursion **) 

54 

55 
goal ListFn.thy "list_rec(Nil,c,h) = c"; 

56 
by (rtac (list_rec_def RS def_Vrec RS trans) 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

57 
by (simp_tac (ZF_ss addsimps List.case_eqns) 1); 
0  58 
val list_rec_Nil = result(); 
59 

60 
goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))"; 

61 
by (rtac (list_rec_def RS def_Vrec RS trans) 1); 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

62 
by (simp_tac (rank_ss addsimps (rank_Cons2::List.case_eqns)) 1); 
0  63 
val list_rec_Cons = result(); 
64 

65 
(*Type checking  proved by induction, as usual*) 

66 
val prems = goal ListFn.thy 

67 
"[ l: list(A); \ 

68 
\ c: C(Nil); \ 

69 
\ !!x y r. [ x:A; y: list(A); r: C(y) ] ==> h(x,y,r): C(Cons(x,y)) \ 

70 
\ ] ==> list_rec(l,c,h) : C(l)"; 

71 
by (list_ind_tac "l" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

72 
by (ALLGOALS (asm_simp_tac 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

73 
(ZF_ss addsimps (prems@[list_rec_Nil,list_rec_Cons])))); 
0  74 
val list_rec_type = result(); 
75 

76 
(** Versions for use with definitions **) 

77 

78 
val [rew] = goal ListFn.thy 

79 
"[ !!l. j(l)==list_rec(l, c, h) ] ==> j(Nil) = c"; 

80 
by (rewtac rew); 

81 
by (rtac list_rec_Nil 1); 

82 
val def_list_rec_Nil = result(); 

83 

84 
val [rew] = goal ListFn.thy 

85 
"[ !!l. j(l)==list_rec(l, c, h) ] ==> j(Cons(a,l)) = h(a,l,j(l))"; 

86 
by (rewtac rew); 

87 
by (rtac list_rec_Cons 1); 

88 
val def_list_rec_Cons = result(); 

89 

90 
fun list_recs def = map standard 

91 
([def] RL [def_list_rec_Nil, def_list_rec_Cons]); 

92 

93 
(** map **) 

94 

95 
val [map_Nil,map_Cons] = list_recs map_def; 

96 

97 
val prems = goalw ListFn.thy [map_def] 

98 
"[ l: list(A); !!x. x: A ==> h(x): B ] ==> map(h,l) : list(B)"; 

99 
by (REPEAT (ares_tac (prems@[list_rec_type, NilI, ConsI]) 1)); 

100 
val map_type = result(); 

101 

102 
val [major] = goal ListFn.thy "l: list(A) ==> map(h,l) : list({h(u). u:A})"; 

103 
by (rtac (major RS map_type) 1); 

104 
by (etac RepFunI 1); 

105 
val map_type2 = result(); 

106 

107 
(** length **) 

108 

109 
val [length_Nil,length_Cons] = list_recs length_def; 

110 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

111 
goalw ListFn.thy [length_def] 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

112 
"!!l. l: list(A) ==> length(l) : nat"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

113 
by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1)); 
0  114 
val length_type = result(); 
115 

116 
(** app **) 

117 

118 
val [app_Nil,app_Cons] = list_recs app_def; 

119 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

120 
goalw ListFn.thy [app_def] 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

121 
"!!xs ys. [ xs: list(A); ys: list(A) ] ==> xs@ys : list(A)"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

122 
by (REPEAT (ares_tac [list_rec_type, ConsI] 1)); 
0  123 
val app_type = result(); 
124 

125 
(** rev **) 

126 

127 
val [rev_Nil,rev_Cons] = list_recs rev_def; 

128 

129 
val prems = goalw ListFn.thy [rev_def] 

130 
"xs: list(A) ==> rev(xs) : list(A)"; 

131 
by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1)); 

132 
val rev_type = result(); 

133 

134 

135 
(** flat **) 

136 

137 
val [flat_Nil,flat_Cons] = list_recs flat_def; 

138 

139 
val prems = goalw ListFn.thy [flat_def] 

140 
"ls: list(list(A)) ==> flat(ls) : list(A)"; 

141 
by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1)); 

142 
val flat_type = result(); 

143 

144 

145 
(** list_add **) 

146 

147 
val [list_add_Nil,list_add_Cons] = list_recs list_add_def; 

148 

149 
val prems = goalw ListFn.thy [list_add_def] 

150 
"xs: list(nat) ==> list_add(xs) : nat"; 

151 
by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, add_type]) 1)); 

152 
val list_add_type = result(); 

153 

154 
(** ListFn simplification **) 

155 

156 
val list_typechecks = 

157 
[NilI, ConsI, list_rec_type, 

158 
map_type, map_type2, app_type, length_type, rev_type, flat_type, 

159 
list_add_type]; 

160 

161 
val list_ss = arith_ss 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

162 
addsimps List.case_eqns 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

163 
addsimps [list_rec_Nil, list_rec_Cons, 
0  164 
map_Nil, map_Cons, 
165 
app_Nil, app_Cons, 

166 
length_Nil, length_Cons, 

167 
rev_Nil, rev_Cons, 

168 
flat_Nil, flat_Cons, 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

169 
list_add_Nil, list_add_Cons] 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

170 
setsolver (type_auto_tac list_typechecks); 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

171 
(*Could also rewrite using the list_typechecks...*) 
0  172 

173 
(*** theorems about map ***) 

174 

175 
val prems = goal ListFn.thy 

176 
"l: list(A) ==> map(%u.u, l) = l"; 

177 
by (list_ind_tac "l" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

178 
by (ALLGOALS (asm_simp_tac list_ss)); 
0  179 
val map_ident = result(); 
180 

181 
val prems = goal ListFn.thy 

182 
"l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)"; 

183 
by (list_ind_tac "l" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

184 
by (ALLGOALS (asm_simp_tac list_ss)); 
0  185 
val map_compose = result(); 
186 

187 
val prems = goal ListFn.thy 

188 
"xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)"; 

189 
by (list_ind_tac "xs" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

190 
by (ALLGOALS (asm_simp_tac list_ss)); 
0  191 
val map_app_distrib = result(); 
192 

193 
val prems = goal ListFn.thy 

194 
"ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))"; 

195 
by (list_ind_tac "ls" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

196 
by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib]))); 
0  197 
val map_flat = result(); 
198 

199 
val prems = goal ListFn.thy 

200 
"l: list(A) ==> \ 

201 
\ list_rec(map(h,l), c, d) = \ 

202 
\ list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))"; 

203 
by (list_ind_tac "l" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

204 
by (ALLGOALS (asm_simp_tac list_ss)); 
0  205 
val list_rec_map = result(); 
206 

207 
(** theorems about list(Collect(A,P))  used in ex/term.ML **) 

208 

209 
(* c : list(Collect(B,P)) ==> c : list(B) *) 

210 
val list_CollectD = standard (Collect_subset RS list_mono RS subsetD); 

211 

212 
val prems = goal ListFn.thy 

213 
"l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"; 

214 
by (list_ind_tac "l" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

215 
by (ALLGOALS (asm_simp_tac list_ss)); 
0  216 
val map_list_Collect = result(); 
217 

218 
(*** theorems about length ***) 

219 

220 
val prems = goal ListFn.thy 

221 
"xs: list(A) ==> length(map(h,xs)) = length(xs)"; 

222 
by (list_ind_tac "xs" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

223 
by (ALLGOALS (asm_simp_tac list_ss)); 
0  224 
val length_map = result(); 
225 

226 
val prems = goal ListFn.thy 

227 
"xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)"; 

228 
by (list_ind_tac "xs" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

229 
by (ALLGOALS (asm_simp_tac list_ss)); 
0  230 
val length_app = result(); 
231 

232 
(* [ m: nat; n: nat ] ==> m #+ succ(n) = succ(n) #+ m 

233 
Used for rewriting below*) 

234 
val add_commute_succ = nat_succI RSN (2,add_commute); 

235 

236 
val prems = goal ListFn.thy 

237 
"xs: list(A) ==> length(rev(xs)) = length(xs)"; 

238 
by (list_ind_tac "xs" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

239 
by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app, add_commute_succ]))); 
0  240 
val length_rev = result(); 
241 

242 
val prems = goal ListFn.thy 

243 
"ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))"; 

244 
by (list_ind_tac "ls" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

245 
by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app]))); 
0  246 
val length_flat = result(); 
247 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

248 
(** Length and drop **) 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

249 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

250 
(*Lemma for the inductive step of drop_length*) 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

251 
goal ListFn.thy 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

252 
"!!xs. xs: list(A) ==> \ 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

253 
\ ALL x. EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

254 
by (etac List.induct 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

255 
by (ALLGOALS (asm_simp_tac (list_ss addsimps [drop_0,drop_succ_Cons]))); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

256 
by (fast_tac ZF_cs 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

257 
val drop_length_Cons_lemma = result(); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

258 
val drop_length_Cons = standard (drop_length_Cons_lemma RS spec); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

259 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

260 
goal ListFn.thy 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

261 
"!!l. l: list(A) ==> ALL i: length(l). EX z zs. drop(i,l) = Cons(z,zs)"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

262 
by (etac List.induct 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

263 
by (ALLGOALS (asm_simp_tac (list_ss addsimps bquant_simps))); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

264 
by (rtac conjI 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

265 
by (etac drop_length_Cons 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

266 
by (rtac ballI 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

267 
by (rtac natE 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

268 
by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

269 
by (assume_tac 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

270 
by (asm_simp_tac (list_ss addsimps [drop_0]) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

271 
by (fast_tac ZF_cs 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

272 
by (asm_simp_tac (list_ss addsimps [drop_succ_Cons]) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

273 
by (dtac bspec 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

274 
by (fast_tac ZF_cs 2); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

275 
by (fast_tac (ZF_cs addEs [succ_in_naturalD,length_type]) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

276 
val drop_length_lemma = result(); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

277 
val drop_length = standard (drop_length_lemma RS bspec); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

278 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

279 

0  280 
(*** theorems about app ***) 
281 

282 
val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs"; 

283 
by (rtac (major RS List.induct) 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

284 
by (ALLGOALS (asm_simp_tac list_ss)); 
0  285 
val app_right_Nil = result(); 
286 

287 
val prems = goal ListFn.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"; 

288 
by (list_ind_tac "xs" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

289 
by (ALLGOALS (asm_simp_tac list_ss)); 
0  290 
val app_assoc = result(); 
291 

292 
val prems = goal ListFn.thy 

293 
"ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)"; 

294 
by (list_ind_tac "ls" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

295 
by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_assoc]))); 
0  296 
val flat_app_distrib = result(); 
297 

298 
(*** theorems about rev ***) 

299 

300 
val prems = goal ListFn.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))"; 

301 
by (list_ind_tac "l" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

302 
by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib]))); 
0  303 
val rev_map_distrib = result(); 
304 

305 
(*Simplifier needs the premises as assumptions because rewriting will not 

306 
instantiate the variable ?A in the rules' typing conditions; note that 

307 
rev_type does not instantiate ?A. Only the premises do. 

308 
*) 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

309 
goal ListFn.thy 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

310 
"!!xs. [ xs: list(A); ys: list(A) ] ==> rev(xs@ys) = rev(ys)@rev(xs)"; 
0  311 
by (etac List.induct 1); 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

312 
by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_right_Nil,app_assoc]))); 
0  313 
val rev_app_distrib = result(); 
314 

315 
val prems = goal ListFn.thy "l: list(A) ==> rev(rev(l))=l"; 

316 
by (list_ind_tac "l" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

317 
by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_app_distrib]))); 
0  318 
val rev_rev_ident = result(); 
319 

320 
val prems = goal ListFn.thy 

321 
"ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))"; 

322 
by (list_ind_tac "ls" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

323 
by (ALLGOALS (asm_simp_tac (list_ss addsimps 
0  324 
[map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil]))); 
325 
val rev_flat = result(); 

326 

327 

328 
(*** theorems about list_add ***) 

329 

330 
val prems = goal ListFn.thy 

331 
"[ xs: list(nat); ys: list(nat) ] ==> \ 

332 
\ list_add(xs@ys) = list_add(ys) #+ list_add(xs)"; 

333 
by (cut_facts_tac prems 1); 

334 
by (list_ind_tac "xs" prems 1); 

335 
by (ALLGOALS 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

336 
(asm_simp_tac (list_ss addsimps [add_0_right, add_assoc RS sym]))); 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

337 
by (rtac (add_commute RS subst_context) 1); 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

338 
by (REPEAT (ares_tac [refl, list_add_type] 1)); 
0  339 
val list_add_app = result(); 
340 

341 
val prems = goal ListFn.thy 

342 
"l: list(nat) ==> list_add(rev(l)) = list_add(l)"; 

343 
by (list_ind_tac "l" prems 1); 

344 
by (ALLGOALS 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

345 
(asm_simp_tac (list_ss addsimps [list_add_app, add_0_right]))); 
0  346 
val list_add_rev = result(); 
347 

348 
val prems = goal ListFn.thy 

349 
"ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))"; 

350 
by (list_ind_tac "ls" prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

351 
by (ALLGOALS (asm_simp_tac (list_ss addsimps [list_add_app]))); 
0  352 
by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1)); 
353 
val list_add_flat = result(); 

354 

355 
(** New induction rule **) 

356 

357 
val major::prems = goal ListFn.thy 

358 
"[ l: list(A); \ 

359 
\ P(Nil); \ 

360 
\ !!x y. [ x: A; y: list(A); P(y) ] ==> P(y @ [x]) \ 

361 
\ ] ==> P(l)"; 

362 
by (rtac (major RS rev_rev_ident RS subst) 1); 

363 
by (rtac (major RS rev_type RS List.induct) 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

364 
by (ALLGOALS (asm_simp_tac (list_ss addsimps prems))); 
0  365 
val list_append_induct = result(); 
366 