src/HOL/UNITY/Comp/AllocBase.thy
changeset 60397 f8a513fedb31
parent 58889 5b7a9633cfa8
child 60515 484559628038
     1.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Mon Jun 08 22:04:19 2015 +0200
     1.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Wed Jun 10 13:24:16 2015 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  section{*Common Declarations for Chandy and Charpentier's Allocator*}
     1.6  
     1.7 -theory AllocBase imports "../UNITY_Main" begin
     1.8 +theory AllocBase imports "../UNITY_Main" "~~/src/HOL/Library/Multiset_Order" begin
     1.9  
    1.10  consts Nclients :: nat  (*Number of clients*)
    1.11  
    1.12 @@ -41,12 +41,19 @@
    1.13  lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
    1.14    by (induct l) (simp_all add: ac_simps)
    1.15  
    1.16 +lemma subseteq_le_multiset: "A #<=# A + B"
    1.17 +unfolding le_multiset_def apply (cases B; simp)
    1.18 +apply (rule HOL.disjI1)
    1.19 +apply (rule union_less_mono2[of "{#}" "_ + {#_#}" A, simplified])
    1.20 +apply (simp add: less_multiset\<^sub>H\<^sub>O)
    1.21 +done
    1.22 +
    1.23  lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
    1.24  apply (rule monoI)
    1.25  apply (unfold prefix_def)
    1.26 -apply (erule genPrefix.induct, auto)
    1.27 +apply (erule genPrefix.induct, simp_all add: add_right_mono)
    1.28  apply (erule order_trans)
    1.29 -apply simp
    1.30 +apply (simp add: less_eq_multiset_def subseteq_le_multiset)
    1.31  done
    1.32  
    1.33  (** setsum **)