7 Delsplits [split_if]; |
7 Delsplits [split_if]; |
8 Goalw [is_maxpref_def] "!(ps::'a list) res. \ |
8 Goalw [is_maxpref_def] "!(ps::'a list) res. \ |
9 \ (maxsplit P res ps qs = (xs,ys)) = \ |
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) \ |
10 \ (if ? us. us <= qs & P(ps@us) then xs@ys=ps@qs & is_maxpref P xs (ps@qs) \ |
11 \ else (xs,ys)=res)"; |
11 \ else (xs,ys)=res)"; |
12 by(induct_tac "qs" 1); |
12 by (induct_tac "qs" 1); |
13 by(simp_tac (simpset() addsplits [split_if]) 1); |
13 by (simp_tac (simpset() addsplits [split_if]) 1); |
14 by(Blast_tac 1); |
14 by (Blast_tac 1); |
15 by(Asm_simp_tac 1); |
15 by (Asm_simp_tac 1); |
16 be thin_rl 1; |
16 by (etac thin_rl 1); |
17 by(Clarify_tac 1); |
17 by (Clarify_tac 1); |
18 by(case_tac "? us. us <= list & P (ps @ a # us)" 1); |
18 by (case_tac "? us. us <= list & P (ps @ a # us)" 1); |
19 by(Asm_simp_tac 1); |
19 by (Asm_simp_tac 1); |
20 by(subgoal_tac "? us. us <= a # list & P (ps @ us)" 1); |
20 by (subgoal_tac "? us. us <= a # list & P (ps @ us)" 1); |
21 by(Asm_simp_tac 1); |
21 by (Asm_simp_tac 1); |
22 by(blast_tac (claset() addIs [prefix_Cons RS iffD2]) 1); |
22 by (blast_tac (claset() addIs [prefix_Cons RS iffD2]) 1); |
23 by(subgoal_tac "~P(ps@[a])" 1); |
23 by (subgoal_tac "~P(ps@[a])" 1); |
24 by(Blast_tac 2); |
24 by (Blast_tac 2); |
25 by(Asm_simp_tac 1); |
25 by (Asm_simp_tac 1); |
26 by(case_tac "? us. us <= a#list & P (ps @ us)" 1); |
26 by (case_tac "? us. us <= a#list & P (ps @ us)" 1); |
27 by(Asm_simp_tac 1); |
27 by (Asm_simp_tac 1); |
28 by(Clarify_tac 1); |
28 by (Clarify_tac 1); |
29 by(exhaust_tac "us" 1); |
29 by (exhaust_tac "us" 1); |
30 br iffI 1; |
30 by (rtac iffI 1); |
31 by(asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1); |
31 by (asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1); |
32 by(Blast_tac 1); |
32 by (Blast_tac 1); |
33 by(asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1); |
33 by (asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1); |
34 by(Clarify_tac 1); |
34 by (Clarify_tac 1); |
35 be disjE 1; |
35 by (etac disjE 1); |
36 by(fast_tac (claset() addDs [prefix_antisym]) 1); |
36 by (fast_tac (claset() addDs [prefix_antisym]) 1); |
37 by(Clarify_tac 1); |
37 by (Clarify_tac 1); |
38 be disjE 1; |
38 by (etac disjE 1); |
39 by(Clarify_tac 1); |
39 by (Clarify_tac 1); |
40 by(Asm_full_simp_tac 1); |
40 by (Asm_full_simp_tac 1); |
41 be disjE 1; |
41 by (etac disjE 1); |
42 by(Clarify_tac 1); |
42 by (Clarify_tac 1); |
43 by(Asm_full_simp_tac 1); |
43 by (Asm_full_simp_tac 1); |
44 by(Blast_tac 1); |
44 by (Blast_tac 1); |
45 by(Asm_full_simp_tac 1); |
45 by (Asm_full_simp_tac 1); |
46 by(subgoal_tac "~P(ps)" 1); |
46 by (subgoal_tac "~P(ps)" 1); |
47 by(Asm_simp_tac 1); |
47 by (Asm_simp_tac 1); |
48 by(fast_tac (claset() addss simpset()) 1); |
48 by (fast_tac (claset() addss simpset()) 1); |
49 qed_spec_mp "maxsplit_lemma"; |
49 qed_spec_mp "maxsplit_lemma"; |
50 Addsplits [split_if]; |
50 Addsplits [split_if]; |
51 |
51 |
52 Goalw [is_maxpref_def] |
52 Goalw [is_maxpref_def] |
53 "~(? us. us<=xs & P us) ==> is_maxpref P ps xs = (ps = [])"; |
53 "~(? us. us<=xs & P us) ==> is_maxpref P ps xs = (ps = [])"; |
54 by(Blast_tac 1); |
54 by (Blast_tac 1); |
55 qed "is_maxpref_Nil"; |
55 qed "is_maxpref_Nil"; |
56 Addsimps [is_maxpref_Nil]; |
56 Addsimps [is_maxpref_Nil]; |
57 |
57 |
58 Goalw [is_maxsplitter_def] |
58 Goalw [is_maxsplitter_def] |
59 "is_maxsplitter P (%xs. maxsplit P ([],xs) [] xs)"; |
59 "is_maxsplitter P (%xs. maxsplit P ([],xs) [] xs)"; |
60 by(simp_tac (simpset() addsimps [maxsplit_lemma]) 1); |
60 by (simp_tac (simpset() addsimps [maxsplit_lemma]) 1); |
61 by(fast_tac (claset() addss simpset()) 1); |
61 by (fast_tac (claset() addss simpset()) 1); |
62 qed "is_maxsplitter_maxsplit"; |
62 qed "is_maxsplitter_maxsplit"; |
63 |
63 |
64 val maxsplit_eq = rewrite_rule [is_maxsplitter_def] is_maxsplitter_maxsplit; |
64 val maxsplit_eq = rewrite_rule [is_maxsplitter_def] is_maxsplitter_maxsplit; |