src/HOL/UNITY/Comp/AllocImpl.thy
changeset 15074 277b3a4da341
parent 14114 e97ca1034caa
child 16417 9bc16273c2d4
equal deleted inserted replaced
15073:279c2daaf517 15074:277b3a4da341
   351 
   351 
   352 subsection{*Theorems for Allocator*}
   352 subsection{*Theorems for Allocator*}
   353 
   353 
   354 lemma alloc_refinement_lemma:
   354 lemma alloc_refinement_lemma:
   355      "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s})
   355      "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s})
   356       \<subseteq> {s. (\<Sum>x \<in> lessThan n. f x) \<le> (\<Sum>x: lessThan n. g x s)}"
   356       \<subseteq> {s. (SUM x: lessThan n. f x) \<le> (SUM x: lessThan n. g x s)}"
   357 apply (induct_tac "n")
   357 apply (induct_tac "n")
   358 apply (auto simp add: lessThan_Suc)
   358 apply (auto simp add: lessThan_Suc)
   359 done
   359 done
   360 
   360 
   361 lemma alloc_refinement:
   361 lemma alloc_refinement: