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