equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 Basis declarations for Chandy and Charpentier's Allocator |
6 Basis declarations for Chandy and Charpentier's Allocator |
|
7 |
|
8 with_path "../Induct" time_use_thy "AllocBase"; |
7 *) |
9 *) |
8 |
10 |
9 Goal "(ALL i. i<n --> f i <= (g i :: nat)) --> sum_below f n <= sum_below g n"; |
11 Goal "(ALL i. i<n --> f i <= (g i :: nat)) --> sum_below f n <= sum_below g n"; |
10 by (induct_tac "n" 1); |
12 by (induct_tac "n" 1); |
11 by Auto_tac; |
13 by Auto_tac; |
20 qed_spec_mp "tokens_mono_prefix"; |
22 qed_spec_mp "tokens_mono_prefix"; |
21 |
23 |
22 Goalw [mono_def] "mono tokens"; |
24 Goalw [mono_def] "mono tokens"; |
23 by (blast_tac (claset() addIs [tokens_mono_prefix]) 1); |
25 by (blast_tac (claset() addIs [tokens_mono_prefix]) 1); |
24 qed "mono_tokens"; |
26 qed "mono_tokens"; |
|
27 |
|
28 Goal "length xs <= k --> map fst [p:zip xs [0..length xs(] . snd p < k] = xs"; |
|
29 by (res_inst_tac [("xs","xs")] rev_induct 1); |
|
30 by Auto_tac; |
|
31 qed_spec_mp "sublist_length_lemma"; |
|
32 |
|
33 Goalw [sublist_def] "sublist l {..length l(} = l"; |
|
34 by (simp_tac (simpset() addsimps [sublist_length_lemma]) 1); |
|
35 qed "sublist_length"; |