src/HOL/UNITY/AllocBase.ML
author paulson
Fri May 26 18:08:46 2000 +0200 (2000-05-26)
changeset 8989 8791e3304748
parent 8928 1d3bf47a4ecc
child 9026 640c4fd8b5b3
permissions -rw-r--r--
sublist and some lemmas about it
     1 (*  Title:      HOL/UNITY/AllocBase
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Basis declarations for Chandy and Charpentier's Allocator
     7 
     8 with_path "../Induct" time_use_thy "AllocBase";
     9 *)
    10 
    11 Goal "(ALL i. i<n --> f i <= (g i :: nat)) --> sum_below f n <= sum_below g n";
    12 by (induct_tac "n" 1);
    13 by Auto_tac;
    14 by (dres_inst_tac [("x","n")] spec 1);
    15 by Auto_tac;
    16 by (arith_tac 1);
    17 qed_spec_mp "sum_mono";
    18 
    19 Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
    20 by (induct_tac "ys" 1);
    21 by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
    22 qed_spec_mp "tokens_mono_prefix";
    23 
    24 Goalw [mono_def] "mono tokens";
    25 by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
    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";