equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1998 TUM |
4 Copyright 1998 TUM |
5 *) |
5 *) |
6 |
6 |
7 goalw thy [foldl2_def] "foldl2 f [] a = a"; |
7 Goalw [foldl2_def] "foldl2 f [] a = a"; |
8 by(Simp_tac 1); |
8 by(Simp_tac 1); |
9 qed "foldl2_Nil"; |
9 qed "foldl2_Nil"; |
10 |
10 |
11 goalw thy [foldl2_def] "foldl2 f (x#xs) a = foldl2 f xs (f x a)"; |
11 Goalw [foldl2_def] "foldl2 f (x#xs) a = foldl2 f xs (f x a)"; |
12 by(Simp_tac 1); |
12 by(Simp_tac 1); |
13 qed "foldl2_Cons"; |
13 qed "foldl2_Cons"; |
14 |
14 |
15 Addsimps [foldl2_Nil,foldl2_Cons]; |
15 Addsimps [foldl2_Nil,foldl2_Cons]; |
16 |
16 |
17 goalw thy [delta_def] "delta A [] s = s"; |
17 Goalw [delta_def] "delta A [] s = s"; |
18 by(Simp_tac 1); |
18 by(Simp_tac 1); |
19 qed "delta_Nil"; |
19 qed "delta_Nil"; |
20 |
20 |
21 goalw thy [delta_def] "delta A (a#w) s = delta A w (next A a s)"; |
21 Goalw [delta_def] "delta A (a#w) s = delta A w (next A a s)"; |
22 by(Simp_tac 1); |
22 by(Simp_tac 1); |
23 qed "delta_Cons"; |
23 qed "delta_Cons"; |
24 |
24 |
25 Addsimps [delta_Nil,delta_Cons]; |
25 Addsimps [delta_Nil,delta_Cons]; |
26 |
26 |
27 goal thy "!q ys. delta A (xs@ys) q = delta A ys (delta A xs q)"; |
27 Goal "!q ys. delta A (xs@ys) q = delta A ys (delta A xs q)"; |
28 by(induct_tac "xs" 1); |
28 by(induct_tac "xs" 1); |
29 by (ALLGOALS Asm_simp_tac); |
29 by (ALLGOALS Asm_simp_tac); |
30 qed "delta_append"; |
30 qed "delta_append"; |
31 Addsimps [delta_append]; |
31 Addsimps [delta_append]; |