src/HOL/Lex/DA.ML

match_bind(_i): 'as' patterns;
assume, theorem, show etc.: propp;
tuned qed msg;

(*  Title:      HOL/Lex/DA.ML
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1998 TUM
*)

Goalw [foldl2_def] "foldl2 f [] a = a";
by (Simp_tac 1);
qed "foldl2_Nil";

Goalw [foldl2_def] "foldl2 f (x#xs) a = foldl2 f xs (f x a)";
by (Simp_tac 1);
qed "foldl2_Cons";

Addsimps [foldl2_Nil,foldl2_Cons];

Goalw [delta_def] "delta A [] s = s";
by (Simp_tac 1);
qed "delta_Nil";

Goalw [delta_def] "delta A (a#w) s = delta A w (next A a s)";
by (Simp_tac 1);
qed "delta_Cons";

Addsimps [delta_Nil,delta_Cons];

Goal "!q ys. delta A (xs@ys) q = delta A ys (delta A xs q)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "delta_append";
Addsimps [delta_append];