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