src/HOL/UNITY/AllocBase.ML
changeset 8989 8791e3304748
parent 8928 1d3bf47a4ecc
child 9026 640c4fd8b5b3
     1.1 --- a/src/HOL/UNITY/AllocBase.ML	Fri May 26 18:07:17 2000 +0200
     1.2 +++ b/src/HOL/UNITY/AllocBase.ML	Fri May 26 18:08:46 2000 +0200
     1.3 @@ -4,6 +4,8 @@
     1.4      Copyright   1998  University of Cambridge
     1.5  
     1.6  Basis declarations for Chandy and Charpentier's Allocator
     1.7 +
     1.8 +with_path "../Induct" time_use_thy "AllocBase";
     1.9  *)
    1.10  
    1.11  Goal "(ALL i. i<n --> f i <= (g i :: nat)) --> sum_below f n <= sum_below g n";
    1.12 @@ -22,3 +24,12 @@
    1.13  Goalw [mono_def] "mono tokens";
    1.14  by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
    1.15  qed "mono_tokens";
    1.16 +
    1.17 +Goal "length xs <= k --> map fst [p:zip xs [0..length xs(] . snd p < k] = xs";
    1.18 +by (res_inst_tac [("xs","xs")] rev_induct 1);
    1.19 +by Auto_tac;
    1.20 +qed_spec_mp "sublist_length_lemma";
    1.21 +
    1.22 +Goalw [sublist_def] "sublist l {..length l(} = l";
    1.23 +by (simp_tac (simpset() addsimps [sublist_length_lemma]) 1);
    1.24 +qed "sublist_length";