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 goal thy "delta A (xs@[y]) q = next A y (delta A xs q)"; |
7 Goal "delta A (xs@[y]) q = next A y (delta A xs q)"; |
8 by(Simp_tac 1); |
8 by(Simp_tac 1); |
9 qed "delta_snoc"; |
9 qed "delta_snoc"; |
10 |
10 |
11 goal thy |
11 Goal |
12 "!q ps res. auto_split A (delta A ps q) res ps xs = \ |
12 "!q ps res. auto_split A (delta A ps q) res ps xs = \ |
13 \ maxsplit (%ys. fin A (delta A ys q)) res ps xs"; |
13 \ maxsplit (%ys. fin A (delta A ys q)) res ps xs"; |
14 by(induct_tac "xs" 1); |
14 by(induct_tac "xs" 1); |
15 by(Simp_tac 1); |
15 by(Simp_tac 1); |
16 by(asm_simp_tac (simpset() addsimps [delta_snoc RS sym] |
16 by(asm_simp_tac (simpset() addsimps [delta_snoc RS sym] |
17 delsimps [delta_append]) 1); |
17 delsimps [delta_append]) 1); |
18 qed_spec_mp "auto_split_lemma"; |
18 qed_spec_mp "auto_split_lemma"; |
19 |
19 |
20 goalw thy [accepts_def] |
20 Goalw [accepts_def] |
21 "auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs"; |
21 "auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs"; |
22 by(stac ((read_instantiate [("s","start A")] delta_Nil) RS sym) 1); |
22 by(stac ((read_instantiate [("s","start A")] delta_Nil) RS sym) 1); |
23 by(stac auto_split_lemma 1); |
23 by(stac auto_split_lemma 1); |
24 by(Simp_tac 1); |
24 by(Simp_tac 1); |
25 qed_spec_mp "auto_split_is_maxsplit"; |
25 qed_spec_mp "auto_split_is_maxsplit"; |
26 |
26 |
27 goal thy |
27 Goal |
28 "is_maxsplitter (accepts A) (%xs. auto_split A (start A) ([],xs) [] xs)"; |
28 "is_maxsplitter (accepts A) (%xs. auto_split A (start A) ([],xs) [] xs)"; |
29 by(simp_tac (simpset() addsimps |
29 by(simp_tac (simpset() addsimps |
30 [auto_split_is_maxsplit,is_maxsplitter_maxsplit]) 1); |
30 [auto_split_is_maxsplit,is_maxsplitter_maxsplit]) 1); |
31 qed "is_maxsplitter_auto_split"; |
31 qed "is_maxsplitter_auto_split"; |
32 |
32 |
33 goalw thy [auto_chop_def] |
33 Goalw [auto_chop_def] |
34 "is_maxchopper (accepts A) (auto_chop A)"; |
34 "is_maxchopper (accepts A) (auto_chop A)"; |
35 br is_maxchopper_chop 1; |
35 br is_maxchopper_chop 1; |
36 br is_maxsplitter_auto_split 1; |
36 br is_maxsplitter_auto_split 1; |
37 qed "is_maxchopper_auto_chop"; |
37 qed "is_maxchopper_auto_chop"; |