4714
|
1 |
(* Title: HOL/Lex/AutoMaxChop.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1998 TUM
|
|
5 |
*)
|
|
6 |
|
5069
|
7 |
Goal "delta A (xs@[y]) q = next A y (delta A xs q)";
|
5132
|
8 |
by (Simp_tac 1);
|
4832
|
9 |
qed "delta_snoc";
|
4714
|
10 |
|
5069
|
11 |
Goal
|
4910
|
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";
|
5132
|
14 |
by (induct_tac "xs" 1);
|
|
15 |
by (Simp_tac 1);
|
|
16 |
by (asm_simp_tac (simpset() addsimps [delta_snoc RS sym]
|
4832
|
17 |
delsimps [delta_append]) 1);
|
4714
|
18 |
qed_spec_mp "auto_split_lemma";
|
|
19 |
|
5069
|
20 |
Goalw [accepts_def]
|
4910
|
21 |
"auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs";
|
5132
|
22 |
by (stac ((read_instantiate [("s","start A")] delta_Nil) RS sym) 1);
|
|
23 |
by (stac auto_split_lemma 1);
|
|
24 |
by (Simp_tac 1);
|
4714
|
25 |
qed_spec_mp "auto_split_is_maxsplit";
|
|
26 |
|
5069
|
27 |
Goal
|
4910
|
28 |
"is_maxsplitter (accepts A) (%xs. auto_split A (start A) ([],xs) [] xs)";
|
5132
|
29 |
by (simp_tac (simpset() addsimps
|
4714
|
30 |
[auto_split_is_maxsplit,is_maxsplitter_maxsplit]) 1);
|
|
31 |
qed "is_maxsplitter_auto_split";
|
|
32 |
|
5069
|
33 |
Goalw [auto_chop_def]
|
4714
|
34 |
"is_maxchopper (accepts A) (auto_chop A)";
|
5132
|
35 |
by (rtac is_maxchopper_chop 1);
|
|
36 |
by (rtac is_maxsplitter_auto_split 1);
|
4714
|
37 |
qed "is_maxchopper_auto_chop";
|