1(*  Title:      HOL/UNITY/Comp/AllocBase.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1998  University of Cambridge
4*)
5
6section\<open>Common Declarations for Chandy and Charpentier's Allocator\<close>
7
8theory AllocBase imports "../UNITY_Main" "HOL-Library.Multiset_Order" begin
9
10consts Nclients :: nat  (*Number of clients*)
11
12axiomatization NbT :: nat  (*Number of tokens in system*)
13  where NbT_pos: "0 < NbT"
14
15abbreviation (input) tokens :: "nat list \<Rightarrow> nat"
16where
17  "tokens \<equiv> sum_list"
18
19abbreviation (input)
20  "bag_of \<equiv> mset"
21
22lemma sum_fun_mono:
23  fixes f :: "nat \<Rightarrow> nat"
24  shows "(\<And>i. i < n \<Longrightarrow> f i \<le> g i) \<Longrightarrow> sum f {..<n} \<le> sum g {..<n}"
25  by (induct n) (auto simp add: lessThan_Suc add_le_mono)
26
27lemma tokens_mono_prefix: "xs \<le> ys \<Longrightarrow> tokens xs \<le> tokens ys"
28  by (induct ys arbitrary: xs) (auto simp add: prefix_Cons)
29
30lemma mono_tokens: "mono tokens"
31  using tokens_mono_prefix by (rule monoI)
32
33
34(** bag_of **)
35
36lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
37  by (fact mset_append)
38
39lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
40apply (rule monoI)
41apply (unfold prefix_def)
42apply (erule genPrefix.induct, simp_all add: add_right_mono)
43apply (erule order_trans)
44apply simp
45done
46
47(** sum **)
48
49declare sum.cong [cong]
50
51lemma bag_of_nths_lemma:
52     "(\<Sum>i\<in> A Int lessThan k. {#if i<k then f i else g i#}) =  
53      (\<Sum>i\<in> A Int lessThan k. {#f i#})"
54by (rule sum.cong, auto)
55
56lemma bag_of_nths:
57     "bag_of (nths l A) =  
58      (\<Sum>i\<in> A Int lessThan (length l). {# l!i #})"
59  by (rule_tac xs = l in rev_induct)
60     (simp_all add: nths_append Int_insert_right lessThan_Suc nth_append 
61                    bag_of_nths_lemma ac_simps)
62
63
64lemma bag_of_nths_Un_Int:
65     "bag_of (nths l (A Un B)) + bag_of (nths l (A Int B)) =  
66      bag_of (nths l A) + bag_of (nths l B)"
67apply (subgoal_tac "A Int B Int {..<length l} =
68                    (A Int {..<length l}) Int (B Int {..<length l}) ")
69apply (simp add: bag_of_nths Int_Un_distrib2 sum.union_inter, blast)
70done
71
72lemma bag_of_nths_Un_disjoint:
73     "A Int B = {}  
74      ==> bag_of (nths l (A Un B)) =  
75          bag_of (nths l A) + bag_of (nths l B)"
76by (simp add: bag_of_nths_Un_Int [symmetric])
77
78lemma bag_of_nths_UN_disjoint [rule_format]:
79     "[| finite I; \<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j \<longrightarrow> A i Int A j = {} |]  
80      ==> bag_of (nths l (\<Union>(A ` I))) =   
81          (\<Sum>i\<in>I. bag_of (nths l (A i)))"
82apply (auto simp add: bag_of_nths)
83unfolding UN_simps [symmetric]
84apply (subst sum.UNION_disjoint)
85apply auto
86done
87
88end
89