equal
deleted
inserted
replaced
1 (* Title: ZF/UNITY/AllocBase.thy |
1 (* Title: ZF/UNITY/AllocBase.thy |
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
2 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
4 Copyright 2001 University of Cambridge |
3 Copyright 2001 University of Cambridge |
5 |
|
6 *) |
4 *) |
7 |
5 |
8 header{*Common declarations for Chandy and Charpentier's Allocator*} |
6 header{*Common declarations for Chandy and Charpentier's Allocator*} |
9 |
7 |
10 theory AllocBase imports Follows MultisetSum Guar begin |
8 theory AllocBase imports Follows MultisetSum Guar begin |
353 apply (rule var_infinite_lemma) |
351 apply (rule var_infinite_lemma) |
354 done |
352 done |
355 |
353 |
356 lemma var_not_Finite: "~Finite(var)" |
354 lemma var_not_Finite: "~Finite(var)" |
357 apply (insert nat_not_Finite) |
355 apply (insert nat_not_Finite) |
358 apply (blast intro: lepoll_Finite [OF nat_lepoll_var]) |
356 apply (blast intro: lepoll_Finite [OF nat_lepoll_var]) |
359 done |
357 done |
360 |
358 |
361 lemma not_Finite_imp_exist: "~Finite(A) ==> \<exists>x. x\<in>A" |
359 lemma not_Finite_imp_exist: "~Finite(A) ==> \<exists>x. x\<in>A" |
362 apply (subgoal_tac "A\<noteq>0") |
360 apply (subgoal_tac "A\<noteq>0") |
363 apply (auto simp add: Finite_0) |
361 apply (auto simp add: Finite_0) |