src/HOL/UNITY/AllocBase.ML
author paulson
Tue May 23 12:31:38 2000 +0200 (2000-05-23)
changeset 8928 1d3bf47a4ecc
child 8989 8791e3304748
permissions -rw-r--r--
new files for the Allocator
     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 
     9 Goal "(ALL i. i<n --> f i <= (g i :: nat)) --> sum_below f n <= sum_below g n";
    10 by (induct_tac "n" 1);
    11 by Auto_tac;
    12 by (dres_inst_tac [("x","n")] spec 1);
    13 by Auto_tac;
    14 by (arith_tac 1);
    15 qed_spec_mp "sum_mono";
    16 
    17 Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
    18 by (induct_tac "ys" 1);
    19 by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
    20 qed_spec_mp "tokens_mono_prefix";
    21 
    22 Goalw [mono_def] "mono tokens";
    23 by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
    24 qed "mono_tokens";