src/HOL/UNITY/Comp/AllocBase.thy
author wenzelm
Sat Jun 14 23:19:51 2008 +0200 (2008-06-14)
changeset 27208 5fe899199f85
parent 24147 edc90be09ac1
child 32960 69916a850301
permissions -rw-r--r--
proper context for tactics derived from res_inst_tac;
     1 (*  Title:      HOL/UNITY/AllocBase.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 *)
     7 
     8 header{*Common Declarations for Chandy and Charpentier's Allocator*}
     9 
    10 theory AllocBase imports "../UNITY_Main" begin
    11 
    12 consts
    13   NbT      :: nat       (*Number of tokens in system*)
    14   Nclients :: nat       (*Number of clients*)
    15 
    16 axioms
    17   NbT_pos:  "0 < NbT"
    18 
    19 (*This function merely sums the elements of a list*)
    20 consts tokens     :: "nat list => nat"
    21 primrec 
    22   "tokens [] = 0"
    23   "tokens (x#xs) = x + tokens xs"
    24 
    25 consts
    26   bag_of :: "'a list => 'a multiset"
    27 
    28 primrec
    29   "bag_of []     = {#}"
    30   "bag_of (x#xs) = {#x#} + bag_of xs"
    31 
    32 lemma setsum_fun_mono [rule_format]:
    33      "!!f :: nat=>nat.  
    34       (ALL i. i<n --> f i <= g i) -->  
    35       setsum f (lessThan n) <= setsum g (lessThan n)"
    36 apply (induct_tac "n")
    37 apply (auto simp add: lessThan_Suc)
    38 done
    39 
    40 lemma tokens_mono_prefix [rule_format]:
    41      "ALL xs. xs <= ys --> tokens xs <= tokens ys"
    42 apply (induct_tac "ys")
    43 apply (auto simp add: prefix_Cons)
    44 done
    45 
    46 lemma mono_tokens: "mono tokens"
    47 apply (unfold mono_def)
    48 apply (blast intro: tokens_mono_prefix)
    49 done
    50 
    51 
    52 (** bag_of **)
    53 
    54 lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
    55 apply (induct_tac "l", simp)
    56  apply (simp add: add_ac)
    57 done
    58 
    59 lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
    60 apply (rule monoI)
    61 apply (unfold prefix_def)
    62 apply (erule genPrefix.induct, auto)
    63 apply (simp add: union_le_mono)
    64 apply (erule order_trans)
    65 apply (rule union_upper1)
    66 done
    67 
    68 (** setsum **)
    69 
    70 declare setsum_cong [cong]
    71 
    72 lemma bag_of_sublist_lemma:
    73      "(\<Sum>i\<in> A Int lessThan k. {#if i<k then f i else g i#}) =  
    74       (\<Sum>i\<in> A Int lessThan k. {#f i#})"
    75 by (rule setsum_cong, auto)
    76 
    77 lemma bag_of_sublist:
    78      "bag_of (sublist l A) =  
    79       (\<Sum>i\<in> A Int lessThan (length l). {# l!i #})"
    80 apply (rule_tac xs = l in rev_induct, simp)
    81 apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
    82                  bag_of_sublist_lemma add_ac)
    83 done
    84 
    85 
    86 lemma bag_of_sublist_Un_Int:
    87      "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) =  
    88       bag_of (sublist l A) + bag_of (sublist l B)"
    89 apply (subgoal_tac "A Int B Int {..<length l} =
    90 	            (A Int {..<length l}) Int (B Int {..<length l}) ")
    91 apply (simp add: bag_of_sublist Int_Un_distrib2 setsum_Un_Int, blast)
    92 done
    93 
    94 lemma bag_of_sublist_Un_disjoint:
    95      "A Int B = {}  
    96       ==> bag_of (sublist l (A Un B)) =  
    97           bag_of (sublist l A) + bag_of (sublist l B)"
    98 by (simp add: bag_of_sublist_Un_Int [symmetric])
    99 
   100 lemma bag_of_sublist_UN_disjoint [rule_format]:
   101      "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]  
   102       ==> bag_of (sublist l (UNION I A)) =   
   103           (\<Sum>i\<in>I. bag_of (sublist l (A i)))"
   104 apply (simp del: UN_simps 
   105             add: UN_simps [symmetric] add: bag_of_sublist)
   106 apply (subst setsum_UN_disjoint, auto)
   107 done
   108 
   109 end