--- a/src/HOL/UNITY/AllocBase.ML Fri May 26 18:07:17 2000 +0200
+++ b/src/HOL/UNITY/AllocBase.ML Fri May 26 18:08:46 2000 +0200
@@ -4,6 +4,8 @@
Copyright 1998 University of Cambridge
Basis declarations for Chandy and Charpentier's Allocator
+
+with_path "../Induct" time_use_thy "AllocBase";
*)
Goal "(ALL i. i<n --> f i <= (g i :: nat)) --> sum_below f n <= sum_below g n";
@@ -22,3 +24,12 @@
Goalw [mono_def] "mono tokens";
by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
qed "mono_tokens";
+
+Goal "length xs <= k --> map fst [p:zip xs [0..length xs(] . snd p < k] = xs";
+by (res_inst_tac [("xs","xs")] rev_induct 1);
+by Auto_tac;
+qed_spec_mp "sublist_length_lemma";
+
+Goalw [sublist_def] "sublist l {..length l(} = l";
+by (simp_tac (simpset() addsimps [sublist_length_lemma]) 1);
+qed "sublist_length";
--- a/src/HOL/UNITY/AllocBase.thy Fri May 26 18:07:17 2000 +0200
+++ b/src/HOL/UNITY/AllocBase.thy Fri May 26 18:08:46 2000 +0200
@@ -4,9 +4,11 @@
Copyright 1998 University of Cambridge
Common declarations for Chandy and Charpentier's Allocator
+
+with_path "../Induct" time_use_thy "AllocBase";
*)
-AllocBase = Rename + Follows +
+AllocBase = Rename + Follows + MultisetOrder +
consts
NbT :: nat (*Number of tokens in system*)
@@ -27,4 +29,7 @@
sum_below_0 "sum_below f 0 = 0"
sum_below_Suc "sum_below f (Suc n) = f(n) + sum_below f n"
+constdefs sublist :: "['a list, nat set] => 'a list"
+ "sublist l A == map fst (filter (%p. snd p : A) (zip l [0..size l(]))"
+
end