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