src/HOL/UNITY/Comp/AllocBase.thy
author nipkow
Fri Jun 19 15:55:22 2015 +0200 (2015-06-19)
changeset 60515 484559628038
parent 60397 f8a513fedb31
child 62430 9527ff088c15
permissions -rw-r--r--
renamed multiset_of -> mset
wenzelm@32960
     1
(*  Title:      HOL/UNITY/Comp/AllocBase.thy
paulson@11194
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@11194
     3
    Copyright   1998  University of Cambridge
paulson@11194
     4
*)
paulson@11194
     5
wenzelm@58889
     6
section{*Common Declarations for Chandy and Charpentier's Allocator*}
paulson@13798
     7
Mathias@60397
     8
theory AllocBase imports "../UNITY_Main" "~~/src/HOL/Library/Multiset_Order" begin
paulson@11194
     9
wenzelm@45827
    10
consts Nclients :: nat  (*Number of clients*)
paulson@11194
    11
wenzelm@45827
    12
axiomatization NbT :: nat  (*Number of tokens in system*)
wenzelm@45827
    13
  where NbT_pos: "0 < NbT"
paulson@11194
    14
paulson@11194
    15
(*This function merely sums the elements of a list*)
haftmann@39246
    16
primrec tokens :: "nat list => nat" where
paulson@11194
    17
  "tokens [] = 0"
haftmann@39246
    18
| "tokens (x#xs) = x + tokens xs"
paulson@11194
    19
nipkow@60515
    20
abbreviation (input) "bag_of \<equiv> mset"
paulson@11194
    21
paulson@13798
    22
lemma setsum_fun_mono [rule_format]:
paulson@13798
    23
     "!!f :: nat=>nat.  
paulson@13798
    24
      (ALL i. i<n --> f i <= g i) -->  
paulson@13798
    25
      setsum f (lessThan n) <= setsum g (lessThan n)"
paulson@13798
    26
apply (induct_tac "n")
paulson@13798
    27
apply (auto simp add: lessThan_Suc)
paulson@13798
    28
done
paulson@13798
    29
wenzelm@46911
    30
lemma tokens_mono_prefix: "xs <= ys ==> tokens xs <= tokens ys"
wenzelm@46911
    31
  by (induct ys arbitrary: xs) (auto simp add: prefix_Cons)
paulson@13798
    32
paulson@13798
    33
lemma mono_tokens: "mono tokens"
paulson@13798
    34
apply (unfold mono_def)
paulson@13798
    35
apply (blast intro: tokens_mono_prefix)
paulson@13798
    36
done
paulson@13798
    37
paulson@13798
    38
paulson@13798
    39
(** bag_of **)
paulson@13798
    40
paulson@13798
    41
lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
haftmann@57514
    42
  by (induct l) (simp_all add: ac_simps)
paulson@13798
    43
Mathias@60397
    44
lemma subseteq_le_multiset: "A #<=# A + B"
Mathias@60397
    45
unfolding le_multiset_def apply (cases B; simp)
Mathias@60397
    46
apply (rule HOL.disjI1)
Mathias@60397
    47
apply (rule union_less_mono2[of "{#}" "_ + {#_#}" A, simplified])
Mathias@60397
    48
apply (simp add: less_multiset\<^sub>H\<^sub>O)
Mathias@60397
    49
done
Mathias@60397
    50
paulson@13798
    51
lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
paulson@13798
    52
apply (rule monoI)
paulson@13798
    53
apply (unfold prefix_def)
Mathias@60397
    54
apply (erule genPrefix.induct, simp_all add: add_right_mono)
paulson@13798
    55
apply (erule order_trans)
Mathias@60397
    56
apply (simp add: less_eq_multiset_def subseteq_le_multiset)
paulson@13798
    57
done
paulson@13798
    58
paulson@13798
    59
(** setsum **)
paulson@13798
    60
haftmann@57418
    61
declare setsum.cong [cong]
paulson@13798
    62
paulson@13798
    63
lemma bag_of_sublist_lemma:
nipkow@15074
    64
     "(\<Sum>i\<in> A Int lessThan k. {#if i<k then f i else g i#}) =  
nipkow@15074
    65
      (\<Sum>i\<in> A Int lessThan k. {#f i#})"
haftmann@57418
    66
by (rule setsum.cong, auto)
paulson@13798
    67
paulson@13798
    68
lemma bag_of_sublist:
paulson@13798
    69
     "bag_of (sublist l A) =  
nipkow@15074
    70
      (\<Sum>i\<in> A Int lessThan (length l). {# l!i #})"
paulson@13798
    71
apply (rule_tac xs = l in rev_induct, simp)
paulson@13798
    72
apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
haftmann@57514
    73
                 bag_of_sublist_lemma ac_simps)
paulson@13798
    74
done
paulson@13798
    75
paulson@13798
    76
paulson@13798
    77
lemma bag_of_sublist_Un_Int:
paulson@13798
    78
     "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) =  
paulson@13798
    79
      bag_of (sublist l A) + bag_of (sublist l B)"
nipkow@15045
    80
apply (subgoal_tac "A Int B Int {..<length l} =
wenzelm@32960
    81
                    (A Int {..<length l}) Int (B Int {..<length l}) ")
haftmann@57418
    82
apply (simp add: bag_of_sublist Int_Un_distrib2 setsum.union_inter, blast)
paulson@13798
    83
done
paulson@13798
    84
paulson@13798
    85
lemma bag_of_sublist_Un_disjoint:
paulson@13798
    86
     "A Int B = {}  
paulson@13798
    87
      ==> bag_of (sublist l (A Un B)) =  
paulson@13798
    88
          bag_of (sublist l A) + bag_of (sublist l B)"
paulson@14114
    89
by (simp add: bag_of_sublist_Un_Int [symmetric])
paulson@13798
    90
paulson@13798
    91
lemma bag_of_sublist_UN_disjoint [rule_format]:
paulson@13798
    92
     "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]  
paulson@13798
    93
      ==> bag_of (sublist l (UNION I A)) =   
nipkow@15074
    94
          (\<Sum>i\<in>I. bag_of (sublist l (A i)))"
paulson@13798
    95
apply (simp del: UN_simps 
paulson@13798
    96
            add: UN_simps [symmetric] add: bag_of_sublist)
haftmann@57418
    97
apply (subst setsum.UNION_disjoint, auto)
paulson@13798
    98
done
paulson@13798
    99
paulson@11194
   100
end