# Theory AllocBase

Up to index of Isabelle/HOL/UNITY

theory AllocBase
imports UNITY_Main
begin

    (*  Title:      HOL/UNITY/AllocBase.thy
        ID:         $Id: AllocBase.thy,v 1.9 2005/06/17 14:13:10 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1998  University of Cambridge

    *)

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

    theory AllocBase imports UNITY_Main begin

    consts
      NbT      :: nat       (*Number of tokens in system*)
      Nclients :: nat       (*Number of clients*)

    axioms
      NbT_pos:  "0 < NbT"

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

    consts
      bag_of :: "'a list => 'a multiset"

    primrec
      "bag_of []     = {#}"
      "bag_of (x#xs) = {#x#} + bag_of xs"

    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)
    apply (drule_tac x = n in spec, arith)
    done

    lemma tokens_mono_prefix [rule_format]:
         "ALL xs. xs <= ys --> tokens xs <= tokens ys"
    apply (induct_tac "ys")
    apply (auto simp add: prefix_Cons)
    done

    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'"
    apply (induct_tac "l", simp)
     apply (simp add: add_ac)
    done

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

    (** setsum **)

    declare setsum_cong [cong]

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

    lemma bag_of_sublist:
         "bag_of (sublist l A) =
          (∑i∈ 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 add_ac)
    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_Un_Int, 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)) =
              (∑i∈I. bag_of (sublist l (A i)))"
    apply (simp del: UN_simps
                add: UN_simps [symmetric] add: bag_of_sublist)
    apply (subst setsum_UN_disjoint, auto)
    done

    ML
    {*
    val NbT_pos = thm "NbT_pos";
    val setsum_fun_mono = thm "setsum_fun_mono";
    val tokens_mono_prefix = thm "tokens_mono_prefix";
    val mono_tokens = thm "mono_tokens";
    val bag_of_append = thm "bag_of_append";
    val mono_bag_of = thm "mono_bag_of";
    val bag_of_sublist_lemma = thm "bag_of_sublist_lemma";
    val bag_of_sublist = thm "bag_of_sublist";
    val bag_of_sublist_Un_Int = thm "bag_of_sublist_Un_Int";
    val bag_of_sublist_Un_disjoint = thm "bag_of_sublist_Un_disjoint";
    val bag_of_sublist_UN_disjoint = thm "bag_of_sublist_UN_disjoint";
    *}

    end

lemma setsum_fun_mono:

      (!!i. i < n ==> f i ≤ g i) ==> setsum f {..<n} ≤ setsum g {..<n}

lemma tokens_mono_prefix:

      xs ≤ ys ==> tokens xs ≤ tokens ys

lemma mono_tokens:

      mono tokens

lemma bag_of_append:

      bag_of (l @ l') = bag_of l + bag_of l'

lemma mono_bag_of:

      mono bag_of

lemma bag_of_sublist_lemma:

      (∑i∈A ∩ {..<k}. {#if i < k then f i else g i#}) = (∑i∈A ∩ {..<k}. {#f i#})

lemma bag_of_sublist:

      bag_of (sublist l A) = (∑i∈A ∩ {..<length l}. {#l ! i#})

lemma bag_of_sublist_Un_Int:

      bag_of (sublist l (A ∪ B)) + bag_of (sublist l (A ∩ B)) =
      bag_of (sublist l A) + bag_of (sublist l B)

lemma bag_of_sublist_Un_disjoint:

      A ∩ B = {}
      ==> bag_of (sublist l (A ∪ B)) = bag_of (sublist l A) + bag_of (sublist l B)

lemma bag_of_sublist_UN_disjoint:

      [| finite I; !!i j. [| i ∈ I; j ∈ I; i ≠ j |] ==> A i ∩ A j = {} |]
      ==> bag_of (sublist l (UNION I A)) = (∑i∈I. bag_of (sublist l (A i)))