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