src/HOL/UNITY/Comp/AllocBase.thy

more succint formulation of membership for multisets, similar to lists;
discontinued ASCII notation for multiset membership;
more theorems on multisets, dropping redundant interpretation;
modernized notation;
some annotations concerning future work

(*  Title:      HOL/UNITY/Comp/AllocBase.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge
*)

section{*Common Declarations for Chandy and Charpentier's Allocator*}

theory AllocBase imports "../UNITY_Main" "~~/src/HOL/Library/Multiset_Order" begin

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

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

(*This function merely sums the elements of a list*)
primrec tokens :: "nat list => nat" where
  "tokens [] = 0"
| "tokens (x#xs) = x + tokens xs"

abbreviation (input) "bag_of \<equiv> mset"

lemma setsum_fun_mono [rule_format]:
     "!!f :: nat=>nat.  
      (ALL i. i<n --> f i <= g i) -->  
      setsum f (lessThan n) <= setsum g (lessThan n)"
apply (induct_tac "n")
apply (auto simp add: lessThan_Suc)
done

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"
apply (unfold mono_def)
apply (blast intro: tokens_mono_prefix)
done


(** bag_of **)

lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
  by (induct l) (simp_all add: ac_simps)

lemma subseteq_le_multiset: "A #\<subseteq># A + B"
unfolding le_multiset_def apply (cases B; simp)
apply (rule HOL.disjI1)
apply (rule union_less_mono2[of "{#}" "_ + {#_#}" A, simplified])
apply (simp add: less_multiset\<^sub>H\<^sub>O)
done

lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
apply (rule monoI)
apply (unfold prefix_def)
apply (erule genPrefix.induct, simp_all add: add_right_mono)
apply (erule order_trans)
apply (simp add: less_eq_multiset_def subseteq_le_multiset)
done

(** setsum **)

declare setsum.cong [cong]

lemma bag_of_sublist_lemma:
     "(\<Sum>i\<in> A Int lessThan k. {#if i<k then f i else g i#}) =  
      (\<Sum>i\<in> A Int lessThan k. {#f i#})"
by (rule setsum.cong, auto)

lemma bag_of_sublist:
     "bag_of (sublist l A) =  
      (\<Sum>i\<in> A Int lessThan (length l). {# l!i #})"
apply (rule_tac xs = l in rev_induct, simp)
apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
                 bag_of_sublist_lemma ac_simps)
done


lemma bag_of_sublist_Un_Int:
     "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) =  
      bag_of (sublist l A) + bag_of (sublist 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_sublist Int_Un_distrib2 setsum.union_inter, blast)
done

lemma bag_of_sublist_Un_disjoint:
     "A Int B = {}  
      ==> bag_of (sublist l (A Un B)) =  
          bag_of (sublist l A) + bag_of (sublist l B)"
by (simp add: bag_of_sublist_Un_Int [symmetric])

lemma bag_of_sublist_UN_disjoint [rule_format]:
     "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]  
      ==> bag_of (sublist l (UNION I A)) =   
          (\<Sum>i\<in>I. bag_of (sublist l (A i)))"
apply (simp del: UN_simps 
            add: UN_simps [symmetric] add: bag_of_sublist)
apply (subst setsum.UNION_disjoint, auto)
done

end