# Theory AllocBase

theory AllocBase
imports UNITY_Main Multiset_Order
```(*  Title:      HOL/UNITY/Comp/AllocBase.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

section‹Common Declarations for Chandy and Charpentier's Allocator›

theory AllocBase imports "../UNITY_Main" "HOL-Library.Multiset_Order" begin

consts Nclients :: nat  (*Number of clients*)

axiomatization NbT :: nat  (*Number of tokens in system*)
where NbT_pos: "0 < NbT"

abbreviation (input) tokens :: "nat list ⇒ nat"
where
"tokens ≡ sum_list"

abbreviation (input)
"bag_of ≡ mset"

lemma sum_fun_mono:
fixes f :: "nat ⇒ nat"
shows "(⋀i. i < n ⟹ f i ≤ g i) ⟹ sum f {..<n} ≤ sum g {..<n}"

lemma tokens_mono_prefix: "xs ≤ ys ⟹ tokens xs ≤ tokens ys"
by (induct ys arbitrary: xs) (auto simp add: prefix_Cons)

lemma mono_tokens: "mono tokens"
using tokens_mono_prefix by (rule monoI)

(** bag_of **)

lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
by (fact mset_append)

lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
apply (rule monoI)
apply (unfold prefix_def)
apply (erule order_trans)
apply simp
done

(** sum **)

declare sum.cong [cong]

lemma bag_of_nths_lemma:
"(∑i∈ A Int lessThan k. {#if i<k then f i else g i#}) =
(∑i∈ A Int lessThan k. {#f i#})"
by (rule sum.cong, auto)

lemma bag_of_nths:
"bag_of (nths l A) =
(∑i∈ A Int lessThan (length l). {# l!i #})"
by (rule_tac xs = l in rev_induct)
(simp_all add: nths_append Int_insert_right lessThan_Suc nth_append
bag_of_nths_lemma ac_simps)

lemma bag_of_nths_Un_Int:
"bag_of (nths l (A Un B)) + bag_of (nths l (A Int B)) =
bag_of (nths l A) + bag_of (nths l B)"
apply (subgoal_tac "A Int B Int {..<length l} =
(A Int {..<length l}) Int (B Int {..<length l}) ")
apply (simp add: bag_of_nths Int_Un_distrib2 sum.union_inter, blast)
done

lemma bag_of_nths_Un_disjoint:
"A Int B = {}
==> bag_of (nths l (A Un B)) =
bag_of (nths l A) + bag_of (nths l B)"