24 qed_spec_mp "tokens_mono_prefix"; |
24 qed_spec_mp "tokens_mono_prefix"; |
25 |
25 |
26 Goalw [mono_def] "mono tokens"; |
26 Goalw [mono_def] "mono tokens"; |
27 by (blast_tac (claset() addIs [tokens_mono_prefix]) 1); |
27 by (blast_tac (claset() addIs [tokens_mono_prefix]) 1); |
28 qed "mono_tokens"; |
28 qed "mono_tokens"; |
29 |
|
30 |
|
31 (*** sublist ***) |
|
32 |
|
33 Goalw [sublist_def] "sublist l {} = []"; |
|
34 by Auto_tac; |
|
35 qed "sublist_empty"; |
|
36 |
|
37 Goalw [sublist_def] "sublist [] A = []"; |
|
38 by Auto_tac; |
|
39 qed "sublist_nil"; |
|
40 |
|
41 Goal "map fst [p:zip xs [i..i + length xs(] . snd p : A] = \ |
|
42 \ map fst [p:zip xs [0..length xs(] . snd p + i : A]"; |
|
43 by (res_inst_tac [("xs","xs")] rev_induct 1); |
|
44 by (asm_simp_tac (simpset() addsimps [add_commute]) 2); |
|
45 by (Simp_tac 1); |
|
46 qed "sublist_shift_lemma"; |
|
47 |
|
48 Goalw [sublist_def] |
|
49 "sublist (l@l') A = sublist l A @ sublist l' {j. j + length l : A}"; |
|
50 by (res_inst_tac [("xs","l'")] rev_induct 1); |
|
51 by (Simp_tac 1); |
|
52 by (asm_simp_tac (simpset() addsimps [inst "i" "0" upt_add_eq_append, |
|
53 zip_append, sublist_shift_lemma]) 1); |
|
54 by (asm_simp_tac (simpset() addsimps [add_commute]) 1); |
|
55 qed "sublist_append"; |
|
56 |
|
57 Addsimps [sublist_empty, sublist_nil]; |
|
58 |
|
59 Goal "sublist (x#l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"; |
|
60 by (res_inst_tac [("xs","l")] rev_induct 1); |
|
61 by (asm_simp_tac (simpset() delsimps [append_Cons] |
|
62 addsimps [append_Cons RS sym, sublist_append]) 2); |
|
63 by (simp_tac (simpset() addsimps [sublist_def]) 1); |
|
64 qed "sublist_Cons"; |
|
65 |
|
66 Goal "sublist [x] A = (if 0 : A then [x] else [])"; |
|
67 by (simp_tac (simpset() addsimps [sublist_Cons]) 1); |
|
68 qed "sublist_singleton"; |
|
69 Addsimps [sublist_singleton]; |
|
70 |
|
71 Goal "sublist l {..n(} = take n l"; |
|
72 by (res_inst_tac [("xs","l")] rev_induct 1); |
|
73 by (asm_simp_tac (simpset() addsplits [nat_diff_split] |
|
74 addsimps [sublist_append]) 2); |
|
75 by (Simp_tac 1); |
|
76 qed "sublist_upt_eq_take"; |
|
77 Addsimps [sublist_upt_eq_take]; |
|
78 |
29 |
79 |
30 |
80 (** bag_of **) |
31 (** bag_of **) |
81 |
32 |
82 Goal "bag_of (l@l') = bag_of l + bag_of l'"; |
33 Goal "bag_of (l@l') = bag_of l + bag_of l'"; |