author | wenzelm |
Wed, 25 Oct 2000 18:39:01 +0200 | |
changeset 10338 | 291ce4c4b50e |
parent 8442 | 96023903c2df |
permissions | -rw-r--r-- |
4714 | 1 |
(* Title: HOL/Lex/MaxPrefix.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1998 TUM |
|
5 |
*) |
|
6 |
||
4832 | 7 |
Delsplits [split_if]; |
5069 | 8 |
Goalw [is_maxpref_def] "!(ps::'a list) res. \ |
4910 | 9 |
\ (maxsplit P res ps qs = (xs,ys)) = \ |
10 |
\ (if ? us. us <= qs & P(ps@us) then xs@ys=ps@qs & is_maxpref P xs (ps@qs) \ |
|
4714 | 11 |
\ else (xs,ys)=res)"; |
5132 | 12 |
by (induct_tac "qs" 1); |
13 |
by (simp_tac (simpset() addsplits [split_if]) 1); |
|
14 |
by (Blast_tac 1); |
|
15 |
by (Asm_simp_tac 1); |
|
16 |
by (etac thin_rl 1); |
|
17 |
by (Clarify_tac 1); |
|
18 |
by (case_tac "? us. us <= list & P (ps @ a # us)" 1); |
|
19 |
by (Asm_simp_tac 1); |
|
20 |
by (subgoal_tac "? us. us <= a # list & P (ps @ us)" 1); |
|
21 |
by (Asm_simp_tac 1); |
|
10338 | 22 |
by (blast_tac (claset() addIs [thm "prefix_Cons" RS iffD2]) 1); |
5132 | 23 |
by (subgoal_tac "~P(ps@[a])" 1); |
24 |
by (Blast_tac 2); |
|
25 |
by (Asm_simp_tac 1); |
|
26 |
by (case_tac "? us. us <= a#list & P (ps @ us)" 1); |
|
27 |
by (Asm_simp_tac 1); |
|
28 |
by (Clarify_tac 1); |
|
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
29 |
by (case_tac "us" 1); |
5132 | 30 |
by (rtac iffI 1); |
10338 | 31 |
by (asm_full_simp_tac (simpset() addsimps [thm "prefix_Cons", thm "prefix_append"]) 1); |
5132 | 32 |
by (Blast_tac 1); |
10338 | 33 |
by (asm_full_simp_tac (simpset() addsimps [thm "prefix_Cons", thm "prefix_append"]) 1); |
5132 | 34 |
by (Clarify_tac 1); |
35 |
by (etac disjE 1); |
|
10338 | 36 |
by (fast_tac (claset() addDs [order_antisym]) 1); |
5132 | 37 |
by (Clarify_tac 1); |
38 |
by (etac disjE 1); |
|
39 |
by (Clarify_tac 1); |
|
40 |
by (Asm_full_simp_tac 1); |
|
41 |
by (etac disjE 1); |
|
42 |
by (Clarify_tac 1); |
|
43 |
by (Asm_full_simp_tac 1); |
|
44 |
by (Blast_tac 1); |
|
45 |
by (Asm_full_simp_tac 1); |
|
46 |
by (subgoal_tac "~P(ps)" 1); |
|
47 |
by (Asm_simp_tac 1); |
|
48 |
by (fast_tac (claset() addss simpset()) 1); |
|
4714 | 49 |
qed_spec_mp "maxsplit_lemma"; |
4832 | 50 |
Addsplits [split_if]; |
4714 | 51 |
|
5069 | 52 |
Goalw [is_maxpref_def] |
5118 | 53 |
"~(? us. us<=xs & P us) ==> is_maxpref P ps xs = (ps = [])"; |
5132 | 54 |
by (Blast_tac 1); |
4714 | 55 |
qed "is_maxpref_Nil"; |
56 |
Addsimps [is_maxpref_Nil]; |
|
57 |
||
5069 | 58 |
Goalw [is_maxsplitter_def] |
4910 | 59 |
"is_maxsplitter P (%xs. maxsplit P ([],xs) [] xs)"; |
5132 | 60 |
by (simp_tac (simpset() addsimps [maxsplit_lemma]) 1); |
61 |
by (fast_tac (claset() addss simpset()) 1); |
|
4714 | 62 |
qed "is_maxsplitter_maxsplit"; |
63 |
||
64 |
val maxsplit_eq = rewrite_rule [is_maxsplitter_def] is_maxsplitter_maxsplit; |